%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : LCL676+1.001 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n010.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 01:32:45 PM UTC 2026 % Result : Theorem 1.53s 1.80s % Output : Proof 1.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL676+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : run_zenon %s %d % 0.11/0.37 % Computer : n010.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Fri Sep 4 14:52:08 UTC 2026 % 0.11/0.37 % CPUTime : % 1.53/1.80 (* PROOF-FOUND *) % 1.53/1.80 % SZS status Theorem % 1.53/1.80 (* BEGIN-PROOF *) % 1.53/1.80 % SZS output start Proof % 1.53/1.80 Theorem main : (~(exists X : zenon_U, (~(((forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(forall X : zenon_U, ((~(r1 Y X))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(p3 Y))))))))))/\((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X))))))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p4 Y)))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/((p4 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p4 Y)))\/(~(p4 X))))))))))\/(((~(forall Y : zenon_U, ((~(r1 X Y))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(p3 X))))))))/\((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X))))))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p1 Y)))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p1 Y)))\/(~(p1 X))))))))))\/(~(((((forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))))/\((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((((forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))/\((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(((forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))/\((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X))))))))))\/(~(((forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))))/\((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))))))))))))/\(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))))))))))))))). % 1.53/1.80 Proof. % 1.53/1.80 assert (zenon_L1_ : forall (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_j : zenon_U), (r1 zenon_TX_j zenon_TY_i) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_h)) -> (r1 zenon_TY_i zenon_TX_h) -> False). % 1.53/1.80 do 3 intro. intros zenon_H3 zenon_H4 zenon_H5 zenon_H6. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TY_i))/\(~(r1 zenon_TX_j zenon_TY_i)))); [ zenon_intro zenon_Ha | zenon_intro zenon_Hb ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_Ha). zenon_intro zenon_Hd. zenon_intro zenon_Hc. % 1.53/1.80 exact (zenon_Hc zenon_H3). % 1.53/1.80 cut ((r1 zenon_TY_i zenon_TX_h) = (r1 zenon_TX_j zenon_TX_h)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H5. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H6. % 1.53/1.80 cut ((zenon_TX_h = zenon_TX_h)); [idtac | apply NNPP; zenon_intro zenon_He]. % 1.53/1.80 cut ((zenon_TY_i = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_Hf]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_Hb); [ zenon_intro zenon_H11 | zenon_intro zenon_H10 ]. % 1.53/1.80 apply zenon_H11. zenon_intro zenon_H12. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TY_i = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_Hf. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TY_i)); [idtac | apply NNPP; zenon_intro zenon_Hd]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_Hd zenon_H12). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H10. zenon_intro zenon_H3. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TY_i). zenon_intro zenon_H16. % 1.53/1.80 generalize (zenon_H16 zenon_TX_h). zenon_intro zenon_H17. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H17); [ zenon_intro zenon_Hc | zenon_intro zenon_H18 ]. % 1.53/1.80 exact (zenon_Hc zenon_H3). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H18); [ zenon_intro zenon_H1a | zenon_intro zenon_H19 ]. % 1.53/1.80 exact (zenon_H1a zenon_H6). % 1.53/1.80 exact (zenon_H5 zenon_H19). % 1.53/1.80 apply zenon_He. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L1_ *) % 1.53/1.80 assert (zenon_L2_ : forall (zenon_TX_bd : zenon_U) (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_j : zenon_U), (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TY_i zenon_TX_h) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_bd)) -> (r1 zenon_TX_h zenon_TX_bd) -> False). % 1.53/1.80 do 4 intro. intros zenon_H3 zenon_H6 zenon_H4 zenon_H1b zenon_H1c. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_h))/\(~(r1 zenon_TX_j zenon_TX_h)))); [ zenon_intro zenon_H1e | zenon_intro zenon_H1f ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_H1e). zenon_intro zenon_H20. zenon_intro zenon_H5. % 1.53/1.80 apply (zenon_L1_ zenon_TX_h zenon_TY_i zenon_TX_j); trivial. % 1.53/1.80 cut ((r1 zenon_TX_h zenon_TX_bd) = (r1 zenon_TX_j zenon_TX_bd)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H1b. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H1c. % 1.53/1.80 cut ((zenon_TX_bd = zenon_TX_bd)); [idtac | apply NNPP; zenon_intro zenon_H21]. % 1.53/1.80 cut ((zenon_TX_h = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H22]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_H1f); [ zenon_intro zenon_H24 | zenon_intro zenon_H23 ]. % 1.53/1.80 apply zenon_H24. zenon_intro zenon_H25. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_h = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H22. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_h)); [idtac | apply NNPP; zenon_intro zenon_H20]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_H20 zenon_H25). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H23. zenon_intro zenon_H19. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_h). zenon_intro zenon_H26. % 1.53/1.80 generalize (zenon_H26 zenon_TX_bd). zenon_intro zenon_H27. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H27); [ zenon_intro zenon_H5 | zenon_intro zenon_H28 ]. % 1.53/1.80 exact (zenon_H5 zenon_H19). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H28); [ zenon_intro zenon_H2a | zenon_intro zenon_H29 ]. % 1.53/1.80 exact (zenon_H2a zenon_H1c). % 1.53/1.80 exact (zenon_H1b zenon_H29). % 1.53/1.80 apply zenon_H21. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L2_ *) % 1.53/1.80 assert (zenon_L3_ : forall (zenon_TX_bt : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U), (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TX_h zenon_TX_bd) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_bt)) -> (r1 zenon_TX_bd zenon_TX_bt) -> False). % 1.53/1.80 do 5 intro. intros zenon_H6 zenon_H3 zenon_H1c zenon_H4 zenon_H2b zenon_H2c. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_bd))/\(~(r1 zenon_TX_j zenon_TX_bd)))); [ zenon_intro zenon_H2e | zenon_intro zenon_H2f ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_H2e). zenon_intro zenon_H30. zenon_intro zenon_H1b. % 1.53/1.80 apply (zenon_L2_ zenon_TX_bd zenon_TX_h zenon_TY_i zenon_TX_j); trivial. % 1.53/1.80 cut ((r1 zenon_TX_bd zenon_TX_bt) = (r1 zenon_TX_j zenon_TX_bt)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H2b. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H2c. % 1.53/1.80 cut ((zenon_TX_bt = zenon_TX_bt)); [idtac | apply NNPP; zenon_intro zenon_H31]. % 1.53/1.80 cut ((zenon_TX_bd = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H32]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_H2f); [ zenon_intro zenon_H34 | zenon_intro zenon_H33 ]. % 1.53/1.80 apply zenon_H34. zenon_intro zenon_H35. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_bd = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H32. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_bd)); [idtac | apply NNPP; zenon_intro zenon_H30]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_H30 zenon_H35). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H33. zenon_intro zenon_H29. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_bd). zenon_intro zenon_H36. % 1.53/1.80 generalize (zenon_H36 zenon_TX_bt). zenon_intro zenon_H37. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H37); [ zenon_intro zenon_H1b | zenon_intro zenon_H38 ]. % 1.53/1.80 exact (zenon_H1b zenon_H29). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H38); [ zenon_intro zenon_H3a | zenon_intro zenon_H39 ]. % 1.53/1.80 exact (zenon_H3a zenon_H2c). % 1.53/1.80 exact (zenon_H2b zenon_H39). % 1.53/1.80 apply zenon_H31. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L3_ *) % 1.53/1.80 assert (zenon_L4_ : forall (zenon_TX_cj : zenon_U) (zenon_TX_bt : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_h : zenon_U), (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_bd zenon_TX_bt) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_cj)) -> (r1 zenon_TX_bt zenon_TX_cj) -> False). % 1.53/1.80 do 6 intro. intros zenon_H1c zenon_H3 zenon_H6 zenon_H2c zenon_H4 zenon_H3b zenon_H3c. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_bt))/\(~(r1 zenon_TX_j zenon_TX_bt)))); [ zenon_intro zenon_H3e | zenon_intro zenon_H3f ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_H3e). zenon_intro zenon_H40. zenon_intro zenon_H2b. % 1.53/1.80 apply (zenon_L3_ zenon_TX_bt zenon_TX_bd zenon_TX_j zenon_TX_h zenon_TY_i); trivial. % 1.53/1.80 cut ((r1 zenon_TX_bt zenon_TX_cj) = (r1 zenon_TX_j zenon_TX_cj)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H3b. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H3c. % 1.53/1.80 cut ((zenon_TX_cj = zenon_TX_cj)); [idtac | apply NNPP; zenon_intro zenon_H41]. % 1.53/1.80 cut ((zenon_TX_bt = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H42]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_H3f); [ zenon_intro zenon_H44 | zenon_intro zenon_H43 ]. % 1.53/1.80 apply zenon_H44. zenon_intro zenon_H45. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_bt = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H42. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_bt)); [idtac | apply NNPP; zenon_intro zenon_H40]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_H40 zenon_H45). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H43. zenon_intro zenon_H39. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_bt). zenon_intro zenon_H46. % 1.53/1.80 generalize (zenon_H46 zenon_TX_cj). zenon_intro zenon_H47. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H47); [ zenon_intro zenon_H2b | zenon_intro zenon_H48 ]. % 1.53/1.80 exact (zenon_H2b zenon_H39). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H48); [ zenon_intro zenon_H4a | zenon_intro zenon_H49 ]. % 1.53/1.80 exact (zenon_H4a zenon_H3c). % 1.53/1.80 exact (zenon_H3b zenon_H49). % 1.53/1.80 apply zenon_H41. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L4_ *) % 1.53/1.80 assert (zenon_L5_ : forall (zenon_TX_cz : zenon_U) (zenon_TX_cj : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_bt : zenon_U) (zenon_TX_bd : zenon_U), (r1 zenon_TX_bd zenon_TX_bt) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_bt zenon_TX_cj) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_cz)) -> (r1 zenon_TX_cj zenon_TX_cz) -> False). % 1.53/1.80 do 7 intro. intros zenon_H2c zenon_H6 zenon_H3 zenon_H1c zenon_H3c zenon_H4 zenon_H4b zenon_H4c. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_cj))/\(~(r1 zenon_TX_j zenon_TX_cj)))); [ zenon_intro zenon_H4e | zenon_intro zenon_H4f ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_H4e). zenon_intro zenon_H50. zenon_intro zenon_H3b. % 1.53/1.80 apply (zenon_L4_ zenon_TX_cj zenon_TX_bt zenon_TY_i zenon_TX_j zenon_TX_bd zenon_TX_h); trivial. % 1.53/1.80 cut ((r1 zenon_TX_cj zenon_TX_cz) = (r1 zenon_TX_j zenon_TX_cz)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H4b. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H4c. % 1.53/1.80 cut ((zenon_TX_cz = zenon_TX_cz)); [idtac | apply NNPP; zenon_intro zenon_H51]. % 1.53/1.80 cut ((zenon_TX_cj = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H52]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_H4f); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 1.53/1.80 apply zenon_H54. zenon_intro zenon_H55. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_cj = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H52. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_cj)); [idtac | apply NNPP; zenon_intro zenon_H50]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_H50 zenon_H55). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H53. zenon_intro zenon_H49. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_cj). zenon_intro zenon_H56. % 1.53/1.80 generalize (zenon_H56 zenon_TX_cz). zenon_intro zenon_H57. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H57); [ zenon_intro zenon_H3b | zenon_intro zenon_H58 ]. % 1.53/1.80 exact (zenon_H3b zenon_H49). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H58); [ zenon_intro zenon_H5a | zenon_intro zenon_H59 ]. % 1.53/1.80 exact (zenon_H5a zenon_H4c). % 1.53/1.80 exact (zenon_H4b zenon_H59). % 1.53/1.80 apply zenon_H51. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L5_ *) % 1.53/1.80 assert (zenon_L6_ : forall (zenon_TX_dp : zenon_U) (zenon_TX_cz : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_h : zenon_U) (zenon_TX_cj : zenon_U) (zenon_TX_bt : zenon_U), (r1 zenon_TX_bt zenon_TX_cj) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_bd zenon_TX_bt) -> (r1 zenon_TX_cj zenon_TX_cz) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_dp)) -> (r1 zenon_TX_cz zenon_TX_dp) -> False). % 1.53/1.80 do 8 intro. intros zenon_H3c zenon_H1c zenon_H3 zenon_H6 zenon_H2c zenon_H4c zenon_H4 zenon_H5b zenon_H5c. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_cz))/\(~(r1 zenon_TX_j zenon_TX_cz)))); [ zenon_intro zenon_H5e | zenon_intro zenon_H5f ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_H5e). zenon_intro zenon_H60. zenon_intro zenon_H4b. % 1.53/1.80 apply (zenon_L5_ zenon_TX_cz zenon_TX_cj zenon_TX_j zenon_TX_h zenon_TY_i zenon_TX_bt zenon_TX_bd); trivial. % 1.53/1.80 cut ((r1 zenon_TX_cz zenon_TX_dp) = (r1 zenon_TX_j zenon_TX_dp)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H5b. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H5c. % 1.53/1.80 cut ((zenon_TX_dp = zenon_TX_dp)); [idtac | apply NNPP; zenon_intro zenon_H61]. % 1.53/1.80 cut ((zenon_TX_cz = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H62]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_H5f); [ zenon_intro zenon_H64 | zenon_intro zenon_H63 ]. % 1.53/1.80 apply zenon_H64. zenon_intro zenon_H65. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_cz = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H62. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_cz)); [idtac | apply NNPP; zenon_intro zenon_H60]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_H60 zenon_H65). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H63. zenon_intro zenon_H59. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_cz). zenon_intro zenon_H66. % 1.53/1.80 generalize (zenon_H66 zenon_TX_dp). zenon_intro zenon_H67. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H67); [ zenon_intro zenon_H4b | zenon_intro zenon_H68 ]. % 1.53/1.80 exact (zenon_H4b zenon_H59). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H68); [ zenon_intro zenon_H6a | zenon_intro zenon_H69 ]. % 1.53/1.80 exact (zenon_H6a zenon_H5c). % 1.53/1.80 exact (zenon_H5b zenon_H69). % 1.53/1.80 apply zenon_H61. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L6_ *) % 1.53/1.80 assert (zenon_L7_ : forall (zenon_TX_ef : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_bt : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_cz : zenon_U) (zenon_TX_cj : zenon_U), (r1 zenon_TX_cj zenon_TX_cz) -> (r1 zenon_TX_bd zenon_TX_bt) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_bt zenon_TX_cj) -> (r1 zenon_TX_cz zenon_TX_dp) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_ef)) -> (r1 zenon_TX_dp zenon_TX_ef) -> False). % 1.53/1.80 do 9 intro. intros zenon_H4c zenon_H2c zenon_H6 zenon_H3 zenon_H1c zenon_H3c zenon_H5c zenon_H4 zenon_H6b zenon_H6c. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_dp))/\(~(r1 zenon_TX_j zenon_TX_dp)))); [ zenon_intro zenon_H6e | zenon_intro zenon_H6f ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_H6e). zenon_intro zenon_H70. zenon_intro zenon_H5b. % 1.53/1.80 apply (zenon_L6_ zenon_TX_dp zenon_TX_cz zenon_TY_i zenon_TX_j zenon_TX_bd zenon_TX_h zenon_TX_cj zenon_TX_bt); trivial. % 1.53/1.80 cut ((r1 zenon_TX_dp zenon_TX_ef) = (r1 zenon_TX_j zenon_TX_ef)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H6b. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H6c. % 1.53/1.80 cut ((zenon_TX_ef = zenon_TX_ef)); [idtac | apply NNPP; zenon_intro zenon_H71]. % 1.53/1.80 cut ((zenon_TX_dp = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H72]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_H6f); [ zenon_intro zenon_H74 | zenon_intro zenon_H73 ]. % 1.53/1.80 apply zenon_H74. zenon_intro zenon_H75. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_dp = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H72. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_dp)); [idtac | apply NNPP; zenon_intro zenon_H70]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_H70 zenon_H75). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H73. zenon_intro zenon_H69. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_dp). zenon_intro zenon_H76. % 1.53/1.80 generalize (zenon_H76 zenon_TX_ef). zenon_intro zenon_H77. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H77); [ zenon_intro zenon_H5b | zenon_intro zenon_H78 ]. % 1.53/1.80 exact (zenon_H5b zenon_H69). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H78); [ zenon_intro zenon_H7a | zenon_intro zenon_H79 ]. % 1.53/1.80 exact (zenon_H7a zenon_H6c). % 1.53/1.80 exact (zenon_H6b zenon_H79). % 1.53/1.80 apply zenon_H71. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L7_ *) % 1.53/1.80 assert (zenon_L8_ : forall (zenon_TX_ev : zenon_U) (zenon_TX_ef : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_h : zenon_U) (zenon_TX_cj : zenon_U) (zenon_TX_bt : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_cz : zenon_U), (r1 zenon_TX_cz zenon_TX_dp) -> (r1 zenon_TX_bt zenon_TX_cj) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_bd zenon_TX_bt) -> (r1 zenon_TX_cj zenon_TX_cz) -> (r1 zenon_TX_dp zenon_TX_ef) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_ev)) -> (r1 zenon_TX_ef zenon_TX_ev) -> False). % 1.53/1.80 do 10 intro. intros zenon_H5c zenon_H3c zenon_H1c zenon_H3 zenon_H6 zenon_H2c zenon_H4c zenon_H6c zenon_H4 zenon_H7b zenon_H7c. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_ef))/\(~(r1 zenon_TX_j zenon_TX_ef)))); [ zenon_intro zenon_H7e | zenon_intro zenon_H7f ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_H7e). zenon_intro zenon_H80. zenon_intro zenon_H6b. % 1.53/1.80 apply (zenon_L7_ zenon_TX_ef zenon_TX_dp zenon_TX_j zenon_TX_h zenon_TY_i zenon_TX_bt zenon_TX_bd zenon_TX_cz zenon_TX_cj); trivial. % 1.53/1.80 cut ((r1 zenon_TX_ef zenon_TX_ev) = (r1 zenon_TX_j zenon_TX_ev)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H7b. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H7c. % 1.53/1.80 cut ((zenon_TX_ev = zenon_TX_ev)); [idtac | apply NNPP; zenon_intro zenon_H81]. % 1.53/1.80 cut ((zenon_TX_ef = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H82]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_H7f); [ zenon_intro zenon_H84 | zenon_intro zenon_H83 ]. % 1.53/1.80 apply zenon_H84. zenon_intro zenon_H85. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_ef = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H82. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_ef)); [idtac | apply NNPP; zenon_intro zenon_H80]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_H80 zenon_H85). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H83. zenon_intro zenon_H79. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_ef). zenon_intro zenon_H86. % 1.53/1.80 generalize (zenon_H86 zenon_TX_ev). zenon_intro zenon_H87. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H87); [ zenon_intro zenon_H6b | zenon_intro zenon_H88 ]. % 1.53/1.80 exact (zenon_H6b zenon_H79). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H88); [ zenon_intro zenon_H8a | zenon_intro zenon_H89 ]. % 1.53/1.80 exact (zenon_H8a zenon_H7c). % 1.53/1.80 exact (zenon_H7b zenon_H89). % 1.53/1.80 apply zenon_H81. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L8_ *) % 1.53/1.80 assert (zenon_L9_ : forall (zenon_TX_fl : zenon_U) (zenon_TX_ev : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_bt : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_cz : zenon_U) (zenon_TX_cj : zenon_U) (zenon_TX_ef : zenon_U) (zenon_TX_dp : zenon_U), (r1 zenon_TX_dp zenon_TX_ef) -> (r1 zenon_TX_cj zenon_TX_cz) -> (r1 zenon_TX_bd zenon_TX_bt) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_bt zenon_TX_cj) -> (r1 zenon_TX_cz zenon_TX_dp) -> (r1 zenon_TX_ef zenon_TX_ev) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_fl)) -> (r1 zenon_TX_ev zenon_TX_fl) -> False). % 1.53/1.80 do 11 intro. intros zenon_H6c zenon_H4c zenon_H2c zenon_H6 zenon_H3 zenon_H1c zenon_H3c zenon_H5c zenon_H7c zenon_H4 zenon_H8b zenon_H8c. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_ev))/\(~(r1 zenon_TX_j zenon_TX_ev)))); [ zenon_intro zenon_H8e | zenon_intro zenon_H8f ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_H8e). zenon_intro zenon_H90. zenon_intro zenon_H7b. % 1.53/1.80 apply (zenon_L8_ zenon_TX_ev zenon_TX_ef zenon_TY_i zenon_TX_j zenon_TX_bd zenon_TX_h zenon_TX_cj zenon_TX_bt zenon_TX_dp zenon_TX_cz); trivial. % 1.53/1.80 cut ((r1 zenon_TX_ev zenon_TX_fl) = (r1 zenon_TX_j zenon_TX_fl)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H8b. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H8c. % 1.53/1.80 cut ((zenon_TX_fl = zenon_TX_fl)); [idtac | apply NNPP; zenon_intro zenon_H91]. % 1.53/1.80 cut ((zenon_TX_ev = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H92]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_H8f); [ zenon_intro zenon_H94 | zenon_intro zenon_H93 ]. % 1.53/1.80 apply zenon_H94. zenon_intro zenon_H95. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_ev = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H92. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_ev)); [idtac | apply NNPP; zenon_intro zenon_H90]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_H90 zenon_H95). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H93. zenon_intro zenon_H89. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_ev). zenon_intro zenon_H96. % 1.53/1.80 generalize (zenon_H96 zenon_TX_fl). zenon_intro zenon_H97. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H97); [ zenon_intro zenon_H7b | zenon_intro zenon_H98 ]. % 1.53/1.80 exact (zenon_H7b zenon_H89). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H98); [ zenon_intro zenon_H9a | zenon_intro zenon_H99 ]. % 1.53/1.80 exact (zenon_H9a zenon_H8c). % 1.53/1.80 exact (zenon_H8b zenon_H99). % 1.53/1.80 apply zenon_H91. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L9_ *) % 1.53/1.80 assert (zenon_L10_ : forall (zenon_TX_gb : zenon_U) (zenon_TX_fl : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_h : zenon_U) (zenon_TX_cj : zenon_U) (zenon_TX_bt : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_cz : zenon_U) (zenon_TX_ev : zenon_U) (zenon_TX_ef : zenon_U), (r1 zenon_TX_ef zenon_TX_ev) -> (r1 zenon_TX_cz zenon_TX_dp) -> (r1 zenon_TX_bt zenon_TX_cj) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_bd zenon_TX_bt) -> (r1 zenon_TX_cj zenon_TX_cz) -> (r1 zenon_TX_dp zenon_TX_ef) -> (r1 zenon_TX_ev zenon_TX_fl) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_gb)) -> (r1 zenon_TX_fl zenon_TX_gb) -> False). % 1.53/1.80 do 12 intro. intros zenon_H7c zenon_H5c zenon_H3c zenon_H1c zenon_H3 zenon_H6 zenon_H2c zenon_H4c zenon_H6c zenon_H8c zenon_H4 zenon_H9b zenon_H9c. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_fl))/\(~(r1 zenon_TX_j zenon_TX_fl)))); [ zenon_intro zenon_H9e | zenon_intro zenon_H9f ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_H9e). zenon_intro zenon_Ha0. zenon_intro zenon_H8b. % 1.53/1.80 apply (zenon_L9_ zenon_TX_fl zenon_TX_ev zenon_TX_j zenon_TX_h zenon_TY_i zenon_TX_bt zenon_TX_bd zenon_TX_cz zenon_TX_cj zenon_TX_ef zenon_TX_dp); trivial. % 1.53/1.80 cut ((r1 zenon_TX_fl zenon_TX_gb) = (r1 zenon_TX_j zenon_TX_gb)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H9b. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H9c. % 1.53/1.80 cut ((zenon_TX_gb = zenon_TX_gb)); [idtac | apply NNPP; zenon_intro zenon_Ha1]. % 1.53/1.80 cut ((zenon_TX_fl = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_Ha2]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_H9f); [ zenon_intro zenon_Ha4 | zenon_intro zenon_Ha3 ]. % 1.53/1.80 apply zenon_Ha4. zenon_intro zenon_Ha5. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_fl = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_Ha2. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_fl)); [idtac | apply NNPP; zenon_intro zenon_Ha0]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_Ha0 zenon_Ha5). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_Ha3. zenon_intro zenon_H99. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_fl). zenon_intro zenon_Ha6. % 1.53/1.80 generalize (zenon_Ha6 zenon_TX_gb). zenon_intro zenon_Ha7. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_Ha7); [ zenon_intro zenon_H8b | zenon_intro zenon_Ha8 ]. % 1.53/1.80 exact (zenon_H8b zenon_H99). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_Ha8); [ zenon_intro zenon_Haa | zenon_intro zenon_Ha9 ]. % 1.53/1.80 exact (zenon_Haa zenon_H9c). % 1.53/1.80 exact (zenon_H9b zenon_Ha9). % 1.53/1.80 apply zenon_Ha1. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L10_ *) % 1.53/1.80 assert (zenon_L11_ : forall (zenon_TX_gr : zenon_U) (zenon_TX_gb : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_bt : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_cz : zenon_U) (zenon_TX_cj : zenon_U) (zenon_TX_ef : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_fl : zenon_U) (zenon_TX_ev : zenon_U), (r1 zenon_TX_ev zenon_TX_fl) -> (r1 zenon_TX_dp zenon_TX_ef) -> (r1 zenon_TX_cj zenon_TX_cz) -> (r1 zenon_TX_bd zenon_TX_bt) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_bt zenon_TX_cj) -> (r1 zenon_TX_cz zenon_TX_dp) -> (r1 zenon_TX_ef zenon_TX_ev) -> (r1 zenon_TX_fl zenon_TX_gb) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_gr)) -> (r1 zenon_TX_gb zenon_TX_gr) -> False). % 1.53/1.80 do 13 intro. intros zenon_H8c zenon_H6c zenon_H4c zenon_H2c zenon_H6 zenon_H3 zenon_H1c zenon_H3c zenon_H5c zenon_H7c zenon_H9c zenon_H4 zenon_Hab zenon_Hac. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_gb))/\(~(r1 zenon_TX_j zenon_TX_gb)))); [ zenon_intro zenon_Hae | zenon_intro zenon_Haf ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_Hae). zenon_intro zenon_Hb0. zenon_intro zenon_H9b. % 1.53/1.80 apply (zenon_L10_ zenon_TX_gb zenon_TX_fl zenon_TY_i zenon_TX_j zenon_TX_bd zenon_TX_h zenon_TX_cj zenon_TX_bt zenon_TX_dp zenon_TX_cz zenon_TX_ev zenon_TX_ef); trivial. % 1.53/1.80 cut ((r1 zenon_TX_gb zenon_TX_gr) = (r1 zenon_TX_j zenon_TX_gr)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_Hab. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_Hac. % 1.53/1.80 cut ((zenon_TX_gr = zenon_TX_gr)); [idtac | apply NNPP; zenon_intro zenon_Hb1]. % 1.53/1.80 cut ((zenon_TX_gb = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_Hb2]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_Haf); [ zenon_intro zenon_Hb4 | zenon_intro zenon_Hb3 ]. % 1.53/1.80 apply zenon_Hb4. zenon_intro zenon_Hb5. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_gb = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_Hb2. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_gb)); [idtac | apply NNPP; zenon_intro zenon_Hb0]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_Hb0 zenon_Hb5). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_Hb3. zenon_intro zenon_Ha9. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_gb). zenon_intro zenon_Hb6. % 1.53/1.80 generalize (zenon_Hb6 zenon_TX_gr). zenon_intro zenon_Hb7. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_Hb7); [ zenon_intro zenon_H9b | zenon_intro zenon_Hb8 ]. % 1.53/1.80 exact (zenon_H9b zenon_Ha9). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_Hb8); [ zenon_intro zenon_Hba | zenon_intro zenon_Hb9 ]. % 1.53/1.80 exact (zenon_Hba zenon_Hac). % 1.53/1.80 exact (zenon_Hab zenon_Hb9). % 1.53/1.80 apply zenon_Hb1. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L11_ *) % 1.53/1.80 assert (zenon_L12_ : forall (zenon_TX_hh : zenon_U) (zenon_TX_gr : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_h : zenon_U) (zenon_TX_cj : zenon_U) (zenon_TX_bt : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_cz : zenon_U) (zenon_TX_ev : zenon_U) (zenon_TX_ef : zenon_U) (zenon_TX_gb : zenon_U) (zenon_TX_fl : zenon_U), (r1 zenon_TX_fl zenon_TX_gb) -> (r1 zenon_TX_ef zenon_TX_ev) -> (r1 zenon_TX_cz zenon_TX_dp) -> (r1 zenon_TX_bt zenon_TX_cj) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_bd zenon_TX_bt) -> (r1 zenon_TX_cj zenon_TX_cz) -> (r1 zenon_TX_dp zenon_TX_ef) -> (r1 zenon_TX_ev zenon_TX_fl) -> (r1 zenon_TX_gb zenon_TX_gr) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_hh)) -> (r1 zenon_TX_gr zenon_TX_hh) -> False). % 1.53/1.80 do 14 intro. intros zenon_H9c zenon_H7c zenon_H5c zenon_H3c zenon_H1c zenon_H3 zenon_H6 zenon_H2c zenon_H4c zenon_H6c zenon_H8c zenon_Hac zenon_H4 zenon_Hbb zenon_Hbc. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_gr))/\(~(r1 zenon_TX_j zenon_TX_gr)))); [ zenon_intro zenon_Hbe | zenon_intro zenon_Hbf ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_Hbe). zenon_intro zenon_Hc0. zenon_intro zenon_Hab. % 1.53/1.80 apply (zenon_L11_ zenon_TX_gr zenon_TX_gb zenon_TX_j zenon_TX_h zenon_TY_i zenon_TX_bt zenon_TX_bd zenon_TX_cz zenon_TX_cj zenon_TX_ef zenon_TX_dp zenon_TX_fl zenon_TX_ev); trivial. % 1.53/1.80 cut ((r1 zenon_TX_gr zenon_TX_hh) = (r1 zenon_TX_j zenon_TX_hh)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_Hbb. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_Hbc. % 1.53/1.80 cut ((zenon_TX_hh = zenon_TX_hh)); [idtac | apply NNPP; zenon_intro zenon_Hc1]. % 1.53/1.80 cut ((zenon_TX_gr = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_Hc2]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_Hbf); [ zenon_intro zenon_Hc4 | zenon_intro zenon_Hc3 ]. % 1.53/1.80 apply zenon_Hc4. zenon_intro zenon_Hc5. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_gr = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_Hc2. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_gr)); [idtac | apply NNPP; zenon_intro zenon_Hc0]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_Hc0 zenon_Hc5). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_Hc3. zenon_intro zenon_Hb9. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_gr). zenon_intro zenon_Hc6. % 1.53/1.80 generalize (zenon_Hc6 zenon_TX_hh). zenon_intro zenon_Hc7. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_Hc7); [ zenon_intro zenon_Hab | zenon_intro zenon_Hc8 ]. % 1.53/1.80 exact (zenon_Hab zenon_Hb9). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_Hc8); [ zenon_intro zenon_Hca | zenon_intro zenon_Hc9 ]. % 1.53/1.80 exact (zenon_Hca zenon_Hbc). % 1.53/1.80 exact (zenon_Hbb zenon_Hc9). % 1.53/1.80 apply zenon_Hc1. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L12_ *) % 1.53/1.80 assert (zenon_L13_ : forall (zenon_TX_hx : zenon_U) (zenon_TX_hh : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_bt : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_cz : zenon_U) (zenon_TX_cj : zenon_U) (zenon_TX_ef : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_fl : zenon_U) (zenon_TX_ev : zenon_U) (zenon_TX_gr : zenon_U) (zenon_TX_gb : zenon_U), (r1 zenon_TX_gb zenon_TX_gr) -> (r1 zenon_TX_ev zenon_TX_fl) -> (r1 zenon_TX_dp zenon_TX_ef) -> (r1 zenon_TX_cj zenon_TX_cz) -> (r1 zenon_TX_bd zenon_TX_bt) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_bt zenon_TX_cj) -> (r1 zenon_TX_cz zenon_TX_dp) -> (r1 zenon_TX_ef zenon_TX_ev) -> (r1 zenon_TX_fl zenon_TX_gb) -> (r1 zenon_TX_gr zenon_TX_hh) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_hx)) -> (r1 zenon_TX_hh zenon_TX_hx) -> False). % 1.53/1.80 do 15 intro. intros zenon_Hac zenon_H8c zenon_H6c zenon_H4c zenon_H2c zenon_H6 zenon_H3 zenon_H1c zenon_H3c zenon_H5c zenon_H7c zenon_H9c zenon_Hbc zenon_H4 zenon_Hcb zenon_Hcc. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_hh))/\(~(r1 zenon_TX_j zenon_TX_hh)))); [ zenon_intro zenon_Hce | zenon_intro zenon_Hcf ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_Hce). zenon_intro zenon_Hd0. zenon_intro zenon_Hbb. % 1.53/1.80 apply (zenon_L12_ zenon_TX_hh zenon_TX_gr zenon_TY_i zenon_TX_j zenon_TX_bd zenon_TX_h zenon_TX_cj zenon_TX_bt zenon_TX_dp zenon_TX_cz zenon_TX_ev zenon_TX_ef zenon_TX_gb zenon_TX_fl); trivial. % 1.53/1.80 cut ((r1 zenon_TX_hh zenon_TX_hx) = (r1 zenon_TX_j zenon_TX_hx)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_Hcb. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_Hcc. % 1.53/1.80 cut ((zenon_TX_hx = zenon_TX_hx)); [idtac | apply NNPP; zenon_intro zenon_Hd1]. % 1.53/1.80 cut ((zenon_TX_hh = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_Hd2]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_Hcf); [ zenon_intro zenon_Hd4 | zenon_intro zenon_Hd3 ]. % 1.53/1.80 apply zenon_Hd4. zenon_intro zenon_Hd5. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_hh = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_Hd2. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_hh)); [idtac | apply NNPP; zenon_intro zenon_Hd0]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_Hd0 zenon_Hd5). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_Hd3. zenon_intro zenon_Hc9. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_hh). zenon_intro zenon_Hd6. % 1.53/1.80 generalize (zenon_Hd6 zenon_TX_hx). zenon_intro zenon_Hd7. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_Hd7); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hd8 ]. % 1.53/1.80 exact (zenon_Hbb zenon_Hc9). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_Hd8); [ zenon_intro zenon_Hda | zenon_intro zenon_Hd9 ]. % 1.53/1.80 exact (zenon_Hda zenon_Hcc). % 1.53/1.80 exact (zenon_Hcb zenon_Hd9). % 1.53/1.80 apply zenon_Hd1. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L13_ *) % 1.53/1.80 assert (zenon_L14_ : forall (zenon_TX_in : zenon_U) (zenon_TX_hx : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_h : zenon_U) (zenon_TX_cj : zenon_U) (zenon_TX_bt : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_cz : zenon_U) (zenon_TX_ev : zenon_U) (zenon_TX_ef : zenon_U) (zenon_TX_gb : zenon_U) (zenon_TX_fl : zenon_U) (zenon_TX_hh : zenon_U) (zenon_TX_gr : zenon_U), (r1 zenon_TX_gr zenon_TX_hh) -> (r1 zenon_TX_fl zenon_TX_gb) -> (r1 zenon_TX_ef zenon_TX_ev) -> (r1 zenon_TX_cz zenon_TX_dp) -> (r1 zenon_TX_bt zenon_TX_cj) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_bd zenon_TX_bt) -> (r1 zenon_TX_cj zenon_TX_cz) -> (r1 zenon_TX_dp zenon_TX_ef) -> (r1 zenon_TX_ev zenon_TX_fl) -> (r1 zenon_TX_gb zenon_TX_gr) -> (r1 zenon_TX_hh zenon_TX_hx) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_in)) -> (r1 zenon_TX_hx zenon_TX_in) -> False). % 1.53/1.80 do 16 intro. intros zenon_Hbc zenon_H9c zenon_H7c zenon_H5c zenon_H3c zenon_H1c zenon_H3 zenon_H6 zenon_H2c zenon_H4c zenon_H6c zenon_H8c zenon_Hac zenon_Hcc zenon_H4 zenon_Hdb zenon_Hdc. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_hx))/\(~(r1 zenon_TX_j zenon_TX_hx)))); [ zenon_intro zenon_Hde | zenon_intro zenon_Hdf ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_Hde). zenon_intro zenon_He0. zenon_intro zenon_Hcb. % 1.53/1.80 apply (zenon_L13_ zenon_TX_hx zenon_TX_hh zenon_TX_j zenon_TX_h zenon_TY_i zenon_TX_bt zenon_TX_bd zenon_TX_cz zenon_TX_cj zenon_TX_ef zenon_TX_dp zenon_TX_fl zenon_TX_ev zenon_TX_gr zenon_TX_gb); trivial. % 1.53/1.80 cut ((r1 zenon_TX_hx zenon_TX_in) = (r1 zenon_TX_j zenon_TX_in)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_Hdb. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_Hdc. % 1.53/1.80 cut ((zenon_TX_in = zenon_TX_in)); [idtac | apply NNPP; zenon_intro zenon_He1]. % 1.53/1.80 cut ((zenon_TX_hx = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_He2]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_Hdf); [ zenon_intro zenon_He4 | zenon_intro zenon_He3 ]. % 1.53/1.80 apply zenon_He4. zenon_intro zenon_He5. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_hx = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_He2. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_hx)); [idtac | apply NNPP; zenon_intro zenon_He0]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_He0 zenon_He5). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_He3. zenon_intro zenon_Hd9. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_hx). zenon_intro zenon_He6. % 1.53/1.80 generalize (zenon_He6 zenon_TX_in). zenon_intro zenon_He7. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_He7); [ zenon_intro zenon_Hcb | zenon_intro zenon_He8 ]. % 1.53/1.80 exact (zenon_Hcb zenon_Hd9). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_He8); [ zenon_intro zenon_Hea | zenon_intro zenon_He9 ]. % 1.53/1.80 exact (zenon_Hea zenon_Hdc). % 1.53/1.80 exact (zenon_Hdb zenon_He9). % 1.53/1.80 apply zenon_He1. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L14_ *) % 1.53/1.80 assert (zenon_L15_ : forall (zenon_TX_jd : zenon_U) (zenon_TX_in : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_bt : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_cz : zenon_U) (zenon_TX_cj : zenon_U) (zenon_TX_ef : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_fl : zenon_U) (zenon_TX_ev : zenon_U) (zenon_TX_gr : zenon_U) (zenon_TX_gb : zenon_U) (zenon_TX_hx : zenon_U) (zenon_TX_hh : zenon_U), (r1 zenon_TX_hh zenon_TX_hx) -> (r1 zenon_TX_gb zenon_TX_gr) -> (r1 zenon_TX_ev zenon_TX_fl) -> (r1 zenon_TX_dp zenon_TX_ef) -> (r1 zenon_TX_cj zenon_TX_cz) -> (r1 zenon_TX_bd zenon_TX_bt) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_bt zenon_TX_cj) -> (r1 zenon_TX_cz zenon_TX_dp) -> (r1 zenon_TX_ef zenon_TX_ev) -> (r1 zenon_TX_fl zenon_TX_gb) -> (r1 zenon_TX_gr zenon_TX_hh) -> (r1 zenon_TX_hx zenon_TX_in) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_jd)) -> (r1 zenon_TX_in zenon_TX_jd) -> False). % 1.53/1.80 do 17 intro. intros zenon_Hcc zenon_Hac zenon_H8c zenon_H6c zenon_H4c zenon_H2c zenon_H6 zenon_H3 zenon_H1c zenon_H3c zenon_H5c zenon_H7c zenon_H9c zenon_Hbc zenon_Hdc zenon_H4 zenon_Heb zenon_Hec. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_in))/\(~(r1 zenon_TX_j zenon_TX_in)))); [ zenon_intro zenon_Hee | zenon_intro zenon_Hef ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_Hee). zenon_intro zenon_Hf0. zenon_intro zenon_Hdb. % 1.53/1.80 apply (zenon_L14_ zenon_TX_in zenon_TX_hx zenon_TY_i zenon_TX_j zenon_TX_bd zenon_TX_h zenon_TX_cj zenon_TX_bt zenon_TX_dp zenon_TX_cz zenon_TX_ev zenon_TX_ef zenon_TX_gb zenon_TX_fl zenon_TX_hh zenon_TX_gr); trivial. % 1.53/1.80 cut ((r1 zenon_TX_in zenon_TX_jd) = (r1 zenon_TX_j zenon_TX_jd)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_Heb. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_Hec. % 1.53/1.80 cut ((zenon_TX_jd = zenon_TX_jd)); [idtac | apply NNPP; zenon_intro zenon_Hf1]. % 1.53/1.80 cut ((zenon_TX_in = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_Hf2]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_Hef); [ zenon_intro zenon_Hf4 | zenon_intro zenon_Hf3 ]. % 1.53/1.80 apply zenon_Hf4. zenon_intro zenon_Hf5. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_in = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_Hf2. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_in)); [idtac | apply NNPP; zenon_intro zenon_Hf0]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_Hf0 zenon_Hf5). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_Hf3. zenon_intro zenon_He9. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_in). zenon_intro zenon_Hf6. % 1.53/1.80 generalize (zenon_Hf6 zenon_TX_jd). zenon_intro zenon_Hf7. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_Hf7); [ zenon_intro zenon_Hdb | zenon_intro zenon_Hf8 ]. % 1.53/1.80 exact (zenon_Hdb zenon_He9). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_Hf8); [ zenon_intro zenon_Hfa | zenon_intro zenon_Hf9 ]. % 1.53/1.80 exact (zenon_Hfa zenon_Hec). % 1.53/1.80 exact (zenon_Heb zenon_Hf9). % 1.53/1.80 apply zenon_Hf1. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L15_ *) % 1.53/1.80 assert (zenon_L16_ : forall (zenon_TX_jt : zenon_U) (zenon_TX_jd : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_h : zenon_U) (zenon_TX_cj : zenon_U) (zenon_TX_bt : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_cz : zenon_U) (zenon_TX_ev : zenon_U) (zenon_TX_ef : zenon_U) (zenon_TX_gb : zenon_U) (zenon_TX_fl : zenon_U) (zenon_TX_hh : zenon_U) (zenon_TX_gr : zenon_U) (zenon_TX_in : zenon_U) (zenon_TX_hx : zenon_U), (r1 zenon_TX_hx zenon_TX_in) -> (r1 zenon_TX_gr zenon_TX_hh) -> (r1 zenon_TX_fl zenon_TX_gb) -> (r1 zenon_TX_ef zenon_TX_ev) -> (r1 zenon_TX_cz zenon_TX_dp) -> (r1 zenon_TX_bt zenon_TX_cj) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_bd zenon_TX_bt) -> (r1 zenon_TX_cj zenon_TX_cz) -> (r1 zenon_TX_dp zenon_TX_ef) -> (r1 zenon_TX_ev zenon_TX_fl) -> (r1 zenon_TX_gb zenon_TX_gr) -> (r1 zenon_TX_hh zenon_TX_hx) -> (r1 zenon_TX_in zenon_TX_jd) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_jt)) -> (r1 zenon_TX_jd zenon_TX_jt) -> False). % 1.53/1.80 do 18 intro. intros zenon_Hdc zenon_Hbc zenon_H9c zenon_H7c zenon_H5c zenon_H3c zenon_H1c zenon_H3 zenon_H6 zenon_H2c zenon_H4c zenon_H6c zenon_H8c zenon_Hac zenon_Hcc zenon_Hec zenon_H4 zenon_Hfb zenon_Hfc. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_jd))/\(~(r1 zenon_TX_j zenon_TX_jd)))); [ zenon_intro zenon_Hfe | zenon_intro zenon_Hff ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_Hfe). zenon_intro zenon_H100. zenon_intro zenon_Heb. % 1.53/1.80 apply (zenon_L15_ zenon_TX_jd zenon_TX_in zenon_TX_j zenon_TX_h zenon_TY_i zenon_TX_bt zenon_TX_bd zenon_TX_cz zenon_TX_cj zenon_TX_ef zenon_TX_dp zenon_TX_fl zenon_TX_ev zenon_TX_gr zenon_TX_gb zenon_TX_hx zenon_TX_hh); trivial. % 1.53/1.80 cut ((r1 zenon_TX_jd zenon_TX_jt) = (r1 zenon_TX_j zenon_TX_jt)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_Hfb. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_Hfc. % 1.53/1.80 cut ((zenon_TX_jt = zenon_TX_jt)); [idtac | apply NNPP; zenon_intro zenon_H101]. % 1.53/1.80 cut ((zenon_TX_jd = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H102]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_Hff); [ zenon_intro zenon_H104 | zenon_intro zenon_H103 ]. % 1.53/1.80 apply zenon_H104. zenon_intro zenon_H105. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_jd = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H102. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_jd)); [idtac | apply NNPP; zenon_intro zenon_H100]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_H100 zenon_H105). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H103. zenon_intro zenon_Hf9. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_jd). zenon_intro zenon_H106. % 1.53/1.80 generalize (zenon_H106 zenon_TX_jt). zenon_intro zenon_H107. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H107); [ zenon_intro zenon_Heb | zenon_intro zenon_H108 ]. % 1.53/1.80 exact (zenon_Heb zenon_Hf9). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H108); [ zenon_intro zenon_H10a | zenon_intro zenon_H109 ]. % 1.53/1.80 exact (zenon_H10a zenon_Hfc). % 1.53/1.80 exact (zenon_Hfb zenon_H109). % 1.53/1.80 apply zenon_H101. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L16_ *) % 1.53/1.80 assert (zenon_L17_ : forall (zenon_TX_kj : zenon_U) (zenon_TX_jt : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_bt : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_cz : zenon_U) (zenon_TX_cj : zenon_U) (zenon_TX_ef : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_fl : zenon_U) (zenon_TX_ev : zenon_U) (zenon_TX_gr : zenon_U) (zenon_TX_gb : zenon_U) (zenon_TX_hx : zenon_U) (zenon_TX_hh : zenon_U) (zenon_TX_jd : zenon_U) (zenon_TX_in : zenon_U), (r1 zenon_TX_in zenon_TX_jd) -> (r1 zenon_TX_hh zenon_TX_hx) -> (r1 zenon_TX_gb zenon_TX_gr) -> (r1 zenon_TX_ev zenon_TX_fl) -> (r1 zenon_TX_dp zenon_TX_ef) -> (r1 zenon_TX_cj zenon_TX_cz) -> (r1 zenon_TX_bd zenon_TX_bt) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_bt zenon_TX_cj) -> (r1 zenon_TX_cz zenon_TX_dp) -> (r1 zenon_TX_ef zenon_TX_ev) -> (r1 zenon_TX_fl zenon_TX_gb) -> (r1 zenon_TX_gr zenon_TX_hh) -> (r1 zenon_TX_hx zenon_TX_in) -> (r1 zenon_TX_jd zenon_TX_jt) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_kj)) -> (r1 zenon_TX_jt zenon_TX_kj) -> False). % 1.53/1.80 do 19 intro. intros zenon_Hec zenon_Hcc zenon_Hac zenon_H8c zenon_H6c zenon_H4c zenon_H2c zenon_H6 zenon_H3 zenon_H1c zenon_H3c zenon_H5c zenon_H7c zenon_H9c zenon_Hbc zenon_Hdc zenon_Hfc zenon_H4 zenon_H10b zenon_H10c. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_jt))/\(~(r1 zenon_TX_j zenon_TX_jt)))); [ zenon_intro zenon_H10e | zenon_intro zenon_H10f ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_H10e). zenon_intro zenon_H110. zenon_intro zenon_Hfb. % 1.53/1.80 apply (zenon_L16_ zenon_TX_jt zenon_TX_jd zenon_TY_i zenon_TX_j zenon_TX_bd zenon_TX_h zenon_TX_cj zenon_TX_bt zenon_TX_dp zenon_TX_cz zenon_TX_ev zenon_TX_ef zenon_TX_gb zenon_TX_fl zenon_TX_hh zenon_TX_gr zenon_TX_in zenon_TX_hx); trivial. % 1.53/1.80 cut ((r1 zenon_TX_jt zenon_TX_kj) = (r1 zenon_TX_j zenon_TX_kj)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H10b. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H10c. % 1.53/1.80 cut ((zenon_TX_kj = zenon_TX_kj)); [idtac | apply NNPP; zenon_intro zenon_H111]. % 1.53/1.80 cut ((zenon_TX_jt = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H112]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_H10f); [ zenon_intro zenon_H114 | zenon_intro zenon_H113 ]. % 1.53/1.80 apply zenon_H114. zenon_intro zenon_H115. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_jt = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H112. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_jt)); [idtac | apply NNPP; zenon_intro zenon_H110]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_H110 zenon_H115). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H113. zenon_intro zenon_H109. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_jt). zenon_intro zenon_H116. % 1.53/1.80 generalize (zenon_H116 zenon_TX_kj). zenon_intro zenon_H117. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H117); [ zenon_intro zenon_Hfb | zenon_intro zenon_H118 ]. % 1.53/1.80 exact (zenon_Hfb zenon_H109). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H118); [ zenon_intro zenon_H11a | zenon_intro zenon_H119 ]. % 1.53/1.80 exact (zenon_H11a zenon_H10c). % 1.53/1.80 exact (zenon_H10b zenon_H119). % 1.53/1.80 apply zenon_H111. apply refl_equal. % 1.53/1.80 (* end of lemma zenon_L17_ *) % 1.53/1.80 assert (zenon_L18_ : forall (zenon_TX_j : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~((forall Y : zenon_U, ((~(r1 zenon_TX_j Y))\/(p2 Y)))\/(~(forall Y : zenon_U, ((~(r1 zenon_TX_j Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_j Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))))))) -> False). % 1.53/1.80 do 1 intro. intros zenon_H4 zenon_H11b zenon_H11c. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H11b). zenon_intro zenon_H11e. zenon_intro zenon_H11d. % 1.53/1.80 apply (zenon_notallex_s (fun Y : zenon_U => ((~(r1 zenon_TX_j Y))\/(p2 Y))) zenon_H11e); [ zenon_intro zenon_H11f; idtac ]. % 1.53/1.80 elim zenon_H11f. zenon_intro zenon_TY_i. zenon_intro zenon_H120. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H120). zenon_intro zenon_H10. zenon_intro zenon_H121. % 1.53/1.80 apply zenon_H10. zenon_intro zenon_H3. % 1.53/1.80 apply zenon_H11d. zenon_intro zenon_H122. % 1.53/1.80 generalize (zenon_H11c zenon_TY_i). zenon_intro zenon_H123. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H123); [ zenon_intro zenon_Hc | zenon_intro zenon_H124 ]. % 1.53/1.80 exact (zenon_Hc zenon_H3). % 1.53/1.80 apply (zenon_or_s _ _ zenon_H124); [ zenon_intro zenon_H126 | zenon_intro zenon_H125 ]. % 1.53/1.80 exact (zenon_H121 zenon_H126). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TY_i X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H125); [ zenon_intro zenon_H127; idtac ]. % 1.53/1.80 elim zenon_H127. zenon_intro zenon_TX_h. zenon_intro zenon_H128. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H128). zenon_intro zenon_H12a. zenon_intro zenon_H129. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H129). zenon_intro zenon_H12c. zenon_intro zenon_H12b. % 1.53/1.80 apply zenon_H12a. zenon_intro zenon_H6. % 1.53/1.80 generalize (zenon_H11c zenon_TX_h). zenon_intro zenon_H12d. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H12d); [ zenon_intro zenon_H5 | zenon_intro zenon_H12e ]. % 1.53/1.80 apply (zenon_L1_ zenon_TX_h zenon_TY_i zenon_TX_j); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H12e); [ zenon_intro zenon_H130 | zenon_intro zenon_H12f ]. % 1.53/1.80 exact (zenon_H12c zenon_H130). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_h X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H12f); [ zenon_intro zenon_H131; idtac ]. % 1.53/1.80 elim zenon_H131. zenon_intro zenon_TX_bd. zenon_intro zenon_H132. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H132). zenon_intro zenon_H134. zenon_intro zenon_H133. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H133). zenon_intro zenon_H136. zenon_intro zenon_H135. % 1.53/1.80 apply zenon_H134. zenon_intro zenon_H1c. % 1.53/1.80 generalize (zenon_H11c zenon_TX_bd). zenon_intro zenon_H137. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H137); [ zenon_intro zenon_H1b | zenon_intro zenon_H138 ]. % 1.53/1.80 apply (zenon_L2_ zenon_TX_bd zenon_TX_h zenon_TY_i zenon_TX_j); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H138); [ zenon_intro zenon_H13a | zenon_intro zenon_H139 ]. % 1.53/1.80 exact (zenon_H136 zenon_H13a). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_bd X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H139); [ zenon_intro zenon_H13b; idtac ]. % 1.53/1.80 elim zenon_H13b. zenon_intro zenon_TX_bt. zenon_intro zenon_H13c. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H13c). zenon_intro zenon_H13e. zenon_intro zenon_H13d. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H13d). zenon_intro zenon_H140. zenon_intro zenon_H13f. % 1.53/1.80 apply zenon_H13e. zenon_intro zenon_H2c. % 1.53/1.80 generalize (zenon_H11c zenon_TX_bt). zenon_intro zenon_H141. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H141); [ zenon_intro zenon_H2b | zenon_intro zenon_H142 ]. % 1.53/1.80 apply (zenon_L3_ zenon_TX_bt zenon_TX_bd zenon_TX_j zenon_TX_h zenon_TY_i); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H142); [ zenon_intro zenon_H144 | zenon_intro zenon_H143 ]. % 1.53/1.80 exact (zenon_H140 zenon_H144). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_bt X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H143); [ zenon_intro zenon_H145; idtac ]. % 1.53/1.80 elim zenon_H145. zenon_intro zenon_TX_cj. zenon_intro zenon_H146. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H146). zenon_intro zenon_H148. zenon_intro zenon_H147. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H147). zenon_intro zenon_H14a. zenon_intro zenon_H149. % 1.53/1.80 apply zenon_H148. zenon_intro zenon_H3c. % 1.53/1.80 generalize (zenon_H11c zenon_TX_cj). zenon_intro zenon_H14b. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H14b); [ zenon_intro zenon_H3b | zenon_intro zenon_H14c ]. % 1.53/1.80 apply (zenon_L4_ zenon_TX_cj zenon_TX_bt zenon_TY_i zenon_TX_j zenon_TX_bd zenon_TX_h); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H14c); [ zenon_intro zenon_H14e | zenon_intro zenon_H14d ]. % 1.53/1.80 exact (zenon_H14a zenon_H14e). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_cj X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H14d); [ zenon_intro zenon_H14f; idtac ]. % 1.53/1.80 elim zenon_H14f. zenon_intro zenon_TX_cz. zenon_intro zenon_H150. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H150). zenon_intro zenon_H152. zenon_intro zenon_H151. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H151). zenon_intro zenon_H154. zenon_intro zenon_H153. % 1.53/1.80 apply zenon_H152. zenon_intro zenon_H4c. % 1.53/1.80 generalize (zenon_H11c zenon_TX_cz). zenon_intro zenon_H155. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H155); [ zenon_intro zenon_H4b | zenon_intro zenon_H156 ]. % 1.53/1.80 apply (zenon_L5_ zenon_TX_cz zenon_TX_cj zenon_TX_j zenon_TX_h zenon_TY_i zenon_TX_bt zenon_TX_bd); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H156); [ zenon_intro zenon_H158 | zenon_intro zenon_H157 ]. % 1.53/1.80 exact (zenon_H154 zenon_H158). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_cz X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H157); [ zenon_intro zenon_H159; idtac ]. % 1.53/1.80 elim zenon_H159. zenon_intro zenon_TX_dp. zenon_intro zenon_H15a. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H15a). zenon_intro zenon_H15c. zenon_intro zenon_H15b. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H15b). zenon_intro zenon_H15e. zenon_intro zenon_H15d. % 1.53/1.80 apply zenon_H15c. zenon_intro zenon_H5c. % 1.53/1.80 generalize (zenon_H11c zenon_TX_dp). zenon_intro zenon_H15f. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H15f); [ zenon_intro zenon_H5b | zenon_intro zenon_H160 ]. % 1.53/1.80 apply (zenon_L6_ zenon_TX_dp zenon_TX_cz zenon_TY_i zenon_TX_j zenon_TX_bd zenon_TX_h zenon_TX_cj zenon_TX_bt); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H160); [ zenon_intro zenon_H162 | zenon_intro zenon_H161 ]. % 1.53/1.80 exact (zenon_H15e zenon_H162). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_dp X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H161); [ zenon_intro zenon_H163; idtac ]. % 1.53/1.80 elim zenon_H163. zenon_intro zenon_TX_ef. zenon_intro zenon_H164. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H164). zenon_intro zenon_H166. zenon_intro zenon_H165. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H165). zenon_intro zenon_H168. zenon_intro zenon_H167. % 1.53/1.80 apply zenon_H166. zenon_intro zenon_H6c. % 1.53/1.80 generalize (zenon_H11c zenon_TX_ef). zenon_intro zenon_H169. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H169); [ zenon_intro zenon_H6b | zenon_intro zenon_H16a ]. % 1.53/1.80 apply (zenon_L7_ zenon_TX_ef zenon_TX_dp zenon_TX_j zenon_TX_h zenon_TY_i zenon_TX_bt zenon_TX_bd zenon_TX_cz zenon_TX_cj); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H16a); [ zenon_intro zenon_H16c | zenon_intro zenon_H16b ]. % 1.53/1.80 exact (zenon_H168 zenon_H16c). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_ef X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H16b); [ zenon_intro zenon_H16d; idtac ]. % 1.53/1.80 elim zenon_H16d. zenon_intro zenon_TX_ev. zenon_intro zenon_H16e. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H16e). zenon_intro zenon_H170. zenon_intro zenon_H16f. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H16f). zenon_intro zenon_H172. zenon_intro zenon_H171. % 1.53/1.80 apply zenon_H170. zenon_intro zenon_H7c. % 1.53/1.80 generalize (zenon_H11c zenon_TX_ev). zenon_intro zenon_H173. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H173); [ zenon_intro zenon_H7b | zenon_intro zenon_H174 ]. % 1.53/1.80 apply (zenon_L8_ zenon_TX_ev zenon_TX_ef zenon_TY_i zenon_TX_j zenon_TX_bd zenon_TX_h zenon_TX_cj zenon_TX_bt zenon_TX_dp zenon_TX_cz); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H174); [ zenon_intro zenon_H176 | zenon_intro zenon_H175 ]. % 1.53/1.80 exact (zenon_H172 zenon_H176). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_ev X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H175); [ zenon_intro zenon_H177; idtac ]. % 1.53/1.80 elim zenon_H177. zenon_intro zenon_TX_fl. zenon_intro zenon_H178. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H178). zenon_intro zenon_H17a. zenon_intro zenon_H179. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H179). zenon_intro zenon_H17c. zenon_intro zenon_H17b. % 1.53/1.80 apply zenon_H17a. zenon_intro zenon_H8c. % 1.53/1.80 generalize (zenon_H11c zenon_TX_fl). zenon_intro zenon_H17d. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H17d); [ zenon_intro zenon_H8b | zenon_intro zenon_H17e ]. % 1.53/1.80 apply (zenon_L9_ zenon_TX_fl zenon_TX_ev zenon_TX_j zenon_TX_h zenon_TY_i zenon_TX_bt zenon_TX_bd zenon_TX_cz zenon_TX_cj zenon_TX_ef zenon_TX_dp); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H17e); [ zenon_intro zenon_H180 | zenon_intro zenon_H17f ]. % 1.53/1.80 exact (zenon_H17c zenon_H180). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_fl X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H17f); [ zenon_intro zenon_H181; idtac ]. % 1.53/1.80 elim zenon_H181. zenon_intro zenon_TX_gb. zenon_intro zenon_H182. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H182). zenon_intro zenon_H184. zenon_intro zenon_H183. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H183). zenon_intro zenon_H186. zenon_intro zenon_H185. % 1.53/1.80 apply zenon_H184. zenon_intro zenon_H9c. % 1.53/1.80 generalize (zenon_H11c zenon_TX_gb). zenon_intro zenon_H187. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H187); [ zenon_intro zenon_H9b | zenon_intro zenon_H188 ]. % 1.53/1.80 apply (zenon_L10_ zenon_TX_gb zenon_TX_fl zenon_TY_i zenon_TX_j zenon_TX_bd zenon_TX_h zenon_TX_cj zenon_TX_bt zenon_TX_dp zenon_TX_cz zenon_TX_ev zenon_TX_ef); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H188); [ zenon_intro zenon_H18a | zenon_intro zenon_H189 ]. % 1.53/1.80 exact (zenon_H186 zenon_H18a). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_gb X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H189); [ zenon_intro zenon_H18b; idtac ]. % 1.53/1.80 elim zenon_H18b. zenon_intro zenon_TX_gr. zenon_intro zenon_H18c. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H18c). zenon_intro zenon_H18e. zenon_intro zenon_H18d. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H18d). zenon_intro zenon_H190. zenon_intro zenon_H18f. % 1.53/1.80 apply zenon_H18e. zenon_intro zenon_Hac. % 1.53/1.80 generalize (zenon_H11c zenon_TX_gr). zenon_intro zenon_H191. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H191); [ zenon_intro zenon_Hab | zenon_intro zenon_H192 ]. % 1.53/1.80 apply (zenon_L11_ zenon_TX_gr zenon_TX_gb zenon_TX_j zenon_TX_h zenon_TY_i zenon_TX_bt zenon_TX_bd zenon_TX_cz zenon_TX_cj zenon_TX_ef zenon_TX_dp zenon_TX_fl zenon_TX_ev); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H192); [ zenon_intro zenon_H194 | zenon_intro zenon_H193 ]. % 1.53/1.80 exact (zenon_H190 zenon_H194). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_gr X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H193); [ zenon_intro zenon_H195; idtac ]. % 1.53/1.80 elim zenon_H195. zenon_intro zenon_TX_hh. zenon_intro zenon_H196. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H196). zenon_intro zenon_H198. zenon_intro zenon_H197. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H197). zenon_intro zenon_H19a. zenon_intro zenon_H199. % 1.53/1.80 apply zenon_H198. zenon_intro zenon_Hbc. % 1.53/1.80 generalize (zenon_H11c zenon_TX_hh). zenon_intro zenon_H19b. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H19b); [ zenon_intro zenon_Hbb | zenon_intro zenon_H19c ]. % 1.53/1.80 apply (zenon_L12_ zenon_TX_hh zenon_TX_gr zenon_TY_i zenon_TX_j zenon_TX_bd zenon_TX_h zenon_TX_cj zenon_TX_bt zenon_TX_dp zenon_TX_cz zenon_TX_ev zenon_TX_ef zenon_TX_gb zenon_TX_fl); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H19c); [ zenon_intro zenon_H19e | zenon_intro zenon_H19d ]. % 1.53/1.80 exact (zenon_H19a zenon_H19e). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_hh X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H19d); [ zenon_intro zenon_H19f; idtac ]. % 1.53/1.80 elim zenon_H19f. zenon_intro zenon_TX_hx. zenon_intro zenon_H1a0. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1a0). zenon_intro zenon_H1a2. zenon_intro zenon_H1a1. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1a1). zenon_intro zenon_H1a4. zenon_intro zenon_H1a3. % 1.53/1.80 apply zenon_H1a2. zenon_intro zenon_Hcc. % 1.53/1.80 generalize (zenon_H11c zenon_TX_hx). zenon_intro zenon_H1a5. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H1a5); [ zenon_intro zenon_Hcb | zenon_intro zenon_H1a6 ]. % 1.53/1.80 apply (zenon_L13_ zenon_TX_hx zenon_TX_hh zenon_TX_j zenon_TX_h zenon_TY_i zenon_TX_bt zenon_TX_bd zenon_TX_cz zenon_TX_cj zenon_TX_ef zenon_TX_dp zenon_TX_fl zenon_TX_ev zenon_TX_gr zenon_TX_gb); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H1a6); [ zenon_intro zenon_H1a8 | zenon_intro zenon_H1a7 ]. % 1.53/1.80 exact (zenon_H1a4 zenon_H1a8). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_hx X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H1a7); [ zenon_intro zenon_H1a9; idtac ]. % 1.53/1.80 elim zenon_H1a9. zenon_intro zenon_TX_in. zenon_intro zenon_H1aa. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1aa). zenon_intro zenon_H1ac. zenon_intro zenon_H1ab. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1ab). zenon_intro zenon_H1ae. zenon_intro zenon_H1ad. % 1.53/1.80 apply zenon_H1ac. zenon_intro zenon_Hdc. % 1.53/1.80 generalize (zenon_H11c zenon_TX_in). zenon_intro zenon_H1af. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H1af); [ zenon_intro zenon_Hdb | zenon_intro zenon_H1b0 ]. % 1.53/1.80 apply (zenon_L14_ zenon_TX_in zenon_TX_hx zenon_TY_i zenon_TX_j zenon_TX_bd zenon_TX_h zenon_TX_cj zenon_TX_bt zenon_TX_dp zenon_TX_cz zenon_TX_ev zenon_TX_ef zenon_TX_gb zenon_TX_fl zenon_TX_hh zenon_TX_gr); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H1b0); [ zenon_intro zenon_H1b2 | zenon_intro zenon_H1b1 ]. % 1.53/1.80 exact (zenon_H1ae zenon_H1b2). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_in X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H1b1); [ zenon_intro zenon_H1b3; idtac ]. % 1.53/1.80 elim zenon_H1b3. zenon_intro zenon_TX_jd. zenon_intro zenon_H1b4. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1b4). zenon_intro zenon_H1b6. zenon_intro zenon_H1b5. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1b5). zenon_intro zenon_H1b8. zenon_intro zenon_H1b7. % 1.53/1.80 apply zenon_H1b6. zenon_intro zenon_Hec. % 1.53/1.80 generalize (zenon_H11c zenon_TX_jd). zenon_intro zenon_H1b9. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H1b9); [ zenon_intro zenon_Heb | zenon_intro zenon_H1ba ]. % 1.53/1.80 apply (zenon_L15_ zenon_TX_jd zenon_TX_in zenon_TX_j zenon_TX_h zenon_TY_i zenon_TX_bt zenon_TX_bd zenon_TX_cz zenon_TX_cj zenon_TX_ef zenon_TX_dp zenon_TX_fl zenon_TX_ev zenon_TX_gr zenon_TX_gb zenon_TX_hx zenon_TX_hh); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H1ba); [ zenon_intro zenon_H1bc | zenon_intro zenon_H1bb ]. % 1.53/1.80 exact (zenon_H1b8 zenon_H1bc). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_jd X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H1bb); [ zenon_intro zenon_H1bd; idtac ]. % 1.53/1.80 elim zenon_H1bd. zenon_intro zenon_TX_jt. zenon_intro zenon_H1be. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1be). zenon_intro zenon_H1c0. zenon_intro zenon_H1bf. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1bf). zenon_intro zenon_H1c2. zenon_intro zenon_H1c1. % 1.53/1.80 apply zenon_H1c0. zenon_intro zenon_Hfc. % 1.53/1.80 generalize (zenon_H11c zenon_TX_jt). zenon_intro zenon_H1c3. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H1c3); [ zenon_intro zenon_Hfb | zenon_intro zenon_H1c4 ]. % 1.53/1.80 apply (zenon_L16_ zenon_TX_jt zenon_TX_jd zenon_TY_i zenon_TX_j zenon_TX_bd zenon_TX_h zenon_TX_cj zenon_TX_bt zenon_TX_dp zenon_TX_cz zenon_TX_ev zenon_TX_ef zenon_TX_gb zenon_TX_fl zenon_TX_hh zenon_TX_gr zenon_TX_in zenon_TX_hx); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H1c4); [ zenon_intro zenon_H1c6 | zenon_intro zenon_H1c5 ]. % 1.53/1.80 exact (zenon_H1c2 zenon_H1c6). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_jt X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H1c5); [ zenon_intro zenon_H1c7; idtac ]. % 1.53/1.80 elim zenon_H1c7. zenon_intro zenon_TX_kj. zenon_intro zenon_H1c8. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1c8). zenon_intro zenon_H1ca. zenon_intro zenon_H1c9. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1c9). zenon_intro zenon_H1cc. zenon_intro zenon_H1cb. % 1.53/1.80 apply zenon_H1ca. zenon_intro zenon_H10c. % 1.53/1.80 generalize (zenon_H11c zenon_TX_kj). zenon_intro zenon_H1cd. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H1cd); [ zenon_intro zenon_H10b | zenon_intro zenon_H1ce ]. % 1.53/1.80 apply (zenon_L17_ zenon_TX_kj zenon_TX_jt zenon_TX_j zenon_TX_h zenon_TY_i zenon_TX_bt zenon_TX_bd zenon_TX_cz zenon_TX_cj zenon_TX_ef zenon_TX_dp zenon_TX_fl zenon_TX_ev zenon_TX_gr zenon_TX_gb zenon_TX_hx zenon_TX_hh zenon_TX_jd zenon_TX_in); trivial. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H1ce); [ zenon_intro zenon_H1d0 | zenon_intro zenon_H1cf ]. % 1.53/1.80 exact (zenon_H1cc zenon_H1d0). % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_kj X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))) zenon_H1cf); [ zenon_intro zenon_H1d1; idtac ]. % 1.53/1.80 elim zenon_H1d1. zenon_intro zenon_TX_ry. zenon_intro zenon_H1d3. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1d3). zenon_intro zenon_H1d5. zenon_intro zenon_H1d4. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1d4). zenon_intro zenon_H1d7. zenon_intro zenon_H1d6. % 1.53/1.80 apply zenon_H1d6. zenon_intro zenon_H1d8. % 1.53/1.80 apply zenon_H1d5. zenon_intro zenon_H1d9. % 1.53/1.80 generalize (zenon_H122 zenon_TX_ry). zenon_intro zenon_H1da. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H1da); [ zenon_intro zenon_H1dc | zenon_intro zenon_H1db ]. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TX_kj))/\(~(r1 zenon_TX_j zenon_TX_kj)))); [ zenon_intro zenon_H1dd | zenon_intro zenon_H1de ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_H1dd). zenon_intro zenon_H1df. zenon_intro zenon_H10b. % 1.53/1.80 apply (zenon_L17_ zenon_TX_kj zenon_TX_jt zenon_TX_j zenon_TX_h zenon_TY_i zenon_TX_bt zenon_TX_bd zenon_TX_cz zenon_TX_cj zenon_TX_ef zenon_TX_dp zenon_TX_fl zenon_TX_ev zenon_TX_gr zenon_TX_gb zenon_TX_hx zenon_TX_hh zenon_TX_jd zenon_TX_in); trivial. % 1.53/1.80 cut ((r1 zenon_TX_kj zenon_TX_ry) = (r1 zenon_TX_j zenon_TX_ry)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H1dc. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H1d9. % 1.53/1.80 cut ((zenon_TX_ry = zenon_TX_ry)); [idtac | apply NNPP; zenon_intro zenon_H1e0]. % 1.53/1.80 cut ((zenon_TX_kj = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H1e1]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_H1de); [ zenon_intro zenon_H1e3 | zenon_intro zenon_H1e2 ]. % 1.53/1.80 apply zenon_H1e3. zenon_intro zenon_H1e4. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_kj = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H1e1. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_kj)); [idtac | apply NNPP; zenon_intro zenon_H1df]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_H1df zenon_H1e4). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H1e2. zenon_intro zenon_H119. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TX_kj). zenon_intro zenon_H1e5. % 1.53/1.80 generalize (zenon_H1e5 zenon_TX_ry). zenon_intro zenon_H1e6. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H1e6); [ zenon_intro zenon_H10b | zenon_intro zenon_H1e7 ]. % 1.53/1.80 exact (zenon_H10b zenon_H119). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H1e7); [ zenon_intro zenon_H1e9 | zenon_intro zenon_H1e8 ]. % 1.53/1.80 exact (zenon_H1e9 zenon_H1d9). % 1.53/1.80 exact (zenon_H1dc zenon_H1e8). % 1.53/1.80 apply zenon_H1e0. apply refl_equal. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H1db); [ zenon_intro zenon_H1eb | zenon_intro zenon_H1ea ]. % 1.53/1.80 exact (zenon_H1d7 zenon_H1eb). % 1.53/1.80 exact (zenon_H1ea zenon_H1d8). % 1.53/1.80 (* end of lemma zenon_L18_ *) % 1.53/1.80 apply NNPP. intro zenon_G. % 1.53/1.80 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z))))))); [ zenon_intro zenon_H4 | zenon_intro zenon_H1ec ]. % 1.53/1.80 apply zenon_G. zenon_intro zenon_H1ed. % 1.53/1.80 elim zenon_H1ed. zenon_intro zenon_TX_j. zenon_intro zenon_H1ee. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1ee). zenon_intro zenon_H1f0. zenon_intro zenon_H1ef. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1ef). zenon_intro zenon_H1f2. zenon_intro zenon_H1f1. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1f1). zenon_intro zenon_H1f4. zenon_intro zenon_H1f3. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1f3). zenon_intro zenon_H1f6. zenon_intro zenon_H1f5. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1f5). zenon_intro zenon_H1f8. zenon_intro zenon_H1f7. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H1f7). zenon_intro zenon_H1fa. zenon_intro zenon_H1f9. % 1.53/1.80 apply zenon_H1f9. zenon_intro zenon_H1fb. % 1.53/1.80 apply (zenon_and_s _ _ zenon_H1fb). zenon_intro zenon_H1fc. zenon_intro zenon_H11c. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_H1f0); [ zenon_intro zenon_H1fd | zenon_intro zenon_H11b ]. % 1.53/1.80 apply (zenon_notallex_s (fun Y : zenon_U => ((~(r1 zenon_TX_j Y))\/((p1 Y)\/(forall X : zenon_U, ((~(r1 Y X))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(p3 Y)))))))))) zenon_H1fd); [ zenon_intro zenon_H1fe; idtac ]. % 1.53/1.80 elim zenon_H1fe. zenon_intro zenon_TY_tr. zenon_intro zenon_H200. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H200). zenon_intro zenon_H202. zenon_intro zenon_H201. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H201). zenon_intro zenon_H204. zenon_intro zenon_H203. % 1.53/1.80 apply zenon_H202. zenon_intro zenon_H205. % 1.53/1.80 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TY_tr X))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(p3 Y))))))) zenon_H203); [ zenon_intro zenon_H206; idtac ]. % 1.53/1.80 elim zenon_H206. zenon_intro zenon_TX_tz. zenon_intro zenon_H208. % 1.53/1.80 apply (zenon_notor_s _ _ zenon_H208). zenon_intro zenon_H20a. zenon_intro zenon_H209. % 1.53/1.80 apply zenon_H20a. zenon_intro zenon_H20b. % 1.53/1.80 apply zenon_H209. zenon_intro zenon_H20c. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_H1f6); [ zenon_intro zenon_H20d | zenon_intro zenon_H11b ]. % 1.53/1.80 apply zenon_H20d. zenon_intro zenon_H20e. % 1.53/1.80 generalize (zenon_H20e zenon_TX_tz). zenon_intro zenon_H20f. % 1.53/1.80 apply (zenon_or_s _ _ zenon_H20f); [ zenon_intro zenon_H211 | zenon_intro zenon_H210 ]. % 1.53/1.80 elim (classic ((~(zenon_TX_j = zenon_TY_tr))/\(~(r1 zenon_TX_j zenon_TY_tr)))); [ zenon_intro zenon_H212 | zenon_intro zenon_H213 ]. % 1.53/1.80 apply (zenon_and_s _ _ zenon_H212). zenon_intro zenon_H215. zenon_intro zenon_H214. % 1.53/1.80 exact (zenon_H214 zenon_H205). % 1.53/1.80 cut ((r1 zenon_TY_tr zenon_TX_tz) = (r1 zenon_TX_j zenon_TX_tz)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H211. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H20b. % 1.53/1.80 cut ((zenon_TX_tz = zenon_TX_tz)); [idtac | apply NNPP; zenon_intro zenon_H216]. % 1.53/1.80 cut ((zenon_TY_tr = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H217]. % 1.53/1.80 congruence. % 1.53/1.80 apply (zenon_notand_s _ _ zenon_H213); [ zenon_intro zenon_H218 | zenon_intro zenon_H202 ]. % 1.53/1.80 apply zenon_H218. zenon_intro zenon_H219. % 1.53/1.80 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TY_tr = zenon_TX_j)). % 1.53/1.80 intro zenon_D_pnotp. % 1.53/1.80 apply zenon_H217. % 1.53/1.80 rewrite <- zenon_D_pnotp. % 1.53/1.80 exact zenon_H13. % 1.53/1.80 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 1.53/1.80 cut ((zenon_TX_j = zenon_TY_tr)); [idtac | apply NNPP; zenon_intro zenon_H215]. % 1.53/1.80 congruence. % 1.53/1.80 exact (zenon_H215 zenon_H219). % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H14. apply refl_equal. % 1.53/1.80 apply zenon_H202. zenon_intro zenon_H205. % 1.53/1.80 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 1.53/1.80 generalize (zenon_H15 zenon_TY_tr). zenon_intro zenon_H21a. % 1.53/1.80 generalize (zenon_H21a zenon_TX_tz). zenon_intro zenon_H21b. % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H21b); [ zenon_intro zenon_H214 | zenon_intro zenon_H21c ]. % 1.53/1.80 exact (zenon_H214 zenon_H205). % 1.53/1.80 apply (zenon_imply_s _ _ zenon_H21c); [ zenon_intro zenon_H21e | zenon_intro zenon_H21d ]. % 1.53/1.80 exact (zenon_H21e zenon_H20b). % 1.53/1.80 exact (zenon_H211 zenon_H21d). % 1.53/1.80 apply zenon_H216. apply refl_equal. % 1.53/1.80 exact (zenon_H210 zenon_H20c). % 1.53/1.81 apply (zenon_L18_ zenon_TX_j); trivial. % 1.53/1.81 apply (zenon_L18_ zenon_TX_j); trivial. % 1.53/1.81 apply zenon_H1ec. zenon_intro zenon_Tx_ux. apply NNPP. zenon_intro zenon_H220. % 1.53/1.81 apply zenon_H220. zenon_intro zenon_Ty_uz. apply NNPP. zenon_intro zenon_H222. % 1.53/1.81 apply zenon_H222. zenon_intro zenon_Tz_vb. apply NNPP. zenon_intro zenon_H224. % 1.53/1.81 apply (zenon_notimply_s _ _ zenon_H224). zenon_intro zenon_H226. zenon_intro zenon_H225. % 1.53/1.81 apply (zenon_notimply_s _ _ zenon_H225). zenon_intro zenon_H228. zenon_intro zenon_H227. % 1.53/1.81 generalize (transitivity zenon_Tx_ux). zenon_intro zenon_H229. % 1.53/1.81 generalize (zenon_H229 zenon_Ty_uz). zenon_intro zenon_H22a. % 1.53/1.81 generalize (zenon_H22a zenon_Tz_vb). zenon_intro zenon_H22b. % 1.53/1.81 apply (zenon_imply_s _ _ zenon_H22b); [ zenon_intro zenon_H22d | zenon_intro zenon_H22c ]. % 1.53/1.81 apply (zenon_notand_s _ _ zenon_H22d); [ zenon_intro zenon_H22f | zenon_intro zenon_H22e ]. % 1.53/1.81 exact (zenon_H22f zenon_H226). % 1.53/1.81 exact (zenon_H22e zenon_H228). % 1.53/1.81 exact (zenon_H227 zenon_H22c). % 1.53/1.81 Qed. % 1.53/1.81 % SZS output end Proof % 1.53/1.81 (* END-PROOF *) % 1.53/1.81 nodes searched: 9474 % 1.53/1.81 max branch formulas: 2983 % 1.53/1.81 proof nodes created: 694 % 1.53/1.81 formulas created: 105046 % 1.53/1.81 %------------------------------------------------------------------------------