Lines Matching refs:interpret
35 Definition interpret[simp]:
36 (interpret �� (BASE Ri n) <=>
38 (interpret �� (EXISTS v f) <=> ���n. interpret �����v���n��� f) ���
39 (interpret �� (ALL v f) <=> ���n. interpret �����v���n��� f)
45 ���x. x���A <=> interpret I���0���x��� (MKEA n Ri)
269 ���x. x ��� A ��� interpret I���0 ��� x��� (MKAE n Ri)
389 ���f. (interpret f (MKAE0 n k (lnot (lnot R))) = interpret f (MKAE0 n k R)) ���
390 (interpret f (MKEA0 n k (lnot (lnot R))) = interpret f (MKEA0 n k R))
401 ((��interpret f (MKEA0 n k R)) ��� interpret f (MKAE0 n k (lnot R))) ���
402 ((��interpret f (MKAE0 n k R)) ��� interpret f (MKEA0 n k (lnot R)))
423 ���m1 n1 n2 f g m2. (n1<m1 ��� n2<m2 ��� interpret f (MKEA0 n1 n2 Ri)) ==>
424 (interpret g (MKAE0 m1 m2 Ri) ��� interpret g (MKEA0 m1 m2 Ri))