%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SYN723+1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 21 13:55:17 EDT 2022 % Result : Theorem 0.18s 0.54s % Output : Proof 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN723+1 : TPTP v8.1.0. Released v2.5.0. % 0.03/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n004.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Tue Jul 12 02:20:37 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.54 (* PROOF-FOUND *) % 0.18/0.54 % SZS status Theorem % 0.18/0.54 (* BEGIN-PROOF *) % 0.18/0.54 % SZS output start Proof % 0.18/0.54 Theorem thm138 : ((exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))<->(((exists X : zenon_U, (q X))<->(forall Y : zenon_U, (r Y)))<->(((exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))<->((exists X : zenon_U, (r X))<->(forall Y : zenon_U, (s Y))))<->((exists X : zenon_U, (forall Y : zenon_U, ((r X)<->(r Y))))<->(((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))))))))). % 0.18/0.54 Proof. % 0.18/0.54 assert (zenon_L1_ : forall (zenon_TY_i : zenon_U), (~(exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))) -> (~(s zenon_TY_i)) -> (~(exists X : zenon_U, (s X))) -> False). % 0.18/0.54 do 1 intro. intros zenon_H5 zenon_H6 zenon_H7. % 0.18/0.54 apply zenon_H5. exists zenon_TY_i. apply NNPP. zenon_intro zenon_H9. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => ((s zenon_TY_i)<->(s Y))) zenon_H9); [ zenon_intro zenon_Ha; idtac ]. % 0.18/0.54 elim zenon_Ha. zenon_intro zenon_TY_l. zenon_intro zenon_Hc. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_Hc); [ zenon_intro zenon_H6; zenon_intro zenon_Hf | zenon_intro zenon_He; zenon_intro zenon_Hd ]. % 0.18/0.54 apply zenon_H7. exists zenon_TY_l. apply NNPP. zenon_intro zenon_Hd. % 0.18/0.54 exact (zenon_Hd zenon_Hf). % 0.18/0.54 exact (zenon_H6 zenon_He). % 0.18/0.54 (* end of lemma zenon_L1_ *) % 0.18/0.54 assert (zenon_L2_ : (~(forall Y : zenon_U, (q Y))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> (~(exists X : zenon_U, (q X))) -> False). % 0.18/0.54 do 0 intro. intros zenon_H10 zenon_H11 zenon_H12. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (q Y)) zenon_H10); [ zenon_intro zenon_H13; idtac ]. % 0.18/0.54 elim zenon_H13. zenon_intro zenon_TY_u. zenon_intro zenon_H15. % 0.18/0.54 apply zenon_H11. exists zenon_TY_u. apply NNPP. zenon_intro zenon_H16. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => ((q zenon_TY_u)<->(q Y))) zenon_H16); [ zenon_intro zenon_H17; idtac ]. % 0.18/0.54 elim zenon_H17. zenon_intro zenon_TY_y. zenon_intro zenon_H19. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H19); [ zenon_intro zenon_H15; zenon_intro zenon_H1c | zenon_intro zenon_H1b; zenon_intro zenon_H1a ]. % 0.18/0.54 apply zenon_H12. exists zenon_TY_y. apply NNPP. zenon_intro zenon_H1a. % 0.18/0.54 exact (zenon_H1a zenon_H1c). % 0.18/0.54 exact (zenon_H15 zenon_H1b). % 0.18/0.54 (* end of lemma zenon_L2_ *) % 0.18/0.54 assert (zenon_L3_ : (exists X : zenon_U, (p X)) -> (forall Y : zenon_U, (p Y)) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> False). % 0.18/0.54 do 0 intro. intros zenon_H1d zenon_H1e zenon_H1f. % 0.18/0.54 elim zenon_H1d. zenon_intro zenon_TX_bg. zenon_intro zenon_H21. % 0.18/0.54 apply zenon_H1f. exists zenon_TX_bg. apply NNPP. zenon_intro zenon_H22. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => ((p zenon_TX_bg)<->(p Y))) zenon_H22); [ zenon_intro zenon_H23; idtac ]. % 0.18/0.54 elim zenon_H23. zenon_intro zenon_TY_bk. zenon_intro zenon_H25. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H25); [ zenon_intro zenon_H28; zenon_intro zenon_H27 | zenon_intro zenon_H21; zenon_intro zenon_H26 ]. % 0.18/0.54 exact (zenon_H28 zenon_H21). % 0.18/0.54 generalize (zenon_H1e zenon_TY_bk). zenon_intro zenon_H27. % 0.18/0.54 exact (zenon_H26 zenon_H27). % 0.18/0.54 (* end of lemma zenon_L3_ *) % 0.18/0.54 assert (zenon_L4_ : ((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> (forall Y : zenon_U, (p Y)) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> (~(exists X : zenon_U, (q X))) -> False). % 0.18/0.54 do 0 intro. intros zenon_H29 zenon_H1f zenon_H1e zenon_H11 zenon_H12. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H29); [ zenon_intro zenon_H2b; zenon_intro zenon_H10 | zenon_intro zenon_H1d; zenon_intro zenon_H2a ]. % 0.18/0.54 apply (zenon_L2_); trivial. % 0.18/0.54 apply (zenon_L3_); trivial. % 0.18/0.54 (* end of lemma zenon_L4_ *) % 0.18/0.54 assert (zenon_L5_ : forall (zenon_TY_bt : zenon_U), (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> (~(p zenon_TY_bt)) -> (~(exists X : zenon_U, (p X))) -> False). % 0.18/0.54 do 1 intro. intros zenon_H1f zenon_H2c zenon_H2b. % 0.18/0.54 apply zenon_H1f. exists zenon_TY_bt. apply NNPP. zenon_intro zenon_H2e. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => ((p zenon_TY_bt)<->(p Y))) zenon_H2e); [ zenon_intro zenon_H2f; idtac ]. % 0.18/0.54 elim zenon_H2f. zenon_intro zenon_TY_bw. zenon_intro zenon_H31. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H31); [ zenon_intro zenon_H2c; zenon_intro zenon_H34 | zenon_intro zenon_H33; zenon_intro zenon_H32 ]. % 0.18/0.54 apply zenon_H2b. exists zenon_TY_bw. apply NNPP. zenon_intro zenon_H32. % 0.18/0.54 exact (zenon_H32 zenon_H34). % 0.18/0.54 exact (zenon_H2c zenon_H33). % 0.18/0.54 (* end of lemma zenon_L5_ *) % 0.18/0.54 assert (zenon_L6_ : forall (zenon_TY_bt : zenon_U), (~((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> (~(exists X : zenon_U, (q X))) -> (~(p zenon_TY_bt)) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> False). % 0.18/0.54 do 1 intro. intros zenon_H35 zenon_H11 zenon_H12 zenon_H2c zenon_H1f. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H35); [ zenon_intro zenon_H2b; zenon_intro zenon_H2a | zenon_intro zenon_H1d; zenon_intro zenon_H10 ]. % 0.18/0.54 apply (zenon_L5_ zenon_TY_bt); trivial. % 0.18/0.54 apply (zenon_L2_); trivial. % 0.18/0.54 (* end of lemma zenon_L6_ *) % 0.18/0.54 assert (zenon_L7_ : forall (zenon_TX_ce : zenon_U) (zenon_TY_i : zenon_U), (exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y)))) -> (~(s zenon_TY_i)) -> (s zenon_TX_ce) -> False). % 0.18/0.54 do 2 intro. intros zenon_H36 zenon_H6 zenon_H37. % 0.18/0.54 elim zenon_H36. zenon_intro zenon_TX_cf. zenon_intro zenon_H0. % 0.18/0.54 generalize (zenon_H0 zenon_E). zenon_intro zenon_H3a. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H3a); [ zenon_intro zenon_H3e; zenon_intro zenon_H3d | zenon_intro zenon_H3c; zenon_intro zenon_H3b ]. % 0.18/0.54 generalize (zenon_H0 zenon_TX_ce). zenon_intro zenon_H3f. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H3f); [ zenon_intro zenon_H3e; zenon_intro zenon_H40 | zenon_intro zenon_H3c; zenon_intro zenon_H37 ]. % 0.18/0.54 exact (zenon_H40 zenon_H37). % 0.18/0.54 exact (zenon_H3e zenon_H3c). % 0.18/0.54 generalize (zenon_H0 zenon_TY_i). zenon_intro zenon_H41. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H41); [ zenon_intro zenon_H3e; zenon_intro zenon_H6 | zenon_intro zenon_H3c; zenon_intro zenon_He ]. % 0.18/0.54 exact (zenon_H3e zenon_H3c). % 0.18/0.54 exact (zenon_H6 zenon_He). % 0.18/0.54 (* end of lemma zenon_L7_ *) % 0.18/0.54 assert (zenon_L8_ : forall (zenon_TY_i : zenon_U), (~(((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))))) -> (~(exists X : zenon_U, (q X))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> (~(s zenon_TY_i)) -> False). % 0.18/0.54 do 1 intro. intros zenon_H42 zenon_H12 zenon_H11 zenon_H1f zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H42); [ zenon_intro zenon_H46; zenon_intro zenon_H45 | zenon_intro zenon_H44; zenon_intro zenon_H43 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L4_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L6_ zenon_TY_bt); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L6_ zenon_TY_bt); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L4_); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 (* end of lemma zenon_L8_ *) % 0.18/0.54 assert (zenon_L9_ : (exists X : zenon_U, (forall Y : zenon_U, ((r X)<->(r Y)))) -> (~(exists X : zenon_U, (r X))) -> (forall Y : zenon_U, (r Y)) -> False). % 0.18/0.54 do 0 intro. intros zenon_H4a zenon_H4b zenon_H4c. % 0.18/0.54 elim zenon_H4a. zenon_intro zenon_TX_cz. zenon_intro zenon_H1. % 0.18/0.54 generalize (zenon_H1 zenon_E). zenon_intro zenon_H4e. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H4e); [ zenon_intro zenon_H52; zenon_intro zenon_H51 | zenon_intro zenon_H50; zenon_intro zenon_H4f ]. % 0.18/0.54 generalize (zenon_H4c zenon_TX_cz). zenon_intro zenon_H50. % 0.18/0.54 exact (zenon_H52 zenon_H50). % 0.18/0.54 apply zenon_H4b. exists zenon_TX_cz. apply NNPP. zenon_intro zenon_H52. % 0.18/0.54 exact (zenon_H52 zenon_H50). % 0.18/0.54 (* end of lemma zenon_L9_ *) % 0.18/0.54 assert (zenon_L10_ : forall (zenon_TX_dh : zenon_U), (~(exists X : zenon_U, (forall Y : zenon_U, ((r X)<->(r Y))))) -> (forall Y : zenon_U, (r Y)) -> (r zenon_TX_dh) -> False). % 0.18/0.54 do 1 intro. intros zenon_H53 zenon_H4c zenon_H54. % 0.18/0.54 apply zenon_H53. exists zenon_TX_dh. apply NNPP. zenon_intro zenon_H56. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => ((r zenon_TX_dh)<->(r Y))) zenon_H56); [ zenon_intro zenon_H57; idtac ]. % 0.18/0.54 elim zenon_H57. zenon_intro zenon_TY_dk. zenon_intro zenon_H59. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H59); [ zenon_intro zenon_H5c; zenon_intro zenon_H5b | zenon_intro zenon_H54; zenon_intro zenon_H5a ]. % 0.18/0.54 exact (zenon_H5c zenon_H54). % 0.18/0.54 generalize (zenon_H4c zenon_TY_dk). zenon_intro zenon_H5b. % 0.18/0.54 exact (zenon_H5a zenon_H5b). % 0.18/0.54 (* end of lemma zenon_L10_ *) % 0.18/0.54 assert (zenon_L11_ : (exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y)))) -> (~(exists X : zenon_U, (s X))) -> (forall Y : zenon_U, (s Y)) -> False). % 0.18/0.54 do 0 intro. intros zenon_H36 zenon_H7 zenon_H5d. % 0.18/0.54 elim zenon_H36. zenon_intro zenon_TX_cf. zenon_intro zenon_H0. % 0.18/0.54 generalize (zenon_H0 zenon_E). zenon_intro zenon_H3a. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H3a); [ zenon_intro zenon_H3e; zenon_intro zenon_H3d | zenon_intro zenon_H3c; zenon_intro zenon_H3b ]. % 0.18/0.54 generalize (zenon_H5d zenon_TX_cf). zenon_intro zenon_H3c. % 0.18/0.54 exact (zenon_H3e zenon_H3c). % 0.18/0.54 apply zenon_H7. exists zenon_TX_cf. apply NNPP. zenon_intro zenon_H3e. % 0.18/0.54 exact (zenon_H3e zenon_H3c). % 0.18/0.54 (* end of lemma zenon_L11_ *) % 0.18/0.54 assert (zenon_L12_ : forall (zenon_TX_ce : zenon_U), (~(exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))) -> (forall Y : zenon_U, (s Y)) -> (s zenon_TX_ce) -> False). % 0.18/0.54 do 1 intro. intros zenon_H5 zenon_H5d zenon_H37. % 0.18/0.54 apply zenon_H5. exists zenon_TX_ce. apply NNPP. zenon_intro zenon_H5e. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => ((s zenon_TX_ce)<->(s Y))) zenon_H5e); [ zenon_intro zenon_H5f; idtac ]. % 0.18/0.54 elim zenon_H5f. zenon_intro zenon_TY_ds. zenon_intro zenon_H61. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H61); [ zenon_intro zenon_H40; zenon_intro zenon_H63 | zenon_intro zenon_H37; zenon_intro zenon_H62 ]. % 0.18/0.54 exact (zenon_H40 zenon_H37). % 0.18/0.54 generalize (zenon_H5d zenon_TY_ds). zenon_intro zenon_H63. % 0.18/0.54 exact (zenon_H62 zenon_H63). % 0.18/0.54 (* end of lemma zenon_L12_ *) % 0.18/0.54 assert (zenon_L13_ : (((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))))) -> (forall Y : zenon_U, (s Y)) -> (~(exists X : zenon_U, (q X))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> False). % 0.18/0.54 do 0 intro. intros zenon_H64 zenon_H5d zenon_H12 zenon_H11 zenon_H1f. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H64); [ zenon_intro zenon_H46; zenon_intro zenon_H43 | zenon_intro zenon_H44; zenon_intro zenon_H45 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L4_); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L6_ zenon_TY_bt); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L6_ zenon_TY_bt); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L4_); trivial. % 0.18/0.54 (* end of lemma zenon_L13_ *) % 0.18/0.54 assert (zenon_L14_ : forall (zenon_TX_dx : zenon_U), (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (forall Y : zenon_U, (q Y)) -> (~(exists X : zenon_U, (q X))) -> False). % 0.18/0.54 do 1 intro. intros zenon_H2 zenon_H2a zenon_H12. % 0.18/0.54 generalize (zenon_H2 zenon_E). zenon_intro zenon_H66. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H66); [ zenon_intro zenon_H6a; zenon_intro zenon_H69 | zenon_intro zenon_H68; zenon_intro zenon_H67 ]. % 0.18/0.54 generalize (zenon_H2a zenon_TX_dx). zenon_intro zenon_H68. % 0.18/0.54 exact (zenon_H6a zenon_H68). % 0.18/0.54 apply zenon_H12. exists zenon_TX_dx. apply NNPP. zenon_intro zenon_H6a. % 0.18/0.54 exact (zenon_H6a zenon_H68). % 0.18/0.54 (* end of lemma zenon_L14_ *) % 0.18/0.54 assert (zenon_L15_ : forall (zenon_TX_dx : zenon_U), (~((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> (forall Y : zenon_U, (p Y)) -> (~(exists X : zenon_U, (q X))) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> False). % 0.18/0.54 do 1 intro. intros zenon_H35 zenon_H1f zenon_H1e zenon_H12 zenon_H2. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H35); [ zenon_intro zenon_H2b; zenon_intro zenon_H2a | zenon_intro zenon_H1d; zenon_intro zenon_H10 ]. % 0.18/0.54 apply (zenon_L14_ zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L3_); trivial. % 0.18/0.54 (* end of lemma zenon_L15_ *) % 0.18/0.54 assert (zenon_L16_ : forall (zenon_TY_bt : zenon_U) (zenon_TX_dx : zenon_U), ((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))) -> (~(exists X : zenon_U, (q X))) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (~(p zenon_TY_bt)) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> False). % 0.18/0.54 do 2 intro. intros zenon_H29 zenon_H12 zenon_H2 zenon_H2c zenon_H1f. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H29); [ zenon_intro zenon_H2b; zenon_intro zenon_H10 | zenon_intro zenon_H1d; zenon_intro zenon_H2a ]. % 0.18/0.54 apply (zenon_L5_ zenon_TY_bt); trivial. % 0.18/0.54 apply (zenon_L14_ zenon_TX_dx); trivial. % 0.18/0.54 (* end of lemma zenon_L16_ *) % 0.18/0.54 assert (zenon_L17_ : forall (zenon_TX_dx : zenon_U), (~(((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))))) -> (forall Y : zenon_U, (s Y)) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (~(exists X : zenon_U, (q X))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> False). % 0.18/0.54 do 1 intro. intros zenon_H42 zenon_H5d zenon_H2 zenon_H12 zenon_H1f. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H42); [ zenon_intro zenon_H46; zenon_intro zenon_H45 | zenon_intro zenon_H44; zenon_intro zenon_H43 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L15_ zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L16_ zenon_TY_bt zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L16_ zenon_TY_bt zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L15_ zenon_TX_dx); trivial. % 0.18/0.54 (* end of lemma zenon_L17_ *) % 0.18/0.54 assert (zenon_L18_ : forall (zenon_TY_i : zenon_U) (zenon_TX_dx : zenon_U), (((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))))) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (~(exists X : zenon_U, (q X))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> (~(s zenon_TY_i)) -> False). % 0.18/0.54 do 2 intro. intros zenon_H64 zenon_H2 zenon_H12 zenon_H1f zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H64); [ zenon_intro zenon_H46; zenon_intro zenon_H43 | zenon_intro zenon_H44; zenon_intro zenon_H45 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L15_ zenon_TX_dx); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L16_ zenon_TY_bt zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L16_ zenon_TY_bt zenon_TX_dx); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L15_ zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 (* end of lemma zenon_L18_ *) % 0.18/0.54 assert (zenon_L19_ : forall (zenon_TY_ee : zenon_U), (~(exists X : zenon_U, (forall Y : zenon_U, ((r X)<->(r Y))))) -> (~(r zenon_TY_ee)) -> (~(exists X : zenon_U, (r X))) -> False). % 0.18/0.54 do 1 intro. intros zenon_H53 zenon_H6b zenon_H4b. % 0.18/0.54 apply zenon_H53. exists zenon_TY_ee. apply NNPP. zenon_intro zenon_H6d. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => ((r zenon_TY_ee)<->(r Y))) zenon_H6d); [ zenon_intro zenon_H6e; idtac ]. % 0.18/0.54 elim zenon_H6e. zenon_intro zenon_TY_eh. zenon_intro zenon_H70. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H70); [ zenon_intro zenon_H6b; zenon_intro zenon_H73 | zenon_intro zenon_H72; zenon_intro zenon_H71 ]. % 0.18/0.54 apply zenon_H4b. exists zenon_TY_eh. apply NNPP. zenon_intro zenon_H71. % 0.18/0.54 exact (zenon_H71 zenon_H73). % 0.18/0.54 exact (zenon_H6b zenon_H72). % 0.18/0.54 (* end of lemma zenon_L19_ *) % 0.18/0.54 assert (zenon_L20_ : forall (zenon_TX_en : zenon_U), (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> (forall Y : zenon_U, (q Y)) -> (q zenon_TX_en) -> False). % 0.18/0.54 do 1 intro. intros zenon_H11 zenon_H2a zenon_H74. % 0.18/0.54 apply zenon_H11. exists zenon_TX_en. apply NNPP. zenon_intro zenon_H76. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => ((q zenon_TX_en)<->(q Y))) zenon_H76); [ zenon_intro zenon_H77; idtac ]. % 0.18/0.54 elim zenon_H77. zenon_intro zenon_TY_eq. zenon_intro zenon_H79. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H79); [ zenon_intro zenon_H7c; zenon_intro zenon_H7b | zenon_intro zenon_H74; zenon_intro zenon_H7a ]. % 0.18/0.54 exact (zenon_H7c zenon_H74). % 0.18/0.54 generalize (zenon_H2a zenon_TY_eq). zenon_intro zenon_H7b. % 0.18/0.54 exact (zenon_H7a zenon_H7b). % 0.18/0.54 (* end of lemma zenon_L20_ *) % 0.18/0.54 assert (zenon_L21_ : forall (zenon_TX_en : zenon_U), (~((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> (forall Y : zenon_U, (p Y)) -> (q zenon_TX_en) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> False). % 0.18/0.54 do 1 intro. intros zenon_H35 zenon_H1f zenon_H1e zenon_H74 zenon_H11. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H35); [ zenon_intro zenon_H2b; zenon_intro zenon_H2a | zenon_intro zenon_H1d; zenon_intro zenon_H10 ]. % 0.18/0.54 apply (zenon_L20_ zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L3_); trivial. % 0.18/0.54 (* end of lemma zenon_L21_ *) % 0.18/0.54 assert (zenon_L22_ : forall (zenon_TY_bt : zenon_U) (zenon_TX_en : zenon_U), ((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))) -> (q zenon_TX_en) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> (~(p zenon_TY_bt)) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> False). % 0.18/0.54 do 2 intro. intros zenon_H29 zenon_H74 zenon_H11 zenon_H2c zenon_H1f. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H29); [ zenon_intro zenon_H2b; zenon_intro zenon_H10 | zenon_intro zenon_H1d; zenon_intro zenon_H2a ]. % 0.18/0.54 apply (zenon_L5_ zenon_TY_bt); trivial. % 0.18/0.54 apply (zenon_L20_ zenon_TX_en); trivial. % 0.18/0.54 (* end of lemma zenon_L22_ *) % 0.18/0.54 assert (zenon_L23_ : forall (zenon_TY_i : zenon_U) (zenon_TX_en : zenon_U), (((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> (q zenon_TX_en) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> (~(s zenon_TY_i)) -> False). % 0.18/0.54 do 2 intro. intros zenon_H64 zenon_H11 zenon_H74 zenon_H1f zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H64); [ zenon_intro zenon_H46; zenon_intro zenon_H43 | zenon_intro zenon_H44; zenon_intro zenon_H45 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L21_ zenon_TX_en); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L22_ zenon_TY_bt zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L22_ zenon_TY_bt zenon_TX_en); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L21_ zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 (* end of lemma zenon_L23_ *) % 0.18/0.54 assert (zenon_L24_ : forall (zenon_TX_en : zenon_U), (~(((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))))) -> (forall Y : zenon_U, (s Y)) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> (q zenon_TX_en) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> False). % 0.18/0.54 do 1 intro. intros zenon_H42 zenon_H5d zenon_H11 zenon_H74 zenon_H1f. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H42); [ zenon_intro zenon_H46; zenon_intro zenon_H45 | zenon_intro zenon_H44; zenon_intro zenon_H43 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L21_ zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L22_ zenon_TY_bt zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L22_ zenon_TY_bt zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L21_ zenon_TX_en); trivial. % 0.18/0.54 (* end of lemma zenon_L24_ *) % 0.18/0.54 assert (zenon_L25_ : forall (zenon_TX_dh : zenon_U) (zenon_TY_ee : zenon_U), (exists X : zenon_U, (forall Y : zenon_U, ((r X)<->(r Y)))) -> (~(r zenon_TY_ee)) -> (r zenon_TX_dh) -> False). % 0.18/0.54 do 2 intro. intros zenon_H4a zenon_H6b zenon_H54. % 0.18/0.54 elim zenon_H4a. zenon_intro zenon_TX_cz. zenon_intro zenon_H1. % 0.18/0.54 generalize (zenon_H1 zenon_E). zenon_intro zenon_H4e. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H4e); [ zenon_intro zenon_H52; zenon_intro zenon_H51 | zenon_intro zenon_H50; zenon_intro zenon_H4f ]. % 0.18/0.54 generalize (zenon_H1 zenon_TX_dh). zenon_intro zenon_H7d. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H7d); [ zenon_intro zenon_H52; zenon_intro zenon_H5c | zenon_intro zenon_H50; zenon_intro zenon_H54 ]. % 0.18/0.54 exact (zenon_H5c zenon_H54). % 0.18/0.54 exact (zenon_H52 zenon_H50). % 0.18/0.54 generalize (zenon_H1 zenon_TY_ee). zenon_intro zenon_H7e. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H7e); [ zenon_intro zenon_H52; zenon_intro zenon_H6b | zenon_intro zenon_H50; zenon_intro zenon_H72 ]. % 0.18/0.54 exact (zenon_H52 zenon_H50). % 0.18/0.54 exact (zenon_H6b zenon_H72). % 0.18/0.54 (* end of lemma zenon_L25_ *) % 0.18/0.54 assert (zenon_L26_ : forall (zenon_TY_u : zenon_U) (zenon_TX_dx : zenon_U), (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (q zenon_TX_dx) -> (~(q zenon_TY_u)) -> False). % 0.18/0.54 do 2 intro. intros zenon_H2 zenon_H68 zenon_H15. % 0.18/0.54 generalize (zenon_H2 zenon_TY_u). zenon_intro zenon_H7f. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H7f); [ zenon_intro zenon_H6a; zenon_intro zenon_H15 | zenon_intro zenon_H68; zenon_intro zenon_H1b ]. % 0.18/0.54 exact (zenon_H6a zenon_H68). % 0.18/0.54 exact (zenon_H15 zenon_H1b). % 0.18/0.54 (* end of lemma zenon_L26_ *) % 0.18/0.54 assert (zenon_L27_ : forall (zenon_TX_en : zenon_U) (zenon_TX_dx : zenon_U), (~(forall Y : zenon_U, (q Y))) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (q zenon_TX_en) -> False). % 0.18/0.54 do 2 intro. intros zenon_H10 zenon_H2 zenon_H74. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (q Y)) zenon_H10); [ zenon_intro zenon_H13; idtac ]. % 0.18/0.54 elim zenon_H13. zenon_intro zenon_TY_u. zenon_intro zenon_H15. % 0.18/0.54 generalize (zenon_H2 zenon_E). zenon_intro zenon_H66. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H66); [ zenon_intro zenon_H6a; zenon_intro zenon_H69 | zenon_intro zenon_H68; zenon_intro zenon_H67 ]. % 0.18/0.54 generalize (zenon_H2 zenon_TX_en). zenon_intro zenon_H80. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H80); [ zenon_intro zenon_H6a; zenon_intro zenon_H7c | zenon_intro zenon_H68; zenon_intro zenon_H74 ]. % 0.18/0.54 exact (zenon_H7c zenon_H74). % 0.18/0.54 exact (zenon_H6a zenon_H68). % 0.18/0.54 apply (zenon_L26_ zenon_TY_u zenon_TX_dx); trivial. % 0.18/0.54 (* end of lemma zenon_L27_ *) % 0.18/0.54 assert (zenon_L28_ : forall (zenon_TX_en : zenon_U) (zenon_TX_dx : zenon_U), ((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> (forall Y : zenon_U, (p Y)) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (q zenon_TX_en) -> False). % 0.18/0.54 do 2 intro. intros zenon_H29 zenon_H1f zenon_H1e zenon_H2 zenon_H74. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H29); [ zenon_intro zenon_H2b; zenon_intro zenon_H10 | zenon_intro zenon_H1d; zenon_intro zenon_H2a ]. % 0.18/0.54 apply (zenon_L27_ zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L3_); trivial. % 0.18/0.54 (* end of lemma zenon_L28_ *) % 0.18/0.54 assert (zenon_L29_ : forall (zenon_TY_bt : zenon_U) (zenon_TX_en : zenon_U) (zenon_TX_dx : zenon_U), (~((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (q zenon_TX_en) -> (~(p zenon_TY_bt)) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> False). % 0.18/0.54 do 3 intro. intros zenon_H35 zenon_H2 zenon_H74 zenon_H2c zenon_H1f. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H35); [ zenon_intro zenon_H2b; zenon_intro zenon_H2a | zenon_intro zenon_H1d; zenon_intro zenon_H10 ]. % 0.18/0.54 apply (zenon_L5_ zenon_TY_bt); trivial. % 0.18/0.54 apply (zenon_L27_ zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 (* end of lemma zenon_L29_ *) % 0.18/0.54 assert (zenon_L30_ : forall (zenon_TX_dx : zenon_U) (zenon_TX_en : zenon_U), (((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))))) -> (forall Y : zenon_U, (s Y)) -> (q zenon_TX_en) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> False). % 0.18/0.54 do 2 intro. intros zenon_H64 zenon_H5d zenon_H74 zenon_H2 zenon_H1f. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H64); [ zenon_intro zenon_H46; zenon_intro zenon_H43 | zenon_intro zenon_H44; zenon_intro zenon_H45 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L28_ zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L29_ zenon_TY_bt zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L29_ zenon_TY_bt zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L28_ zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 (* end of lemma zenon_L30_ *) % 0.18/0.54 assert (zenon_L31_ : forall (zenon_TY_i : zenon_U) (zenon_TX_dx : zenon_U) (zenon_TX_en : zenon_U), (~(((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))))) -> (q zenon_TX_en) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((p X)<->(p Y))))) -> (~(s zenon_TY_i)) -> False). % 0.18/0.54 do 3 intro. intros zenon_H42 zenon_H74 zenon_H2 zenon_H1f zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H42); [ zenon_intro zenon_H46; zenon_intro zenon_H45 | zenon_intro zenon_H44; zenon_intro zenon_H43 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L28_ zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L29_ zenon_TY_bt zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L29_ zenon_TY_bt zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L28_ zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 (* end of lemma zenon_L31_ *) % 0.18/0.54 assert (zenon_L32_ : forall (zenon_TX_fa : zenon_U), (~(exists X : zenon_U, (p X))) -> (p zenon_TX_fa) -> False). % 0.18/0.54 do 1 intro. intros zenon_H2b zenon_H81. % 0.18/0.54 apply zenon_H2b. exists zenon_TX_fa. apply NNPP. zenon_intro zenon_H83. % 0.18/0.54 exact (zenon_H83 zenon_H81). % 0.18/0.54 (* end of lemma zenon_L32_ *) % 0.18/0.54 assert (zenon_L33_ : forall (zenon_TX_fa : zenon_U), (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> (forall Y : zenon_U, (p Y)) -> (~(exists X : zenon_U, (p X))) -> False). % 0.18/0.54 do 1 intro. intros zenon_H3 zenon_H1e zenon_H2b. % 0.18/0.54 generalize (zenon_H3 zenon_E). zenon_intro zenon_H84. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H84); [ zenon_intro zenon_H83; zenon_intro zenon_H86 | zenon_intro zenon_H81; zenon_intro zenon_H85 ]. % 0.18/0.54 generalize (zenon_H1e zenon_TX_fa). zenon_intro zenon_H81. % 0.18/0.54 exact (zenon_H83 zenon_H81). % 0.18/0.54 apply (zenon_L32_ zenon_TX_fa); trivial. % 0.18/0.54 (* end of lemma zenon_L33_ *) % 0.18/0.54 assert (zenon_L34_ : forall (zenon_TX_fa : zenon_U), (~((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> (~(exists X : zenon_U, (q X))) -> (forall Y : zenon_U, (p Y)) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> False). % 0.18/0.54 do 1 intro. intros zenon_H35 zenon_H11 zenon_H12 zenon_H1e zenon_H3. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H35); [ zenon_intro zenon_H2b; zenon_intro zenon_H2a | zenon_intro zenon_H1d; zenon_intro zenon_H10 ]. % 0.18/0.54 apply (zenon_L33_ zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L2_); trivial. % 0.18/0.54 (* end of lemma zenon_L34_ *) % 0.18/0.54 assert (zenon_L35_ : forall (zenon_TX_fa : zenon_U) (zenon_TY_bt : zenon_U), (exists X : zenon_U, (p X)) -> (~(p zenon_TY_bt)) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> False). % 0.18/0.54 do 2 intro. intros zenon_H1d zenon_H2c zenon_H3. % 0.18/0.54 elim zenon_H1d. zenon_intro zenon_TX_bg. zenon_intro zenon_H21. % 0.18/0.54 generalize (zenon_H3 zenon_E). zenon_intro zenon_H84. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H84); [ zenon_intro zenon_H83; zenon_intro zenon_H86 | zenon_intro zenon_H81; zenon_intro zenon_H85 ]. % 0.18/0.54 generalize (zenon_H3 zenon_TX_bg). zenon_intro zenon_H87. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H87); [ zenon_intro zenon_H83; zenon_intro zenon_H28 | zenon_intro zenon_H81; zenon_intro zenon_H21 ]. % 0.18/0.54 exact (zenon_H28 zenon_H21). % 0.18/0.54 exact (zenon_H83 zenon_H81). % 0.18/0.54 generalize (zenon_H3 zenon_TY_bt). zenon_intro zenon_H88. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H88); [ zenon_intro zenon_H83; zenon_intro zenon_H2c | zenon_intro zenon_H81; zenon_intro zenon_H33 ]. % 0.18/0.54 exact (zenon_H83 zenon_H81). % 0.18/0.54 exact (zenon_H2c zenon_H33). % 0.18/0.54 (* end of lemma zenon_L35_ *) % 0.18/0.54 assert (zenon_L36_ : forall (zenon_TY_bt : zenon_U) (zenon_TX_fa : zenon_U), ((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> (~(p zenon_TY_bt)) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> (~(exists X : zenon_U, (q X))) -> False). % 0.18/0.54 do 2 intro. intros zenon_H29 zenon_H3 zenon_H2c zenon_H11 zenon_H12. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H29); [ zenon_intro zenon_H2b; zenon_intro zenon_H10 | zenon_intro zenon_H1d; zenon_intro zenon_H2a ]. % 0.18/0.54 apply (zenon_L2_); trivial. % 0.18/0.54 apply (zenon_L35_ zenon_TX_fa zenon_TY_bt); trivial. % 0.18/0.54 (* end of lemma zenon_L36_ *) % 0.18/0.54 assert (zenon_L37_ : forall (zenon_TY_i : zenon_U) (zenon_TX_fa : zenon_U), (((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))))) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> (~(exists X : zenon_U, (q X))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> (~(s zenon_TY_i)) -> False). % 0.18/0.54 do 2 intro. intros zenon_H64 zenon_H3 zenon_H12 zenon_H11 zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H64); [ zenon_intro zenon_H46; zenon_intro zenon_H43 | zenon_intro zenon_H44; zenon_intro zenon_H45 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L34_ zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L36_ zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L36_ zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L34_ zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 (* end of lemma zenon_L37_ *) % 0.18/0.54 assert (zenon_L38_ : forall (zenon_TX_fa : zenon_U), (~(((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))))) -> (forall Y : zenon_U, (s Y)) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> (~(exists X : zenon_U, (q X))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> False). % 0.18/0.54 do 1 intro. intros zenon_H42 zenon_H5d zenon_H3 zenon_H12 zenon_H11. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H42); [ zenon_intro zenon_H46; zenon_intro zenon_H45 | zenon_intro zenon_H44; zenon_intro zenon_H43 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L34_ zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L36_ zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L36_ zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L34_ zenon_TX_fa); trivial. % 0.18/0.54 (* end of lemma zenon_L38_ *) % 0.18/0.54 assert (zenon_L39_ : forall (zenon_TX_fa : zenon_U) (zenon_TX_dx : zenon_U), ((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))) -> (~(exists X : zenon_U, (q X))) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (forall Y : zenon_U, (p Y)) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> False). % 0.18/0.54 do 2 intro. intros zenon_H29 zenon_H12 zenon_H2 zenon_H1e zenon_H3. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H29); [ zenon_intro zenon_H2b; zenon_intro zenon_H10 | zenon_intro zenon_H1d; zenon_intro zenon_H2a ]. % 0.18/0.54 apply (zenon_L33_ zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L14_ zenon_TX_dx); trivial. % 0.18/0.54 (* end of lemma zenon_L39_ *) % 0.18/0.54 assert (zenon_L40_ : forall (zenon_TX_dx : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TX_fa : zenon_U), (~((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> (~(p zenon_TY_bt)) -> (~(exists X : zenon_U, (q X))) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> False). % 0.18/0.54 do 3 intro. intros zenon_H35 zenon_H3 zenon_H2c zenon_H12 zenon_H2. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H35); [ zenon_intro zenon_H2b; zenon_intro zenon_H2a | zenon_intro zenon_H1d; zenon_intro zenon_H10 ]. % 0.18/0.54 apply (zenon_L14_ zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L35_ zenon_TX_fa zenon_TY_bt); trivial. % 0.18/0.54 (* end of lemma zenon_L40_ *) % 0.18/0.54 assert (zenon_L41_ : forall (zenon_TX_dx : zenon_U) (zenon_TX_fa : zenon_U), (((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))))) -> (forall Y : zenon_U, (s Y)) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (~(exists X : zenon_U, (q X))) -> False). % 0.18/0.54 do 2 intro. intros zenon_H64 zenon_H5d zenon_H3 zenon_H2 zenon_H12. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H64); [ zenon_intro zenon_H46; zenon_intro zenon_H43 | zenon_intro zenon_H44; zenon_intro zenon_H45 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L39_ zenon_TX_fa zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L40_ zenon_TX_dx zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L40_ zenon_TX_dx zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L39_ zenon_TX_fa zenon_TX_dx); trivial. % 0.18/0.54 (* end of lemma zenon_L41_ *) % 0.18/0.54 assert (zenon_L42_ : forall (zenon_TY_i : zenon_U) (zenon_TX_dx : zenon_U) (zenon_TX_fa : zenon_U), (~(((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))))) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (~(exists X : zenon_U, (q X))) -> (~(s zenon_TY_i)) -> False). % 0.18/0.54 do 3 intro. intros zenon_H42 zenon_H3 zenon_H2 zenon_H12 zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H42); [ zenon_intro zenon_H46; zenon_intro zenon_H45 | zenon_intro zenon_H44; zenon_intro zenon_H43 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L39_ zenon_TX_fa zenon_TX_dx); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L40_ zenon_TX_dx zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L40_ zenon_TX_dx zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L39_ zenon_TX_fa zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 (* end of lemma zenon_L42_ *) % 0.18/0.54 assert (zenon_L43_ : forall (zenon_TX_fa : zenon_U) (zenon_TX_en : zenon_U), ((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))) -> (q zenon_TX_en) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> (forall Y : zenon_U, (p Y)) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> False). % 0.18/0.54 do 2 intro. intros zenon_H29 zenon_H74 zenon_H11 zenon_H1e zenon_H3. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H29); [ zenon_intro zenon_H2b; zenon_intro zenon_H10 | zenon_intro zenon_H1d; zenon_intro zenon_H2a ]. % 0.18/0.54 apply (zenon_L33_ zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L20_ zenon_TX_en); trivial. % 0.18/0.54 (* end of lemma zenon_L43_ *) % 0.18/0.54 assert (zenon_L44_ : forall (zenon_TX_en : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TX_fa : zenon_U), (~((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> (~(p zenon_TY_bt)) -> (q zenon_TX_en) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> False). % 0.18/0.54 do 3 intro. intros zenon_H35 zenon_H3 zenon_H2c zenon_H74 zenon_H11. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H35); [ zenon_intro zenon_H2b; zenon_intro zenon_H2a | zenon_intro zenon_H1d; zenon_intro zenon_H10 ]. % 0.18/0.54 apply (zenon_L20_ zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L35_ zenon_TX_fa zenon_TY_bt); trivial. % 0.18/0.54 (* end of lemma zenon_L44_ *) % 0.18/0.54 assert (zenon_L45_ : forall (zenon_TY_i : zenon_U) (zenon_TX_en : zenon_U) (zenon_TX_fa : zenon_U), (~(((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))))) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> (q zenon_TX_en) -> (~(s zenon_TY_i)) -> False). % 0.18/0.54 do 3 intro. intros zenon_H42 zenon_H3 zenon_H11 zenon_H74 zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H42); [ zenon_intro zenon_H46; zenon_intro zenon_H45 | zenon_intro zenon_H44; zenon_intro zenon_H43 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L43_ zenon_TX_fa zenon_TX_en); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L44_ zenon_TX_en zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L44_ zenon_TX_en zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L43_ zenon_TX_fa zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 (* end of lemma zenon_L45_ *) % 0.18/0.54 assert (zenon_L46_ : forall (zenon_TX_en : zenon_U) (zenon_TX_fa : zenon_U), (((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))))) -> (forall Y : zenon_U, (s Y)) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> (~(exists X : zenon_U, (forall Y : zenon_U, ((q X)<->(q Y))))) -> (q zenon_TX_en) -> False). % 0.18/0.54 do 2 intro. intros zenon_H64 zenon_H5d zenon_H3 zenon_H11 zenon_H74. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H64); [ zenon_intro zenon_H46; zenon_intro zenon_H43 | zenon_intro zenon_H44; zenon_intro zenon_H45 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L43_ zenon_TX_fa zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L44_ zenon_TX_en zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L44_ zenon_TX_en zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L43_ zenon_TX_fa zenon_TX_en); trivial. % 0.18/0.54 (* end of lemma zenon_L46_ *) % 0.18/0.54 assert (zenon_L47_ : forall (zenon_TX_fa : zenon_U) (zenon_TX_en : zenon_U) (zenon_TX_dx : zenon_U), (~((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (q zenon_TX_en) -> (forall Y : zenon_U, (p Y)) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> False). % 0.18/0.54 do 3 intro. intros zenon_H35 zenon_H2 zenon_H74 zenon_H1e zenon_H3. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H35); [ zenon_intro zenon_H2b; zenon_intro zenon_H2a | zenon_intro zenon_H1d; zenon_intro zenon_H10 ]. % 0.18/0.54 apply (zenon_L33_ zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L27_ zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 (* end of lemma zenon_L47_ *) % 0.18/0.54 assert (zenon_L48_ : forall (zenon_TX_en : zenon_U) (zenon_TX_dx : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TX_fa : zenon_U), ((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> (~(p zenon_TY_bt)) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (q zenon_TX_en) -> False). % 0.18/0.54 do 4 intro. intros zenon_H29 zenon_H3 zenon_H2c zenon_H2 zenon_H74. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H29); [ zenon_intro zenon_H2b; zenon_intro zenon_H10 | zenon_intro zenon_H1d; zenon_intro zenon_H2a ]. % 0.18/0.54 apply (zenon_L27_ zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L35_ zenon_TX_fa zenon_TY_bt); trivial. % 0.18/0.54 (* end of lemma zenon_L48_ *) % 0.18/0.54 assert (zenon_L49_ : forall (zenon_TX_dx : zenon_U) (zenon_TX_en : zenon_U) (zenon_TX_fa : zenon_U), (~(((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y)))))) -> (forall Y : zenon_U, (s Y)) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> (q zenon_TX_en) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> False). % 0.18/0.54 do 3 intro. intros zenon_H42 zenon_H5d zenon_H3 zenon_H74 zenon_H2. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H42); [ zenon_intro zenon_H46; zenon_intro zenon_H45 | zenon_intro zenon_H44; zenon_intro zenon_H43 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L47_ zenon_TX_fa zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L48_ zenon_TX_en zenon_TX_dx zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L48_ zenon_TX_en zenon_TX_dx zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L11_); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L12_ zenon_TX_ce); trivial. % 0.18/0.54 apply (zenon_L47_ zenon_TX_fa zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 (* end of lemma zenon_L49_ *) % 0.18/0.54 assert (zenon_L50_ : forall (zenon_TY_i : zenon_U) (zenon_TX_dx : zenon_U) (zenon_TX_en : zenon_U) (zenon_TX_fa : zenon_U), (((exists X : zenon_U, (s X))<->(forall Y : zenon_U, (p Y)))<->((exists X : zenon_U, (forall Y : zenon_U, ((s X)<->(s Y))))<->((exists X : zenon_U, (p X))<->(forall Y : zenon_U, (q Y))))) -> (forall Y : zenon_U, ((p zenon_TX_fa)<->(p Y))) -> (q zenon_TX_en) -> (forall Y : zenon_U, ((q zenon_TX_dx)<->(q Y))) -> (~(s zenon_TY_i)) -> False). % 0.18/0.54 do 4 intro. intros zenon_H64 zenon_H3 zenon_H74 zenon_H2 zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H64); [ zenon_intro zenon_H46; zenon_intro zenon_H43 | zenon_intro zenon_H44; zenon_intro zenon_H45 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H46); [ zenon_intro zenon_H7; zenon_intro zenon_H1e | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L47_ zenon_TX_fa zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H29 | zenon_intro zenon_H36; zenon_intro zenon_H35 ]. % 0.18/0.54 apply (zenon_L48_ zenon_TX_en zenon_TX_dx zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H7; zenon_intro zenon_H47 | zenon_intro zenon_H48; zenon_intro zenon_H1e ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (p Y)) zenon_H47); [ zenon_intro zenon_H49; idtac ]. % 0.18/0.54 elim zenon_H49. zenon_intro zenon_TY_bt. zenon_intro zenon_H2c. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L1_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L48_ zenon_TX_en zenon_TX_dx zenon_TY_bt zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H48. zenon_intro zenon_TX_ce. zenon_intro zenon_H37. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H5; zenon_intro zenon_H35 | zenon_intro zenon_H36; zenon_intro zenon_H29 ]. % 0.18/0.54 apply (zenon_L47_ zenon_TX_fa zenon_TX_en zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L7_ zenon_TX_ce zenon_TY_i); trivial. % 0.18/0.54 (* end of lemma zenon_L50_ *) % 0.18/0.54 apply NNPP. intro zenon_G. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_G); [ zenon_intro zenon_H1f; zenon_intro zenon_H8b | zenon_intro zenon_H8a; zenon_intro zenon_H89 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H8b); [ zenon_intro zenon_H8f; zenon_intro zenon_H8e | zenon_intro zenon_H8d; zenon_intro zenon_H8c ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H8f); [ zenon_intro zenon_H12; zenon_intro zenon_H4c | zenon_intro zenon_H91; zenon_intro zenon_H90 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H8e); [ zenon_intro zenon_H95; zenon_intro zenon_H94 | zenon_intro zenon_H93; zenon_intro zenon_H92 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H95); [ zenon_intro zenon_H11; zenon_intro zenon_H98 | zenon_intro zenon_H97; zenon_intro zenon_H96 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L8_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L13_); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L17_ zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L18_ zenon_TY_i zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H93); [ zenon_intro zenon_H11; zenon_intro zenon_H96 | zenon_intro zenon_H97; zenon_intro zenon_H98 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L13_); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L8_ zenon_TY_i); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L18_ zenon_TY_i zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L17_ zenon_TX_dx); trivial. % 0.18/0.54 elim zenon_H91. zenon_intro zenon_TX_en. zenon_intro zenon_H74. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (r Y)) zenon_H90); [ zenon_intro zenon_H9c; idtac ]. % 0.18/0.54 elim zenon_H9c. zenon_intro zenon_TY_ee. zenon_intro zenon_H6b. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H8e); [ zenon_intro zenon_H95; zenon_intro zenon_H94 | zenon_intro zenon_H93; zenon_intro zenon_H92 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H95); [ zenon_intro zenon_H11; zenon_intro zenon_H98 | zenon_intro zenon_H97; zenon_intro zenon_H96 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L23_ zenon_TY_i zenon_TX_en); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L24_ zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L30_ zenon_TX_dx zenon_TX_en); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L31_ zenon_TY_i zenon_TX_dx zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H93); [ zenon_intro zenon_H11; zenon_intro zenon_H96 | zenon_intro zenon_H97; zenon_intro zenon_H98 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L24_ zenon_TX_en); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L23_ zenon_TY_i zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L31_ zenon_TY_i zenon_TX_dx zenon_TX_en); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L30_ zenon_TX_dx zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H8d); [ zenon_intro zenon_H12; zenon_intro zenon_H90 | zenon_intro zenon_H91; zenon_intro zenon_H4c ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (r Y)) zenon_H90); [ zenon_intro zenon_H9c; idtac ]. % 0.18/0.54 elim zenon_H9c. zenon_intro zenon_TY_ee. zenon_intro zenon_H6b. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H8c); [ zenon_intro zenon_H95; zenon_intro zenon_H92 | zenon_intro zenon_H93; zenon_intro zenon_H94 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H95); [ zenon_intro zenon_H11; zenon_intro zenon_H98 | zenon_intro zenon_H97; zenon_intro zenon_H96 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L8_ zenon_TY_i); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L13_); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L17_ zenon_TX_dx); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L18_ zenon_TY_i zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H93); [ zenon_intro zenon_H11; zenon_intro zenon_H96 | zenon_intro zenon_H97; zenon_intro zenon_H98 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L13_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L8_ zenon_TY_i); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L18_ zenon_TY_i zenon_TX_dx); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L17_ zenon_TX_dx); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 elim zenon_H91. zenon_intro zenon_TX_en. zenon_intro zenon_H74. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H8c); [ zenon_intro zenon_H95; zenon_intro zenon_H92 | zenon_intro zenon_H93; zenon_intro zenon_H94 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H95); [ zenon_intro zenon_H11; zenon_intro zenon_H98 | zenon_intro zenon_H97; zenon_intro zenon_H96 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L23_ zenon_TY_i zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L24_ zenon_TX_en); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L30_ zenon_TX_dx zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L31_ zenon_TY_i zenon_TX_dx zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H93); [ zenon_intro zenon_H11; zenon_intro zenon_H96 | zenon_intro zenon_H97; zenon_intro zenon_H98 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L24_ zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L23_ zenon_TY_i zenon_TX_en); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L31_ zenon_TY_i zenon_TX_dx zenon_TX_en); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L30_ zenon_TX_dx zenon_TX_en); trivial. % 0.18/0.54 elim zenon_H8a. zenon_intro zenon_TX_fa. zenon_intro zenon_H3. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H89); [ zenon_intro zenon_H8f; zenon_intro zenon_H8c | zenon_intro zenon_H8d; zenon_intro zenon_H8e ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H8f); [ zenon_intro zenon_H12; zenon_intro zenon_H4c | zenon_intro zenon_H91; zenon_intro zenon_H90 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H8c); [ zenon_intro zenon_H95; zenon_intro zenon_H92 | zenon_intro zenon_H93; zenon_intro zenon_H94 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H95); [ zenon_intro zenon_H11; zenon_intro zenon_H98 | zenon_intro zenon_H97; zenon_intro zenon_H96 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L37_ zenon_TY_i zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L38_ zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L41_ zenon_TX_dx zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L42_ zenon_TY_i zenon_TX_dx zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H93); [ zenon_intro zenon_H11; zenon_intro zenon_H96 | zenon_intro zenon_H97; zenon_intro zenon_H98 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L38_ zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L37_ zenon_TY_i zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L42_ zenon_TY_i zenon_TX_dx zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L41_ zenon_TX_dx zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H91. zenon_intro zenon_TX_en. zenon_intro zenon_H74. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (r Y)) zenon_H90); [ zenon_intro zenon_H9c; idtac ]. % 0.18/0.54 elim zenon_H9c. zenon_intro zenon_TY_ee. zenon_intro zenon_H6b. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H8c); [ zenon_intro zenon_H95; zenon_intro zenon_H92 | zenon_intro zenon_H93; zenon_intro zenon_H94 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H95); [ zenon_intro zenon_H11; zenon_intro zenon_H98 | zenon_intro zenon_H97; zenon_intro zenon_H96 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L45_ zenon_TY_i zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L46_ zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L49_ zenon_TX_dx zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L50_ zenon_TY_i zenon_TX_dx zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H93); [ zenon_intro zenon_H11; zenon_intro zenon_H96 | zenon_intro zenon_H97; zenon_intro zenon_H98 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L46_ zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L45_ zenon_TY_i zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L50_ zenon_TY_i zenon_TX_dx zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L49_ zenon_TX_dx zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H8d); [ zenon_intro zenon_H12; zenon_intro zenon_H90 | zenon_intro zenon_H91; zenon_intro zenon_H4c ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (r Y)) zenon_H90); [ zenon_intro zenon_H9c; idtac ]. % 0.18/0.54 elim zenon_H9c. zenon_intro zenon_TY_ee. zenon_intro zenon_H6b. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H8e); [ zenon_intro zenon_H95; zenon_intro zenon_H94 | zenon_intro zenon_H93; zenon_intro zenon_H92 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H95); [ zenon_intro zenon_H11; zenon_intro zenon_H98 | zenon_intro zenon_H97; zenon_intro zenon_H96 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L37_ zenon_TY_i zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L38_ zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L41_ zenon_TX_dx zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L42_ zenon_TY_i zenon_TX_dx zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H93); [ zenon_intro zenon_H11; zenon_intro zenon_H96 | zenon_intro zenon_H97; zenon_intro zenon_H98 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L38_ zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L37_ zenon_TY_i zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L19_ zenon_TY_ee); trivial. % 0.18/0.54 apply (zenon_L42_ zenon_TY_i zenon_TX_dx zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L41_ zenon_TX_dx zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L25_ zenon_TX_dh zenon_TY_ee); trivial. % 0.18/0.54 elim zenon_H91. zenon_intro zenon_TX_en. zenon_intro zenon_H74. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H8e); [ zenon_intro zenon_H95; zenon_intro zenon_H94 | zenon_intro zenon_H93; zenon_intro zenon_H92 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H95); [ zenon_intro zenon_H11; zenon_intro zenon_H98 | zenon_intro zenon_H97; zenon_intro zenon_H96 ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L45_ zenon_TY_i zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L46_ zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L49_ zenon_TX_dx zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H53; zenon_intro zenon_H42 | zenon_intro zenon_H4a; zenon_intro zenon_H64 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L50_ zenon_TY_i zenon_TX_dx zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H93); [ zenon_intro zenon_H11; zenon_intro zenon_H96 | zenon_intro zenon_H97; zenon_intro zenon_H98 ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H96); [ zenon_intro zenon_H4b; zenon_intro zenon_H5d | zenon_intro zenon_H99; zenon_intro zenon_H9a ]. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L46_ zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L45_ zenon_TY_i zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 elim zenon_H97. zenon_intro zenon_TX_dx. zenon_intro zenon_H2. % 0.18/0.54 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H4b; zenon_intro zenon_H9a | zenon_intro zenon_H99; zenon_intro zenon_H5d ]. % 0.18/0.54 apply (zenon_notallex_s (fun Y : zenon_U => (s Y)) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 0.18/0.54 elim zenon_H9b. zenon_intro zenon_TY_i. zenon_intro zenon_H6. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L50_ zenon_TY_i zenon_TX_dx zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 apply (zenon_L9_); trivial. % 0.18/0.54 elim zenon_H99. zenon_intro zenon_TX_dh. zenon_intro zenon_H54. % 0.18/0.54 apply (zenon_notequiv_s _ _ zenon_H92); [ zenon_intro zenon_H53; zenon_intro zenon_H64 | zenon_intro zenon_H4a; zenon_intro zenon_H42 ]. % 0.18/0.54 apply (zenon_L10_ zenon_TX_dh); trivial. % 0.18/0.54 apply (zenon_L49_ zenon_TX_dx zenon_TX_en zenon_TX_fa); trivial. % 0.18/0.54 Qed. % 0.18/0.54 % SZS output end Proof % 0.18/0.54 (* END-PROOF *) % 0.18/0.54 nodes searched: 1109 % 0.18/0.54 max branch formulas: 74 % 0.18/0.54 proof nodes created: 550 % 0.18/0.54 formulas created: 1194 % 0.18/0.54 %------------------------------------------------------------------------------