Theorem Sample 3
(Click "Prove" to run)
Prove Theorem:
(=> (and (exists ?X (F ?X)) (exists ?X (G ?X))) (<=> (and (forall ?X (=> (F ?X) (H ?X))) (forall ?X (=> (G ?X) (J ?X)))) (forall (?X ?Y) (=> (and (F ?X) (G ?Y)) (and (H ?X) (J ?Y))))))
Proof Trace