%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : KRS084+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n022.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 : Sun Jul 17 03:39:24 EDT 2022 % Result : Unsatisfiable 244.33s 244.62s % Output : Proof 244.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS084+1 : TPTP v8.1.0. Released v3.1.0. % 0.03/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n022.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 Jun 7 07:32:05 EDT 2022 % 0.12/0.33 % CPUTime : % 244.33/244.62 (* PROOF-FOUND *) % 244.33/244.62 % SZS status Unsatisfiable % 244.33/244.62 (* BEGIN-PROOF *) % 244.33/244.62 % SZS output start Proof % 244.33/244.62 Theorem zenon_thm : False. % 244.33/244.62 Proof. % 244.33/244.62 assert (zenon_L1_ : forall (zenon_TY_bc : zenon_U) (zenon_TY_bd : zenon_U), (rf zenon_TY_bd (i2003_11_14_17_19_35232)) -> (rf zenon_TY_bd zenon_TY_bc) -> (~((i2003_11_14_17_19_35232) = zenon_TY_bc)) -> False). % 244.33/244.62 do 2 intro. intros zenon_H19 zenon_H1a zenon_H1b. % 244.33/244.62 generalize (axiom_4 zenon_TY_bd). zenon_intro zenon_H1e. % 244.33/244.62 generalize (zenon_H1e (i2003_11_14_17_19_35232)). zenon_intro zenon_H1f. % 244.33/244.62 generalize (zenon_H1f zenon_TY_bc). zenon_intro zenon_H20. % 244.33/244.62 apply (zenon_imply_s _ _ zenon_H20); [ zenon_intro zenon_H22 | zenon_intro zenon_H21 ]. % 244.33/244.62 apply (zenon_notand_s _ _ zenon_H22); [ zenon_intro zenon_H24 | zenon_intro zenon_H23 ]. % 244.33/244.62 exact (zenon_H24 zenon_H19). % 244.33/244.62 exact (zenon_H23 zenon_H1a). % 244.33/244.62 exact (zenon_H1b zenon_H21). % 244.33/244.62 (* end of lemma zenon_L1_ *) % 244.33/244.62 assert (zenon_L2_ : ((exists Y : zenon_U, ((rinvF (i2003_11_14_17_19_35232) Y)/\(cd Y)))/\((forall Y : zenon_U, ((rinvR (i2003_11_14_17_19_35232) Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z)))))/\(~(cc (i2003_11_14_17_19_35232))))) -> (~(cUnsatisfiable (i2003_11_14_17_19_35232))) -> False). % 244.33/244.62 do 0 intro. intros zenon_H25 zenon_H26. % 244.33/244.62 generalize (axiom_2 (i2003_11_14_17_19_35232)). zenon_intro zenon_H27. % 244.33/244.62 apply (zenon_equiv_s _ _ zenon_H27); [ zenon_intro zenon_H26; zenon_intro zenon_H28 | zenon_intro axiom_8; zenon_intro zenon_H25 ]. % 244.33/244.62 exact (zenon_H28 zenon_H25). % 244.33/244.62 exact (zenon_H26 axiom_8). % 244.33/244.62 (* end of lemma zenon_L2_ *) % 244.33/244.62 assert (zenon_L3_ : forall (zenon_TY_bt : zenon_U) (zenon_TY_bc : zenon_U) (zenon_TZ_bu : zenon_U), (forall Z : zenon_U, (((rf zenon_TZ_bu zenon_TY_bc)/\(rf zenon_TZ_bu Z))->(zenon_TY_bc = Z))) -> (rf zenon_TZ_bu zenon_TY_bc) -> (rf zenon_TZ_bu zenon_TY_bt) -> (~(zenon_TY_bc = zenon_TY_bt)) -> False). % 244.33/244.62 do 3 intro. intros zenon_H29 zenon_H2a zenon_H2b zenon_H2c. % 244.33/244.62 generalize (zenon_H29 zenon_TY_bt). zenon_intro zenon_H2f. % 244.33/244.62 apply (zenon_imply_s _ _ zenon_H2f); [ zenon_intro zenon_H31 | zenon_intro zenon_H30 ]. % 244.33/244.62 apply (zenon_notand_s _ _ zenon_H31); [ zenon_intro zenon_H33 | zenon_intro zenon_H32 ]. % 244.33/244.62 exact (zenon_H33 zenon_H2a). % 244.33/244.62 exact (zenon_H32 zenon_H2b). % 244.33/244.62 exact (zenon_H2c zenon_H30). % 244.33/244.62 (* end of lemma zenon_L3_ *) % 244.33/244.62 assert (zenon_L4_ : forall (zenon_TY_bt : zenon_U) (zenon_TY_bc : zenon_U) (zenon_TZ_bu : zenon_U), (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_bu Y)/\(rf zenon_TZ_bu Z))->(Y = Z)))) -> (~(zenon_TY_bc = zenon_TY_bt)) -> (rf zenon_TZ_bu zenon_TY_bt) -> (rf zenon_TZ_bu zenon_TY_bc) -> False). % 244.33/244.62 do 3 intro. intros zenon_H34 zenon_H2c zenon_H2b zenon_H2a. % 244.33/244.62 generalize (zenon_H34 zenon_TY_bc). zenon_intro zenon_H29. % 244.33/244.62 apply (zenon_L3_ zenon_TY_bt zenon_TY_bc zenon_TZ_bu); trivial. % 244.33/244.62 (* end of lemma zenon_L4_ *) % 244.33/244.62 assert (zenon_L5_ : forall (zenon_TY_bc : zenon_U), ((exists Z : zenon_U, ((rinvF zenon_TY_bc Z)/\(cd Z)))/\((forall Y : zenon_U, ((rinvR zenon_TY_bc Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z)))))/\(~(cc zenon_TY_bc)))) -> (~(cUnsatisfiable zenon_TY_bc)) -> False). % 244.33/244.62 do 1 intro. intros zenon_H35 zenon_H36. % 244.33/244.62 generalize (axiom_2 zenon_TY_bc). zenon_intro zenon_H37. % 244.33/244.62 apply (zenon_equiv_s _ _ zenon_H37); [ zenon_intro zenon_H36; zenon_intro zenon_H39 | zenon_intro zenon_H38; zenon_intro zenon_H35 ]. % 244.33/244.62 exact (zenon_H39 zenon_H35). % 244.33/244.62 exact (zenon_H36 zenon_H38). % 244.33/244.62 (* end of lemma zenon_L5_ *) % 244.33/244.62 assert (zenon_L6_ : (~((i2003_11_14_17_19_35232) = (i2003_11_14_17_19_35232))) -> False). % 244.33/244.62 do 0 intro. intros zenon_H3a. % 244.33/244.62 apply zenon_H3a. apply refl_equal. % 244.33/244.62 (* end of lemma zenon_L6_ *) % 244.33/244.62 assert (zenon_L7_ : forall (zenon_TY_bt : zenon_U) (zenon_TY_cl : zenon_U) (zenon_TZ_cm : zenon_U), (forall Z : zenon_U, (((rf zenon_TZ_cm zenon_TY_cl)/\(rf zenon_TZ_cm Z))->(zenon_TY_cl = Z))) -> (rf zenon_TZ_cm zenon_TY_cl) -> (rf zenon_TZ_cm zenon_TY_bt) -> (~(zenon_TY_cl = zenon_TY_bt)) -> False). % 244.33/244.62 do 3 intro. intros zenon_H3b zenon_H3c zenon_H3d zenon_H3e. % 244.33/244.62 generalize (zenon_H3b zenon_TY_bt). zenon_intro zenon_H41. % 244.33/244.62 apply (zenon_imply_s _ _ zenon_H41); [ zenon_intro zenon_H43 | zenon_intro zenon_H42 ]. % 244.33/244.62 apply (zenon_notand_s _ _ zenon_H43); [ zenon_intro zenon_H45 | zenon_intro zenon_H44 ]. % 244.33/244.62 exact (zenon_H45 zenon_H3c). % 244.33/244.62 exact (zenon_H44 zenon_H3d). % 244.33/244.62 exact (zenon_H3e zenon_H42). % 244.33/244.62 (* end of lemma zenon_L7_ *) % 244.33/244.62 assert (zenon_L8_ : forall (zenon_TY_cl : zenon_U) (zenon_TZ_cm : zenon_U) (zenon_TY_bc : zenon_U) (zenon_TY_bt : zenon_U), (zenon_TY_bt = zenon_TY_bc) -> (rf zenon_TZ_cm zenon_TY_cl) -> (rf zenon_TZ_cm zenon_TY_bt) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_cm Y)/\(rf zenon_TZ_cm Z))->(Y = Z)))) -> (~(zenon_TY_bc = zenon_TY_cl)) -> False). % 244.33/244.62 do 4 intro. intros zenon_H46 zenon_H3c zenon_H3d zenon_H47 zenon_H48. % 244.33/244.62 elim (classic (zenon_TY_cl = zenon_TY_cl)); [ zenon_intro zenon_H49 | zenon_intro zenon_H4a ]. % 244.33/244.62 cut ((zenon_TY_cl = zenon_TY_cl) = (zenon_TY_bc = zenon_TY_cl)). % 244.33/244.62 intro zenon_D_pnotp. % 244.33/244.62 apply zenon_H48. % 244.33/244.62 rewrite <- zenon_D_pnotp. % 244.33/244.62 exact zenon_H49. % 244.33/244.62 cut ((zenon_TY_cl = zenon_TY_cl)); [idtac | apply NNPP; zenon_intro zenon_H4a]. % 244.33/244.62 cut ((zenon_TY_cl = zenon_TY_bc)); [idtac | apply NNPP; zenon_intro zenon_H4b]. % 244.33/244.62 congruence. % 244.33/244.62 cut ((zenon_TY_bt = zenon_TY_bc) = (zenon_TY_cl = zenon_TY_bc)). % 244.33/244.62 intro zenon_D_pnotp. % 244.33/244.62 apply zenon_H4b. % 244.33/244.62 rewrite <- zenon_D_pnotp. % 244.33/244.62 exact zenon_H46. % 244.33/244.62 cut ((zenon_TY_bc = zenon_TY_bc)); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 244.33/244.62 cut ((zenon_TY_bt = zenon_TY_cl)); [idtac | apply NNPP; zenon_intro zenon_H4d]. % 244.33/244.62 congruence. % 244.33/244.62 elim (classic (zenon_TY_cl = zenon_TY_cl)); [ zenon_intro zenon_H49 | zenon_intro zenon_H4a ]. % 244.33/244.62 cut ((zenon_TY_cl = zenon_TY_cl) = (zenon_TY_bt = zenon_TY_cl)). % 244.33/244.62 intro zenon_D_pnotp. % 244.33/244.62 apply zenon_H4d. % 244.33/244.62 rewrite <- zenon_D_pnotp. % 244.33/244.62 exact zenon_H49. % 244.33/244.62 cut ((zenon_TY_cl = zenon_TY_cl)); [idtac | apply NNPP; zenon_intro zenon_H4a]. % 244.33/244.62 cut ((zenon_TY_cl = zenon_TY_bt)); [idtac | apply NNPP; zenon_intro zenon_H3e]. % 244.33/244.62 congruence. % 244.33/244.62 generalize (zenon_H47 zenon_TY_cl). zenon_intro zenon_H3b. % 244.33/244.62 apply (zenon_L7_ zenon_TY_bt zenon_TY_cl zenon_TZ_cm); trivial. % 244.33/244.62 apply zenon_H4a. apply refl_equal. % 244.33/244.62 apply zenon_H4a. apply refl_equal. % 244.33/244.62 apply zenon_H4c. apply refl_equal. % 244.33/244.62 apply zenon_H4a. apply refl_equal. % 244.33/244.62 apply zenon_H4a. apply refl_equal. % 244.33/244.62 (* end of lemma zenon_L8_ *) % 244.33/244.62 assert (zenon_L9_ : forall (zenon_TY_cl : zenon_U) (zenon_TZ_cm : zenon_U) (zenon_TY_bc : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TZ_bu : zenon_U), (((rf zenon_TZ_bu zenon_TY_bt)/\(rf zenon_TZ_bu zenon_TY_bc))->(zenon_TY_bt = zenon_TY_bc)) -> (rf zenon_TZ_bu zenon_TY_bc) -> (rf zenon_TZ_bu zenon_TY_bt) -> (rf zenon_TZ_cm zenon_TY_cl) -> (rf zenon_TZ_cm zenon_TY_bt) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_cm Y)/\(rf zenon_TZ_cm Z))->(Y = Z)))) -> (~(zenon_TY_bc = zenon_TY_cl)) -> False). % 244.33/244.62 do 5 intro. intros zenon_H4e zenon_H2a zenon_H2b zenon_H3c zenon_H3d zenon_H47 zenon_H48. % 244.33/244.62 apply (zenon_imply_s _ _ zenon_H4e); [ zenon_intro zenon_H4f | zenon_intro zenon_H46 ]. % 244.33/244.62 apply (zenon_notand_s _ _ zenon_H4f); [ zenon_intro zenon_H32 | zenon_intro zenon_H33 ]. % 244.33/244.62 exact (zenon_H32 zenon_H2b). % 244.33/244.62 exact (zenon_H33 zenon_H2a). % 244.33/244.62 apply (zenon_L8_ zenon_TY_cl zenon_TZ_cm zenon_TY_bc zenon_TY_bt); trivial. % 244.33/244.62 (* end of lemma zenon_L9_ *) % 244.33/244.62 assert (zenon_L10_ : forall (zenon_TZ_cm : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TZ_bu : zenon_U) (zenon_TY_bc : zenon_U) (zenon_TY_cl : zenon_U), (~((i2003_11_14_17_19_35232) = zenon_TY_cl)) -> ((i2003_11_14_17_19_35232) = zenon_TY_bc) -> (forall Z : zenon_U, (((rf zenon_TZ_bu zenon_TY_bt)/\(rf zenon_TZ_bu Z))->(zenon_TY_bt = Z))) -> (rf zenon_TZ_bu zenon_TY_bt) -> (rf zenon_TZ_bu zenon_TY_bc) -> (rf zenon_TZ_cm zenon_TY_cl) -> (rf zenon_TZ_cm zenon_TY_bt) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_cm Y)/\(rf zenon_TZ_cm Z))->(Y = Z)))) -> False). % 244.33/244.62 do 5 intro. intros zenon_H50 zenon_H21 zenon_H51 zenon_H2b zenon_H2a zenon_H3c zenon_H3d zenon_H47. % 244.33/244.62 cut (((i2003_11_14_17_19_35232) = zenon_TY_bc) = ((i2003_11_14_17_19_35232) = zenon_TY_cl)). % 244.33/244.62 intro zenon_D_pnotp. % 244.33/244.62 apply zenon_H50. % 244.33/244.62 rewrite <- zenon_D_pnotp. % 244.33/244.62 exact zenon_H21. % 244.33/244.62 cut ((zenon_TY_bc = zenon_TY_cl)); [idtac | apply NNPP; zenon_intro zenon_H48]. % 244.33/244.62 cut (((i2003_11_14_17_19_35232) = (i2003_11_14_17_19_35232))); [idtac | apply NNPP; zenon_intro zenon_H3a]. % 244.33/244.62 congruence. % 244.33/244.62 apply zenon_H3a. apply refl_equal. % 244.33/244.62 generalize (zenon_H51 zenon_TY_bc). zenon_intro zenon_H4e. % 244.33/244.62 apply (zenon_L9_ zenon_TY_cl zenon_TZ_cm zenon_TY_bc zenon_TY_bt zenon_TZ_bu); trivial. % 244.33/244.62 (* end of lemma zenon_L10_ *) % 244.33/244.62 assert (zenon_L11_ : forall (zenon_TY_bc : zenon_U) (zenon_TZ_bu : zenon_U), (rf zenon_TZ_bu zenon_TY_bc) -> (~(rinvF zenon_TY_bc zenon_TZ_bu)) -> False). % 244.33/244.62 do 2 intro. intros zenon_H2a zenon_H52. % 244.33/244.62 generalize (axiom_5 zenon_TY_bc). zenon_intro zenon_H53. % 244.33/244.62 generalize (zenon_H53 zenon_TZ_bu). zenon_intro zenon_H54. % 244.33/244.62 apply (zenon_equiv_s _ _ zenon_H54); [ zenon_intro zenon_H52; zenon_intro zenon_H33 | zenon_intro zenon_H55; zenon_intro zenon_H2a ]. % 244.33/244.62 exact (zenon_H33 zenon_H2a). % 244.33/244.62 exact (zenon_H52 zenon_H55). % 244.33/244.62 (* end of lemma zenon_L11_ *) % 244.33/244.62 assert (zenon_L12_ : forall (zenon_TZ_bu : zenon_U) (zenon_TY_bc : zenon_U), (forall C : zenon_U, (((zenon_TY_bc = (i2003_11_14_17_19_35232))/\(rinvF zenon_TY_bc C))->(rinvF (i2003_11_14_17_19_35232) C))) -> ((i2003_11_14_17_19_35232) = zenon_TY_bc) -> (rf zenon_TZ_bu zenon_TY_bc) -> (~(rf zenon_TZ_bu (i2003_11_14_17_19_35232))) -> False). % 244.33/244.62 do 2 intro. intros zenon_H56 zenon_H21 zenon_H2a zenon_H57. % 244.33/244.62 generalize (zenon_H56 zenon_TZ_bu). zenon_intro zenon_H58. % 244.33/244.62 apply (zenon_imply_s _ _ zenon_H58); [ zenon_intro zenon_H5a | zenon_intro zenon_H59 ]. % 244.33/244.62 apply (zenon_notand_s _ _ zenon_H5a); [ zenon_intro zenon_H5b | zenon_intro zenon_H52 ]. % 244.33/244.62 apply zenon_H5b. apply sym_equal. exact zenon_H21. % 244.33/244.62 apply (zenon_L11_ zenon_TY_bc zenon_TZ_bu); trivial. % 244.33/244.62 generalize (axiom_5 (i2003_11_14_17_19_35232)). zenon_intro zenon_H5c. % 244.33/244.62 generalize (zenon_H5c zenon_TZ_bu). zenon_intro zenon_H5d. % 244.33/244.62 apply (zenon_equiv_s _ _ zenon_H5d); [ zenon_intro zenon_H5f; zenon_intro zenon_H57 | zenon_intro zenon_H59; zenon_intro zenon_H5e ]. % 244.33/244.62 exact (zenon_H5f zenon_H59). % 244.33/244.62 exact (zenon_H57 zenon_H5e). % 244.33/244.62 (* end of lemma zenon_L12_ *) % 244.33/244.62 assert (zenon_L13_ : forall (zenon_TY_bd : zenon_U), (rf zenon_TY_bd (i2003_11_14_17_19_35232)) -> (~(rinvF (i2003_11_14_17_19_35232) zenon_TY_bd)) -> False). % 244.33/244.62 do 1 intro. intros zenon_H19 zenon_H60. % 244.33/244.62 generalize (axiom_5 (i2003_11_14_17_19_35232)). zenon_intro zenon_H5c. % 244.33/244.62 generalize (zenon_H5c zenon_TY_bd). zenon_intro zenon_H61. % 244.33/244.62 apply (zenon_equiv_s _ _ zenon_H61); [ zenon_intro zenon_H60; zenon_intro zenon_H24 | zenon_intro zenon_H62; zenon_intro zenon_H19 ]. % 244.33/244.62 exact (zenon_H24 zenon_H19). % 244.33/244.62 exact (zenon_H60 zenon_H62). % 244.33/244.62 (* end of lemma zenon_L13_ *) % 244.33/244.62 assert (zenon_L14_ : forall (zenon_TY_bd : zenon_U) (zenon_TZ_cm : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TY_cl : zenon_U) (zenon_TY_bc : zenon_U), (forall C : zenon_U, (((zenon_TY_bc = zenon_TY_cl)/\(rf C zenon_TY_bc))->(rf C zenon_TY_cl))) -> (zenon_TY_bt = zenon_TY_bc) -> (rf zenon_TZ_cm zenon_TY_cl) -> (rf zenon_TZ_cm zenon_TY_bt) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_cm Y)/\(rf zenon_TZ_cm Z))->(Y = Z)))) -> (rf zenon_TY_bd zenon_TY_bc) -> (~(rf zenon_TY_bd zenon_TY_cl)) -> False). % 244.33/244.62 do 5 intro. intros zenon_H63 zenon_H46 zenon_H3c zenon_H3d zenon_H47 zenon_H1a zenon_H64. % 244.33/244.62 generalize (zenon_H63 zenon_TY_bd). zenon_intro zenon_H65. % 244.33/244.62 apply (zenon_imply_s _ _ zenon_H65); [ zenon_intro zenon_H67 | zenon_intro zenon_H66 ]. % 244.33/244.62 apply (zenon_notand_s _ _ zenon_H67); [ zenon_intro zenon_H48 | zenon_intro zenon_H23 ]. % 244.33/244.62 apply (zenon_L8_ zenon_TY_cl zenon_TZ_cm zenon_TY_bc zenon_TY_bt); trivial. % 244.33/244.62 exact (zenon_H23 zenon_H1a). % 244.33/244.62 exact (zenon_H64 zenon_H66). % 244.33/244.62 (* end of lemma zenon_L14_ *) % 244.33/244.62 assert (zenon_L15_ : forall (zenon_TY_bt : zenon_U) (zenon_TZ_cm : zenon_U) (zenon_TY_cl : zenon_U) (zenon_TY_bd : zenon_U) (zenon_TY_bc : zenon_U), (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_bc = B)/\(rf C zenon_TY_bc))->(rf C B)))) -> (~(rf zenon_TY_bd zenon_TY_cl)) -> (rf zenon_TY_bd zenon_TY_bc) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_cm Y)/\(rf zenon_TZ_cm Z))->(Y = Z)))) -> (rf zenon_TZ_cm zenon_TY_bt) -> (rf zenon_TZ_cm zenon_TY_cl) -> (zenon_TY_bt = zenon_TY_bc) -> False). % 244.33/244.62 do 5 intro. intros zenon_H68 zenon_H64 zenon_H1a zenon_H47 zenon_H3d zenon_H3c zenon_H46. % 244.33/244.62 generalize (zenon_H68 zenon_TY_cl). zenon_intro zenon_H63. % 244.33/244.62 apply (zenon_L14_ zenon_TY_bd zenon_TZ_cm zenon_TY_bt zenon_TY_cl zenon_TY_bc); trivial. % 244.33/244.62 (* end of lemma zenon_L15_ *) % 244.33/244.62 assert (zenon_L16_ : forall (zenon_TY_cl : zenon_U) (zenon_TZ_cm : zenon_U), (rf zenon_TZ_cm zenon_TY_cl) -> (~(rinvF zenon_TY_cl zenon_TZ_cm)) -> False). % 244.33/244.62 do 2 intro. intros zenon_H3c zenon_H69. % 244.33/244.62 generalize (axiom_5 zenon_TY_cl). zenon_intro zenon_H6a. % 244.33/244.62 generalize (zenon_H6a zenon_TZ_cm). zenon_intro zenon_H6b. % 244.33/244.62 apply (zenon_equiv_s _ _ zenon_H6b); [ zenon_intro zenon_H69; zenon_intro zenon_H45 | zenon_intro zenon_H6c; zenon_intro zenon_H3c ]. % 244.33/244.62 exact (zenon_H45 zenon_H3c). % 244.33/244.62 exact (zenon_H69 zenon_H6c). % 244.33/244.62 (* end of lemma zenon_L16_ *) % 244.33/244.62 assert (zenon_L17_ : forall (zenon_TY_cl : zenon_U) (zenon_TZ_eh : zenon_U), (rf zenon_TZ_eh zenon_TY_cl) -> (~(rinvF zenon_TY_cl zenon_TZ_eh)) -> False). % 244.33/244.62 do 2 intro. intros zenon_H6d zenon_H6e. % 244.33/244.62 generalize (axiom_5 zenon_TY_cl). zenon_intro zenon_H6a. % 244.33/244.62 generalize (zenon_H6a zenon_TZ_eh). zenon_intro zenon_H70. % 244.33/244.62 apply (zenon_equiv_s _ _ zenon_H70); [ zenon_intro zenon_H6e; zenon_intro zenon_H72 | zenon_intro zenon_H71; zenon_intro zenon_H6d ]. % 244.33/244.62 exact (zenon_H72 zenon_H6d). % 244.33/244.62 exact (zenon_H6e zenon_H71). % 244.33/244.62 (* end of lemma zenon_L17_ *) % 244.33/244.62 assert (zenon_L18_ : forall (zenon_TZ_cm : zenon_U), (rf zenon_TZ_cm (i2003_11_14_17_19_35232)) -> (~(rinvF (i2003_11_14_17_19_35232) zenon_TZ_cm)) -> False). % 244.33/244.62 do 1 intro. intros zenon_H73 zenon_H74. % 244.33/244.62 generalize (axiom_5 (i2003_11_14_17_19_35232)). zenon_intro zenon_H5c. % 244.33/244.62 generalize (zenon_H5c zenon_TZ_cm). zenon_intro zenon_H75. % 244.33/244.62 apply (zenon_equiv_s _ _ zenon_H75); [ zenon_intro zenon_H74; zenon_intro zenon_H77 | zenon_intro zenon_H76; zenon_intro zenon_H73 ]. % 244.33/244.62 exact (zenon_H77 zenon_H73). % 244.33/244.62 exact (zenon_H74 zenon_H76). % 244.33/244.62 (* end of lemma zenon_L18_ *) % 244.33/244.62 assert (zenon_L19_ : forall (zenon_TY_bt : zenon_U) (zenon_TZ_eh : zenon_U), (rf zenon_TZ_eh zenon_TY_bt) -> (~(rinvF zenon_TY_bt zenon_TZ_eh)) -> False). % 244.33/244.62 do 2 intro. intros zenon_H78 zenon_H79. % 244.33/244.62 generalize (axiom_5 zenon_TY_bt). zenon_intro zenon_H7a. % 244.33/244.62 generalize (zenon_H7a zenon_TZ_eh). zenon_intro zenon_H7b. % 244.33/244.62 apply (zenon_equiv_s _ _ zenon_H7b); [ zenon_intro zenon_H79; zenon_intro zenon_H7d | zenon_intro zenon_H7c; zenon_intro zenon_H78 ]. % 244.33/244.62 exact (zenon_H7d zenon_H78). % 244.33/244.62 exact (zenon_H79 zenon_H7c). % 244.33/244.62 (* end of lemma zenon_L19_ *) % 244.33/244.62 assert (zenon_L20_ : forall (zenon_TY_ey : zenon_U) (zenon_TZ_ez : zenon_U), (rf zenon_TZ_ez zenon_TY_ey) -> (~(rinvF zenon_TY_ey zenon_TZ_ez)) -> False). % 244.33/244.62 do 2 intro. intros zenon_H7e zenon_H7f. % 244.33/244.62 generalize (axiom_5 zenon_TY_ey). zenon_intro zenon_H82. % 244.33/244.62 generalize (zenon_H82 zenon_TZ_ez). zenon_intro zenon_H83. % 244.33/244.62 apply (zenon_equiv_s _ _ zenon_H83); [ zenon_intro zenon_H7f; zenon_intro zenon_H85 | zenon_intro zenon_H84; zenon_intro zenon_H7e ]. % 244.33/244.62 exact (zenon_H85 zenon_H7e). % 244.33/244.62 exact (zenon_H7f zenon_H84). % 244.33/244.62 (* end of lemma zenon_L20_ *) % 244.33/244.62 assert (zenon_L21_ : forall (zenon_TZ_ez : zenon_U) (zenon_TY_bc : zenon_U) (zenon_TY_ey : zenon_U), (forall C : zenon_U, (((zenon_TY_ey = zenon_TY_bc)/\(rinvF zenon_TY_ey C))->(rinvF zenon_TY_bc C))) -> (zenon_TY_ey = zenon_TY_bc) -> (rf zenon_TZ_ez zenon_TY_ey) -> (~(rf zenon_TZ_ez zenon_TY_bc)) -> False). % 244.33/244.62 do 3 intro. intros zenon_H86 zenon_H87 zenon_H7e zenon_H88. % 244.33/244.62 generalize (zenon_H86 zenon_TZ_ez). zenon_intro zenon_H89. % 244.33/244.62 apply (zenon_imply_s _ _ zenon_H89); [ zenon_intro zenon_H8b | zenon_intro zenon_H8a ]. % 244.33/244.62 apply (zenon_notand_s _ _ zenon_H8b); [ zenon_intro zenon_H8c | zenon_intro zenon_H7f ]. % 244.33/244.62 exact (zenon_H8c zenon_H87). % 244.33/244.62 apply (zenon_L20_ zenon_TY_ey zenon_TZ_ez); trivial. % 244.33/244.62 generalize (axiom_5 zenon_TY_bc). zenon_intro zenon_H53. % 244.33/244.62 generalize (zenon_H53 zenon_TZ_ez). zenon_intro zenon_H8d. % 244.33/244.62 apply (zenon_equiv_s _ _ zenon_H8d); [ zenon_intro zenon_H8f; zenon_intro zenon_H88 | zenon_intro zenon_H8a; zenon_intro zenon_H8e ]. % 244.33/244.62 exact (zenon_H8f zenon_H8a). % 244.33/244.62 exact (zenon_H88 zenon_H8e). % 244.33/244.62 (* end of lemma zenon_L21_ *) % 244.33/244.62 assert (zenon_L22_ : forall (zenon_TY_bt : zenon_U) (zenon_TZ_cm : zenon_U), (rf zenon_TZ_cm zenon_TY_bt) -> (~(rinvF zenon_TY_bt zenon_TZ_cm)) -> False). % 244.33/244.62 do 2 intro. intros zenon_H3d zenon_H90. % 244.33/244.62 generalize (axiom_5 zenon_TY_bt). zenon_intro zenon_H7a. % 244.33/244.62 generalize (zenon_H7a zenon_TZ_cm). zenon_intro zenon_H91. % 244.33/244.62 apply (zenon_equiv_s _ _ zenon_H91); [ zenon_intro zenon_H90; zenon_intro zenon_H44 | zenon_intro zenon_H92; zenon_intro zenon_H3d ]. % 244.33/244.62 exact (zenon_H44 zenon_H3d). % 244.33/244.62 exact (zenon_H90 zenon_H92). % 244.33/244.62 (* end of lemma zenon_L22_ *) % 244.33/244.62 assert (zenon_L23_ : forall (zenon_TY_bt : zenon_U) (zenon_TY_bd : zenon_U), (rf zenon_TY_bd zenon_TY_bt) -> (~(rinvF zenon_TY_bt zenon_TY_bd)) -> False). % 244.33/244.62 do 2 intro. intros zenon_H93 zenon_H94. % 244.33/244.62 generalize (axiom_5 zenon_TY_bt). zenon_intro zenon_H7a. % 244.33/244.62 generalize (zenon_H7a zenon_TY_bd). zenon_intro zenon_H95. % 244.33/244.62 apply (zenon_equiv_s _ _ zenon_H95); [ zenon_intro zenon_H94; zenon_intro zenon_H97 | zenon_intro zenon_H96; zenon_intro zenon_H93 ]. % 244.33/244.62 exact (zenon_H97 zenon_H93). % 244.33/244.62 exact (zenon_H94 zenon_H96). % 244.33/244.62 (* end of lemma zenon_L23_ *) % 244.33/244.62 assert (zenon_L24_ : forall (zenon_TZ_ez : zenon_U), (rinvF (i2003_11_14_17_19_35232) zenon_TZ_ez) -> (~(rf zenon_TZ_ez (i2003_11_14_17_19_35232))) -> False). % 244.33/244.62 do 1 intro. intros zenon_H98 zenon_H99. % 244.33/244.62 generalize (axiom_5 (i2003_11_14_17_19_35232)). zenon_intro zenon_H5c. % 244.33/244.62 generalize (zenon_H5c zenon_TZ_ez). zenon_intro zenon_H9a. % 244.33/244.62 apply (zenon_equiv_s _ _ zenon_H9a); [ zenon_intro zenon_H9c; zenon_intro zenon_H99 | zenon_intro zenon_H98; zenon_intro zenon_H9b ]. % 244.33/244.62 exact (zenon_H9c zenon_H98). % 244.33/244.62 exact (zenon_H99 zenon_H9b). % 244.33/244.62 (* end of lemma zenon_L24_ *) % 244.33/244.62 assert (zenon_L25_ : forall (zenon_TZ_ez : zenon_U) (zenon_TY_ey : zenon_U), (forall C : zenon_U, (((zenon_TY_ey = (i2003_11_14_17_19_35232))/\(rinvF zenon_TY_ey C))->(rinvF (i2003_11_14_17_19_35232) C))) -> (zenon_TY_ey = (i2003_11_14_17_19_35232)) -> (rf zenon_TZ_ez zenon_TY_ey) -> (~(rf zenon_TZ_ez (i2003_11_14_17_19_35232))) -> False). % 244.33/244.62 do 2 intro. intros zenon_H9d zenon_H9e zenon_H7e zenon_H99. % 244.33/244.62 generalize (zenon_H9d zenon_TZ_ez). zenon_intro zenon_H9f. % 244.33/244.62 apply (zenon_imply_s _ _ zenon_H9f); [ zenon_intro zenon_Ha0 | zenon_intro zenon_H98 ]. % 244.33/244.62 apply (zenon_notand_s _ _ zenon_Ha0); [ zenon_intro zenon_Ha1 | zenon_intro zenon_H7f ]. % 244.33/244.62 exact (zenon_Ha1 zenon_H9e). % 244.33/244.62 apply (zenon_L20_ zenon_TY_ey zenon_TZ_ez); trivial. % 244.33/244.62 apply (zenon_L24_ zenon_TZ_ez); trivial. % 244.33/244.62 (* end of lemma zenon_L25_ *) % 244.33/244.62 assert (zenon_L26_ : forall (zenon_TY_ey : zenon_U) (zenon_TY_gj : zenon_U) (zenon_TZ_ez : zenon_U), (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_ez Y)/\(rf zenon_TZ_ez Z))->(Y = Z)))) -> (~((i2003_11_14_17_19_35232) = zenon_TY_gj)) -> (rf zenon_TZ_ez zenon_TY_ey) -> (zenon_TY_ey = (i2003_11_14_17_19_35232)) -> (forall C : zenon_U, (((zenon_TY_ey = (i2003_11_14_17_19_35232))/\(rinvF zenon_TY_ey C))->(rinvF (i2003_11_14_17_19_35232) C))) -> (rf zenon_TZ_ez zenon_TY_gj) -> False). % 244.33/244.62 do 3 intro. intros zenon_Ha2 zenon_Ha3 zenon_H7e zenon_H9e zenon_H9d zenon_Ha4. % 244.33/244.62 generalize (zenon_Ha2 zenon_TY_gj). zenon_intro zenon_Ha6. % 244.33/244.62 generalize (zenon_Ha6 (i2003_11_14_17_19_35232)). zenon_intro zenon_Ha7. % 244.33/244.62 apply (zenon_imply_s _ _ zenon_Ha7); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Ha8 ]. % 244.33/244.62 apply (zenon_notand_s _ _ zenon_Ha9); [ zenon_intro zenon_Haa | zenon_intro zenon_H99 ]. % 244.33/244.62 exact (zenon_Haa zenon_Ha4). % 244.33/244.62 apply (zenon_L25_ zenon_TZ_ez zenon_TY_ey); trivial. % 244.33/244.62 apply zenon_Ha3. apply sym_equal. exact zenon_Ha8. % 244.33/244.62 (* end of lemma zenon_L26_ *) % 244.33/244.62 assert (zenon_L27_ : forall (zenon_TY_ey : zenon_U) (zenon_TY_gj : zenon_U) (zenon_TZ_ez : zenon_U), (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_ez Y)/\(rf zenon_TZ_ez Z))->(Y = Z)))) -> (~(zenon_TY_gj = (i2003_11_14_17_19_35232))) -> (rf zenon_TZ_ez zenon_TY_ey) -> (zenon_TY_ey = (i2003_11_14_17_19_35232)) -> (forall C : zenon_U, (((zenon_TY_ey = (i2003_11_14_17_19_35232))/\(rinvF zenon_TY_ey C))->(rinvF (i2003_11_14_17_19_35232) C))) -> (rf zenon_TZ_ez zenon_TY_gj) -> False). % 244.33/244.62 do 3 intro. intros zenon_Ha2 zenon_Hab zenon_H7e zenon_H9e zenon_H9d zenon_Ha4. % 244.33/244.62 generalize (zenon_Ha2 zenon_TY_gj). zenon_intro zenon_Ha6. % 244.33/244.62 generalize (zenon_Ha6 (i2003_11_14_17_19_35232)). zenon_intro zenon_Ha7. % 244.33/244.62 apply (zenon_imply_s _ _ zenon_Ha7); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Ha8 ]. % 244.33/244.62 apply (zenon_notand_s _ _ zenon_Ha9); [ zenon_intro zenon_Haa | zenon_intro zenon_H99 ]. % 244.33/244.62 exact (zenon_Haa zenon_Ha4). % 244.33/244.62 apply (zenon_L25_ zenon_TZ_ez zenon_TY_ey); trivial. % 244.33/244.62 exact (zenon_Hab zenon_Ha8). % 244.33/244.62 (* end of lemma zenon_L27_ *) % 244.33/244.62 assert (zenon_L28_ : forall (zenon_TY_ey : zenon_U) (zenon_TY_gj : zenon_U) (zenon_TZ_ez : zenon_U) (zenon_TY_cl : zenon_U), ((i2003_11_14_17_19_35232) = zenon_TY_cl) -> (rf zenon_TZ_ez zenon_TY_gj) -> (forall C : zenon_U, (((zenon_TY_ey = (i2003_11_14_17_19_35232))/\(rinvF zenon_TY_ey C))->(rinvF (i2003_11_14_17_19_35232) C))) -> (zenon_TY_ey = (i2003_11_14_17_19_35232)) -> (rf zenon_TZ_ez zenon_TY_ey) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_ez Y)/\(rf zenon_TZ_ez Z))->(Y = Z)))) -> (~(zenon_TY_cl = zenon_TY_gj)) -> False). % 244.33/244.62 do 4 intro. intros zenon_Hac zenon_Ha4 zenon_H9d zenon_H9e zenon_H7e zenon_Ha2 zenon_Had. % 244.33/244.62 elim (classic (zenon_TY_gj = zenon_TY_gj)); [ zenon_intro zenon_Hae | zenon_intro zenon_Haf ]. % 244.33/244.62 cut ((zenon_TY_gj = zenon_TY_gj) = (zenon_TY_cl = zenon_TY_gj)). % 244.33/244.62 intro zenon_D_pnotp. % 244.33/244.62 apply zenon_Had. % 244.33/244.62 rewrite <- zenon_D_pnotp. % 244.33/244.62 exact zenon_Hae. % 244.33/244.62 cut ((zenon_TY_gj = zenon_TY_gj)); [idtac | apply NNPP; zenon_intro zenon_Haf]. % 244.33/244.62 cut ((zenon_TY_gj = zenon_TY_cl)); [idtac | apply NNPP; zenon_intro zenon_Hb0]. % 244.33/244.63 congruence. % 244.33/244.63 cut (((i2003_11_14_17_19_35232) = zenon_TY_cl) = (zenon_TY_gj = zenon_TY_cl)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_Hb0. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_Hac. % 244.33/244.63 cut ((zenon_TY_cl = zenon_TY_cl)); [idtac | apply NNPP; zenon_intro zenon_H4a]. % 244.33/244.63 cut (((i2003_11_14_17_19_35232) = zenon_TY_gj)); [idtac | apply NNPP; zenon_intro zenon_Ha3]. % 244.33/244.63 congruence. % 244.33/244.63 elim (classic (zenon_TY_gj = zenon_TY_gj)); [ zenon_intro zenon_Hae | zenon_intro zenon_Haf ]. % 244.33/244.63 cut ((zenon_TY_gj = zenon_TY_gj) = ((i2003_11_14_17_19_35232) = zenon_TY_gj)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_Ha3. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_Hae. % 244.33/244.63 cut ((zenon_TY_gj = zenon_TY_gj)); [idtac | apply NNPP; zenon_intro zenon_Haf]. % 244.33/244.63 cut ((zenon_TY_gj = (i2003_11_14_17_19_35232))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 244.33/244.63 congruence. % 244.33/244.63 apply (zenon_L27_ zenon_TY_ey zenon_TY_gj zenon_TZ_ez); trivial. % 244.33/244.63 apply zenon_Haf. apply refl_equal. % 244.33/244.63 apply zenon_Haf. apply refl_equal. % 244.33/244.63 apply zenon_H4a. apply refl_equal. % 244.33/244.63 apply zenon_Haf. apply refl_equal. % 244.33/244.63 apply zenon_Haf. apply refl_equal. % 244.33/244.63 (* end of lemma zenon_L28_ *) % 244.33/244.63 assert (zenon_L29_ : forall (zenon_TZ_eh : zenon_U) (zenon_TY_ey : zenon_U) (zenon_TZ_ez : zenon_U) (zenon_TY_gj : zenon_U) (zenon_TY_cl : zenon_U), (forall C : zenon_U, (((zenon_TY_cl = zenon_TY_gj)/\(rf C zenon_TY_cl))->(rf C zenon_TY_gj))) -> ((i2003_11_14_17_19_35232) = zenon_TY_cl) -> (rf zenon_TZ_ez zenon_TY_gj) -> (forall C : zenon_U, (((zenon_TY_ey = (i2003_11_14_17_19_35232))/\(rinvF zenon_TY_ey C))->(rinvF (i2003_11_14_17_19_35232) C))) -> (zenon_TY_ey = (i2003_11_14_17_19_35232)) -> (rf zenon_TZ_ez zenon_TY_ey) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_ez Y)/\(rf zenon_TZ_ez Z))->(Y = Z)))) -> (rf zenon_TZ_eh zenon_TY_cl) -> (~(rf zenon_TZ_eh zenon_TY_gj)) -> False). % 244.33/244.63 do 5 intro. intros zenon_Hb1 zenon_Hac zenon_Ha4 zenon_H9d zenon_H9e zenon_H7e zenon_Ha2 zenon_H6d zenon_Hb2. % 244.33/244.63 generalize (zenon_Hb1 zenon_TZ_eh). zenon_intro zenon_Hb3. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_Hb3); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hb4 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_Hb5); [ zenon_intro zenon_Had | zenon_intro zenon_H72 ]. % 244.33/244.63 apply (zenon_L28_ zenon_TY_ey zenon_TY_gj zenon_TZ_ez zenon_TY_cl); trivial. % 244.33/244.63 exact (zenon_H72 zenon_H6d). % 244.33/244.63 exact (zenon_Hb2 zenon_Hb4). % 244.33/244.63 (* end of lemma zenon_L29_ *) % 244.33/244.63 assert (zenon_L30_ : forall (zenon_TY_gj : zenon_U) (zenon_TZ_hc : zenon_U), (rf zenon_TZ_hc zenon_TY_gj) -> (~(rinvF zenon_TY_gj zenon_TZ_hc)) -> False). % 244.33/244.63 do 2 intro. intros zenon_Hb6 zenon_Hb7. % 244.33/244.63 generalize (axiom_5 zenon_TY_gj). zenon_intro zenon_Hb9. % 244.33/244.63 generalize (zenon_Hb9 zenon_TZ_hc). zenon_intro zenon_Hba. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_Hba); [ zenon_intro zenon_Hb7; zenon_intro zenon_Hbc | zenon_intro zenon_Hbb; zenon_intro zenon_Hb6 ]. % 244.33/244.63 exact (zenon_Hbc zenon_Hb6). % 244.33/244.63 exact (zenon_Hb7 zenon_Hbb). % 244.33/244.63 (* end of lemma zenon_L30_ *) % 244.33/244.63 assert (zenon_L31_ : forall (zenon_TY_bc : zenon_U) (zenon_TY_hk : zenon_U) (zenon_TZ_hc : zenon_U), (rf zenon_TZ_hc zenon_TY_hk) -> (rf zenon_TZ_hc zenon_TY_bc) -> (~(zenon_TY_hk = zenon_TY_bc)) -> False). % 244.33/244.63 do 3 intro. intros zenon_Hbd zenon_Hbe zenon_Hbf. % 244.33/244.63 generalize (axiom_4 zenon_TZ_hc). zenon_intro zenon_Hc1. % 244.33/244.63 generalize (zenon_Hc1 zenon_TY_hk). zenon_intro zenon_Hc2. % 244.33/244.63 generalize (zenon_Hc2 zenon_TY_bc). zenon_intro zenon_Hc3. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_Hc3); [ zenon_intro zenon_Hc5 | zenon_intro zenon_Hc4 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_Hc5); [ zenon_intro zenon_Hc7 | zenon_intro zenon_Hc6 ]. % 244.33/244.63 exact (zenon_Hc7 zenon_Hbd). % 244.33/244.63 exact (zenon_Hc6 zenon_Hbe). % 244.33/244.63 exact (zenon_Hbf zenon_Hc4). % 244.33/244.63 (* end of lemma zenon_L31_ *) % 244.33/244.63 assert (zenon_L32_ : forall (zenon_TY_hk : zenon_U) (zenon_TZ_hc : zenon_U) (zenon_TY_gj : zenon_U) (zenon_TY_bc : zenon_U), (zenon_TY_bc = zenon_TY_gj) -> (rf zenon_TZ_hc zenon_TY_gj) -> (~(zenon_TY_hk = zenon_TY_bc)) -> (rf zenon_TZ_hc zenon_TY_hk) -> False). % 244.33/244.63 do 4 intro. intros zenon_Hc8 zenon_Hb6 zenon_Hbf zenon_Hbd. % 244.33/244.63 generalize (rinvF_substitution_1 zenon_TY_gj). zenon_intro zenon_Hc9. % 244.33/244.63 generalize (zenon_Hc9 zenon_TY_bc). zenon_intro zenon_Hca. % 244.33/244.63 generalize (zenon_Hca zenon_TZ_hc). zenon_intro zenon_Hcb. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_Hcb); [ zenon_intro zenon_Hcd | zenon_intro zenon_Hcc ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_Hcd); [ zenon_intro zenon_Hce | zenon_intro zenon_Hb7 ]. % 244.33/244.63 apply zenon_Hce. apply sym_equal. exact zenon_Hc8. % 244.33/244.63 apply (zenon_L30_ zenon_TY_gj zenon_TZ_hc); trivial. % 244.33/244.63 generalize (axiom_5 zenon_TY_bc). zenon_intro zenon_H53. % 244.33/244.63 generalize (zenon_H53 zenon_TZ_hc). zenon_intro zenon_Hcf. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_Hcf); [ zenon_intro zenon_Hd0; zenon_intro zenon_Hc6 | zenon_intro zenon_Hcc; zenon_intro zenon_Hbe ]. % 244.33/244.63 exact (zenon_Hd0 zenon_Hcc). % 244.33/244.63 apply (zenon_L31_ zenon_TY_bc zenon_TY_hk zenon_TZ_hc); trivial. % 244.33/244.63 (* end of lemma zenon_L32_ *) % 244.33/244.63 assert (zenon_L33_ : forall (zenon_TY_hk : zenon_U) (zenon_TZ_hc : zenon_U) (zenon_TY_gj : zenon_U) (zenon_TY_ey : zenon_U) (zenon_TY_bc : zenon_U) (zenon_TZ_ez : zenon_U), (forall Z : zenon_U, (((rf zenon_TZ_ez zenon_TY_bc)/\(rf zenon_TZ_ez Z))->(zenon_TY_bc = Z))) -> (forall C : zenon_U, (((zenon_TY_ey = zenon_TY_bc)/\(rinvF zenon_TY_ey C))->(rinvF zenon_TY_bc C))) -> (zenon_TY_ey = zenon_TY_bc) -> (rf zenon_TZ_ez zenon_TY_ey) -> (rf zenon_TZ_ez zenon_TY_gj) -> (rf zenon_TZ_hc zenon_TY_gj) -> (~(zenon_TY_hk = zenon_TY_bc)) -> (rf zenon_TZ_hc zenon_TY_hk) -> False). % 244.33/244.63 do 6 intro. intros zenon_Hd1 zenon_H86 zenon_H87 zenon_H7e zenon_Ha4 zenon_Hb6 zenon_Hbf zenon_Hbd. % 244.33/244.63 generalize (zenon_Hd1 zenon_TY_gj). zenon_intro zenon_Hd2. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_Hd2); [ zenon_intro zenon_Hd3 | zenon_intro zenon_Hc8 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_Hd3); [ zenon_intro zenon_H88 | zenon_intro zenon_Haa ]. % 244.33/244.63 apply (zenon_L21_ zenon_TZ_ez zenon_TY_bc zenon_TY_ey); trivial. % 244.33/244.63 exact (zenon_Haa zenon_Ha4). % 244.33/244.63 apply (zenon_L32_ zenon_TY_hk zenon_TZ_hc zenon_TY_gj zenon_TY_bc); trivial. % 244.33/244.63 (* end of lemma zenon_L33_ *) % 244.33/244.63 assert (zenon_L34_ : forall (zenon_TY_ey : zenon_U) (zenon_TZ_ez : zenon_U) (zenon_TY_hk : zenon_U) (zenon_TZ_hc : zenon_U) (zenon_TY_gj : zenon_U) (zenon_TY_bc : zenon_U), (zenon_TY_bc = zenon_TY_gj) -> (rf zenon_TZ_hc zenon_TY_hk) -> (rf zenon_TZ_hc zenon_TY_gj) -> (rf zenon_TZ_ez zenon_TY_gj) -> (rf zenon_TZ_ez zenon_TY_ey) -> (zenon_TY_ey = zenon_TY_bc) -> (forall C : zenon_U, (((zenon_TY_ey = zenon_TY_bc)/\(rinvF zenon_TY_ey C))->(rinvF zenon_TY_bc C))) -> (forall Z : zenon_U, (((rf zenon_TZ_ez zenon_TY_bc)/\(rf zenon_TZ_ez Z))->(zenon_TY_bc = Z))) -> (~(zenon_TY_gj = zenon_TY_hk)) -> False). % 244.33/244.63 do 6 intro. intros zenon_Hc8 zenon_Hbd zenon_Hb6 zenon_Ha4 zenon_H7e zenon_H87 zenon_H86 zenon_Hd1 zenon_Hd4. % 244.33/244.63 elim (classic (zenon_TY_hk = zenon_TY_hk)); [ zenon_intro zenon_Hd5 | zenon_intro zenon_Hd6 ]. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_hk) = (zenon_TY_gj = zenon_TY_hk)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_Hd4. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_Hd5. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_hk)); [idtac | apply NNPP; zenon_intro zenon_Hd6]. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_gj)); [idtac | apply NNPP; zenon_intro zenon_Hd7]. % 244.33/244.63 congruence. % 244.33/244.63 cut ((zenon_TY_bc = zenon_TY_gj) = (zenon_TY_hk = zenon_TY_gj)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_Hd7. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_Hc8. % 244.33/244.63 cut ((zenon_TY_gj = zenon_TY_gj)); [idtac | apply NNPP; zenon_intro zenon_Haf]. % 244.33/244.63 cut ((zenon_TY_bc = zenon_TY_hk)); [idtac | apply NNPP; zenon_intro zenon_Hd8]. % 244.33/244.63 congruence. % 244.33/244.63 elim (classic (zenon_TY_hk = zenon_TY_hk)); [ zenon_intro zenon_Hd5 | zenon_intro zenon_Hd6 ]. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_hk) = (zenon_TY_bc = zenon_TY_hk)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_Hd8. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_Hd5. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_hk)); [idtac | apply NNPP; zenon_intro zenon_Hd6]. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_bc)); [idtac | apply NNPP; zenon_intro zenon_Hbf]. % 244.33/244.63 congruence. % 244.33/244.63 apply (zenon_L33_ zenon_TY_hk zenon_TZ_hc zenon_TY_gj zenon_TY_ey zenon_TY_bc zenon_TZ_ez); trivial. % 244.33/244.63 apply zenon_Hd6. apply refl_equal. % 244.33/244.63 apply zenon_Hd6. apply refl_equal. % 244.33/244.63 apply zenon_Haf. apply refl_equal. % 244.33/244.63 apply zenon_Hd6. apply refl_equal. % 244.33/244.63 apply zenon_Hd6. apply refl_equal. % 244.33/244.63 (* end of lemma zenon_L34_ *) % 244.33/244.63 assert (zenon_L35_ : forall (zenon_TY_hk : zenon_U) (zenon_TZ_il : zenon_U), (rf zenon_TZ_il zenon_TY_hk) -> (~(rinvF zenon_TY_hk zenon_TZ_il)) -> False). % 244.33/244.63 do 2 intro. intros zenon_Hd9 zenon_Hda. % 244.33/244.63 generalize (axiom_5 zenon_TY_hk). zenon_intro zenon_Hdc. % 244.33/244.63 generalize (zenon_Hdc zenon_TZ_il). zenon_intro zenon_Hdd. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_Hdd); [ zenon_intro zenon_Hda; zenon_intro zenon_Hdf | zenon_intro zenon_Hde; zenon_intro zenon_Hd9 ]. % 244.33/244.63 exact (zenon_Hdf zenon_Hd9). % 244.33/244.63 exact (zenon_Hda zenon_Hde). % 244.33/244.63 (* end of lemma zenon_L35_ *) % 244.33/244.63 assert (zenon_L36_ : forall (zenon_TY_hk : zenon_U) (zenon_TY_is : zenon_U) (zenon_TZ_il : zenon_U) (zenon_TY_gj : zenon_U) (zenon_TY_bc : zenon_U), (zenon_TY_bc = zenon_TY_gj) -> (rf zenon_TZ_il zenon_TY_is) -> (rf zenon_TZ_il zenon_TY_hk) -> (zenon_TY_hk = zenon_TY_bc) -> (~(zenon_TY_gj = zenon_TY_is)) -> False). % 244.33/244.63 do 5 intro. intros zenon_Hc8 zenon_He0 zenon_Hd9 zenon_Hc4 zenon_He1. % 244.33/244.63 elim (classic (zenon_TY_is = zenon_TY_is)); [ zenon_intro zenon_He3 | zenon_intro zenon_He4 ]. % 244.33/244.63 cut ((zenon_TY_is = zenon_TY_is) = (zenon_TY_gj = zenon_TY_is)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_He1. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_He3. % 244.33/244.63 cut ((zenon_TY_is = zenon_TY_is)); [idtac | apply NNPP; zenon_intro zenon_He4]. % 244.33/244.63 cut ((zenon_TY_is = zenon_TY_gj)); [idtac | apply NNPP; zenon_intro zenon_He5]. % 244.33/244.63 congruence. % 244.33/244.63 cut ((zenon_TY_bc = zenon_TY_gj) = (zenon_TY_is = zenon_TY_gj)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_He5. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_Hc8. % 244.33/244.63 cut ((zenon_TY_gj = zenon_TY_gj)); [idtac | apply NNPP; zenon_intro zenon_Haf]. % 244.33/244.63 cut ((zenon_TY_bc = zenon_TY_is)); [idtac | apply NNPP; zenon_intro zenon_He6]. % 244.33/244.63 congruence. % 244.33/244.63 elim (classic (zenon_TY_is = zenon_TY_is)); [ zenon_intro zenon_He3 | zenon_intro zenon_He4 ]. % 244.33/244.63 cut ((zenon_TY_is = zenon_TY_is) = (zenon_TY_bc = zenon_TY_is)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_He6. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_He3. % 244.33/244.63 cut ((zenon_TY_is = zenon_TY_is)); [idtac | apply NNPP; zenon_intro zenon_He4]. % 244.33/244.63 cut ((zenon_TY_is = zenon_TY_bc)); [idtac | apply NNPP; zenon_intro zenon_He7]. % 244.33/244.63 congruence. % 244.33/244.63 generalize (rinvF_substitution_1 zenon_TY_hk). zenon_intro zenon_He8. % 244.33/244.63 generalize (zenon_He8 zenon_TY_bc). zenon_intro zenon_He9. % 244.33/244.63 generalize (axiom_4 zenon_TZ_il). zenon_intro zenon_Hea. % 244.33/244.63 generalize (zenon_Hea zenon_TY_bc). zenon_intro zenon_Heb. % 244.33/244.63 generalize (zenon_He9 zenon_TZ_il). zenon_intro zenon_Hec. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_Hec); [ zenon_intro zenon_Hee | zenon_intro zenon_Hed ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_Hee); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hda ]. % 244.33/244.63 exact (zenon_Hbf zenon_Hc4). % 244.33/244.63 apply (zenon_L35_ zenon_TY_hk zenon_TZ_il); trivial. % 244.33/244.63 generalize (axiom_5 zenon_TY_bc). zenon_intro zenon_H53. % 244.33/244.63 generalize (zenon_H53 zenon_TZ_il). zenon_intro zenon_Hef. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_Hef); [ zenon_intro zenon_Hf2; zenon_intro zenon_Hf1 | zenon_intro zenon_Hed; zenon_intro zenon_Hf0 ]. % 244.33/244.63 exact (zenon_Hf2 zenon_Hed). % 244.33/244.63 generalize (zenon_Heb zenon_TY_is). zenon_intro zenon_Hf3. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_Hf3); [ zenon_intro zenon_Hf5 | zenon_intro zenon_Hf4 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_Hf5); [ zenon_intro zenon_Hf1 | zenon_intro zenon_Hf6 ]. % 244.33/244.63 exact (zenon_Hf1 zenon_Hf0). % 244.33/244.63 exact (zenon_Hf6 zenon_He0). % 244.33/244.63 apply zenon_He7. apply sym_equal. exact zenon_Hf4. % 244.33/244.63 apply zenon_He4. apply refl_equal. % 244.33/244.63 apply zenon_He4. apply refl_equal. % 244.33/244.63 apply zenon_Haf. apply refl_equal. % 244.33/244.63 apply zenon_He4. apply refl_equal. % 244.33/244.63 apply zenon_He4. apply refl_equal. % 244.33/244.63 (* end of lemma zenon_L36_ *) % 244.33/244.63 assert (zenon_L37_ : forall (zenon_TY_hk : zenon_U) (zenon_TZ_il : zenon_U) (zenon_TY_bc : zenon_U) (zenon_TY_gj : zenon_U) (zenon_TY_is : zenon_U) (zenon_TY_bt : zenon_U), (~(zenon_TY_bt = zenon_TY_is)) -> (zenon_TY_bt = zenon_TY_gj) -> (zenon_TY_bc = zenon_TY_gj) -> (rf zenon_TZ_il zenon_TY_is) -> (rf zenon_TZ_il zenon_TY_hk) -> (zenon_TY_hk = zenon_TY_bc) -> False). % 244.33/244.63 do 6 intro. intros zenon_Hf7 zenon_Hf8 zenon_Hc8 zenon_He0 zenon_Hd9 zenon_Hc4. % 244.33/244.63 cut ((zenon_TY_bt = zenon_TY_gj) = (zenon_TY_bt = zenon_TY_is)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_Hf7. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_Hf8. % 244.33/244.63 cut ((zenon_TY_gj = zenon_TY_is)); [idtac | apply NNPP; zenon_intro zenon_He1]. % 244.33/244.63 cut ((zenon_TY_bt = zenon_TY_bt)); [idtac | apply NNPP; zenon_intro zenon_Hf9]. % 244.33/244.63 congruence. % 244.33/244.63 apply zenon_Hf9. apply refl_equal. % 244.33/244.63 apply (zenon_L36_ zenon_TY_hk zenon_TY_is zenon_TZ_il zenon_TY_gj zenon_TY_bc); trivial. % 244.33/244.63 (* end of lemma zenon_L37_ *) % 244.33/244.63 assert (zenon_L38_ : forall (zenon_TY_bc : zenon_U) (zenon_TZ_cm : zenon_U), (rf zenon_TZ_cm zenon_TY_bc) -> (~(rinvR zenon_TY_bc zenon_TZ_cm)) -> False). % 244.33/244.63 do 2 intro. intros zenon_Hfa zenon_Hfb. % 244.33/244.63 generalize (axiom_6 zenon_TY_bc). zenon_intro zenon_Hfc. % 244.33/244.63 generalize (zenon_Hfc zenon_TZ_cm). zenon_intro zenon_Hfd. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_Hfd); [ zenon_intro zenon_Hfb; zenon_intro zenon_H100 | zenon_intro zenon_Hff; zenon_intro zenon_Hfe ]. % 244.33/244.63 generalize (axiom_9 zenon_TZ_cm). zenon_intro zenon_H101. % 244.33/244.63 generalize (zenon_H101 zenon_TY_bc). zenon_intro zenon_H102. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H102); [ zenon_intro zenon_H103 | zenon_intro zenon_Hfe ]. % 244.33/244.63 exact (zenon_H103 zenon_Hfa). % 244.33/244.63 exact (zenon_H100 zenon_Hfe). % 244.33/244.63 exact (zenon_Hfb zenon_Hff). % 244.33/244.63 (* end of lemma zenon_L38_ *) % 244.33/244.63 assert (zenon_L39_ : forall (zenon_TZ_cm : zenon_U), (exists Y : zenon_U, ((rinvF zenon_TZ_cm Y)/\(cd Y))) -> (forall B : zenon_U, (((zenon_TZ_cm = B)/\(cc zenon_TZ_cm))->(cc B))) -> (cc zenon_TZ_cm) -> False). % 244.33/244.63 do 1 intro. intros zenon_H104 zenon_H105 zenon_H106. % 244.33/244.63 elim zenon_H104. zenon_intro zenon_TY_kd. zenon_intro zenon_H108. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H108). zenon_intro zenon_H10a. zenon_intro zenon_H109. % 244.33/244.63 generalize (axiom_5 zenon_TZ_cm). zenon_intro zenon_H10b. % 244.33/244.63 generalize (zenon_H10b zenon_TY_kd). zenon_intro zenon_H10c. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H10c); [ zenon_intro zenon_H10f; zenon_intro zenon_H10e | zenon_intro zenon_H10a; zenon_intro zenon_H10d ]. % 244.33/244.63 exact (zenon_H10f zenon_H10a). % 244.33/244.63 generalize (axiom_3 zenon_TY_kd). zenon_intro zenon_H110. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H110); [ zenon_intro zenon_H113; zenon_intro zenon_H112 | zenon_intro zenon_H109; zenon_intro zenon_H111 ]. % 244.33/244.63 exact (zenon_H113 zenon_H109). % 244.33/244.63 apply (zenon_and_s _ _ zenon_H111). zenon_intro zenon_H115. zenon_intro zenon_H114. % 244.33/244.63 elim zenon_H115. zenon_intro zenon_TY_ks. zenon_intro zenon_H117. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H117). zenon_intro zenon_H119. zenon_intro zenon_H118. % 244.33/244.63 generalize (axiom_4 zenon_TY_kd). zenon_intro zenon_H11a. % 244.33/244.63 generalize (zenon_H105 zenon_TY_ks). zenon_intro zenon_H11b. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H11b); [ zenon_intro zenon_H11d | zenon_intro zenon_H11c ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H11d); [ zenon_intro zenon_H11f | zenon_intro zenon_H11e ]. % 244.33/244.63 generalize (zenon_H11a zenon_TY_ks). zenon_intro zenon_H120. % 244.33/244.63 generalize (zenon_H120 zenon_TZ_cm). zenon_intro zenon_H121. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H121); [ zenon_intro zenon_H123 | zenon_intro zenon_H122 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H123); [ zenon_intro zenon_H124 | zenon_intro zenon_H10e ]. % 244.33/244.63 exact (zenon_H124 zenon_H119). % 244.33/244.63 exact (zenon_H10e zenon_H10d). % 244.33/244.63 apply zenon_H11f. apply sym_equal. exact zenon_H122. % 244.33/244.63 exact (zenon_H11e zenon_H106). % 244.33/244.63 exact (zenon_H118 zenon_H11c). % 244.33/244.63 (* end of lemma zenon_L39_ *) % 244.33/244.63 assert (zenon_L40_ : forall (zenon_TZ_cm : zenon_U) (zenon_TY_bt : zenon_U), (rinvR zenon_TY_bt zenon_TZ_cm) -> (forall Y : zenon_U, ((rinvR zenon_TY_bt Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z))))) -> (forall B : zenon_U, (((zenon_TZ_cm = B)/\(cc zenon_TZ_cm))->(cc B))) -> (cc zenon_TZ_cm) -> False). % 244.33/244.63 do 2 intro. intros zenon_H125 zenon_H126 zenon_H105 zenon_H106. % 244.33/244.63 generalize (axiom_6 zenon_TY_bt). zenon_intro zenon_H127. % 244.33/244.63 generalize (zenon_H127 zenon_TZ_cm). zenon_intro zenon_H128. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H128); [ zenon_intro zenon_H12b; zenon_intro zenon_H12a | zenon_intro zenon_H125; zenon_intro zenon_H129 ]. % 244.33/244.63 exact (zenon_H12b zenon_H125). % 244.33/244.63 generalize (zenon_H126 zenon_TZ_cm). zenon_intro zenon_H12c. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H12c); [ zenon_intro zenon_H12b | zenon_intro zenon_H104 ]. % 244.33/244.63 generalize (axiom_6 zenon_TY_bt). zenon_intro zenon_H127. % 244.33/244.63 generalize (zenon_H127 zenon_TZ_cm). zenon_intro zenon_H128. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H128); [ zenon_intro zenon_H12b; zenon_intro zenon_H12a | zenon_intro zenon_H125; zenon_intro zenon_H129 ]. % 244.33/244.63 exact (zenon_H12a zenon_H129). % 244.33/244.63 exact (zenon_H12b zenon_H125). % 244.33/244.63 apply (zenon_L39_ zenon_TZ_cm); trivial. % 244.33/244.63 (* end of lemma zenon_L40_ *) % 244.33/244.63 assert (zenon_L41_ : forall (zenon_TY_bd : zenon_U) (zenon_TZ_eh : zenon_U) (zenon_TZ_cm : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TY_gj : zenon_U) (zenon_TY_ey : zenon_U) (zenon_TY_bc : zenon_U) (zenon_TZ_ez : zenon_U) (zenon_TY_hk : zenon_U), (exists Z : zenon_U, ((rinvF zenon_TY_hk Z)/\(cd Z))) -> (forall Z : zenon_U, (((rf zenon_TZ_ez zenon_TY_bc)/\(rf zenon_TZ_ez Z))->(zenon_TY_bc = Z))) -> (forall C : zenon_U, (((zenon_TY_ey = zenon_TY_bc)/\(rinvF zenon_TY_ey C))->(rinvF zenon_TY_bc C))) -> (zenon_TY_ey = zenon_TY_bc) -> (rf zenon_TZ_ez zenon_TY_gj) -> (forall Z : zenon_U, (((rf zenon_TZ_ez zenon_TY_bt)/\(rf zenon_TZ_ez Z))->(zenon_TY_bt = Z))) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_cm Y)/\(rf zenon_TZ_cm Z))->(Y = Z)))) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_bt = B)/\(rinvF zenon_TY_bt C))->(rinvF B C)))) -> (rf zenon_TZ_eh zenon_TY_bt) -> (rf zenon_TY_bd zenon_TY_hk) -> (forall C : zenon_U, (((zenon_TY_bc = (i2003_11_14_17_19_35232))/\(rinvR zenon_TY_bc C))->(rinvR (i2003_11_14_17_19_35232) C))) -> ((i2003_11_14_17_19_35232) = zenon_TY_bc) -> (cc zenon_TZ_cm) -> (forall B : zenon_U, (((zenon_TZ_cm = B)/\(cc zenon_TZ_cm))->(cc B))) -> (forall Y : zenon_U, ((rinvR zenon_TY_bt Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z))))) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_eh Y)/\(rf zenon_TZ_eh Z))->(Y = Z)))) -> (rf zenon_TY_bd zenon_TY_bt) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TY_bd Y)/\(rf zenon_TY_bd Z))->(Y = Z)))) -> (rf zenon_TZ_cm zenon_TY_bc) -> (rf zenon_TZ_cm (i2003_11_14_17_19_35232)) -> (rf zenon_TZ_cm zenon_TY_hk) -> (rf zenon_TZ_ez zenon_TY_ey) -> (zenon_TY_bt = zenon_TY_ey) -> (forall C : zenon_U, (((zenon_TY_ey = zenon_TY_bt)/\(rinvF zenon_TY_ey C))->(rinvF zenon_TY_bt C))) -> False). % 244.33/244.63 do 9 intro. intros zenon_H12d zenon_Hd1 zenon_H86 zenon_H87 zenon_Ha4 zenon_H12e zenon_H47 zenon_H12f zenon_H78 zenon_H130 zenon_H131 zenon_H21 zenon_H106 zenon_H105 zenon_H126 zenon_H132 zenon_H93 zenon_H1e zenon_Hfa zenon_H73 zenon_H133 zenon_H7e zenon_H134 zenon_H135. % 244.33/244.63 elim zenon_H12d. zenon_intro zenon_TZ_il. zenon_intro zenon_H136. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H136). zenon_intro zenon_Hde. zenon_intro zenon_H137. % 244.33/244.63 generalize (axiom_5 zenon_TY_hk). zenon_intro zenon_Hdc. % 244.33/244.63 generalize (zenon_Hdc zenon_TZ_il). zenon_intro zenon_Hdd. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_Hdd); [ zenon_intro zenon_Hda; zenon_intro zenon_Hdf | zenon_intro zenon_Hde; zenon_intro zenon_Hd9 ]. % 244.33/244.63 exact (zenon_Hda zenon_Hde). % 244.33/244.63 generalize (axiom_3 zenon_TZ_il). zenon_intro zenon_H138. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H138); [ zenon_intro zenon_H13b; zenon_intro zenon_H13a | zenon_intro zenon_H137; zenon_intro zenon_H139 ]. % 244.33/244.63 exact (zenon_H13b zenon_H137). % 244.33/244.63 apply (zenon_and_s _ _ zenon_H139). zenon_intro zenon_H13d. zenon_intro zenon_H13c. % 244.33/244.63 elim zenon_H13d. zenon_intro zenon_TY_is. zenon_intro zenon_H13e. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H13e). zenon_intro zenon_He0. zenon_intro zenon_H13f. % 244.33/244.63 generalize (zenon_H135 zenon_TZ_ez). zenon_intro zenon_H140. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H140); [ zenon_intro zenon_H142 | zenon_intro zenon_H141 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H142); [ zenon_intro zenon_H143 | zenon_intro zenon_H7f ]. % 244.33/244.63 apply zenon_H143. apply sym_equal. exact zenon_H134. % 244.33/244.63 apply (zenon_L20_ zenon_TY_ey zenon_TZ_ez); trivial. % 244.33/244.63 generalize (axiom_5 zenon_TY_bt). zenon_intro zenon_H7a. % 244.33/244.63 generalize (zenon_H7a zenon_TZ_ez). zenon_intro zenon_H144. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H144); [ zenon_intro zenon_H147; zenon_intro zenon_H146 | zenon_intro zenon_H141; zenon_intro zenon_H145 ]. % 244.33/244.63 exact (zenon_H147 zenon_H141). % 244.33/244.63 generalize (zenon_Hd1 zenon_TY_gj). zenon_intro zenon_Hd2. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_Hd2); [ zenon_intro zenon_Hd3 | zenon_intro zenon_Hc8 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_Hd3); [ zenon_intro zenon_H88 | zenon_intro zenon_Haa ]. % 244.33/244.63 apply (zenon_L21_ zenon_TZ_ez zenon_TY_bc zenon_TY_ey); trivial. % 244.33/244.63 exact (zenon_Haa zenon_Ha4). % 244.33/244.63 generalize (zenon_H12e zenon_TY_gj). zenon_intro zenon_H148. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H148); [ zenon_intro zenon_H149 | zenon_intro zenon_Hf8 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H149); [ zenon_intro zenon_H146 | zenon_intro zenon_Haa ]. % 244.33/244.63 exact (zenon_H146 zenon_H145). % 244.33/244.63 exact (zenon_Haa zenon_Ha4). % 244.33/244.63 generalize (zenon_H47 zenon_TY_hk). zenon_intro zenon_H14a. % 244.33/244.63 generalize (zenon_H14a (i2003_11_14_17_19_35232)). zenon_intro zenon_H14b. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H14b); [ zenon_intro zenon_H14d | zenon_intro zenon_H14c ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H14d); [ zenon_intro zenon_H14e | zenon_intro zenon_H77 ]. % 244.33/244.63 exact (zenon_H14e zenon_H133). % 244.33/244.63 exact (zenon_H77 zenon_H73). % 244.33/244.63 generalize (zenon_H14a zenon_TY_bc). zenon_intro zenon_H14f. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H14f); [ zenon_intro zenon_H150 | zenon_intro zenon_Hc4 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H150); [ zenon_intro zenon_H14e | zenon_intro zenon_H103 ]. % 244.33/244.63 exact (zenon_H14e zenon_H133). % 244.33/244.63 exact (zenon_H103 zenon_Hfa). % 244.33/244.63 generalize (zenon_H1e zenon_TY_hk). zenon_intro zenon_H151. % 244.33/244.63 generalize (zenon_H12f zenon_TY_is). zenon_intro zenon_H152. % 244.33/244.63 generalize (zenon_H152 zenon_TY_bd). zenon_intro zenon_H153. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H153); [ zenon_intro zenon_H155 | zenon_intro zenon_H154 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H155); [ zenon_intro zenon_Hf7 | zenon_intro zenon_H94 ]. % 244.33/244.63 apply (zenon_L37_ zenon_TY_hk zenon_TZ_il zenon_TY_bc zenon_TY_gj zenon_TY_is zenon_TY_bt); trivial. % 244.33/244.63 apply (zenon_L23_ zenon_TY_bt zenon_TY_bd); trivial. % 244.33/244.63 generalize (axiom_5 zenon_TY_is). zenon_intro zenon_H156. % 244.33/244.63 generalize (zenon_H156 zenon_TY_bd). zenon_intro zenon_H157. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H157); [ zenon_intro zenon_H15a; zenon_intro zenon_H159 | zenon_intro zenon_H154; zenon_intro zenon_H158 ]. % 244.33/244.63 exact (zenon_H15a zenon_H154). % 244.33/244.63 generalize (zenon_H152 zenon_TZ_eh). zenon_intro zenon_H15b. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H15b); [ zenon_intro zenon_H15d | zenon_intro zenon_H15c ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H15d); [ zenon_intro zenon_Hf7 | zenon_intro zenon_H79 ]. % 244.33/244.63 apply (zenon_L37_ zenon_TY_hk zenon_TZ_il zenon_TY_bc zenon_TY_gj zenon_TY_is zenon_TY_bt); trivial. % 244.33/244.63 apply (zenon_L19_ zenon_TY_bt zenon_TZ_eh); trivial. % 244.33/244.63 generalize (axiom_5 zenon_TY_is). zenon_intro zenon_H156. % 244.33/244.63 generalize (zenon_H156 zenon_TZ_eh). zenon_intro zenon_H15e. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H15e); [ zenon_intro zenon_H161; zenon_intro zenon_H160 | zenon_intro zenon_H15c; zenon_intro zenon_H15f ]. % 244.33/244.63 exact (zenon_H161 zenon_H15c). % 244.33/244.63 generalize (zenon_H132 zenon_TY_is). zenon_intro zenon_H162. % 244.33/244.63 generalize (zenon_H162 zenon_TY_bt). zenon_intro zenon_H163. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H163); [ zenon_intro zenon_H165 | zenon_intro zenon_H164 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H165); [ zenon_intro zenon_H160 | zenon_intro zenon_H7d ]. % 244.33/244.63 exact (zenon_H160 zenon_H15f). % 244.33/244.63 exact (zenon_H7d zenon_H78). % 244.33/244.63 generalize (rinvR_substitution_1 zenon_TY_is). zenon_intro zenon_H166. % 244.33/244.63 generalize (zenon_H166 zenon_TY_bt). zenon_intro zenon_H167. % 244.33/244.63 generalize (zenon_H151 zenon_TY_is). zenon_intro zenon_H168. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H168); [ zenon_intro zenon_H16a | zenon_intro zenon_H169 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H16a); [ zenon_intro zenon_H16b | zenon_intro zenon_H159 ]. % 244.33/244.63 exact (zenon_H16b zenon_H130). % 244.33/244.63 exact (zenon_H159 zenon_H158). % 244.33/244.63 generalize (rinvR_substitution_1 zenon_TY_hk). zenon_intro zenon_H16c. % 244.33/244.63 generalize (zenon_H16c zenon_TY_is). zenon_intro zenon_H16d. % 244.33/244.63 generalize (zenon_H131 zenon_TZ_cm). zenon_intro zenon_H16e. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H16e); [ zenon_intro zenon_H170 | zenon_intro zenon_H16f ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H170); [ zenon_intro zenon_H5b | zenon_intro zenon_Hfb ]. % 244.33/244.63 apply zenon_H5b. apply sym_equal. exact zenon_H21. % 244.33/244.63 apply (zenon_L38_ zenon_TY_bc zenon_TZ_cm); trivial. % 244.33/244.63 generalize (axiom_6 (i2003_11_14_17_19_35232)). zenon_intro zenon_H171. % 244.33/244.63 generalize (zenon_H171 zenon_TZ_cm). zenon_intro zenon_H172. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H172); [ zenon_intro zenon_H175; zenon_intro zenon_H174 | zenon_intro zenon_H16f; zenon_intro zenon_H173 ]. % 244.33/244.63 exact (zenon_H175 zenon_H16f). % 244.33/244.63 generalize (zenon_H16d zenon_TZ_cm). zenon_intro zenon_H176. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H176); [ zenon_intro zenon_H178 | zenon_intro zenon_H177 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H178); [ zenon_intro zenon_H17a | zenon_intro zenon_H179 ]. % 244.33/244.63 exact (zenon_H17a zenon_H169). % 244.33/244.63 generalize (axiom_6 zenon_TY_hk). zenon_intro zenon_H17b. % 244.33/244.63 generalize (zenon_H17b zenon_TZ_cm). zenon_intro zenon_H17c. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H17c); [ zenon_intro zenon_H179; zenon_intro zenon_H17f | zenon_intro zenon_H17e; zenon_intro zenon_H17d ]. % 244.33/244.63 elim (classic ((i2003_11_14_17_19_35232) = zenon_TY_hk)); [ zenon_intro zenon_H180 | zenon_intro zenon_H181 ]. % 244.33/244.63 cut ((rr zenon_TZ_cm (i2003_11_14_17_19_35232)) = (rr zenon_TZ_cm zenon_TY_hk)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_H17f. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_H173. % 244.33/244.63 cut (((i2003_11_14_17_19_35232) = zenon_TY_hk)); [idtac | apply NNPP; zenon_intro zenon_H181]. % 244.33/244.63 cut ((zenon_TZ_cm = zenon_TZ_cm)); [idtac | apply NNPP; zenon_intro zenon_H182]. % 244.33/244.63 congruence. % 244.33/244.63 apply zenon_H182. apply refl_equal. % 244.33/244.63 exact (zenon_H181 zenon_H180). % 244.33/244.63 apply zenon_H181. apply sym_equal. exact zenon_H14c. % 244.33/244.63 exact (zenon_H179 zenon_H17e). % 244.33/244.63 generalize (axiom_6 zenon_TY_is). zenon_intro zenon_H183. % 244.33/244.63 generalize (zenon_H183 zenon_TZ_cm). zenon_intro zenon_H184. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H184); [ zenon_intro zenon_H187; zenon_intro zenon_H186 | zenon_intro zenon_H177; zenon_intro zenon_H185 ]. % 244.33/244.63 exact (zenon_H187 zenon_H177). % 244.33/244.63 generalize (zenon_H167 zenon_TZ_cm). zenon_intro zenon_H188. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H188); [ zenon_intro zenon_H189 | zenon_intro zenon_H125 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H189); [ zenon_intro zenon_H18a | zenon_intro zenon_H187 ]. % 244.33/244.63 exact (zenon_H18a zenon_H164). % 244.33/244.63 generalize (axiom_6 zenon_TY_is). zenon_intro zenon_H183. % 244.33/244.63 generalize (zenon_H183 zenon_TZ_cm). zenon_intro zenon_H184. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H184); [ zenon_intro zenon_H187; zenon_intro zenon_H186 | zenon_intro zenon_H177; zenon_intro zenon_H185 ]. % 244.33/244.63 exact (zenon_H186 zenon_H185). % 244.33/244.63 exact (zenon_H187 zenon_H177). % 244.33/244.63 apply (zenon_L40_ zenon_TZ_cm zenon_TY_bt); trivial. % 244.33/244.63 (* end of lemma zenon_L41_ *) % 244.33/244.63 assert (zenon_L42_ : forall (zenon_TZ_ez : zenon_U) (zenon_TZ_bu : zenon_U) (zenon_TY_cl : zenon_U) (zenon_TY_bc : zenon_U) (zenon_TZ_eh : zenon_U) (zenon_TZ_cm : zenon_U) (zenon_TY_ey : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TY_bd : zenon_U) (zenon_TY_gj : zenon_U), (exists Z : zenon_U, ((rinvF zenon_TY_gj Z)/\(cd Z))) -> (rf zenon_TY_bd zenon_TY_bt) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_ey = B)/\(rinvF zenon_TY_ey C))->(rinvF B C)))) -> (forall Z : zenon_U, (((rf zenon_TZ_cm zenon_TY_bt)/\(rf zenon_TZ_cm Z))->(zenon_TY_bt = Z))) -> (rf zenon_TZ_cm (i2003_11_14_17_19_35232)) -> (forall B : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(cUnsatisfiable (i2003_11_14_17_19_35232)))->(cUnsatisfiable B))) -> ((exists Y : zenon_U, ((rinvF (i2003_11_14_17_19_35232) Y)/\(cd Y)))/\((forall Y : zenon_U, ((rinvR (i2003_11_14_17_19_35232) Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z)))))/\(~(cc (i2003_11_14_17_19_35232))))) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_cm Y)/\(rf zenon_TZ_cm Z))->(Y = Z)))) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_bt = B)/\(rinvF zenon_TY_bt C))->(rinvF B C)))) -> (rf zenon_TZ_eh zenon_TY_bt) -> (forall C : zenon_U, (((zenon_TY_bc = (i2003_11_14_17_19_35232))/\(rinvR zenon_TY_bc C))->(rinvR (i2003_11_14_17_19_35232) C))) -> ((i2003_11_14_17_19_35232) = zenon_TY_bc) -> (cc zenon_TZ_cm) -> (forall B : zenon_U, (((zenon_TZ_cm = B)/\(cc zenon_TZ_cm))->(cc B))) -> (forall Y : zenon_U, ((rinvR zenon_TY_bt Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z))))) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_eh Y)/\(rf zenon_TZ_eh Z))->(Y = Z)))) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TY_bd Y)/\(rf zenon_TY_bd Z))->(Y = Z)))) -> (rf zenon_TZ_cm zenon_TY_bc) -> (forall C : zenon_U, (((zenon_TY_ey = zenon_TY_bt)/\(rinvF zenon_TY_ey C))->(rinvF zenon_TY_bt C))) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_cl = B)/\(rf C zenon_TY_cl))->(rf C B)))) -> (forall Z : zenon_U, (((rf zenon_TZ_eh zenon_TY_bc)/\(rf zenon_TZ_eh Z))->(zenon_TY_bc = Z))) -> (rf zenon_TZ_eh zenon_TY_bc) -> ((i2003_11_14_17_19_35232) = zenon_TY_cl) -> (rf zenon_TZ_eh zenon_TY_cl) -> (zenon_TY_ey = zenon_TY_bc) -> (forall C : zenon_U, (((zenon_TY_ey = zenon_TY_bc)/\(rinvF zenon_TY_ey C))->(rinvF zenon_TY_bc C))) -> (rf zenon_TZ_bu (i2003_11_14_17_19_35232)) -> (rf zenon_TZ_ez zenon_TY_gj) -> (forall C : zenon_U, (((zenon_TY_ey = (i2003_11_14_17_19_35232))/\(rinvF zenon_TY_ey C))->(rinvF (i2003_11_14_17_19_35232) C))) -> (zenon_TY_ey = (i2003_11_14_17_19_35232)) -> (rf zenon_TZ_ez zenon_TY_ey) -> (rf zenon_TZ_bu zenon_TY_bt) -> (forall Z : zenon_U, (((rf zenon_TZ_bu zenon_TY_bt)/\(rf zenon_TZ_bu Z))->(zenon_TY_bt = Z))) -> (forall B : zenon_U, (forall C : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(rf C (i2003_11_14_17_19_35232)))->(rf C B)))) -> (rf zenon_TZ_cm zenon_TY_bt) -> (zenon_TY_bt = zenon_TY_ey) -> False). % 244.33/244.63 do 10 intro. intros zenon_H18b zenon_H93 zenon_H18c zenon_H18d zenon_H73 zenon_H18e zenon_H25 zenon_H47 zenon_H12f zenon_H78 zenon_H131 zenon_H21 zenon_H106 zenon_H105 zenon_H126 zenon_H132 zenon_H1e zenon_Hfa zenon_H135 zenon_H18f zenon_H190 zenon_H191 zenon_Hac zenon_H6d zenon_H87 zenon_H86 zenon_H5e zenon_Ha4 zenon_H9d zenon_H9e zenon_H7e zenon_H2b zenon_H51 zenon_H192 zenon_H3d zenon_H134. % 244.33/244.63 elim zenon_H18b. zenon_intro zenon_TZ_hc. zenon_intro zenon_H193. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H193). zenon_intro zenon_Hbb. zenon_intro zenon_H194. % 244.33/244.63 generalize (axiom_5 zenon_TY_gj). zenon_intro zenon_Hb9. % 244.33/244.63 generalize (zenon_Hb9 zenon_TZ_hc). zenon_intro zenon_Hba. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_Hba); [ zenon_intro zenon_Hb7; zenon_intro zenon_Hbc | zenon_intro zenon_Hbb; zenon_intro zenon_Hb6 ]. % 244.33/244.63 exact (zenon_Hb7 zenon_Hbb). % 244.33/244.63 generalize (axiom_3 zenon_TZ_hc). zenon_intro zenon_H195. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H195); [ zenon_intro zenon_H198; zenon_intro zenon_H197 | zenon_intro zenon_H194; zenon_intro zenon_H196 ]. % 244.33/244.63 exact (zenon_H198 zenon_H194). % 244.33/244.63 apply (zenon_and_s _ _ zenon_H196). zenon_intro zenon_H19a. zenon_intro zenon_H199. % 244.33/244.63 elim zenon_H19a. zenon_intro zenon_TY_hk. zenon_intro zenon_H19b. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H19b). zenon_intro zenon_Hbd. zenon_intro zenon_H19c. % 244.33/244.63 generalize (axiom_4 zenon_TZ_ez). zenon_intro zenon_Ha2. % 244.33/244.63 generalize (zenon_Ha2 zenon_TY_bt). zenon_intro zenon_H12e. % 244.33/244.63 generalize (zenon_Ha2 zenon_TY_bc). zenon_intro zenon_Hd1. % 244.33/244.63 generalize (zenon_H12f zenon_TY_ey). zenon_intro zenon_H19d. % 244.33/244.63 generalize (zenon_H19d zenon_TZ_cm). zenon_intro zenon_H19e. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H19e); [ zenon_intro zenon_H1a0 | zenon_intro zenon_H19f ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H1a0); [ zenon_intro zenon_H1a1 | zenon_intro zenon_H90 ]. % 244.33/244.63 exact (zenon_H1a1 zenon_H134). % 244.33/244.63 apply (zenon_L22_ zenon_TY_bt zenon_TZ_cm); trivial. % 244.33/244.63 generalize (axiom_5 zenon_TY_ey). zenon_intro zenon_H82. % 244.33/244.63 generalize (zenon_H82 zenon_TZ_cm). zenon_intro zenon_H1a2. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H1a2); [ zenon_intro zenon_H1a5; zenon_intro zenon_H1a4 | zenon_intro zenon_H19f; zenon_intro zenon_H1a3 ]. % 244.33/244.63 exact (zenon_H1a5 zenon_H19f). % 244.33/244.63 generalize (zenon_H19d zenon_TY_bd). zenon_intro zenon_H1a6. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H1a6); [ zenon_intro zenon_H1a8 | zenon_intro zenon_H1a7 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H1a8); [ zenon_intro zenon_H1a1 | zenon_intro zenon_H94 ]. % 244.33/244.63 exact (zenon_H1a1 zenon_H134). % 244.33/244.63 apply (zenon_L23_ zenon_TY_bt zenon_TY_bd); trivial. % 244.33/244.63 generalize (axiom_5 zenon_TY_ey). zenon_intro zenon_H82. % 244.33/244.63 generalize (zenon_H82 zenon_TY_bd). zenon_intro zenon_H1a9. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H1a9); [ zenon_intro zenon_H1ac; zenon_intro zenon_H1ab | zenon_intro zenon_H1a7; zenon_intro zenon_H1aa ]. % 244.33/244.63 exact (zenon_H1ac zenon_H1a7). % 244.33/244.63 generalize (zenon_H192 zenon_TY_gj). zenon_intro zenon_H1ad. % 244.33/244.63 generalize (zenon_H18c zenon_TY_hk). zenon_intro zenon_H1ae. % 244.33/244.63 generalize (zenon_H1ae zenon_TZ_cm). zenon_intro zenon_H1af. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H1af); [ zenon_intro zenon_H1b1 | zenon_intro zenon_H1b0 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H1b1); [ zenon_intro zenon_H1b2 | zenon_intro zenon_H1a5 ]. % 244.33/244.63 elim (classic (zenon_TY_hk = zenon_TY_hk)); [ zenon_intro zenon_Hd5 | zenon_intro zenon_Hd6 ]. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_hk) = (zenon_TY_ey = zenon_TY_hk)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_H1b2. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_Hd5. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_hk)); [idtac | apply NNPP; zenon_intro zenon_Hd6]. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_ey)); [idtac | apply NNPP; zenon_intro zenon_H1b3]. % 244.33/244.63 congruence. % 244.33/244.63 cut ((zenon_TY_bt = zenon_TY_ey) = (zenon_TY_hk = zenon_TY_ey)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_H1b3. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_H134. % 244.33/244.63 cut ((zenon_TY_ey = zenon_TY_ey)); [idtac | apply NNPP; zenon_intro zenon_H1b4]. % 244.33/244.63 cut ((zenon_TY_bt = zenon_TY_hk)); [idtac | apply NNPP; zenon_intro zenon_H1b5]. % 244.33/244.63 congruence. % 244.33/244.63 elim (classic (zenon_TY_hk = zenon_TY_hk)); [ zenon_intro zenon_Hd5 | zenon_intro zenon_Hd6 ]. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_hk) = (zenon_TY_bt = zenon_TY_hk)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_H1b5. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_Hd5. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_hk)); [idtac | apply NNPP; zenon_intro zenon_Hd6]. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_bt)); [idtac | apply NNPP; zenon_intro zenon_H1b6]. % 244.33/244.63 congruence. % 244.33/244.63 generalize (zenon_H18f zenon_TY_gj). zenon_intro zenon_Hb1. % 244.33/244.63 generalize (zenon_H51 zenon_TY_gj). zenon_intro zenon_H1b7. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H1b7); [ zenon_intro zenon_H1b8 | zenon_intro zenon_Hf8 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H1b8); [ zenon_intro zenon_H32 | zenon_intro zenon_H1b9 ]. % 244.33/244.63 exact (zenon_H32 zenon_H2b). % 244.33/244.63 generalize (zenon_H1ad zenon_TZ_bu). zenon_intro zenon_H1ba. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H1ba); [ zenon_intro zenon_H1bc | zenon_intro zenon_H1bb ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H1bc); [ zenon_intro zenon_Ha3 | zenon_intro zenon_H57 ]. % 244.33/244.63 apply (zenon_L26_ zenon_TY_ey zenon_TY_gj zenon_TZ_ez); trivial. % 244.33/244.63 exact (zenon_H57 zenon_H5e). % 244.33/244.63 exact (zenon_H1b9 zenon_H1bb). % 244.33/244.63 elim (classic (zenon_TY_bt = zenon_TY_bt)); [ zenon_intro zenon_H1bd | zenon_intro zenon_Hf9 ]. % 244.33/244.63 cut ((zenon_TY_bt = zenon_TY_bt) = (zenon_TY_hk = zenon_TY_bt)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_H1b6. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_H1bd. % 244.33/244.63 cut ((zenon_TY_bt = zenon_TY_bt)); [idtac | apply NNPP; zenon_intro zenon_Hf9]. % 244.33/244.63 cut ((zenon_TY_bt = zenon_TY_hk)); [idtac | apply NNPP; zenon_intro zenon_H1b5]. % 244.33/244.63 congruence. % 244.33/244.63 cut ((zenon_TY_bt = zenon_TY_gj) = (zenon_TY_bt = zenon_TY_hk)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_H1b5. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_Hf8. % 244.33/244.63 cut ((zenon_TY_gj = zenon_TY_hk)); [idtac | apply NNPP; zenon_intro zenon_Hd4]. % 244.33/244.63 cut ((zenon_TY_bt = zenon_TY_bt)); [idtac | apply NNPP; zenon_intro zenon_Hf9]. % 244.33/244.63 congruence. % 244.33/244.63 apply zenon_Hf9. apply refl_equal. % 244.33/244.63 generalize (zenon_H190 zenon_TY_gj). zenon_intro zenon_H1be. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H1be); [ zenon_intro zenon_H1bf | zenon_intro zenon_Hc8 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H1bf); [ zenon_intro zenon_H1c0 | zenon_intro zenon_Hb2 ]. % 244.33/244.63 exact (zenon_H1c0 zenon_H191). % 244.33/244.63 apply (zenon_L29_ zenon_TZ_eh zenon_TY_ey zenon_TZ_ez zenon_TY_gj zenon_TY_cl); trivial. % 244.33/244.63 apply (zenon_L34_ zenon_TY_ey zenon_TZ_ez zenon_TY_hk zenon_TZ_hc zenon_TY_gj zenon_TY_bc); trivial. % 244.33/244.63 apply zenon_Hf9. apply refl_equal. % 244.33/244.63 apply zenon_Hf9. apply refl_equal. % 244.33/244.63 apply zenon_Hd6. apply refl_equal. % 244.33/244.63 apply zenon_Hd6. apply refl_equal. % 244.33/244.63 apply zenon_H1b4. apply refl_equal. % 244.33/244.63 apply zenon_Hd6. apply refl_equal. % 244.33/244.63 apply zenon_Hd6. apply refl_equal. % 244.33/244.63 generalize (axiom_5 zenon_TY_ey). zenon_intro zenon_H82. % 244.33/244.63 generalize (zenon_H82 zenon_TZ_cm). zenon_intro zenon_H1a2. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H1a2); [ zenon_intro zenon_H1a5; zenon_intro zenon_H1a4 | zenon_intro zenon_H19f; zenon_intro zenon_H1a3 ]. % 244.33/244.63 exact (zenon_H1a4 zenon_H1a3). % 244.33/244.63 exact (zenon_H1a5 zenon_H19f). % 244.33/244.63 generalize (axiom_5 zenon_TY_hk). zenon_intro zenon_Hdc. % 244.33/244.63 generalize (zenon_Hdc zenon_TZ_cm). zenon_intro zenon_H1c1. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H1c1); [ zenon_intro zenon_H1c2; zenon_intro zenon_H14e | zenon_intro zenon_H1b0; zenon_intro zenon_H133 ]. % 244.33/244.63 exact (zenon_H1c2 zenon_H1b0). % 244.33/244.63 generalize (zenon_H1ae zenon_TY_bd). zenon_intro zenon_H1c3. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H1c3); [ zenon_intro zenon_H1c5 | zenon_intro zenon_H1c4 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H1c5); [ zenon_intro zenon_H1b2 | zenon_intro zenon_H1ac ]. % 244.33/244.63 elim (classic (zenon_TY_hk = zenon_TY_hk)); [ zenon_intro zenon_Hd5 | zenon_intro zenon_Hd6 ]. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_hk) = (zenon_TY_ey = zenon_TY_hk)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_H1b2. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_Hd5. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_hk)); [idtac | apply NNPP; zenon_intro zenon_Hd6]. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_ey)); [idtac | apply NNPP; zenon_intro zenon_H1b3]. % 244.33/244.63 congruence. % 244.33/244.63 cut ((zenon_TY_bt = zenon_TY_ey) = (zenon_TY_hk = zenon_TY_ey)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_H1b3. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_H134. % 244.33/244.63 cut ((zenon_TY_ey = zenon_TY_ey)); [idtac | apply NNPP; zenon_intro zenon_H1b4]. % 244.33/244.63 cut ((zenon_TY_bt = zenon_TY_hk)); [idtac | apply NNPP; zenon_intro zenon_H1b5]. % 244.33/244.63 congruence. % 244.33/244.63 elim (classic (zenon_TY_hk = zenon_TY_hk)); [ zenon_intro zenon_Hd5 | zenon_intro zenon_Hd6 ]. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_hk) = (zenon_TY_bt = zenon_TY_hk)). % 244.33/244.63 intro zenon_D_pnotp. % 244.33/244.63 apply zenon_H1b5. % 244.33/244.63 rewrite <- zenon_D_pnotp. % 244.33/244.63 exact zenon_Hd5. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_hk)); [idtac | apply NNPP; zenon_intro zenon_Hd6]. % 244.33/244.63 cut ((zenon_TY_hk = zenon_TY_bt)); [idtac | apply NNPP; zenon_intro zenon_H1b6]. % 244.33/244.63 congruence. % 244.33/244.63 generalize (zenon_H18d zenon_TY_hk). zenon_intro zenon_H1c6. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H1c6); [ zenon_intro zenon_H1c8 | zenon_intro zenon_H1c7 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H1c8); [ zenon_intro zenon_H44 | zenon_intro zenon_H14e ]. % 244.33/244.63 exact (zenon_H44 zenon_H3d). % 244.33/244.63 exact (zenon_H14e zenon_H133). % 244.33/244.63 apply zenon_H1b6. apply sym_equal. exact zenon_H1c7. % 244.33/244.63 apply zenon_Hd6. apply refl_equal. % 244.33/244.63 apply zenon_Hd6. apply refl_equal. % 244.33/244.63 apply zenon_H1b4. apply refl_equal. % 244.33/244.63 apply zenon_Hd6. apply refl_equal. % 244.33/244.63 apply zenon_Hd6. apply refl_equal. % 244.33/244.63 generalize (axiom_5 zenon_TY_ey). zenon_intro zenon_H82. % 244.33/244.63 generalize (zenon_H82 zenon_TY_bd). zenon_intro zenon_H1a9. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H1a9); [ zenon_intro zenon_H1ac; zenon_intro zenon_H1ab | zenon_intro zenon_H1a7; zenon_intro zenon_H1aa ]. % 244.33/244.63 exact (zenon_H1ab zenon_H1aa). % 244.33/244.63 exact (zenon_H1ac zenon_H1a7). % 244.33/244.63 generalize (axiom_5 zenon_TY_hk). zenon_intro zenon_Hdc. % 244.33/244.63 generalize (zenon_Hdc zenon_TY_bd). zenon_intro zenon_H1c9. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H1c9); [ zenon_intro zenon_H1ca; zenon_intro zenon_H16b | zenon_intro zenon_H1c4; zenon_intro zenon_H130 ]. % 244.33/244.63 exact (zenon_H1ca zenon_H1c4). % 244.33/244.63 generalize (zenon_H47 zenon_TY_hk). zenon_intro zenon_H14a. % 244.33/244.63 generalize (zenon_H14a (i2003_11_14_17_19_35232)). zenon_intro zenon_H14b. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H14b); [ zenon_intro zenon_H14d | zenon_intro zenon_H14c ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H14d); [ zenon_intro zenon_H14e | zenon_intro zenon_H77 ]. % 244.33/244.63 exact (zenon_H14e zenon_H133). % 244.33/244.63 exact (zenon_H77 zenon_H73). % 244.33/244.63 generalize (zenon_H18e zenon_TY_hk). zenon_intro zenon_H1cb. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H1cb); [ zenon_intro zenon_H1cd | zenon_intro zenon_H1cc ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H1cd); [ zenon_intro zenon_H181 | zenon_intro zenon_H26 ]. % 244.33/244.63 apply zenon_H181. apply sym_equal. exact zenon_H14c. % 244.33/244.63 apply (zenon_L2_); trivial. % 244.33/244.63 generalize (axiom_2 zenon_TY_hk). zenon_intro zenon_H1ce. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H1ce); [ zenon_intro zenon_H1d1; zenon_intro zenon_H1d0 | zenon_intro zenon_H1cc; zenon_intro zenon_H1cf ]. % 244.33/244.63 exact (zenon_H1d1 zenon_H1cc). % 244.33/244.63 apply (zenon_and_s _ _ zenon_H1cf). zenon_intro zenon_H12d. zenon_intro zenon_H1d2. % 244.33/244.63 apply (zenon_L41_ zenon_TY_bd zenon_TZ_eh zenon_TZ_cm zenon_TY_bt zenon_TY_gj zenon_TY_ey zenon_TY_bc zenon_TZ_ez zenon_TY_hk); trivial. % 244.33/244.63 (* end of lemma zenon_L42_ *) % 244.33/244.63 assert (zenon_L43_ : forall (zenon_TY_bd : zenon_U) (zenon_TY_bc : zenon_U) (zenon_TY_cl : zenon_U) (zenon_TZ_eh : zenon_U) (zenon_TZ_bu : zenon_U) (zenon_TZ_cm : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TY_ey : zenon_U), (exists Z : zenon_U, ((rinvF zenon_TY_ey Z)/\(cd Z))) -> (zenon_TY_bt = zenon_TY_ey) -> (rf zenon_TZ_cm zenon_TY_bt) -> (forall B : zenon_U, (forall C : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(rf C (i2003_11_14_17_19_35232)))->(rf C B)))) -> (forall Z : zenon_U, (((rf zenon_TZ_bu zenon_TY_bt)/\(rf zenon_TZ_bu Z))->(zenon_TY_bt = Z))) -> (rf zenon_TZ_bu zenon_TY_bt) -> (zenon_TY_ey = (i2003_11_14_17_19_35232)) -> (forall C : zenon_U, (((zenon_TY_ey = (i2003_11_14_17_19_35232))/\(rinvF zenon_TY_ey C))->(rinvF (i2003_11_14_17_19_35232) C))) -> (rf zenon_TZ_bu (i2003_11_14_17_19_35232)) -> (rf zenon_TZ_eh zenon_TY_cl) -> ((i2003_11_14_17_19_35232) = zenon_TY_cl) -> (rf zenon_TZ_eh zenon_TY_bc) -> (forall Z : zenon_U, (((rf zenon_TZ_eh zenon_TY_bc)/\(rf zenon_TZ_eh Z))->(zenon_TY_bc = Z))) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_cl = B)/\(rf C zenon_TY_cl))->(rf C B)))) -> (forall C : zenon_U, (((zenon_TY_ey = zenon_TY_bt)/\(rinvF zenon_TY_ey C))->(rinvF zenon_TY_bt C))) -> (rf zenon_TZ_cm zenon_TY_bc) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TY_bd Y)/\(rf zenon_TY_bd Z))->(Y = Z)))) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_eh Y)/\(rf zenon_TZ_eh Z))->(Y = Z)))) -> (forall Y : zenon_U, ((rinvR zenon_TY_bt Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z))))) -> (forall B : zenon_U, (((zenon_TZ_cm = B)/\(cc zenon_TZ_cm))->(cc B))) -> (cc zenon_TZ_cm) -> ((i2003_11_14_17_19_35232) = zenon_TY_bc) -> (forall C : zenon_U, (((zenon_TY_bc = (i2003_11_14_17_19_35232))/\(rinvR zenon_TY_bc C))->(rinvR (i2003_11_14_17_19_35232) C))) -> (rf zenon_TZ_eh zenon_TY_bt) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_bt = B)/\(rinvF zenon_TY_bt C))->(rinvF B C)))) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_cm Y)/\(rf zenon_TZ_cm Z))->(Y = Z)))) -> ((exists Y : zenon_U, ((rinvF (i2003_11_14_17_19_35232) Y)/\(cd Y)))/\((forall Y : zenon_U, ((rinvR (i2003_11_14_17_19_35232) Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z)))))/\(~(cc (i2003_11_14_17_19_35232))))) -> (forall B : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(cUnsatisfiable (i2003_11_14_17_19_35232)))->(cUnsatisfiable B))) -> (rf zenon_TZ_cm (i2003_11_14_17_19_35232)) -> (forall Z : zenon_U, (((rf zenon_TZ_cm zenon_TY_bt)/\(rf zenon_TZ_cm Z))->(zenon_TY_bt = Z))) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_ey = B)/\(rinvF zenon_TY_ey C))->(rinvF B C)))) -> (rf zenon_TY_bd zenon_TY_bt) -> ((exists Z : zenon_U, ((rinvF zenon_TY_bc Z)/\(cd Z)))/\((forall Y : zenon_U, ((rinvR zenon_TY_bc Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z)))))/\(~(cc zenon_TY_bc)))) -> (forall B : zenon_U, (((zenon_TY_bc = B)/\(cUnsatisfiable zenon_TY_bc))->(cUnsatisfiable B))) -> (zenon_TY_ey = zenon_TY_bc) -> (forall C : zenon_U, (((zenon_TY_ey = zenon_TY_bc)/\(rinvF zenon_TY_ey C))->(rinvF zenon_TY_bc C))) -> False). % 244.33/244.63 do 8 intro. intros zenon_H1d3 zenon_H134 zenon_H3d zenon_H192 zenon_H51 zenon_H2b zenon_H9e zenon_H9d zenon_H5e zenon_H6d zenon_Hac zenon_H191 zenon_H190 zenon_H18f zenon_H135 zenon_Hfa zenon_H1e zenon_H132 zenon_H126 zenon_H105 zenon_H106 zenon_H21 zenon_H131 zenon_H78 zenon_H12f zenon_H47 zenon_H25 zenon_H18e zenon_H73 zenon_H18d zenon_H18c zenon_H93 zenon_H35 zenon_H1d4 zenon_H87 zenon_H86. % 244.33/244.63 elim zenon_H1d3. zenon_intro zenon_TZ_ez. zenon_intro zenon_H1d5. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H1d5). zenon_intro zenon_H84. zenon_intro zenon_H1d6. % 244.33/244.63 generalize (axiom_5 zenon_TY_ey). zenon_intro zenon_H82. % 244.33/244.63 generalize (zenon_H82 zenon_TZ_ez). zenon_intro zenon_H83. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H83); [ zenon_intro zenon_H7f; zenon_intro zenon_H85 | zenon_intro zenon_H84; zenon_intro zenon_H7e ]. % 244.33/244.63 exact (zenon_H7f zenon_H84). % 244.33/244.63 generalize (axiom_3 zenon_TZ_ez). zenon_intro zenon_H1d7. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H1d7); [ zenon_intro zenon_H1da; zenon_intro zenon_H1d9 | zenon_intro zenon_H1d6; zenon_intro zenon_H1d8 ]. % 244.33/244.63 exact (zenon_H1da zenon_H1d6). % 244.33/244.63 apply (zenon_and_s _ _ zenon_H1d8). zenon_intro zenon_H1dc. zenon_intro zenon_H1db. % 244.33/244.63 elim zenon_H1dc. zenon_intro zenon_TY_gj. zenon_intro zenon_H1dd. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H1dd). zenon_intro zenon_Ha4. zenon_intro zenon_H1de. % 244.33/244.63 generalize (axiom_4 zenon_TZ_ez). zenon_intro zenon_Ha2. % 244.33/244.63 generalize (zenon_Ha2 zenon_TY_gj). zenon_intro zenon_Ha6. % 244.33/244.63 generalize (zenon_Ha6 zenon_TY_bc). zenon_intro zenon_H1df. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H1df); [ zenon_intro zenon_H1e1 | zenon_intro zenon_H1e0 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H1e1); [ zenon_intro zenon_Haa | zenon_intro zenon_H88 ]. % 244.33/244.63 exact (zenon_Haa zenon_Ha4). % 244.33/244.63 apply (zenon_L21_ zenon_TZ_ez zenon_TY_bc zenon_TY_ey); trivial. % 244.33/244.63 generalize (zenon_H1d4 zenon_TY_gj). zenon_intro zenon_H1e2. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H1e2); [ zenon_intro zenon_H1e4 | zenon_intro zenon_H1e3 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H1e4); [ zenon_intro zenon_H1e5 | zenon_intro zenon_H36 ]. % 244.33/244.63 apply zenon_H1e5. apply sym_equal. exact zenon_H1e0. % 244.33/244.63 apply (zenon_L5_ zenon_TY_bc); trivial. % 244.33/244.63 generalize (axiom_2 zenon_TY_gj). zenon_intro zenon_H1e6. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H1e6); [ zenon_intro zenon_H1e9; zenon_intro zenon_H1e8 | zenon_intro zenon_H1e3; zenon_intro zenon_H1e7 ]. % 244.33/244.63 exact (zenon_H1e9 zenon_H1e3). % 244.33/244.63 apply (zenon_and_s _ _ zenon_H1e7). zenon_intro zenon_H18b. zenon_intro zenon_H1ea. % 244.33/244.63 apply (zenon_L42_ zenon_TZ_ez zenon_TZ_bu zenon_TY_cl zenon_TY_bc zenon_TZ_eh zenon_TZ_cm zenon_TY_ey zenon_TY_bt zenon_TY_bd zenon_TY_gj); trivial. % 244.33/244.63 (* end of lemma zenon_L43_ *) % 244.33/244.63 assert (zenon_L44_ : forall (zenon_TZ_bu : zenon_U) (zenon_TZ_cm : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TY_bd : zenon_U) (zenon_TY_ey : zenon_U) (zenon_TZ_eh : zenon_U) (zenon_TY_bc : zenon_U) (zenon_TY_cl : zenon_U), (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_cl = B)/\(rinvF zenon_TY_cl C))->(rinvF B C)))) -> (forall C : zenon_U, ((((i2003_11_14_17_19_35232) = zenon_TY_bc)/\(rinvF (i2003_11_14_17_19_35232) C))->(rinvF zenon_TY_bc C))) -> ((i2003_11_14_17_19_35232) = zenon_TY_bc) -> (rf zenon_TZ_eh zenon_TY_ey) -> (forall B : zenon_U, (((zenon_TY_bc = B)/\(cUnsatisfiable zenon_TY_bc))->(cUnsatisfiable B))) -> (rf zenon_TY_bd zenon_TY_bt) -> (forall Z : zenon_U, (((rf zenon_TZ_cm zenon_TY_bt)/\(rf zenon_TZ_cm Z))->(zenon_TY_bt = Z))) -> (forall B : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(cUnsatisfiable (i2003_11_14_17_19_35232)))->(cUnsatisfiable B))) -> ((exists Y : zenon_U, ((rinvF (i2003_11_14_17_19_35232) Y)/\(cd Y)))/\((forall Y : zenon_U, ((rinvR (i2003_11_14_17_19_35232) Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z)))))/\(~(cc (i2003_11_14_17_19_35232))))) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_cm Y)/\(rf zenon_TZ_cm Z))->(Y = Z)))) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_bt = B)/\(rinvF zenon_TY_bt C))->(rinvF B C)))) -> (forall C : zenon_U, (((zenon_TY_bc = (i2003_11_14_17_19_35232))/\(rinvR zenon_TY_bc C))->(rinvR (i2003_11_14_17_19_35232) C))) -> (cc zenon_TZ_cm) -> (forall Y : zenon_U, ((rinvR zenon_TY_bt Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z))))) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TY_bd Y)/\(rf zenon_TY_bd Z))->(Y = Z)))) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_cl = B)/\(rf C zenon_TY_cl))->(rf C B)))) -> (rf zenon_TZ_bu (i2003_11_14_17_19_35232)) -> (rf zenon_TZ_bu zenon_TY_bt) -> (forall Z : zenon_U, (((rf zenon_TZ_bu zenon_TY_bt)/\(rf zenon_TZ_bu Z))->(zenon_TY_bt = Z))) -> (forall B : zenon_U, (forall C : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(rf C (i2003_11_14_17_19_35232)))->(rf C B)))) -> (rf zenon_TZ_cm zenon_TY_bt) -> ((exists Z : zenon_U, ((rinvF zenon_TY_bc Z)/\(cd Z)))/\((forall Y : zenon_U, ((rinvR zenon_TY_bc Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z)))))/\(~(cc zenon_TY_bc)))) -> (zenon_TY_bt = zenon_TY_bc) -> (zenon_TY_bt = zenon_TY_cl) -> (rf zenon_TZ_eh zenon_TY_cl) -> (rf zenon_TZ_cm zenon_TY_cl) -> ((i2003_11_14_17_19_35232) = zenon_TY_cl) -> False). % 244.33/244.63 do 8 intro. intros zenon_H1eb zenon_H1ec zenon_H21 zenon_H1ed zenon_H1d4 zenon_H93 zenon_H18d zenon_H18e zenon_H25 zenon_H47 zenon_H12f zenon_H131 zenon_H106 zenon_H126 zenon_H1e zenon_H18f zenon_H5e zenon_H2b zenon_H51 zenon_H192 zenon_H3d zenon_H35 zenon_H46 zenon_H1ee zenon_H6d zenon_H3c zenon_Hac. % 244.33/244.63 generalize (axiom_4 zenon_TZ_eh). zenon_intro zenon_H132. % 244.33/244.63 generalize (zenon_H12f zenon_TY_bc). zenon_intro zenon_H1ef. % 244.33/244.63 generalize (cc_substitution_1 zenon_TZ_cm). zenon_intro zenon_H105. % 244.33/244.63 generalize (zenon_H132 zenon_TY_bt). zenon_intro zenon_H1f0. % 244.33/244.63 generalize (zenon_H1eb (i2003_11_14_17_19_35232)). zenon_intro zenon_H1f1. % 244.33/244.63 generalize (zenon_H1f1 zenon_TZ_cm). zenon_intro zenon_H1f2. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H1f2); [ zenon_intro zenon_H1f3 | zenon_intro zenon_H76 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H1f3); [ zenon_intro zenon_H1f4 | zenon_intro zenon_H69 ]. % 244.33/244.63 apply zenon_H1f4. apply sym_equal. exact zenon_Hac. % 244.33/244.63 apply (zenon_L16_ zenon_TY_cl zenon_TZ_cm); trivial. % 244.33/244.63 generalize (axiom_5 (i2003_11_14_17_19_35232)). zenon_intro zenon_H5c. % 244.33/244.63 generalize (zenon_H5c zenon_TZ_cm). zenon_intro zenon_H75. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H75); [ zenon_intro zenon_H74; zenon_intro zenon_H77 | zenon_intro zenon_H76; zenon_intro zenon_H73 ]. % 244.33/244.63 exact (zenon_H74 zenon_H76). % 244.33/244.63 generalize (zenon_H132 zenon_TY_bc). zenon_intro zenon_H190. % 244.33/244.63 generalize (zenon_H1f1 zenon_TZ_eh). zenon_intro zenon_H1f5. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H1f5); [ zenon_intro zenon_H1f7 | zenon_intro zenon_H1f6 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H1f7); [ zenon_intro zenon_H1f4 | zenon_intro zenon_H6e ]. % 244.33/244.63 apply zenon_H1f4. apply sym_equal. exact zenon_Hac. % 244.33/244.63 apply (zenon_L17_ zenon_TY_cl zenon_TZ_eh); trivial. % 244.33/244.63 generalize (axiom_5 (i2003_11_14_17_19_35232)). zenon_intro zenon_H5c. % 244.33/244.63 generalize (zenon_H5c zenon_TZ_eh). zenon_intro zenon_H1f8. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H1f8); [ zenon_intro zenon_H1fb; zenon_intro zenon_H1fa | zenon_intro zenon_H1f6; zenon_intro zenon_H1f9 ]. % 244.33/244.63 exact (zenon_H1fb zenon_H1f6). % 244.33/244.63 generalize (zenon_H1eb zenon_TY_bt). zenon_intro zenon_H1fc. % 244.33/244.63 generalize (zenon_H1fc zenon_TZ_eh). zenon_intro zenon_H1fd. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H1fd); [ zenon_intro zenon_H1fe | zenon_intro zenon_H7c ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H1fe); [ zenon_intro zenon_H3e | zenon_intro zenon_H6e ]. % 244.33/244.63 apply zenon_H3e. apply sym_equal. exact zenon_H1ee. % 244.33/244.63 apply (zenon_L17_ zenon_TY_cl zenon_TZ_eh); trivial. % 244.33/244.63 generalize (axiom_5 zenon_TY_bt). zenon_intro zenon_H7a. % 244.33/244.63 generalize (zenon_H7a zenon_TZ_eh). zenon_intro zenon_H7b. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H7b); [ zenon_intro zenon_H79; zenon_intro zenon_H7d | zenon_intro zenon_H7c; zenon_intro zenon_H78 ]. % 244.33/244.63 exact (zenon_H79 zenon_H7c). % 244.33/244.63 generalize (zenon_H1ec zenon_TZ_cm). zenon_intro zenon_H1ff. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H1ff); [ zenon_intro zenon_H201 | zenon_intro zenon_H200 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H201); [ zenon_intro zenon_H1b | zenon_intro zenon_H74 ]. % 244.33/244.63 exact (zenon_H1b zenon_H21). % 244.33/244.63 apply (zenon_L18_ zenon_TZ_cm); trivial. % 244.33/244.63 generalize (axiom_5 zenon_TY_bc). zenon_intro zenon_H53. % 244.33/244.63 generalize (zenon_H53 zenon_TZ_cm). zenon_intro zenon_H202. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H202); [ zenon_intro zenon_H203; zenon_intro zenon_H103 | zenon_intro zenon_H200; zenon_intro zenon_Hfa ]. % 244.33/244.63 exact (zenon_H203 zenon_H200). % 244.33/244.63 generalize (zenon_H1ef zenon_TZ_eh). zenon_intro zenon_H204. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H204); [ zenon_intro zenon_H206 | zenon_intro zenon_H205 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H206); [ zenon_intro zenon_H207 | zenon_intro zenon_H79 ]. % 244.33/244.63 exact (zenon_H207 zenon_H46). % 244.33/244.63 apply (zenon_L19_ zenon_TY_bt zenon_TZ_eh); trivial. % 244.33/244.63 generalize (axiom_5 zenon_TY_bc). zenon_intro zenon_H53. % 244.33/244.63 generalize (zenon_H53 zenon_TZ_eh). zenon_intro zenon_H208. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H208); [ zenon_intro zenon_H209; zenon_intro zenon_H1c0 | zenon_intro zenon_H205; zenon_intro zenon_H191 ]. % 244.33/244.63 exact (zenon_H209 zenon_H205). % 244.33/244.63 generalize (zenon_H1f0 zenon_TY_ey). zenon_intro zenon_H20a. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H20a); [ zenon_intro zenon_H20b | zenon_intro zenon_H134 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H20b); [ zenon_intro zenon_H7d | zenon_intro zenon_H20c ]. % 244.33/244.63 exact (zenon_H7d zenon_H78). % 244.33/244.63 exact (zenon_H20c zenon_H1ed). % 244.33/244.63 generalize (rinvF_substitution_1 zenon_TY_ey). zenon_intro zenon_H18c. % 244.33/244.63 generalize (zenon_H18c zenon_TY_bc). zenon_intro zenon_H86. % 244.33/244.63 generalize (zenon_H18c (i2003_11_14_17_19_35232)). zenon_intro zenon_H9d. % 244.33/244.63 generalize (zenon_H18c zenon_TY_bt). zenon_intro zenon_H135. % 244.33/244.63 generalize (zenon_H132 zenon_TY_ey). zenon_intro zenon_H20d. % 244.33/244.63 generalize (zenon_H20d (i2003_11_14_17_19_35232)). zenon_intro zenon_H20e. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H20e); [ zenon_intro zenon_H20f | zenon_intro zenon_H9e ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H20f); [ zenon_intro zenon_H20c | zenon_intro zenon_H1fa ]. % 244.33/244.63 exact (zenon_H20c zenon_H1ed). % 244.33/244.63 exact (zenon_H1fa zenon_H1f9). % 244.33/244.63 generalize (zenon_H20d zenon_TY_bc). zenon_intro zenon_H210. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H210); [ zenon_intro zenon_H211 | zenon_intro zenon_H87 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H211); [ zenon_intro zenon_H20c | zenon_intro zenon_H1c0 ]. % 244.33/244.63 exact (zenon_H20c zenon_H1ed). % 244.33/244.63 exact (zenon_H1c0 zenon_H191). % 244.33/244.63 generalize (zenon_H1d4 zenon_TY_ey). zenon_intro zenon_H212. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H212); [ zenon_intro zenon_H214 | zenon_intro zenon_H213 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H214); [ zenon_intro zenon_H215 | zenon_intro zenon_H36 ]. % 244.33/244.63 apply zenon_H215. apply sym_equal. exact zenon_H87. % 244.33/244.63 apply (zenon_L5_ zenon_TY_bc); trivial. % 244.33/244.63 generalize (axiom_2 zenon_TY_ey). zenon_intro zenon_H216. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H216); [ zenon_intro zenon_H219; zenon_intro zenon_H218 | zenon_intro zenon_H213; zenon_intro zenon_H217 ]. % 244.33/244.63 exact (zenon_H219 zenon_H213). % 244.33/244.63 apply (zenon_and_s _ _ zenon_H217). zenon_intro zenon_H1d3. zenon_intro zenon_H21a. % 244.33/244.63 apply (zenon_L43_ zenon_TY_bd zenon_TY_bc zenon_TY_cl zenon_TZ_eh zenon_TZ_bu zenon_TZ_cm zenon_TY_bt zenon_TY_ey); trivial. % 244.33/244.63 (* end of lemma zenon_L44_ *) % 244.33/244.63 assert (zenon_L45_ : forall (zenon_TY_cl : zenon_U) (zenon_TZ_bu : zenon_U) (zenon_TZ_cm : zenon_U) (zenon_TY_bc : zenon_U) (zenon_TY_bd : zenon_U) (zenon_TY_bt : zenon_U), (cUnsatisfiable zenon_TY_bt) -> (rf zenon_TY_bd (i2003_11_14_17_19_35232)) -> (rf zenon_TY_bd zenon_TY_bc) -> (forall C : zenon_U, (((zenon_TY_bc = (i2003_11_14_17_19_35232))/\(rinvF zenon_TY_bc C))->(rinvF (i2003_11_14_17_19_35232) C))) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_bc = B)/\(rf C zenon_TY_bc))->(rf C B)))) -> ((exists Z : zenon_U, ((rinvF zenon_TY_bc Z)/\(cd Z)))/\((forall Y : zenon_U, ((rinvR zenon_TY_bc Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z)))))/\(~(cc zenon_TY_bc)))) -> (forall B : zenon_U, (forall C : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(rf C (i2003_11_14_17_19_35232)))->(rf C B)))) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TY_bd Y)/\(rf zenon_TY_bd Z))->(Y = Z)))) -> (cc zenon_TZ_cm) -> (forall C : zenon_U, (((zenon_TY_bc = (i2003_11_14_17_19_35232))/\(rinvR zenon_TY_bc C))->(rinvR (i2003_11_14_17_19_35232) C))) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_bt = B)/\(rinvF zenon_TY_bt C))->(rinvF B C)))) -> (forall B : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(cUnsatisfiable (i2003_11_14_17_19_35232)))->(cUnsatisfiable B))) -> (forall B : zenon_U, (((zenon_TY_bc = B)/\(cUnsatisfiable zenon_TY_bc))->(cUnsatisfiable B))) -> (forall C : zenon_U, ((((i2003_11_14_17_19_35232) = zenon_TY_bc)/\(rinvF (i2003_11_14_17_19_35232) C))->(rinvF zenon_TY_bc C))) -> ((exists Y : zenon_U, ((rinvF (i2003_11_14_17_19_35232) Y)/\(cd Y)))/\((forall Y : zenon_U, ((rinvR (i2003_11_14_17_19_35232) Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z)))))/\(~(cc (i2003_11_14_17_19_35232))))) -> (rf zenon_TZ_bu zenon_TY_bt) -> (rf zenon_TZ_bu zenon_TY_bc) -> (rf zenon_TZ_cm zenon_TY_cl) -> (rf zenon_TZ_cm zenon_TY_bt) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_bu Y)/\(rf zenon_TZ_bu Z))->(Y = Z)))) -> (forall B : zenon_U, (forall C : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(rinvF (i2003_11_14_17_19_35232) C))->(rinvF B C)))) -> False). % 244.33/244.63 do 6 intro. intros zenon_H21b zenon_H19 zenon_H1a zenon_H56 zenon_H68 zenon_H35 zenon_H192 zenon_H1e zenon_H106 zenon_H131 zenon_H12f zenon_H18e zenon_H1d4 zenon_H1ec zenon_H25 zenon_H2b zenon_H2a zenon_H3c zenon_H3d zenon_H34 zenon_H21c. % 244.33/244.63 generalize (axiom_2 zenon_TY_bt). zenon_intro zenon_H21d. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H21d); [ zenon_intro zenon_H220; zenon_intro zenon_H21f | zenon_intro zenon_H21b; zenon_intro zenon_H21e ]. % 244.33/244.63 exact (zenon_H220 zenon_H21b). % 244.33/244.63 apply (zenon_and_s _ _ zenon_H21e). zenon_intro zenon_H222. zenon_intro zenon_H221. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H221). zenon_intro zenon_H126. zenon_intro zenon_H223. % 244.33/244.63 generalize (zenon_H21c zenon_TY_bt). zenon_intro zenon_H224. % 244.33/244.63 generalize (zenon_H1e zenon_TY_bt). zenon_intro zenon_H225. % 244.33/244.63 generalize (rf_substitution_2 zenon_TY_cl). zenon_intro zenon_H18f. % 244.33/244.63 generalize (zenon_H1e (i2003_11_14_17_19_35232)). zenon_intro zenon_H1f. % 244.33/244.63 generalize (zenon_H34 zenon_TY_bt). zenon_intro zenon_H51. % 244.33/244.63 generalize (zenon_H1f zenon_TY_bc). zenon_intro zenon_H20. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H20); [ zenon_intro zenon_H22 | zenon_intro zenon_H21 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H22); [ zenon_intro zenon_H24 | zenon_intro zenon_H23 ]. % 244.33/244.63 exact (zenon_H24 zenon_H19). % 244.33/244.63 exact (zenon_H23 zenon_H1a). % 244.33/244.63 generalize (axiom_4 zenon_TZ_cm). zenon_intro zenon_H47. % 244.33/244.63 generalize (zenon_H18e zenon_TY_cl). zenon_intro zenon_H226. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H226); [ zenon_intro zenon_H228 | zenon_intro zenon_H227 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H228); [ zenon_intro zenon_H50 | zenon_intro zenon_H26 ]. % 244.33/244.63 apply (zenon_L10_ zenon_TZ_cm zenon_TY_bt zenon_TZ_bu zenon_TY_bc zenon_TY_cl); trivial. % 244.33/244.63 apply (zenon_L2_); trivial. % 244.33/244.63 generalize (axiom_2 zenon_TY_cl). zenon_intro zenon_H229. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H229); [ zenon_intro zenon_H22c; zenon_intro zenon_H22b | zenon_intro zenon_H227; zenon_intro zenon_H22a ]. % 244.33/244.63 exact (zenon_H22c zenon_H227). % 244.33/244.63 apply (zenon_and_s _ _ zenon_H22a). zenon_intro zenon_H22e. zenon_intro zenon_H22d. % 244.33/244.63 elim zenon_H22e. zenon_intro zenon_TZ_eh. zenon_intro zenon_H22f. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H22f). zenon_intro zenon_H71. zenon_intro zenon_H230. % 244.33/244.63 generalize (axiom_5 zenon_TY_cl). zenon_intro zenon_H6a. % 244.33/244.63 generalize (zenon_H6a zenon_TZ_eh). zenon_intro zenon_H70. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H70); [ zenon_intro zenon_H6e; zenon_intro zenon_H72 | zenon_intro zenon_H71; zenon_intro zenon_H6d ]. % 244.33/244.63 exact (zenon_H6e zenon_H71). % 244.33/244.63 generalize (axiom_3 zenon_TZ_eh). zenon_intro zenon_H231. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H231); [ zenon_intro zenon_H234; zenon_intro zenon_H233 | zenon_intro zenon_H230; zenon_intro zenon_H232 ]. % 244.33/244.63 exact (zenon_H234 zenon_H230). % 244.33/244.63 apply (zenon_and_s _ _ zenon_H232). zenon_intro zenon_H236. zenon_intro zenon_H235. % 244.33/244.63 elim zenon_H236. zenon_intro zenon_TY_ey. zenon_intro zenon_H237. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H237). zenon_intro zenon_H1ed. zenon_intro zenon_H238. % 244.33/244.63 generalize (zenon_H51 zenon_TY_bc). zenon_intro zenon_H4e. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H4e); [ zenon_intro zenon_H4f | zenon_intro zenon_H46 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H4f); [ zenon_intro zenon_H32 | zenon_intro zenon_H33 ]. % 244.33/244.63 exact (zenon_H32 zenon_H2b). % 244.33/244.63 exact (zenon_H33 zenon_H2a). % 244.33/244.63 generalize (zenon_H51 (i2003_11_14_17_19_35232)). zenon_intro zenon_H239. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H239); [ zenon_intro zenon_H23b | zenon_intro zenon_H23a ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H23b); [ zenon_intro zenon_H32 | zenon_intro zenon_H57 ]. % 244.33/244.63 exact (zenon_H32 zenon_H2b). % 244.33/244.63 apply (zenon_L12_ zenon_TZ_bu zenon_TY_bc); trivial. % 244.33/244.63 generalize (zenon_H224 zenon_TY_bd). zenon_intro zenon_H23c. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H23c); [ zenon_intro zenon_H23d | zenon_intro zenon_H96 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H23d); [ zenon_intro zenon_H23e | zenon_intro zenon_H60 ]. % 244.33/244.63 apply zenon_H23e. apply sym_equal. exact zenon_H23a. % 244.33/244.63 apply (zenon_L13_ zenon_TY_bd); trivial. % 244.33/244.63 generalize (axiom_5 zenon_TY_bt). zenon_intro zenon_H7a. % 244.33/244.63 generalize (zenon_H7a zenon_TY_bd). zenon_intro zenon_H95. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H95); [ zenon_intro zenon_H94; zenon_intro zenon_H97 | zenon_intro zenon_H96; zenon_intro zenon_H93 ]. % 244.33/244.63 exact (zenon_H94 zenon_H96). % 244.33/244.63 generalize (rinvF_substitution_1 zenon_TY_cl). zenon_intro zenon_H1eb. % 244.33/244.63 generalize (zenon_H47 zenon_TY_bt). zenon_intro zenon_H18d. % 244.33/244.63 generalize (zenon_H56 zenon_TZ_bu). zenon_intro zenon_H58. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H58); [ zenon_intro zenon_H5a | zenon_intro zenon_H59 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H5a); [ zenon_intro zenon_H5b | zenon_intro zenon_H52 ]. % 244.33/244.63 apply zenon_H5b. apply sym_equal. exact zenon_H21. % 244.33/244.63 apply (zenon_L11_ zenon_TY_bc zenon_TZ_bu); trivial. % 244.33/244.63 generalize (axiom_5 (i2003_11_14_17_19_35232)). zenon_intro zenon_H5c. % 244.33/244.63 generalize (zenon_H5c zenon_TZ_bu). zenon_intro zenon_H5d. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H5d); [ zenon_intro zenon_H5f; zenon_intro zenon_H57 | zenon_intro zenon_H59; zenon_intro zenon_H5e ]. % 244.33/244.63 exact (zenon_H5f zenon_H59). % 244.33/244.63 generalize (zenon_H225 zenon_TY_cl). zenon_intro zenon_H23f. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H23f); [ zenon_intro zenon_H240 | zenon_intro zenon_H1ee ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H240); [ zenon_intro zenon_H97 | zenon_intro zenon_H64 ]. % 244.33/244.63 exact (zenon_H97 zenon_H93). % 244.33/244.63 apply (zenon_L15_ zenon_TY_bt zenon_TZ_cm zenon_TY_cl zenon_TY_bd zenon_TY_bc); trivial. % 244.33/244.63 generalize (zenon_H68 zenon_TY_cl). zenon_intro zenon_H63. % 244.33/244.63 generalize (zenon_H1f zenon_TY_cl). zenon_intro zenon_H241. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H241); [ zenon_intro zenon_H242 | zenon_intro zenon_Hac ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H242); [ zenon_intro zenon_H24 | zenon_intro zenon_H64 ]. % 244.33/244.63 exact (zenon_H24 zenon_H19). % 244.33/244.63 apply (zenon_L14_ zenon_TY_bd zenon_TZ_cm zenon_TY_bt zenon_TY_cl zenon_TY_bc); trivial. % 244.33/244.63 apply (zenon_L44_ zenon_TZ_bu zenon_TZ_cm zenon_TY_bt zenon_TY_bd zenon_TY_ey zenon_TZ_eh zenon_TY_bc zenon_TY_cl); trivial. % 244.33/244.63 (* end of lemma zenon_L45_ *) % 244.33/244.63 assert (zenon_L46_ : forall (zenon_TZ_bu : zenon_U) (zenon_TY_bc : zenon_U) (zenon_TY_bd : zenon_U) (zenon_TY_bt : zenon_U), (exists Z : zenon_U, ((rinvF zenon_TY_bt Z)/\(cd Z))) -> (rf zenon_TY_bd (i2003_11_14_17_19_35232)) -> (rf zenon_TY_bd zenon_TY_bc) -> (forall C : zenon_U, (((zenon_TY_bc = (i2003_11_14_17_19_35232))/\(rinvF zenon_TY_bc C))->(rinvF (i2003_11_14_17_19_35232) C))) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_bc = B)/\(rf C zenon_TY_bc))->(rf C B)))) -> (forall B : zenon_U, (forall C : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(rf C (i2003_11_14_17_19_35232)))->(rf C B)))) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TY_bd Y)/\(rf zenon_TY_bd Z))->(Y = Z)))) -> (forall C : zenon_U, (((zenon_TY_bc = (i2003_11_14_17_19_35232))/\(rinvR zenon_TY_bc C))->(rinvR (i2003_11_14_17_19_35232) C))) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_bt = B)/\(rinvF zenon_TY_bt C))->(rinvF B C)))) -> (forall B : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(cUnsatisfiable (i2003_11_14_17_19_35232)))->(cUnsatisfiable B))) -> (forall B : zenon_U, (((zenon_TY_bc = B)/\(cUnsatisfiable zenon_TY_bc))->(cUnsatisfiable B))) -> (forall C : zenon_U, ((((i2003_11_14_17_19_35232) = zenon_TY_bc)/\(rinvF (i2003_11_14_17_19_35232) C))->(rinvF zenon_TY_bc C))) -> ((exists Y : zenon_U, ((rinvF (i2003_11_14_17_19_35232) Y)/\(cd Y)))/\((forall Y : zenon_U, ((rinvR (i2003_11_14_17_19_35232) Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z)))))/\(~(cc (i2003_11_14_17_19_35232))))) -> (forall B : zenon_U, (forall C : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(rinvF (i2003_11_14_17_19_35232) C))->(rinvF B C)))) -> ((exists Z : zenon_U, ((rinvF zenon_TY_bc Z)/\(cd Z)))/\((forall Y : zenon_U, ((rinvR zenon_TY_bc Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z)))))/\(~(cc zenon_TY_bc)))) -> (rf zenon_TZ_bu zenon_TY_bc) -> (rf zenon_TZ_bu zenon_TY_bt) -> (forall Y : zenon_U, (forall Z : zenon_U, (((rf zenon_TZ_bu Y)/\(rf zenon_TZ_bu Z))->(Y = Z)))) -> False). % 244.33/244.63 do 4 intro. intros zenon_H222 zenon_H19 zenon_H1a zenon_H56 zenon_H68 zenon_H192 zenon_H1e zenon_H131 zenon_H12f zenon_H18e zenon_H1d4 zenon_H1ec zenon_H25 zenon_H21c zenon_H35 zenon_H2a zenon_H2b zenon_H34. % 244.33/244.63 elim zenon_H222. zenon_intro zenon_TZ_cm. zenon_intro zenon_H243. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H243). zenon_intro zenon_H92. zenon_intro zenon_H244. % 244.33/244.63 generalize (axiom_5 zenon_TY_bt). zenon_intro zenon_H7a. % 244.33/244.63 generalize (zenon_H7a zenon_TZ_cm). zenon_intro zenon_H91. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H91); [ zenon_intro zenon_H90; zenon_intro zenon_H44 | zenon_intro zenon_H92; zenon_intro zenon_H3d ]. % 244.33/244.63 exact (zenon_H90 zenon_H92). % 244.33/244.63 generalize (axiom_3 zenon_TZ_cm). zenon_intro zenon_H245. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H245); [ zenon_intro zenon_H248; zenon_intro zenon_H247 | zenon_intro zenon_H244; zenon_intro zenon_H246 ]. % 244.33/244.63 exact (zenon_H248 zenon_H244). % 244.33/244.63 apply (zenon_and_s _ _ zenon_H246). zenon_intro zenon_H249. zenon_intro zenon_H106. % 244.33/244.63 elim zenon_H249. zenon_intro zenon_TY_cl. zenon_intro zenon_H24a. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H24a). zenon_intro zenon_H3c. zenon_intro zenon_H24b. % 244.33/244.63 generalize (zenon_H1d4 zenon_TY_bt). zenon_intro zenon_H24c. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H24c); [ zenon_intro zenon_H24d | zenon_intro zenon_H21b ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H24d); [ zenon_intro zenon_H2c | zenon_intro zenon_H36 ]. % 244.33/244.63 apply (zenon_L4_ zenon_TY_bt zenon_TY_bc zenon_TZ_bu); trivial. % 244.33/244.63 apply (zenon_L5_ zenon_TY_bc); trivial. % 244.33/244.63 apply (zenon_L45_ zenon_TY_cl zenon_TZ_bu zenon_TZ_cm zenon_TY_bc zenon_TY_bd zenon_TY_bt); trivial. % 244.33/244.63 (* end of lemma zenon_L46_ *) % 244.33/244.63 assert (zenon_L47_ : forall (zenon_TY_bd : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TZ_bu : zenon_U) (zenon_TY_bc : zenon_U), (cUnsatisfiable zenon_TY_bc) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_bc = B)/\(rinvR zenon_TY_bc C))->(rinvR B C)))) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_bc = B)/\(rinvF zenon_TY_bc C))->(rinvF B C)))) -> (rf zenon_TZ_bu zenon_TY_bt) -> (rf zenon_TZ_bu zenon_TY_bc) -> (rf zenon_TY_bd (i2003_11_14_17_19_35232)) -> (rf zenon_TY_bd zenon_TY_bc) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_bc = B)/\(rf C zenon_TY_bc))->(rf C B)))) -> (forall B : zenon_U, (forall C : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(rf C (i2003_11_14_17_19_35232)))->(rf C B)))) -> (forall B : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(cUnsatisfiable (i2003_11_14_17_19_35232)))->(cUnsatisfiable B))) -> (forall B : zenon_U, (((zenon_TY_bc = B)/\(cUnsatisfiable zenon_TY_bc))->(cUnsatisfiable B))) -> ((exists Y : zenon_U, ((rinvF (i2003_11_14_17_19_35232) Y)/\(cd Y)))/\((forall Y : zenon_U, ((rinvR (i2003_11_14_17_19_35232) Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z)))))/\(~(cc (i2003_11_14_17_19_35232))))) -> (forall B : zenon_U, (forall C : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(rinvF (i2003_11_14_17_19_35232) C))->(rinvF B C)))) -> False). % 244.33/244.63 do 4 intro. intros zenon_H38 zenon_H24e zenon_H24f zenon_H2b zenon_H2a zenon_H19 zenon_H1a zenon_H68 zenon_H192 zenon_H18e zenon_H1d4 zenon_H25 zenon_H21c. % 244.33/244.63 generalize (axiom_2 zenon_TY_bc). zenon_intro zenon_H37. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H37); [ zenon_intro zenon_H36; zenon_intro zenon_H39 | zenon_intro zenon_H38; zenon_intro zenon_H35 ]. % 244.33/244.63 exact (zenon_H36 zenon_H38). % 244.33/244.63 generalize (zenon_H24e (i2003_11_14_17_19_35232)). zenon_intro zenon_H131. % 244.33/244.63 generalize (zenon_H21c zenon_TY_bc). zenon_intro zenon_H1ec. % 244.33/244.63 generalize (zenon_H24f (i2003_11_14_17_19_35232)). zenon_intro zenon_H56. % 244.33/244.63 generalize (axiom_4 zenon_TZ_bu). zenon_intro zenon_H34. % 244.33/244.63 generalize (axiom_4 zenon_TY_bd). zenon_intro zenon_H1e. % 244.33/244.63 generalize (rinvF_substitution_1 zenon_TY_bt). zenon_intro zenon_H12f. % 244.33/244.63 generalize (zenon_H1d4 zenon_TY_bt). zenon_intro zenon_H24c. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H24c); [ zenon_intro zenon_H24d | zenon_intro zenon_H21b ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H24d); [ zenon_intro zenon_H2c | zenon_intro zenon_H36 ]. % 244.33/244.63 apply (zenon_L4_ zenon_TY_bt zenon_TY_bc zenon_TZ_bu); trivial. % 244.33/244.63 apply (zenon_L5_ zenon_TY_bc); trivial. % 244.33/244.63 generalize (axiom_2 zenon_TY_bt). zenon_intro zenon_H21d. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H21d); [ zenon_intro zenon_H220; zenon_intro zenon_H21f | zenon_intro zenon_H21b; zenon_intro zenon_H21e ]. % 244.33/244.63 exact (zenon_H220 zenon_H21b). % 244.33/244.63 apply (zenon_and_s _ _ zenon_H21e). zenon_intro zenon_H222. zenon_intro zenon_H221. % 244.33/244.63 apply (zenon_L46_ zenon_TZ_bu zenon_TY_bc zenon_TY_bd zenon_TY_bt); trivial. % 244.33/244.63 (* end of lemma zenon_L47_ *) % 244.33/244.63 assert (zenon_L48_ : forall (zenon_TY_bd : zenon_U) (zenon_TY_bc : zenon_U), (exists Z : zenon_U, ((rinvF zenon_TY_bc Z)/\(cd Z))) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_bc = B)/\(rinvR zenon_TY_bc C))->(rinvR B C)))) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_bc = B)/\(rinvF zenon_TY_bc C))->(rinvF B C)))) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_bc = B)/\(rf C zenon_TY_bc))->(rf C B)))) -> (forall B : zenon_U, (forall C : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(rf C (i2003_11_14_17_19_35232)))->(rf C B)))) -> (forall B : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(cUnsatisfiable (i2003_11_14_17_19_35232)))->(cUnsatisfiable B))) -> (forall B : zenon_U, (((zenon_TY_bc = B)/\(cUnsatisfiable zenon_TY_bc))->(cUnsatisfiable B))) -> (forall B : zenon_U, (forall C : zenon_U, ((((i2003_11_14_17_19_35232) = B)/\(rinvF (i2003_11_14_17_19_35232) C))->(rinvF B C)))) -> ((exists Y : zenon_U, ((rinvF (i2003_11_14_17_19_35232) Y)/\(cd Y)))/\((forall Y : zenon_U, ((rinvR (i2003_11_14_17_19_35232) Y)->(exists Z : zenon_U, ((rinvF Y Z)/\(cd Z)))))/\(~(cc (i2003_11_14_17_19_35232))))) -> (rf zenon_TY_bd zenon_TY_bc) -> (rf zenon_TY_bd (i2003_11_14_17_19_35232)) -> False). % 244.33/244.63 do 2 intro. intros zenon_H250 zenon_H24e zenon_H24f zenon_H68 zenon_H192 zenon_H18e zenon_H1d4 zenon_H21c zenon_H25 zenon_H1a zenon_H19. % 244.33/244.63 elim zenon_H250. zenon_intro zenon_TZ_bu. zenon_intro zenon_H251. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H251). zenon_intro zenon_H55. zenon_intro zenon_H252. % 244.33/244.63 generalize (axiom_5 zenon_TY_bc). zenon_intro zenon_H53. % 244.33/244.63 generalize (zenon_H53 zenon_TZ_bu). zenon_intro zenon_H54. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H54); [ zenon_intro zenon_H52; zenon_intro zenon_H33 | zenon_intro zenon_H55; zenon_intro zenon_H2a ]. % 244.33/244.63 exact (zenon_H52 zenon_H55). % 244.33/244.63 generalize (axiom_3 zenon_TZ_bu). zenon_intro zenon_H253. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H253); [ zenon_intro zenon_H256; zenon_intro zenon_H255 | zenon_intro zenon_H252; zenon_intro zenon_H254 ]. % 244.33/244.63 exact (zenon_H256 zenon_H252). % 244.33/244.63 apply (zenon_and_s _ _ zenon_H254). zenon_intro zenon_H258. zenon_intro zenon_H257. % 244.33/244.63 elim zenon_H258. zenon_intro zenon_TY_bt. zenon_intro zenon_H259. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H259). zenon_intro zenon_H2b. zenon_intro zenon_H223. % 244.33/244.63 generalize (zenon_H18e zenon_TY_bc). zenon_intro zenon_H25a. % 244.33/244.63 apply (zenon_imply_s _ _ zenon_H25a); [ zenon_intro zenon_H25b | zenon_intro zenon_H38 ]. % 244.33/244.63 apply (zenon_notand_s _ _ zenon_H25b); [ zenon_intro zenon_H1b | zenon_intro zenon_H26 ]. % 244.33/244.63 apply (zenon_L1_ zenon_TY_bc zenon_TY_bd); trivial. % 244.33/244.63 apply (zenon_L2_); trivial. % 244.33/244.63 apply (zenon_L47_ zenon_TY_bd zenon_TY_bt zenon_TZ_bu zenon_TY_bc); trivial. % 244.33/244.63 (* end of lemma zenon_L48_ *) % 244.33/244.63 generalize (axiom_2 (i2003_11_14_17_19_35232)). zenon_intro zenon_H27. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H27); [ zenon_intro zenon_H26; zenon_intro zenon_H28 | zenon_intro axiom_8; zenon_intro zenon_H25 ]. % 244.33/244.63 exact (zenon_H26 axiom_8). % 244.33/244.63 apply (zenon_and_s _ _ zenon_H25). zenon_intro zenon_H25d. zenon_intro zenon_H25c. % 244.33/244.63 elim zenon_H25d. zenon_intro zenon_TY_bd. zenon_intro zenon_H25e. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H25e). zenon_intro zenon_H62. zenon_intro zenon_H25f. % 244.33/244.63 generalize (axiom_5 (i2003_11_14_17_19_35232)). zenon_intro zenon_H5c. % 244.33/244.63 generalize (zenon_H5c zenon_TY_bd). zenon_intro zenon_H61. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H61); [ zenon_intro zenon_H60; zenon_intro zenon_H24 | zenon_intro zenon_H62; zenon_intro zenon_H19 ]. % 244.33/244.63 exact (zenon_H60 zenon_H62). % 244.33/244.63 generalize (axiom_3 zenon_TY_bd). zenon_intro zenon_H260. % 244.33/244.63 apply (zenon_equiv_s _ _ zenon_H260); [ zenon_intro zenon_H263; zenon_intro zenon_H262 | zenon_intro zenon_H25f; zenon_intro zenon_H261 ]. % 244.33/244.63 exact (zenon_H263 zenon_H25f). % 244.33/244.63 apply (zenon_and_s _ _ zenon_H261). zenon_intro zenon_H265. zenon_intro zenon_H264. % 244.33/244.63 elim zenon_H265. zenon_intro zenon_TY_bc. zenon_intro zenon_H266. % 244.33/244.63 apply (zenon_and_s _ _ zenon_H266). zenon_intro zenon_H1a. zenon_intro zenon_H267. % 244.33/244.63 generalize (cUnsatisfiable_substitution_1 zenon_TY_bc). zenon_intro zenon_H1d4. % 244.33/244.63 generalize (cUnsatisfiable_substitution_1 (i2003_11_14_17_19_35232)). zenon_intro zenon_H18e. % 244.33/244.63 generalize (rf_substitution_2 zenon_TY_bc). zenon_intro zenon_H68. % 244.33/244.63 generalize (rinvF_substitution_1 (i2003_11_14_17_19_35232)). zenon_intro zenon_H21c. % 244.33/244.64 generalize (rinvF_substitution_1 zenon_TY_bc). zenon_intro zenon_H24f. % 244.33/244.64 generalize (rinvR_substitution_1 zenon_TY_bc). zenon_intro zenon_H24e. % 244.33/244.64 generalize (rf_substitution_2 (i2003_11_14_17_19_35232)). zenon_intro zenon_H192. % 244.33/244.64 generalize (zenon_H18e zenon_TY_bc). zenon_intro zenon_H25a. % 244.33/244.64 apply (zenon_imply_s _ _ zenon_H25a); [ zenon_intro zenon_H25b | zenon_intro zenon_H38 ]. % 244.33/244.64 apply (zenon_notand_s _ _ zenon_H25b); [ zenon_intro zenon_H1b | zenon_intro zenon_H26 ]. % 244.33/244.64 apply (zenon_L1_ zenon_TY_bc zenon_TY_bd); trivial. % 244.33/244.64 apply (zenon_L2_); trivial. % 244.33/244.64 generalize (axiom_2 zenon_TY_bc). zenon_intro zenon_H37. % 244.33/244.64 apply (zenon_equiv_s _ _ zenon_H37); [ zenon_intro zenon_H36; zenon_intro zenon_H39 | zenon_intro zenon_H38; zenon_intro zenon_H35 ]. % 244.33/244.64 exact (zenon_H36 zenon_H38). % 244.33/244.64 apply (zenon_and_s _ _ zenon_H35). zenon_intro zenon_H250. zenon_intro zenon_H268. % 244.33/244.64 apply (zenon_L48_ zenon_TY_bd zenon_TY_bc); trivial. % 244.33/244.64 Qed. % 244.33/244.64 % SZS output end Proof % 244.33/244.64 (* END-PROOF *) % 244.33/244.64 nodes searched: 44487918 % 244.33/244.64 max branch formulas: 115884 % 244.33/244.64 proof nodes created: 159933 % 244.33/244.64 formulas created: 12590160 % 244.33/244.64 %------------------------------------------------------------------------------