equal
deleted
inserted
replaced
765 "(ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)", |
765 "(ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)", |
766 "(ALL x:{}. P x) = True", |
766 "(ALL x:{}. P x) = True", |
767 "(ALL x:UNIV. P x) = (ALL x. P x)", |
767 "(ALL x:UNIV. P x) = (ALL x. P x)", |
768 "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))", |
768 "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))", |
769 "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)", |
769 "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)", |
|
770 "(ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)", |
770 "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)", |
771 "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)", |
771 "(ALL x:f``A. P x) = (ALL x:A. P(f x))", |
772 "(ALL x:f``A. P x) = (ALL x:A. P(f x))", |
772 "(~(ALL x:A. P x)) = (EX x:A. ~P x)"]; |
773 "(~(ALL x:A. P x)) = (EX x:A. ~P x)"]; |
773 |
774 |
774 val ball_conj_distrib = |
775 val ball_conj_distrib = |
779 "(EX x:A. P & Q x) = (P & (EX x:A. Q x))", |
780 "(EX x:A. P & Q x) = (P & (EX x:A. Q x))", |
780 "(EX x:{}. P x) = False", |
781 "(EX x:{}. P x) = False", |
781 "(EX x:UNIV. P x) = (EX x. P x)", |
782 "(EX x:UNIV. P x) = (EX x. P x)", |
782 "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))", |
783 "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))", |
783 "(EX x:Union(A). P x) = (EX y:A. EX x:y. P x)", |
784 "(EX x:Union(A). P x) = (EX y:A. EX x:y. P x)", |
|
785 "(EX x: UNION A B. P x) = (EX a:A. EX x: B a. P x)", |
784 "(EX x:Collect Q. P x) = (EX x. Q x & P x)", |
786 "(EX x:Collect Q. P x) = (EX x. Q x & P x)", |
785 "(EX x:f``A. P x) = (EX x:A. P(f x))", |
787 "(EX x:f``A. P x) = (EX x:A. P(f x))", |
786 "(~(EX x:A. P x)) = (ALL x:A. ~P x)"]; |
788 "(~(EX x:A. P x)) = (ALL x:A. ~P x)"]; |
787 |
789 |
788 val bex_disj_distrib = |
790 val bex_disj_distrib = |