%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : ALG139+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 14 18:30:13 EDT 2022 % Result : Unsatisfiable 3.14s 3.35s % Output : Proof 3.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : ALG139+1 : TPTP v8.1.0. Released v2.7.0. % 0.11/0.13 % Command : run_zenon %s %d % 0.12/0.34 % Computer : n023.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Thu Jun 9 07:15:08 EDT 2022 % 0.12/0.34 % CPUTime : % 3.14/3.35 (* PROOF-FOUND *) % 3.14/3.35 % SZS status Unsatisfiable % 3.14/3.35 (* BEGIN-PROOF *) % 3.14/3.35 % SZS output start Proof % 3.14/3.35 Theorem zenon_thm : False. % 3.14/3.35 Proof. % 3.14/3.35 assert (zenon_L1_ : (((op (e1) (e1)) = (e1))/\(~((op (e1) (e1)) = (e1)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H1d. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1d). zenon_intro zenon_H1f. zenon_intro zenon_H1e. % 3.14/3.35 exact (zenon_H1e zenon_H1f). % 3.14/3.35 (* end of lemma zenon_L1_ *) % 3.14/3.35 assert (zenon_L2_ : (~((e2) = (e2))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H20. % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L2_ *) % 3.14/3.35 assert (zenon_L3_ : (((op (e0) (e0)) = (e3))/\(~((op (e3) (e3)) = (e0)))) -> ((op (e0) (e0)) = (e2)) -> (~((e2) = (e3))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H21 zenon_H22 zenon_H23. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H21). zenon_intro zenon_H25. zenon_intro zenon_H24. % 3.14/3.35 elim (classic ((e3) = (e3))); [ zenon_intro zenon_H26 | zenon_intro zenon_H27 ]. % 3.14/3.35 cut (((e3) = (e3)) = ((e2) = (e3))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H23. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H26. % 3.14/3.35 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H27]. % 3.14/3.35 cut (((e3) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H28]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e0) (e0)) = (e2)) = ((e3) = (e2))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H28. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H22. % 3.14/3.35 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 3.14/3.35 cut (((op (e0) (e0)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H29]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H29 zenon_H25). % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L3_ *) % 3.14/3.35 assert (zenon_L4_ : (~((e3) = (e3))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H27. % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L4_ *) % 3.14/3.35 assert (zenon_L5_ : (~((e0) = (e3))) -> ((op (e1) (e1)) = (e3)) -> ((op (e1) (e1)) = (e0)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H2a zenon_H2b zenon_H2c. % 3.14/3.35 cut (((op (e1) (e1)) = (e3)) = ((e0) = (e3))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H2a. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H2b. % 3.14/3.35 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H27]. % 3.14/3.35 cut (((op (e1) (e1)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H2d]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H2d zenon_H2c). % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L5_ *) % 3.14/3.35 assert (zenon_L6_ : (((op (e1) (e1)) = (e3))/\(~((op (e3) (e3)) = (e1)))) -> ((op (e1) (e1)) = (e0)) -> (~((e0) = (e3))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H2e zenon_H2c zenon_H2a. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H2e). zenon_intro zenon_H2b. zenon_intro zenon_H2f. % 3.14/3.35 apply (zenon_L5_); trivial. % 3.14/3.35 (* end of lemma zenon_L6_ *) % 3.14/3.35 assert (zenon_L7_ : (~((e1) = (e1))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H30. % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L7_ *) % 3.14/3.35 assert (zenon_L8_ : ((op (e2) (e2)) = (e1)) -> ((op (e2) (e2)) = (e3)) -> (~((e1) = (e3))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H31 zenon_H32 zenon_H33. % 3.14/3.35 elim (classic ((e3) = (e3))); [ zenon_intro zenon_H26 | zenon_intro zenon_H27 ]. % 3.14/3.35 cut (((e3) = (e3)) = ((e1) = (e3))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H33. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H26. % 3.14/3.35 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H27]. % 3.14/3.35 cut (((e3) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H34]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e2) (e2)) = (e1)) = ((e3) = (e1))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H34. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H31. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((op (e2) (e2)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H35]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H35 zenon_H32). % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L8_ *) % 3.14/3.35 assert (zenon_L9_ : (((op (e2) (e2)) = (e3))/\(~((op (e3) (e3)) = (e2)))) -> ((op (e2) (e2)) = (e1)) -> (~((e1) = (e3))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H36 zenon_H31 zenon_H33. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H36). zenon_intro zenon_H32. zenon_intro zenon_H37. % 3.14/3.35 apply (zenon_L8_); trivial. % 3.14/3.35 (* end of lemma zenon_L9_ *) % 3.14/3.35 assert (zenon_L10_ : (((op (e3) (e3)) = (e3))/\(~((op (e3) (e3)) = (e3)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H38. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H38). zenon_intro zenon_H3a. zenon_intro zenon_H39. % 3.14/3.35 exact (zenon_H39 zenon_H3a). % 3.14/3.35 (* end of lemma zenon_L10_ *) % 3.14/3.35 assert (zenon_L11_ : (((op (e1) (e1)) = (e2))/\(~((op (e2) (e2)) = (e1)))) -> (~((op (e1) (e1)) = (e2))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H3b zenon_H3c. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H3b). zenon_intro zenon_H3e. zenon_intro zenon_H3d. % 3.14/3.35 exact (zenon_H3c zenon_H3e). % 3.14/3.35 (* end of lemma zenon_L11_ *) % 3.14/3.35 assert (zenon_L12_ : (((op (e2) (e2)) = (e2))/\(~((op (e2) (e2)) = (e2)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H3f. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H3f). zenon_intro zenon_H41. zenon_intro zenon_H40. % 3.14/3.35 exact (zenon_H40 zenon_H41). % 3.14/3.35 (* end of lemma zenon_L12_ *) % 3.14/3.35 assert (zenon_L13_ : ((op (e3) (e0)) = (e0)) -> ((op (e2) (e0)) = (e0)) -> (~((op (e2) (e0)) = (op (e3) (e0)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H42 zenon_H43 zenon_H44. % 3.14/3.35 elim (classic ((op (e3) (e0)) = (op (e3) (e0)))); [ zenon_intro zenon_H45 | zenon_intro zenon_H46 ]. % 3.14/3.35 cut (((op (e3) (e0)) = (op (e3) (e0))) = ((op (e2) (e0)) = (op (e3) (e0)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H44. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H45. % 3.14/3.35 cut (((op (e3) (e0)) = (op (e3) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H46]. % 3.14/3.35 cut (((op (e3) (e0)) = (op (e2) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H47]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e0)) = (e0)) = ((op (e3) (e0)) = (op (e2) (e0)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H47. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H42. % 3.14/3.35 cut (((e0) = (op (e2) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H48]. % 3.14/3.35 cut (((op (e3) (e0)) = (op (e3) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H46]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H46. apply refl_equal. % 3.14/3.35 apply zenon_H48. apply sym_equal. exact zenon_H43. % 3.14/3.35 apply zenon_H46. apply refl_equal. % 3.14/3.35 apply zenon_H46. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L13_ *) % 3.14/3.35 assert (zenon_L14_ : (~((op (e1) (e1)) = (op (e3) (e1)))) -> ((op (e1) (e1)) = (e0)) -> ((op (e3) (e1)) = (e0)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H49 zenon_H2c zenon_H4a. % 3.14/3.35 cut (((op (e1) (e1)) = (e0)) = ((op (e1) (e1)) = (op (e3) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H49. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H2c. % 3.14/3.35 cut (((e0) = (op (e3) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H4b]. % 3.14/3.35 cut (((op (e1) (e1)) = (op (e1) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H4c. apply refl_equal. % 3.14/3.35 apply zenon_H4b. apply sym_equal. exact zenon_H4a. % 3.14/3.35 (* end of lemma zenon_L14_ *) % 3.14/3.35 assert (zenon_L15_ : (~((op (e3) (e0)) = (op (e3) (e2)))) -> ((op (e3) (e0)) = (e0)) -> ((op (e3) (e2)) = (e0)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H4d zenon_H42 zenon_H4e. % 3.14/3.35 cut (((op (e3) (e0)) = (e0)) = ((op (e3) (e0)) = (op (e3) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H4d. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H42. % 3.14/3.35 cut (((e0) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H4f]. % 3.14/3.35 cut (((op (e3) (e0)) = (op (e3) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H46]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H46. apply refl_equal. % 3.14/3.35 apply zenon_H4f. apply sym_equal. exact zenon_H4e. % 3.14/3.35 (* end of lemma zenon_L15_ *) % 3.14/3.35 assert (zenon_L16_ : (~((e0) = (e0))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H50. % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L16_ *) % 3.14/3.35 assert (zenon_L17_ : (~((op (op (e0) (e0)) (e0)) = (op (e3) (e0)))) -> ((op (e0) (e0)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H51 zenon_H25. % 3.14/3.35 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 3.14/3.35 cut (((op (e0) (e0)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H29]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H29 zenon_H25). % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L17_ *) % 3.14/3.35 assert (zenon_L18_ : (~((op (op (e0) (e0)) (op (e0) (e0))) = (op (e3) (e3)))) -> ((op (e0) (e0)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H52 zenon_H25. % 3.14/3.35 cut (((op (e0) (e0)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H29]. % 3.14/3.35 cut (((op (e0) (e0)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H29]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H29 zenon_H25). % 3.14/3.35 exact (zenon_H29 zenon_H25). % 3.14/3.35 (* end of lemma zenon_L18_ *) % 3.14/3.35 assert (zenon_L19_ : ((op (e3) (e0)) = (e1)) -> ((op (e3) (e3)) = (e2)) -> ((op (e0) (e0)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H53 zenon_H54 zenon_H25. % 3.14/3.35 apply (zenon_notand_s _ _ ax14); [ zenon_intro zenon_H56 | zenon_intro zenon_H55 ]. % 3.14/3.35 elim (classic ((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0)))); [ zenon_intro zenon_H57 | zenon_intro zenon_H58 ]. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0))) = ((e1) = (op (op (e0) (e0)) (e0)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H56. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H57. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H58]. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H59]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e0)) = (e1)) = ((op (op (e0) (e0)) (e0)) = (e1))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H59. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H53. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((op (e3) (e0)) = (op (op (e0) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H5a]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0)))); [ zenon_intro zenon_H57 | zenon_intro zenon_H58 ]. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0))) = ((op (e3) (e0)) = (op (op (e0) (e0)) (e0)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H5a. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H57. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H58]. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (op (e3) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H51]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L17_); trivial. % 3.14/3.35 apply zenon_H58. apply refl_equal. % 3.14/3.35 apply zenon_H58. apply refl_equal. % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 apply zenon_H58. apply refl_equal. % 3.14/3.35 apply zenon_H58. apply refl_equal. % 3.14/3.35 apply (zenon_notand_s _ _ zenon_H55); [ zenon_intro zenon_H5c | zenon_intro zenon_H5b ]. % 3.14/3.35 elim (classic ((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0))))); [ zenon_intro zenon_H5d | zenon_intro zenon_H5e ]. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0)))) = ((e2) = (op (op (e0) (e0)) (op (e0) (e0))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H5c. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H5d. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H5e]. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5f]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e2)) = ((op (op (e0) (e0)) (op (e0) (e0))) = (e2))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H5f. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H54. % 3.14/3.35 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (op (e0) (e0)) (op (e0) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H60]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0))))); [ zenon_intro zenon_H5d | zenon_intro zenon_H5e ]. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0)))) = ((op (e3) (e3)) = (op (op (e0) (e0)) (op (e0) (e0))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H60. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H5d. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H5e]. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H52]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L18_); trivial. % 3.14/3.35 apply zenon_H5e. apply refl_equal. % 3.14/3.35 apply zenon_H5e. apply refl_equal. % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 apply zenon_H5e. apply refl_equal. % 3.14/3.35 apply zenon_H5e. apply refl_equal. % 3.14/3.35 apply zenon_H5b. apply sym_equal. exact zenon_H25. % 3.14/3.35 (* end of lemma zenon_L19_ *) % 3.14/3.35 assert (zenon_L20_ : ((op (e3) (e3)) = (e2)) -> ((op (e3) (e0)) = (e2)) -> (~((op (e3) (e0)) = (op (e3) (e3)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H54 zenon_H61 zenon_H62. % 3.14/3.35 elim (classic ((op (e3) (e3)) = (op (e3) (e3)))); [ zenon_intro zenon_H63 | zenon_intro zenon_H64 ]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3))) = ((op (e3) (e0)) = (op (e3) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H62. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H63. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e2)) = ((op (e3) (e3)) = (op (e3) (e0)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H65. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H54. % 3.14/3.35 cut (((e2) = (op (e3) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H66]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_H66. apply sym_equal. exact zenon_H61. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L20_ *) % 3.14/3.35 assert (zenon_L21_ : (~((op (e0) (e0)) = (op (e3) (e0)))) -> ((op (e0) (e0)) = (e3)) -> ((op (e3) (e0)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H67 zenon_H25 zenon_H68. % 3.14/3.35 cut (((op (e0) (e0)) = (e3)) = ((op (e0) (e0)) = (op (e3) (e0)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H67. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H25. % 3.14/3.35 cut (((e3) = (op (e3) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H69]. % 3.14/3.35 cut (((op (e0) (e0)) = (op (e0) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H6a]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H6a. apply refl_equal. % 3.14/3.35 apply zenon_H69. apply sym_equal. exact zenon_H68. % 3.14/3.35 (* end of lemma zenon_L21_ *) % 3.14/3.35 assert (zenon_L22_ : (((op (e3) (e0)) = (e0))\/(((op (e3) (e0)) = (e1))\/(((op (e3) (e0)) = (e2))\/((op (e3) (e0)) = (e3))))) -> ((op (e3) (e2)) = (e0)) -> (~((op (e3) (e0)) = (op (e3) (e2)))) -> (~((op (e3) (e0)) = (op (e3) (e3)))) -> ((op (e3) (e3)) = (e2)) -> (~((op (e0) (e0)) = (op (e3) (e0)))) -> ((op (e0) (e0)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H6b zenon_H4e zenon_H4d zenon_H62 zenon_H54 zenon_H67 zenon_H25. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H6b); [ zenon_intro zenon_H42 | zenon_intro zenon_H6c ]. % 3.14/3.35 apply (zenon_L15_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H6c); [ zenon_intro zenon_H53 | zenon_intro zenon_H6d ]. % 3.14/3.35 apply (zenon_L19_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H6d); [ zenon_intro zenon_H61 | zenon_intro zenon_H68 ]. % 3.14/3.35 apply (zenon_L20_); trivial. % 3.14/3.35 apply (zenon_L21_); trivial. % 3.14/3.35 (* end of lemma zenon_L22_ *) % 3.14/3.35 assert (zenon_L23_ : (((op (e3) (e0)) = (e0))\/(((op (e3) (e1)) = (e0))\/(((op (e3) (e2)) = (e0))\/((op (e3) (e3)) = (e0))))) -> (~((op (e2) (e0)) = (op (e3) (e0)))) -> ((op (e2) (e0)) = (e0)) -> ((op (e1) (e1)) = (e0)) -> (~((op (e1) (e1)) = (op (e3) (e1)))) -> ((op (e0) (e0)) = (e3)) -> (~((op (e0) (e0)) = (op (e3) (e0)))) -> ((op (e3) (e3)) = (e2)) -> (~((op (e3) (e0)) = (op (e3) (e3)))) -> (~((op (e3) (e0)) = (op (e3) (e2)))) -> (((op (e3) (e0)) = (e0))\/(((op (e3) (e0)) = (e1))\/(((op (e3) (e0)) = (e2))\/((op (e3) (e0)) = (e3))))) -> (~((op (e3) (e3)) = (e0))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H6e zenon_H44 zenon_H43 zenon_H2c zenon_H49 zenon_H25 zenon_H67 zenon_H54 zenon_H62 zenon_H4d zenon_H6b zenon_H24. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H6e); [ zenon_intro zenon_H42 | zenon_intro zenon_H6f ]. % 3.14/3.35 apply (zenon_L13_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H6f); [ zenon_intro zenon_H4a | zenon_intro zenon_H70 ]. % 3.14/3.35 apply (zenon_L14_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H70); [ zenon_intro zenon_H4e | zenon_intro zenon_H71 ]. % 3.14/3.35 apply (zenon_L22_); trivial. % 3.14/3.35 exact (zenon_H24 zenon_H71). % 3.14/3.35 (* end of lemma zenon_L23_ *) % 3.14/3.35 assert (zenon_L24_ : (~((op (e1) (e1)) = (op (e2) (e1)))) -> ((op (e1) (e1)) = (e0)) -> ((op (e2) (e1)) = (e0)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H72 zenon_H2c zenon_H73. % 3.14/3.35 cut (((op (e1) (e1)) = (e0)) = ((op (e1) (e1)) = (op (e2) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H72. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H2c. % 3.14/3.35 cut (((e0) = (op (e2) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H74]. % 3.14/3.35 cut (((op (e1) (e1)) = (op (e1) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H4c. apply refl_equal. % 3.14/3.35 apply zenon_H74. apply sym_equal. exact zenon_H73. % 3.14/3.35 (* end of lemma zenon_L24_ *) % 3.14/3.35 assert (zenon_L25_ : ((op (e2) (e2)) = (e0)) -> ((op (e2) (e2)) = (e1)) -> (~((e0) = (e1))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H75 zenon_H31 zenon_H76. % 3.14/3.35 elim (classic ((e1) = (e1))); [ zenon_intro zenon_H77 | zenon_intro zenon_H30 ]. % 3.14/3.35 cut (((e1) = (e1)) = ((e0) = (e1))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H76. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H77. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((e1) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H78]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e2) (e2)) = (e0)) = ((e1) = (e0))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H78. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H75. % 3.14/3.35 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 3.14/3.35 cut (((op (e2) (e2)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H3d]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H3d zenon_H31). % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L25_ *) % 3.14/3.35 assert (zenon_L26_ : (~((op (op (e3) (e3)) (e3)) = (op (e2) (e3)))) -> ((op (e3) (e3)) = (e2)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H79 zenon_H54. % 3.14/3.35 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H27]. % 3.14/3.35 cut (((op (e3) (e3)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H37]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H37 zenon_H54). % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L26_ *) % 3.14/3.35 assert (zenon_L27_ : (~((op (op (e3) (e3)) (op (e3) (e3))) = (op (e2) (e2)))) -> ((op (e3) (e3)) = (e2)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H7a zenon_H54. % 3.14/3.35 cut (((op (e3) (e3)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H37]. % 3.14/3.35 cut (((op (e3) (e3)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H37]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H37 zenon_H54). % 3.14/3.35 exact (zenon_H37 zenon_H54). % 3.14/3.35 (* end of lemma zenon_L27_ *) % 3.14/3.35 assert (zenon_L28_ : ((op (e2) (e3)) = (e0)) -> ((op (e2) (e2)) = (e1)) -> ((op (e3) (e3)) = (e2)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H7b zenon_H31 zenon_H54. % 3.14/3.35 apply (zenon_notand_s _ _ ax7); [ zenon_intro zenon_H7d | zenon_intro zenon_H7c ]. % 3.14/3.35 elim (classic ((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3)))); [ zenon_intro zenon_H7e | zenon_intro zenon_H7f ]. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3))) = ((e0) = (op (op (e3) (e3)) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H7d. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H7e. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H7f]. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H80]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e2) (e3)) = (e0)) = ((op (op (e3) (e3)) (e3)) = (e0))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H80. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H7b. % 3.14/3.35 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 3.14/3.35 cut (((op (e2) (e3)) = (op (op (e3) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H81]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3)))); [ zenon_intro zenon_H7e | zenon_intro zenon_H7f ]. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3))) = ((op (e2) (e3)) = (op (op (e3) (e3)) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H81. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H7e. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H7f]. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H79]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L26_); trivial. % 3.14/3.35 apply zenon_H7f. apply refl_equal. % 3.14/3.35 apply zenon_H7f. apply refl_equal. % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 apply zenon_H7f. apply refl_equal. % 3.14/3.35 apply zenon_H7f. apply refl_equal. % 3.14/3.35 apply (zenon_notand_s _ _ zenon_H7c); [ zenon_intro zenon_H83 | zenon_intro zenon_H82 ]. % 3.14/3.35 elim (classic ((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3))))); [ zenon_intro zenon_H84 | zenon_intro zenon_H85 ]. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3)))) = ((e1) = (op (op (e3) (e3)) (op (e3) (e3))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H83. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H84. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H85]. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H86]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e2) (e2)) = (e1)) = ((op (op (e3) (e3)) (op (e3) (e3))) = (e1))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H86. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H31. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((op (e2) (e2)) = (op (op (e3) (e3)) (op (e3) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H87]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3))))); [ zenon_intro zenon_H84 | zenon_intro zenon_H85 ]. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3)))) = ((op (e2) (e2)) = (op (op (e3) (e3)) (op (e3) (e3))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H87. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H84. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H85]. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (e2) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H7a]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L27_); trivial. % 3.14/3.35 apply zenon_H85. apply refl_equal. % 3.14/3.35 apply zenon_H85. apply refl_equal. % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 apply zenon_H85. apply refl_equal. % 3.14/3.35 apply zenon_H85. apply refl_equal. % 3.14/3.35 apply zenon_H82. apply sym_equal. exact zenon_H54. % 3.14/3.35 (* end of lemma zenon_L28_ *) % 3.14/3.35 assert (zenon_L29_ : (((op (e2) (e2)) = (e3))/\(~((op (e3) (e3)) = (e2)))) -> (~((op (e2) (e2)) = (e3))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H36 zenon_H35. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H36). zenon_intro zenon_H32. zenon_intro zenon_H37. % 3.14/3.35 exact (zenon_H35 zenon_H32). % 3.14/3.35 (* end of lemma zenon_L29_ *) % 3.14/3.35 assert (zenon_L30_ : (((op (e1) (e1)) = (e3))/\(~((op (e3) (e3)) = (e1)))) -> (~((op (e1) (e1)) = (e3))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H2e zenon_H88. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H2e). zenon_intro zenon_H2b. zenon_intro zenon_H2f. % 3.14/3.35 exact (zenon_H88 zenon_H2b). % 3.14/3.35 (* end of lemma zenon_L30_ *) % 3.14/3.35 assert (zenon_L31_ : (~((op (e0) (e0)) = (op (e0) (e1)))) -> ((op (e0) (e0)) = (e2)) -> ((op (e0) (e1)) = (e2)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H89 zenon_H22 zenon_H8a. % 3.14/3.35 cut (((op (e0) (e0)) = (e2)) = ((op (e0) (e0)) = (op (e0) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H89. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H22. % 3.14/3.35 cut (((e2) = (op (e0) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H8b]. % 3.14/3.35 cut (((op (e0) (e0)) = (op (e0) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H6a]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H6a. apply refl_equal. % 3.14/3.35 apply zenon_H8b. apply sym_equal. exact zenon_H8a. % 3.14/3.35 (* end of lemma zenon_L31_ *) % 3.14/3.35 assert (zenon_L32_ : (~((e0) = (e2))) -> ((op (e1) (e1)) = (e2)) -> ((op (e1) (e1)) = (e0)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H8c zenon_H3e zenon_H2c. % 3.14/3.35 cut (((op (e1) (e1)) = (e2)) = ((e0) = (e2))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H8c. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H3e. % 3.14/3.35 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 3.14/3.35 cut (((op (e1) (e1)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H2d]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H2d zenon_H2c). % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L32_ *) % 3.14/3.35 assert (zenon_L33_ : ((op (e2) (e0)) = (e1)) -> ((op (e0) (e0)) = (e2)) -> (~((e1) = (op (op (e0) (e0)) (e0)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H8d zenon_H22 zenon_H56. % 3.14/3.35 elim (classic ((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0)))); [ zenon_intro zenon_H57 | zenon_intro zenon_H58 ]. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0))) = ((e1) = (op (op (e0) (e0)) (e0)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H56. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H57. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H58]. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H59]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e2) (e0)) = (e1)) = ((op (op (e0) (e0)) (e0)) = (e1))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H59. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H8d. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((op (e2) (e0)) = (op (op (e0) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H8e]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0)))); [ zenon_intro zenon_H57 | zenon_intro zenon_H58 ]. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0))) = ((op (e2) (e0)) = (op (op (e0) (e0)) (e0)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H8e. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H57. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H58]. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (op (e2) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 3.14/3.35 cut (((op (e0) (e0)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H90]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H90 zenon_H22). % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 apply zenon_H58. apply refl_equal. % 3.14/3.35 apply zenon_H58. apply refl_equal. % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 apply zenon_H58. apply refl_equal. % 3.14/3.35 apply zenon_H58. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L33_ *) % 3.14/3.35 assert (zenon_L34_ : ((op (e2) (e0)) = (e1)) -> ((op (e2) (e2)) = (e3)) -> ((op (e0) (e0)) = (e2)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H8d zenon_H32 zenon_H22. % 3.14/3.35 apply (zenon_notand_s _ _ ax16); [ zenon_intro zenon_H56 | zenon_intro zenon_H91 ]. % 3.14/3.35 apply (zenon_L33_); trivial. % 3.14/3.35 apply (zenon_notand_s _ _ zenon_H91); [ zenon_intro zenon_H93 | zenon_intro zenon_H92 ]. % 3.14/3.35 elim (classic ((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0))))); [ zenon_intro zenon_H5d | zenon_intro zenon_H5e ]. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0)))) = ((e3) = (op (op (e0) (e0)) (op (e0) (e0))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H93. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H5d. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H5e]. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H94]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e2) (e2)) = (e3)) = ((op (op (e0) (e0)) (op (e0) (e0))) = (e3))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H94. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H32. % 3.14/3.35 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H27]. % 3.14/3.35 cut (((op (e2) (e2)) = (op (op (e0) (e0)) (op (e0) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H95]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0))))); [ zenon_intro zenon_H5d | zenon_intro zenon_H5e ]. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0)))) = ((op (e2) (e2)) = (op (op (e0) (e0)) (op (e0) (e0))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H95. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H5d. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H5e]. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (e2) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H96]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e0) (e0)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H90]. % 3.14/3.35 cut (((op (e0) (e0)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H90]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H90 zenon_H22). % 3.14/3.35 exact (zenon_H90 zenon_H22). % 3.14/3.35 apply zenon_H5e. apply refl_equal. % 3.14/3.35 apply zenon_H5e. apply refl_equal. % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 apply zenon_H5e. apply refl_equal. % 3.14/3.35 apply zenon_H5e. apply refl_equal. % 3.14/3.35 apply zenon_H92. apply sym_equal. exact zenon_H22. % 3.14/3.35 (* end of lemma zenon_L34_ *) % 3.14/3.35 assert (zenon_L35_ : (~((op (e2) (e0)) = (op (e2) (e1)))) -> ((op (e2) (e0)) = (e1)) -> ((op (e2) (e1)) = (e1)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H97 zenon_H8d zenon_H98. % 3.14/3.35 cut (((op (e2) (e0)) = (e1)) = ((op (e2) (e0)) = (op (e2) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H97. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H8d. % 3.14/3.35 cut (((e1) = (op (e2) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H99]. % 3.14/3.35 cut (((op (e2) (e0)) = (op (e2) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H9a]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H9a. apply refl_equal. % 3.14/3.35 apply zenon_H99. apply sym_equal. exact zenon_H98. % 3.14/3.35 (* end of lemma zenon_L35_ *) % 3.14/3.35 assert (zenon_L36_ : (~((op (e2) (e0)) = (op (e2) (e1)))) -> ((op (e2) (e0)) = (e2)) -> ((op (e2) (e1)) = (e2)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H97 zenon_H9b zenon_H9c. % 3.14/3.35 cut (((op (e2) (e0)) = (e2)) = ((op (e2) (e0)) = (op (e2) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H97. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H9b. % 3.14/3.35 cut (((e2) = (op (e2) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H9d]. % 3.14/3.35 cut (((op (e2) (e0)) = (op (e2) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H9a]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H9a. apply refl_equal. % 3.14/3.35 apply zenon_H9d. apply sym_equal. exact zenon_H9c. % 3.14/3.35 (* end of lemma zenon_L36_ *) % 3.14/3.35 assert (zenon_L37_ : ((op (e2) (e2)) = (e3)) -> ((op (e2) (e0)) = (e3)) -> (~((op (e2) (e0)) = (op (e2) (e2)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H32 zenon_H9e zenon_H9f. % 3.14/3.35 elim (classic ((op (e2) (e2)) = (op (e2) (e2)))); [ zenon_intro zenon_Ha0 | zenon_intro zenon_Ha1 ]. % 3.14/3.35 cut (((op (e2) (e2)) = (op (e2) (e2))) = ((op (e2) (e0)) = (op (e2) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H9f. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Ha0. % 3.14/3.35 cut (((op (e2) (e2)) = (op (e2) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Ha1]. % 3.14/3.35 cut (((op (e2) (e2)) = (op (e2) (e0)))); [idtac | apply NNPP; zenon_intro zenon_Ha2]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e2) (e2)) = (e3)) = ((op (e2) (e2)) = (op (e2) (e0)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Ha2. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H32. % 3.14/3.35 cut (((e3) = (op (e2) (e0)))); [idtac | apply NNPP; zenon_intro zenon_Ha3]. % 3.14/3.35 cut (((op (e2) (e2)) = (op (e2) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Ha1]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_Ha1. apply refl_equal. % 3.14/3.35 apply zenon_Ha3. apply sym_equal. exact zenon_H9e. % 3.14/3.35 apply zenon_Ha1. apply refl_equal. % 3.14/3.35 apply zenon_Ha1. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L37_ *) % 3.14/3.35 assert (zenon_L38_ : (((op (e2) (e0)) = (e0))\/(((op (e2) (e0)) = (e1))\/(((op (e2) (e0)) = (e2))\/((op (e2) (e0)) = (e3))))) -> (~((op (e2) (e0)) = (op (e3) (e0)))) -> ((op (e3) (e0)) = (e0)) -> ((op (e2) (e1)) = (e1)) -> ((op (e2) (e1)) = (e2)) -> (~((op (e2) (e0)) = (op (e2) (e1)))) -> ((op (e2) (e2)) = (e3)) -> (~((op (e2) (e0)) = (op (e2) (e2)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_Ha4 zenon_H44 zenon_H42 zenon_H98 zenon_H9c zenon_H97 zenon_H32 zenon_H9f. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Ha4); [ zenon_intro zenon_H43 | zenon_intro zenon_Ha5 ]. % 3.14/3.35 apply (zenon_L13_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Ha5); [ zenon_intro zenon_H8d | zenon_intro zenon_Ha6 ]. % 3.14/3.35 apply (zenon_L35_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Ha6); [ zenon_intro zenon_H9b | zenon_intro zenon_H9e ]. % 3.14/3.35 apply (zenon_L36_); trivial. % 3.14/3.35 apply (zenon_L37_); trivial. % 3.14/3.35 (* end of lemma zenon_L38_ *) % 3.14/3.35 assert (zenon_L39_ : (~((op (op (e2) (e2)) (e2)) = (op (e3) (e2)))) -> ((op (e2) (e2)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Ha7 zenon_H32. % 3.14/3.35 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 3.14/3.35 cut (((op (e2) (e2)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H35]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H35 zenon_H32). % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L39_ *) % 3.14/3.35 assert (zenon_L40_ : (~((op (op (e2) (e2)) (op (e2) (e2))) = (op (e3) (e3)))) -> ((op (e2) (e2)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Ha8 zenon_H32. % 3.14/3.35 cut (((op (e2) (e2)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H35]. % 3.14/3.35 cut (((op (e2) (e2)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H35]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H35 zenon_H32). % 3.14/3.35 exact (zenon_H35 zenon_H32). % 3.14/3.35 (* end of lemma zenon_L40_ *) % 3.14/3.35 assert (zenon_L41_ : ((op (e3) (e2)) = (e0)) -> ((op (e3) (e3)) = (e1)) -> ((op (e2) (e2)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H4e zenon_Ha9 zenon_H32. % 3.14/3.35 apply (zenon_notand_s _ _ ax6); [ zenon_intro zenon_Hab | zenon_intro zenon_Haa ]. % 3.14/3.35 elim (classic ((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2)))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2))) = ((e0) = (op (op (e2) (e2)) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hab. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hac. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e2)) = (e0)) = ((op (op (e2) (e2)) (e2)) = (e0))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hae. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H4e. % 3.14/3.35 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 3.14/3.35 cut (((op (e3) (e2)) = (op (op (e2) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Haf]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2)))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2))) = ((op (e3) (e2)) = (op (op (e2) (e2)) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Haf. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hac. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Ha7]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L39_); trivial. % 3.14/3.35 apply zenon_Had. apply refl_equal. % 3.14/3.35 apply zenon_Had. apply refl_equal. % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 apply zenon_Had. apply refl_equal. % 3.14/3.35 apply zenon_Had. apply refl_equal. % 3.14/3.35 apply (zenon_notand_s _ _ zenon_Haa); [ zenon_intro zenon_Hb1 | zenon_intro zenon_Hb0 ]. % 3.14/3.35 elim (classic ((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2))))); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hb3 ]. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2)))) = ((e1) = (op (op (e2) (e2)) (op (e2) (e2))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hb1. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hb2. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2))))); [idtac | apply NNPP; zenon_intro zenon_Hb3]. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (e1))); [idtac | apply NNPP; zenon_intro zenon_Hb4]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e1)) = ((op (op (e2) (e2)) (op (e2) (e2))) = (e1))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hb4. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Ha9. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (op (e2) (e2)) (op (e2) (e2))))); [idtac | apply NNPP; zenon_intro zenon_Hb5]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2))))); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hb3 ]. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2)))) = ((op (e3) (e3)) = (op (op (e2) (e2)) (op (e2) (e2))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hb5. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hb2. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2))))); [idtac | apply NNPP; zenon_intro zenon_Hb3]. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Ha8]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L40_); trivial. % 3.14/3.35 apply zenon_Hb3. apply refl_equal. % 3.14/3.35 apply zenon_Hb3. apply refl_equal. % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 apply zenon_Hb3. apply refl_equal. % 3.14/3.35 apply zenon_Hb3. apply refl_equal. % 3.14/3.35 apply zenon_Hb0. apply sym_equal. exact zenon_H32. % 3.14/3.35 (* end of lemma zenon_L41_ *) % 3.14/3.35 assert (zenon_L42_ : ((op (e3) (e3)) = (e0)) -> ((op (e3) (e3)) = (e1)) -> (~((e0) = (e1))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H71 zenon_Ha9 zenon_H76. % 3.14/3.35 elim (classic ((e1) = (e1))); [ zenon_intro zenon_H77 | zenon_intro zenon_H30 ]. % 3.14/3.35 cut (((e1) = (e1)) = ((e0) = (e1))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H76. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H77. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((e1) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H78]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e0)) = ((e1) = (e0))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H78. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H71. % 3.14/3.35 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 3.14/3.35 cut (((op (e3) (e3)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H2f]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H2f zenon_Ha9). % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L42_ *) % 3.14/3.35 assert (zenon_L43_ : (((op (e3) (e3)) = (e1))/\(~((op (e1) (e1)) = (e3)))) -> ((op (e3) (e3)) = (e0)) -> (~((e0) = (e1))) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hb6 zenon_H71 zenon_H76. % 3.14/3.35 apply (zenon_and_s _ _ zenon_Hb6). zenon_intro zenon_Ha9. zenon_intro zenon_H88. % 3.14/3.35 apply (zenon_L42_); trivial. % 3.14/3.35 (* end of lemma zenon_L43_ *) % 3.14/3.35 assert (zenon_L44_ : (((op (e3) (e0)) = (e0))\/(((op (e3) (e1)) = (e0))\/(((op (e3) (e2)) = (e0))\/((op (e3) (e3)) = (e0))))) -> (~((op (e2) (e0)) = (op (e2) (e2)))) -> (~((op (e2) (e0)) = (op (e2) (e1)))) -> ((op (e2) (e1)) = (e2)) -> ((op (e2) (e1)) = (e1)) -> (~((op (e2) (e0)) = (op (e3) (e0)))) -> (((op (e2) (e0)) = (e0))\/(((op (e2) (e0)) = (e1))\/(((op (e2) (e0)) = (e2))\/((op (e2) (e0)) = (e3))))) -> ((op (e1) (e1)) = (e0)) -> (~((op (e1) (e1)) = (op (e3) (e1)))) -> ((op (e2) (e2)) = (e3)) -> ((op (e3) (e3)) = (e1)) -> (((op (e3) (e3)) = (e1))/\(~((op (e1) (e1)) = (e3)))) -> (~((e0) = (e1))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H6e zenon_H9f zenon_H97 zenon_H9c zenon_H98 zenon_H44 zenon_Ha4 zenon_H2c zenon_H49 zenon_H32 zenon_Ha9 zenon_Hb6 zenon_H76. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H6e); [ zenon_intro zenon_H42 | zenon_intro zenon_H6f ]. % 3.14/3.35 apply (zenon_L38_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H6f); [ zenon_intro zenon_H4a | zenon_intro zenon_H70 ]. % 3.14/3.35 apply (zenon_L14_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H70); [ zenon_intro zenon_H4e | zenon_intro zenon_H71 ]. % 3.14/3.35 apply (zenon_L41_); trivial. % 3.14/3.35 apply (zenon_L43_); trivial. % 3.14/3.35 (* end of lemma zenon_L44_ *) % 3.14/3.35 assert (zenon_L45_ : ((op (e3) (e3)) = (e1)) -> ((op (e2) (e3)) = (e1)) -> (~((op (e2) (e3)) = (op (e3) (e3)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_Ha9 zenon_Hb7 zenon_Hb8. % 3.14/3.35 elim (classic ((op (e3) (e3)) = (op (e3) (e3)))); [ zenon_intro zenon_H63 | zenon_intro zenon_H64 ]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3))) = ((op (e2) (e3)) = (op (e3) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hb8. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H63. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hb9]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e1)) = ((op (e3) (e3)) = (op (e2) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hb9. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Ha9. % 3.14/3.35 cut (((e1) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hba]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_Hba. apply sym_equal. exact zenon_Hb7. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L45_ *) % 3.14/3.35 assert (zenon_L46_ : ((op (e3) (e3)) = (e1)) -> ((op (e3) (e2)) = (e1)) -> (~((op (e3) (e2)) = (op (e3) (e3)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_Ha9 zenon_Hbb zenon_Hbc. % 3.14/3.35 elim (classic ((op (e3) (e3)) = (op (e3) (e3)))); [ zenon_intro zenon_H63 | zenon_intro zenon_H64 ]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3))) = ((op (e3) (e2)) = (op (e3) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hbc. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H63. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hbd]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e1)) = ((op (e3) (e3)) = (op (e3) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hbd. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Ha9. % 3.14/3.35 cut (((e1) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hbe]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_Hbe. apply sym_equal. exact zenon_Hbb. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L46_ *) % 3.14/3.35 assert (zenon_L47_ : (~((op (e3) (e1)) = (op (e3) (e2)))) -> ((op (e3) (e1)) = (e2)) -> ((op (e3) (e2)) = (e2)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hbf zenon_Hc0 zenon_Hc1. % 3.14/3.35 cut (((op (e3) (e1)) = (e2)) = ((op (e3) (e1)) = (op (e3) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hbf. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hc0. % 3.14/3.35 cut (((e2) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hc2]. % 3.14/3.35 cut (((op (e3) (e1)) = (op (e3) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hc3]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_Hc3. apply refl_equal. % 3.14/3.35 apply zenon_Hc2. apply sym_equal. exact zenon_Hc1. % 3.14/3.35 (* end of lemma zenon_L47_ *) % 3.14/3.35 assert (zenon_L48_ : (~((op (e2) (e2)) = (op (e3) (e2)))) -> ((op (e2) (e2)) = (e3)) -> ((op (e3) (e2)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hc4 zenon_H32 zenon_Hc5. % 3.14/3.35 cut (((op (e2) (e2)) = (e3)) = ((op (e2) (e2)) = (op (e3) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hc4. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H32. % 3.14/3.35 cut (((e3) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hc6]. % 3.14/3.35 cut (((op (e2) (e2)) = (op (e2) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Ha1]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_Ha1. apply refl_equal. % 3.14/3.35 apply zenon_Hc6. apply sym_equal. exact zenon_Hc5. % 3.14/3.35 (* end of lemma zenon_L48_ *) % 3.14/3.35 assert (zenon_L49_ : (((op (e3) (e2)) = (e0))\/(((op (e3) (e2)) = (e1))\/(((op (e3) (e2)) = (e2))\/((op (e3) (e2)) = (e3))))) -> (~((op (e3) (e2)) = (op (e3) (e3)))) -> ((op (e3) (e3)) = (e1)) -> ((op (e3) (e1)) = (e2)) -> (~((op (e3) (e1)) = (op (e3) (e2)))) -> (~((op (e2) (e2)) = (op (e3) (e2)))) -> ((op (e2) (e2)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hc7 zenon_Hbc zenon_Ha9 zenon_Hc0 zenon_Hbf zenon_Hc4 zenon_H32. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hc7); [ zenon_intro zenon_H4e | zenon_intro zenon_Hc8 ]. % 3.14/3.35 apply (zenon_L41_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hc8); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hc9 ]. % 3.14/3.35 apply (zenon_L46_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hc9); [ zenon_intro zenon_Hc1 | zenon_intro zenon_Hc5 ]. % 3.14/3.35 apply (zenon_L47_); trivial. % 3.14/3.35 apply (zenon_L48_); trivial. % 3.14/3.35 (* end of lemma zenon_L49_ *) % 3.14/3.35 assert (zenon_L50_ : ((op (e3) (e3)) = (e1)) -> ((op (e3) (e3)) = (e2)) -> (~((e1) = (e2))) -> False). % 3.14/3.35 do 0 intro. intros zenon_Ha9 zenon_H54 zenon_Hca. % 3.14/3.35 elim (classic ((e2) = (e2))); [ zenon_intro zenon_Hcb | zenon_intro zenon_H20 ]. % 3.14/3.35 cut (((e2) = (e2)) = ((e1) = (e2))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hca. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hcb. % 3.14/3.35 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 3.14/3.35 cut (((e2) = (e1))); [idtac | apply NNPP; zenon_intro zenon_Hcc]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e1)) = ((e2) = (e1))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hcc. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Ha9. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((op (e3) (e3)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H37]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H37 zenon_H54). % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L50_ *) % 3.14/3.35 assert (zenon_L51_ : (((op (e3) (e3)) = (e2))/\(~((op (e2) (e2)) = (e3)))) -> ((op (e3) (e3)) = (e1)) -> (~((e1) = (e2))) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hcd zenon_Ha9 zenon_Hca. % 3.14/3.35 apply (zenon_and_s _ _ zenon_Hcd). zenon_intro zenon_H54. zenon_intro zenon_H35. % 3.14/3.35 apply (zenon_L50_); trivial. % 3.14/3.35 (* end of lemma zenon_L51_ *) % 3.14/3.35 assert (zenon_L52_ : ((op (e0) (e0)) = (e1)) -> ((op (e0) (e0)) = (e2)) -> (~((e1) = (e2))) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hce zenon_H22 zenon_Hca. % 3.14/3.35 elim (classic ((e2) = (e2))); [ zenon_intro zenon_Hcb | zenon_intro zenon_H20 ]. % 3.14/3.35 cut (((e2) = (e2)) = ((e1) = (e2))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hca. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hcb. % 3.14/3.35 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 3.14/3.35 cut (((e2) = (e1))); [idtac | apply NNPP; zenon_intro zenon_Hcc]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e0) (e0)) = (e1)) = ((e2) = (e1))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hcc. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hce. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((op (e0) (e0)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H90]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H90 zenon_H22). % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L52_ *) % 3.14/3.35 assert (zenon_L53_ : (((op (e0) (e0)) = (e2))/\(~((op (e2) (e2)) = (e0)))) -> ((op (e0) (e0)) = (e1)) -> (~((e1) = (e2))) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hcf zenon_Hce zenon_Hca. % 3.14/3.35 apply (zenon_and_s _ _ zenon_Hcf). zenon_intro zenon_H22. zenon_intro zenon_Hd0. % 3.14/3.35 apply (zenon_L52_); trivial. % 3.14/3.35 (* end of lemma zenon_L53_ *) % 3.14/3.35 assert (zenon_L54_ : ((op (e0) (e0)) = (e1)) -> ((op (e0) (e0)) = (e3)) -> (~((e1) = (e3))) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hce zenon_H25 zenon_H33. % 3.14/3.35 elim (classic ((e3) = (e3))); [ zenon_intro zenon_H26 | zenon_intro zenon_H27 ]. % 3.14/3.35 cut (((e3) = (e3)) = ((e1) = (e3))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H33. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H26. % 3.14/3.35 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H27]. % 3.14/3.35 cut (((e3) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H34]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e0) (e0)) = (e1)) = ((e3) = (e1))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H34. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hce. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((op (e0) (e0)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H29]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H29 zenon_H25). % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L54_ *) % 3.14/3.35 assert (zenon_L55_ : (((op (e0) (e0)) = (e3))/\(~((op (e3) (e3)) = (e0)))) -> ((op (e0) (e0)) = (e1)) -> (~((e1) = (e3))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H21 zenon_Hce zenon_H33. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H21). zenon_intro zenon_H25. zenon_intro zenon_H24. % 3.14/3.35 apply (zenon_L54_); trivial. % 3.14/3.35 (* end of lemma zenon_L55_ *) % 3.14/3.35 assert (zenon_L56_ : ((op (e1) (e1)) = (e2)) -> ((op (e1) (e1)) = (e3)) -> (~((e2) = (e3))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H3e zenon_H2b zenon_H23. % 3.14/3.35 elim (classic ((e3) = (e3))); [ zenon_intro zenon_H26 | zenon_intro zenon_H27 ]. % 3.14/3.35 cut (((e3) = (e3)) = ((e2) = (e3))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H23. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H26. % 3.14/3.35 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H27]. % 3.14/3.35 cut (((e3) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H28]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e1) (e1)) = (e2)) = ((e3) = (e2))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H28. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H3e. % 3.14/3.35 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 3.14/3.35 cut (((op (e1) (e1)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H88]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H88 zenon_H2b). % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L56_ *) % 3.14/3.35 assert (zenon_L57_ : (((op (e1) (e1)) = (e3))/\(~((op (e3) (e3)) = (e1)))) -> ((op (e1) (e1)) = (e2)) -> (~((e2) = (e3))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H2e zenon_H3e zenon_H23. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H2e). zenon_intro zenon_H2b. zenon_intro zenon_H2f. % 3.14/3.35 apply (zenon_L56_); trivial. % 3.14/3.35 (* end of lemma zenon_L57_ *) % 3.14/3.35 assert (zenon_L58_ : (~((e0) = (e3))) -> ((op (e2) (e2)) = (e3)) -> ((op (e2) (e2)) = (e0)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H2a zenon_H32 zenon_H75. % 3.14/3.35 cut (((op (e2) (e2)) = (e3)) = ((e0) = (e3))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H2a. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H32. % 3.14/3.35 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H27]. % 3.14/3.35 cut (((op (e2) (e2)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_Hd0]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_Hd0 zenon_H75). % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L58_ *) % 3.14/3.35 assert (zenon_L59_ : (((op (e2) (e2)) = (e3))/\(~((op (e3) (e3)) = (e2)))) -> ((op (e2) (e2)) = (e0)) -> (~((e0) = (e3))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H36 zenon_H75 zenon_H2a. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H36). zenon_intro zenon_H32. zenon_intro zenon_H37. % 3.14/3.35 apply (zenon_L58_); trivial. % 3.14/3.35 (* end of lemma zenon_L59_ *) % 3.14/3.35 assert (zenon_L60_ : ((op (e1) (e1)) = (e3)) -> ((op (e0) (e1)) = (e3)) -> (~((op (e0) (e1)) = (op (e1) (e1)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H2b zenon_Hd1 zenon_Hd2. % 3.14/3.35 elim (classic ((op (e1) (e1)) = (op (e1) (e1)))); [ zenon_intro zenon_Hd3 | zenon_intro zenon_H4c ]. % 3.14/3.35 cut (((op (e1) (e1)) = (op (e1) (e1))) = ((op (e0) (e1)) = (op (e1) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hd2. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hd3. % 3.14/3.35 cut (((op (e1) (e1)) = (op (e1) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 3.14/3.35 cut (((op (e1) (e1)) = (op (e0) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hd4]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e1) (e1)) = (e3)) = ((op (e1) (e1)) = (op (e0) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hd4. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H2b. % 3.14/3.35 cut (((e3) = (op (e0) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 3.14/3.35 cut (((op (e1) (e1)) = (op (e1) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H4c. apply refl_equal. % 3.14/3.35 apply zenon_Hd5. apply sym_equal. exact zenon_Hd1. % 3.14/3.35 apply zenon_H4c. apply refl_equal. % 3.14/3.35 apply zenon_H4c. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L60_ *) % 3.14/3.35 assert (zenon_L61_ : (~((op (op (e1) (e1)) (e1)) = (op (e3) (e1)))) -> ((op (e1) (e1)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hd6 zenon_H2b. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((op (e1) (e1)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H88]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H88 zenon_H2b). % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L61_ *) % 3.14/3.35 assert (zenon_L62_ : (~((op (op (e1) (e1)) (op (e1) (e1))) = (op (e3) (e3)))) -> ((op (e1) (e1)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hd7 zenon_H2b. % 3.14/3.35 cut (((op (e1) (e1)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H88]. % 3.14/3.35 cut (((op (e1) (e1)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H88]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H88 zenon_H2b). % 3.14/3.35 exact (zenon_H88 zenon_H2b). % 3.14/3.35 (* end of lemma zenon_L62_ *) % 3.14/3.35 assert (zenon_L63_ : ((op (e3) (e1)) = (e0)) -> ((op (e3) (e3)) = (e2)) -> ((op (e1) (e1)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H4a zenon_H54 zenon_H2b. % 3.14/3.35 apply (zenon_notand_s _ _ ax8); [ zenon_intro zenon_Hd9 | zenon_intro zenon_Hd8 ]. % 3.14/3.35 elim (classic ((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1)))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1))) = ((e0) = (op (op (e1) (e1)) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hd9. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hda. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_Hdc]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e1)) = (e0)) = ((op (op (e1) (e1)) (e1)) = (e0))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hdc. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H4a. % 3.14/3.35 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 3.14/3.35 cut (((op (e3) (e1)) = (op (op (e1) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hdd]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1)))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1))) = ((op (e3) (e1)) = (op (op (e1) (e1)) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hdd. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hda. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (op (e3) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hd6]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L61_); trivial. % 3.14/3.35 apply zenon_Hdb. apply refl_equal. % 3.14/3.35 apply zenon_Hdb. apply refl_equal. % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 apply zenon_Hdb. apply refl_equal. % 3.14/3.35 apply zenon_Hdb. apply refl_equal. % 3.14/3.35 apply (zenon_notand_s _ _ zenon_Hd8); [ zenon_intro zenon_Hdf | zenon_intro zenon_Hde ]. % 3.14/3.35 elim (classic ((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1))))); [ zenon_intro zenon_He0 | zenon_intro zenon_He1 ]. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1)))) = ((e2) = (op (op (e1) (e1)) (op (e1) (e1))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hdf. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_He0. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1))))); [idtac | apply NNPP; zenon_intro zenon_He1]. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (e2))); [idtac | apply NNPP; zenon_intro zenon_He2]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e2)) = ((op (op (e1) (e1)) (op (e1) (e1))) = (e2))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_He2. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H54. % 3.14/3.35 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (op (e1) (e1)) (op (e1) (e1))))); [idtac | apply NNPP; zenon_intro zenon_He3]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1))))); [ zenon_intro zenon_He0 | zenon_intro zenon_He1 ]. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1)))) = ((op (e3) (e3)) = (op (op (e1) (e1)) (op (e1) (e1))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_He3. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_He0. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1))))); [idtac | apply NNPP; zenon_intro zenon_He1]. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hd7]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L62_); trivial. % 3.14/3.35 apply zenon_He1. apply refl_equal. % 3.14/3.35 apply zenon_He1. apply refl_equal. % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 apply zenon_He1. apply refl_equal. % 3.14/3.35 apply zenon_He1. apply refl_equal. % 3.14/3.35 apply zenon_Hde. apply sym_equal. exact zenon_H2b. % 3.14/3.35 (* end of lemma zenon_L63_ *) % 3.14/3.35 assert (zenon_L64_ : (~((op (e3) (e1)) = (op (e3) (e2)))) -> ((op (e3) (e1)) = (e1)) -> ((op (e3) (e2)) = (e1)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hbf zenon_He4 zenon_Hbb. % 3.14/3.35 cut (((op (e3) (e1)) = (e1)) = ((op (e3) (e1)) = (op (e3) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hbf. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_He4. % 3.14/3.35 cut (((e1) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hbe]. % 3.14/3.35 cut (((op (e3) (e1)) = (op (e3) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hc3]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_Hc3. apply refl_equal. % 3.14/3.35 apply zenon_Hbe. apply sym_equal. exact zenon_Hbb. % 3.14/3.35 (* end of lemma zenon_L64_ *) % 3.14/3.35 assert (zenon_L65_ : ((op (e3) (e3)) = (e2)) -> ((op (e3) (e2)) = (e2)) -> (~((op (e3) (e2)) = (op (e3) (e3)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H54 zenon_Hc1 zenon_Hbc. % 3.14/3.35 elim (classic ((op (e3) (e3)) = (op (e3) (e3)))); [ zenon_intro zenon_H63 | zenon_intro zenon_H64 ]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3))) = ((op (e3) (e2)) = (op (e3) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hbc. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H63. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hbd]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e2)) = ((op (e3) (e3)) = (op (e3) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hbd. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H54. % 3.14/3.35 cut (((e2) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hc2]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_Hc2. apply sym_equal. exact zenon_Hc1. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L65_ *) % 3.14/3.35 assert (zenon_L66_ : (~((op (e0) (e2)) = (op (e3) (e2)))) -> ((op (e0) (e2)) = (e3)) -> ((op (e3) (e2)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_He5 zenon_He6 zenon_Hc5. % 3.14/3.35 cut (((op (e0) (e2)) = (e3)) = ((op (e0) (e2)) = (op (e3) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_He5. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_He6. % 3.14/3.35 cut (((e3) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hc6]. % 3.14/3.35 cut (((op (e0) (e2)) = (op (e0) (e2)))); [idtac | apply NNPP; zenon_intro zenon_He7]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_He7. apply refl_equal. % 3.14/3.35 apply zenon_Hc6. apply sym_equal. exact zenon_Hc5. % 3.14/3.35 (* end of lemma zenon_L66_ *) % 3.14/3.35 assert (zenon_L67_ : (((op (e3) (e2)) = (e0))\/(((op (e3) (e2)) = (e1))\/(((op (e3) (e2)) = (e2))\/((op (e3) (e2)) = (e3))))) -> ((op (e2) (e2)) = (e0)) -> (~((op (e2) (e2)) = (op (e3) (e2)))) -> ((op (e3) (e1)) = (e1)) -> (~((op (e3) (e1)) = (op (e3) (e2)))) -> (~((op (e3) (e2)) = (op (e3) (e3)))) -> ((op (e3) (e3)) = (e2)) -> (~((op (e0) (e2)) = (op (e3) (e2)))) -> ((op (e0) (e2)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hc7 zenon_H75 zenon_Hc4 zenon_He4 zenon_Hbf zenon_Hbc zenon_H54 zenon_He5 zenon_He6. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hc7); [ zenon_intro zenon_H4e | zenon_intro zenon_Hc8 ]. % 3.14/3.35 cut (((op (e2) (e2)) = (e0)) = ((op (e2) (e2)) = (op (e3) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hc4. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H75. % 3.14/3.35 cut (((e0) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H4f]. % 3.14/3.35 cut (((op (e2) (e2)) = (op (e2) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Ha1]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_Ha1. apply refl_equal. % 3.14/3.35 apply zenon_H4f. apply sym_equal. exact zenon_H4e. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hc8); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hc9 ]. % 3.14/3.35 apply (zenon_L64_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hc9); [ zenon_intro zenon_Hc1 | zenon_intro zenon_Hc5 ]. % 3.14/3.35 apply (zenon_L65_); trivial. % 3.14/3.35 apply (zenon_L66_); trivial. % 3.14/3.35 (* end of lemma zenon_L67_ *) % 3.14/3.35 assert (zenon_L68_ : ((op (e3) (e3)) = (e2)) -> ((op (e3) (e1)) = (e2)) -> (~((op (e3) (e1)) = (op (e3) (e3)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H54 zenon_Hc0 zenon_He8. % 3.14/3.35 elim (classic ((op (e3) (e3)) = (op (e3) (e3)))); [ zenon_intro zenon_H63 | zenon_intro zenon_H64 ]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3))) = ((op (e3) (e1)) = (op (e3) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_He8. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H63. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e1)))); [idtac | apply NNPP; zenon_intro zenon_He9]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e2)) = ((op (e3) (e3)) = (op (e3) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_He9. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H54. % 3.14/3.35 cut (((e2) = (op (e3) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hea]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_Hea. apply sym_equal. exact zenon_Hc0. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L68_ *) % 3.14/3.35 assert (zenon_L69_ : (~((op (e1) (e1)) = (op (e3) (e1)))) -> ((op (e1) (e1)) = (e3)) -> ((op (e3) (e1)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H49 zenon_H2b zenon_Heb. % 3.14/3.35 cut (((op (e1) (e1)) = (e3)) = ((op (e1) (e1)) = (op (e3) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H49. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H2b. % 3.14/3.35 cut (((e3) = (op (e3) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hec]. % 3.14/3.35 cut (((op (e1) (e1)) = (op (e1) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H4c. apply refl_equal. % 3.14/3.35 apply zenon_Hec. apply sym_equal. exact zenon_Heb. % 3.14/3.35 (* end of lemma zenon_L69_ *) % 3.14/3.35 assert (zenon_L70_ : (((op (e3) (e1)) = (e0))\/(((op (e3) (e1)) = (e1))\/(((op (e3) (e1)) = (e2))\/((op (e3) (e1)) = (e3))))) -> ((op (e0) (e2)) = (e3)) -> (~((op (e0) (e2)) = (op (e3) (e2)))) -> (~((op (e3) (e2)) = (op (e3) (e3)))) -> (~((op (e3) (e1)) = (op (e3) (e2)))) -> (~((op (e2) (e2)) = (op (e3) (e2)))) -> ((op (e2) (e2)) = (e0)) -> (((op (e3) (e2)) = (e0))\/(((op (e3) (e2)) = (e1))\/(((op (e3) (e2)) = (e2))\/((op (e3) (e2)) = (e3))))) -> (~((op (e3) (e1)) = (op (e3) (e3)))) -> ((op (e3) (e3)) = (e2)) -> (~((op (e1) (e1)) = (op (e3) (e1)))) -> ((op (e1) (e1)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hed zenon_He6 zenon_He5 zenon_Hbc zenon_Hbf zenon_Hc4 zenon_H75 zenon_Hc7 zenon_He8 zenon_H54 zenon_H49 zenon_H2b. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hed); [ zenon_intro zenon_H4a | zenon_intro zenon_Hee ]. % 3.14/3.35 apply (zenon_L63_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hee); [ zenon_intro zenon_He4 | zenon_intro zenon_Hef ]. % 3.14/3.35 apply (zenon_L67_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hef); [ zenon_intro zenon_Hc0 | zenon_intro zenon_Heb ]. % 3.14/3.35 apply (zenon_L68_); trivial. % 3.14/3.35 apply (zenon_L69_); trivial. % 3.14/3.35 (* end of lemma zenon_L70_ *) % 3.14/3.35 assert (zenon_L71_ : ((op (e0) (e3)) = (e1)) -> ((op (e0) (e3)) = (e3)) -> (~((e1) = (e3))) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hf0 zenon_Hf1 zenon_H33. % 3.14/3.35 elim (classic ((e3) = (e3))); [ zenon_intro zenon_H26 | zenon_intro zenon_H27 ]. % 3.14/3.35 cut (((e3) = (e3)) = ((e1) = (e3))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H33. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H26. % 3.14/3.35 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H27]. % 3.14/3.35 cut (((e3) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H34]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e0) (e3)) = (e1)) = ((e3) = (e1))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H34. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hf0. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((op (e0) (e3)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_Hf2]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_Hf2 zenon_Hf1). % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L71_ *) % 3.14/3.35 assert (zenon_L72_ : (~((op (e2) (e2)) = (op (e2) (e3)))) -> ((op (e2) (e2)) = (e0)) -> ((op (e2) (e3)) = (e0)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hf3 zenon_H75 zenon_H7b. % 3.14/3.35 cut (((op (e2) (e2)) = (e0)) = ((op (e2) (e2)) = (op (e2) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hf3. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H75. % 3.14/3.35 cut (((e0) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hf4]. % 3.14/3.35 cut (((op (e2) (e2)) = (op (e2) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Ha1]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_Ha1. apply refl_equal. % 3.14/3.35 apply zenon_Hf4. apply sym_equal. exact zenon_H7b. % 3.14/3.35 (* end of lemma zenon_L72_ *) % 3.14/3.35 assert (zenon_L73_ : (~((op (e1) (e3)) = (op (e2) (e3)))) -> ((op (e1) (e3)) = (e1)) -> ((op (e2) (e3)) = (e1)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hf5 zenon_Hf6 zenon_Hb7. % 3.14/3.35 cut (((op (e1) (e3)) = (e1)) = ((op (e1) (e3)) = (op (e2) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hf5. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hf6. % 3.14/3.35 cut (((e1) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hba]. % 3.14/3.35 cut (((op (e1) (e3)) = (op (e1) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hf7]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_Hf7. apply refl_equal. % 3.14/3.35 apply zenon_Hba. apply sym_equal. exact zenon_Hb7. % 3.14/3.35 (* end of lemma zenon_L73_ *) % 3.14/3.35 assert (zenon_L74_ : ((op (e3) (e3)) = (e2)) -> ((op (e2) (e3)) = (e2)) -> (~((op (e2) (e3)) = (op (e3) (e3)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H54 zenon_Hf8 zenon_Hb8. % 3.14/3.35 elim (classic ((op (e3) (e3)) = (op (e3) (e3)))); [ zenon_intro zenon_H63 | zenon_intro zenon_H64 ]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3))) = ((op (e2) (e3)) = (op (e3) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hb8. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H63. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hb9]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e2)) = ((op (e3) (e3)) = (op (e2) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hb9. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H54. % 3.14/3.35 cut (((e2) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hf9]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_Hf9. apply sym_equal. exact zenon_Hf8. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L74_ *) % 3.14/3.35 assert (zenon_L75_ : (~((op (e0) (e3)) = (op (e2) (e3)))) -> ((op (e0) (e3)) = (e3)) -> ((op (e2) (e3)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hfa zenon_Hf1 zenon_Hfb. % 3.14/3.35 cut (((op (e0) (e3)) = (e3)) = ((op (e0) (e3)) = (op (e2) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hfa. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hf1. % 3.14/3.35 cut (((e3) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hfc]. % 3.14/3.35 cut (((op (e0) (e3)) = (op (e0) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hfd]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_Hfd. apply refl_equal. % 3.14/3.35 apply zenon_Hfc. apply sym_equal. exact zenon_Hfb. % 3.14/3.35 (* end of lemma zenon_L75_ *) % 3.14/3.35 assert (zenon_L76_ : (((op (e2) (e3)) = (e0))\/(((op (e2) (e3)) = (e1))\/(((op (e2) (e3)) = (e2))\/((op (e2) (e3)) = (e3))))) -> ((op (e2) (e2)) = (e0)) -> (~((op (e2) (e2)) = (op (e2) (e3)))) -> ((op (e1) (e3)) = (e1)) -> (~((op (e1) (e3)) = (op (e2) (e3)))) -> (~((op (e2) (e3)) = (op (e3) (e3)))) -> ((op (e3) (e3)) = (e2)) -> (~((op (e0) (e3)) = (op (e2) (e3)))) -> ((op (e0) (e3)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hfe zenon_H75 zenon_Hf3 zenon_Hf6 zenon_Hf5 zenon_Hb8 zenon_H54 zenon_Hfa zenon_Hf1. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hfe); [ zenon_intro zenon_H7b | zenon_intro zenon_Hff ]. % 3.14/3.35 apply (zenon_L72_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hff); [ zenon_intro zenon_Hb7 | zenon_intro zenon_H100 ]. % 3.14/3.35 apply (zenon_L73_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H100); [ zenon_intro zenon_Hf8 | zenon_intro zenon_Hfb ]. % 3.14/3.35 apply (zenon_L74_); trivial. % 3.14/3.35 apply (zenon_L75_); trivial. % 3.14/3.35 (* end of lemma zenon_L76_ *) % 3.14/3.35 assert (zenon_L77_ : ((op (e2) (e3)) = (e1)) -> ((op (e2) (e2)) = (e0)) -> ((op (e3) (e3)) = (e2)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hb7 zenon_H75 zenon_H54. % 3.14/3.35 apply (zenon_notand_s _ _ ax13); [ zenon_intro zenon_H102 | zenon_intro zenon_H101 ]. % 3.14/3.35 elim (classic ((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3)))); [ zenon_intro zenon_H7e | zenon_intro zenon_H7f ]. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3))) = ((e1) = (op (op (e3) (e3)) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H102. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H7e. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H7f]. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H103]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e2) (e3)) = (e1)) = ((op (op (e3) (e3)) (e3)) = (e1))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H103. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hb7. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((op (e2) (e3)) = (op (op (e3) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H81]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3)))); [ zenon_intro zenon_H7e | zenon_intro zenon_H7f ]. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3))) = ((op (e2) (e3)) = (op (op (e3) (e3)) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H81. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H7e. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H7f]. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H79]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L26_); trivial. % 3.14/3.35 apply zenon_H7f. apply refl_equal. % 3.14/3.35 apply zenon_H7f. apply refl_equal. % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 apply zenon_H7f. apply refl_equal. % 3.14/3.35 apply zenon_H7f. apply refl_equal. % 3.14/3.35 apply (zenon_notand_s _ _ zenon_H101); [ zenon_intro zenon_H104 | zenon_intro zenon_H82 ]. % 3.14/3.35 elim (classic ((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3))))); [ zenon_intro zenon_H84 | zenon_intro zenon_H85 ]. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3)))) = ((e0) = (op (op (e3) (e3)) (op (e3) (e3))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H104. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H84. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H85]. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H105]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e2) (e2)) = (e0)) = ((op (op (e3) (e3)) (op (e3) (e3))) = (e0))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H105. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H75. % 3.14/3.35 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 3.14/3.35 cut (((op (e2) (e2)) = (op (op (e3) (e3)) (op (e3) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H87]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3))))); [ zenon_intro zenon_H84 | zenon_intro zenon_H85 ]. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3)))) = ((op (e2) (e2)) = (op (op (e3) (e3)) (op (e3) (e3))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H87. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H84. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H85]. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (e2) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H7a]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L27_); trivial. % 3.14/3.35 apply zenon_H85. apply refl_equal. % 3.14/3.35 apply zenon_H85. apply refl_equal. % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 apply zenon_H85. apply refl_equal. % 3.14/3.35 apply zenon_H85. apply refl_equal. % 3.14/3.35 apply zenon_H82. apply sym_equal. exact zenon_H54. % 3.14/3.35 (* end of lemma zenon_L77_ *) % 3.14/3.35 assert (zenon_L78_ : (((op (e2) (e2)) = (e1))/\(~((op (e1) (e1)) = (e2)))) -> ((op (e2) (e2)) = (e0)) -> (~((e0) = (e1))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H106 zenon_H75 zenon_H76. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H106). zenon_intro zenon_H31. zenon_intro zenon_H3c. % 3.14/3.35 apply (zenon_L25_); trivial. % 3.14/3.35 (* end of lemma zenon_L78_ *) % 3.14/3.35 assert (zenon_L79_ : ((op (e0) (e3)) = (e0)) -> ((op (e0) (e1)) = (e0)) -> (~((op (e0) (e1)) = (op (e0) (e3)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H107 zenon_H108 zenon_H109. % 3.14/3.35 elim (classic ((op (e0) (e3)) = (op (e0) (e3)))); [ zenon_intro zenon_H10a | zenon_intro zenon_Hfd ]. % 3.14/3.35 cut (((op (e0) (e3)) = (op (e0) (e3))) = ((op (e0) (e1)) = (op (e0) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H109. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H10a. % 3.14/3.35 cut (((op (e0) (e3)) = (op (e0) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hfd]. % 3.14/3.35 cut (((op (e0) (e3)) = (op (e0) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H10b]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e0) (e3)) = (e0)) = ((op (e0) (e3)) = (op (e0) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H10b. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H107. % 3.14/3.35 cut (((e0) = (op (e0) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H10c]. % 3.14/3.35 cut (((op (e0) (e3)) = (op (e0) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hfd]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_Hfd. apply refl_equal. % 3.14/3.35 apply zenon_H10c. apply sym_equal. exact zenon_H108. % 3.14/3.35 apply zenon_Hfd. apply refl_equal. % 3.14/3.35 apply zenon_Hfd. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L79_ *) % 3.14/3.35 assert (zenon_L80_ : ((op (e2) (e2)) = (e0)) -> ((op (e2) (e1)) = (e0)) -> (~((op (e2) (e1)) = (op (e2) (e2)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H75 zenon_H73 zenon_H10d. % 3.14/3.35 elim (classic ((op (e2) (e2)) = (op (e2) (e2)))); [ zenon_intro zenon_Ha0 | zenon_intro zenon_Ha1 ]. % 3.14/3.35 cut (((op (e2) (e2)) = (op (e2) (e2))) = ((op (e2) (e1)) = (op (e2) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H10d. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Ha0. % 3.14/3.35 cut (((op (e2) (e2)) = (op (e2) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Ha1]. % 3.14/3.35 cut (((op (e2) (e2)) = (op (e2) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H10e]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e2) (e2)) = (e0)) = ((op (e2) (e2)) = (op (e2) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H10e. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H75. % 3.14/3.35 cut (((e0) = (op (e2) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H74]. % 3.14/3.35 cut (((op (e2) (e2)) = (op (e2) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Ha1]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_Ha1. apply refl_equal. % 3.14/3.35 apply zenon_H74. apply sym_equal. exact zenon_H73. % 3.14/3.35 apply zenon_Ha1. apply refl_equal. % 3.14/3.35 apply zenon_Ha1. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L80_ *) % 3.14/3.35 assert (zenon_L81_ : (~((op (e3) (e0)) = (op (e3) (e1)))) -> ((op (e3) (e0)) = (e0)) -> ((op (e3) (e1)) = (e0)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H10f zenon_H42 zenon_H4a. % 3.14/3.35 cut (((op (e3) (e0)) = (e0)) = ((op (e3) (e0)) = (op (e3) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H10f. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H42. % 3.14/3.35 cut (((e0) = (op (e3) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H4b]. % 3.14/3.35 cut (((op (e3) (e0)) = (op (e3) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H46]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H46. apply refl_equal. % 3.14/3.35 apply zenon_H4b. apply sym_equal. exact zenon_H4a. % 3.14/3.35 (* end of lemma zenon_L81_ *) % 3.14/3.35 assert (zenon_L82_ : (((op (e0) (e1)) = (e0))\/(((op (e1) (e1)) = (e0))\/(((op (e2) (e1)) = (e0))\/((op (e3) (e1)) = (e0))))) -> (~((op (e0) (e1)) = (op (e0) (e3)))) -> ((op (e0) (e3)) = (e0)) -> ((op (e1) (e1)) = (e2)) -> (~((e0) = (e2))) -> (~((op (e2) (e1)) = (op (e2) (e2)))) -> ((op (e2) (e2)) = (e0)) -> (~((op (e3) (e0)) = (op (e3) (e1)))) -> ((op (e3) (e0)) = (e0)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H110 zenon_H109 zenon_H107 zenon_H3e zenon_H8c zenon_H10d zenon_H75 zenon_H10f zenon_H42. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H110); [ zenon_intro zenon_H108 | zenon_intro zenon_H111 ]. % 3.14/3.35 apply (zenon_L79_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H111); [ zenon_intro zenon_H2c | zenon_intro zenon_H112 ]. % 3.14/3.35 apply (zenon_L32_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H112); [ zenon_intro zenon_H73 | zenon_intro zenon_H4a ]. % 3.14/3.35 apply (zenon_L80_); trivial. % 3.14/3.35 apply (zenon_L81_); trivial. % 3.14/3.35 (* end of lemma zenon_L82_ *) % 3.14/3.35 assert (zenon_L83_ : ((op (e3) (e3)) = (e1)) -> ((op (e3) (e0)) = (e1)) -> (~((op (e3) (e0)) = (op (e3) (e3)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_Ha9 zenon_H53 zenon_H62. % 3.14/3.35 elim (classic ((op (e3) (e3)) = (op (e3) (e3)))); [ zenon_intro zenon_H63 | zenon_intro zenon_H64 ]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3))) = ((op (e3) (e0)) = (op (e3) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H62. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H63. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e1)) = ((op (e3) (e3)) = (op (e3) (e0)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H65. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Ha9. % 3.14/3.35 cut (((e1) = (op (e3) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H113]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_H113. apply sym_equal. exact zenon_H53. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L83_ *) % 3.14/3.35 assert (zenon_L84_ : ((op (e3) (e0)) = (e2)) -> ((op (e0) (e0)) = (e3)) -> (~((e2) = (op (op (e0) (e0)) (e0)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H61 zenon_H25 zenon_H114. % 3.14/3.35 elim (classic ((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0)))); [ zenon_intro zenon_H57 | zenon_intro zenon_H58 ]. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0))) = ((e2) = (op (op (e0) (e0)) (e0)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H114. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H57. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H58]. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H115]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e0)) = (e2)) = ((op (op (e0) (e0)) (e0)) = (e2))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H115. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H61. % 3.14/3.35 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 3.14/3.35 cut (((op (e3) (e0)) = (op (op (e0) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H5a]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0)))); [ zenon_intro zenon_H57 | zenon_intro zenon_H58 ]. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0))) = ((op (e3) (e0)) = (op (op (e0) (e0)) (e0)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H5a. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H57. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H58]. % 3.14/3.35 cut (((op (op (e0) (e0)) (e0)) = (op (e3) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H51]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L17_); trivial. % 3.14/3.35 apply zenon_H58. apply refl_equal. % 3.14/3.35 apply zenon_H58. apply refl_equal. % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 apply zenon_H58. apply refl_equal. % 3.14/3.35 apply zenon_H58. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L84_ *) % 3.14/3.35 assert (zenon_L85_ : ((op (e3) (e0)) = (e2)) -> ((op (e3) (e3)) = (e1)) -> ((op (e0) (e0)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H61 zenon_Ha9 zenon_H25. % 3.14/3.35 apply (zenon_notand_s _ _ ax20); [ zenon_intro zenon_H114 | zenon_intro zenon_H116 ]. % 3.14/3.35 apply (zenon_L84_); trivial. % 3.14/3.35 apply (zenon_notand_s _ _ zenon_H116); [ zenon_intro zenon_H117 | zenon_intro zenon_H5b ]. % 3.14/3.35 elim (classic ((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0))))); [ zenon_intro zenon_H5d | zenon_intro zenon_H5e ]. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0)))) = ((e1) = (op (op (e0) (e0)) (op (e0) (e0))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H117. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H5d. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H5e]. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H118]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e1)) = ((op (op (e0) (e0)) (op (e0) (e0))) = (e1))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H118. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Ha9. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (op (e0) (e0)) (op (e0) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H60]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0))))); [ zenon_intro zenon_H5d | zenon_intro zenon_H5e ]. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0)))) = ((op (e3) (e3)) = (op (op (e0) (e0)) (op (e0) (e0))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H60. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H5d. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H5e]. % 3.14/3.35 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H52]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L18_); trivial. % 3.14/3.35 apply zenon_H5e. apply refl_equal. % 3.14/3.35 apply zenon_H5e. apply refl_equal. % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 apply zenon_H5e. apply refl_equal. % 3.14/3.35 apply zenon_H5e. apply refl_equal. % 3.14/3.35 apply zenon_H5b. apply sym_equal. exact zenon_H25. % 3.14/3.35 (* end of lemma zenon_L85_ *) % 3.14/3.35 assert (zenon_L86_ : (((op (e3) (e0)) = (e0))\/(((op (e3) (e0)) = (e1))\/(((op (e3) (e0)) = (e2))\/((op (e3) (e0)) = (e3))))) -> (~((op (e3) (e0)) = (op (e3) (e1)))) -> ((op (e2) (e2)) = (e0)) -> (~((op (e2) (e1)) = (op (e2) (e2)))) -> (~((e0) = (e2))) -> ((op (e1) (e1)) = (e2)) -> ((op (e0) (e3)) = (e0)) -> (~((op (e0) (e1)) = (op (e0) (e3)))) -> (((op (e0) (e1)) = (e0))\/(((op (e1) (e1)) = (e0))\/(((op (e2) (e1)) = (e0))\/((op (e3) (e1)) = (e0))))) -> (~((op (e3) (e0)) = (op (e3) (e3)))) -> ((op (e3) (e3)) = (e1)) -> (~((op (e0) (e0)) = (op (e3) (e0)))) -> ((op (e0) (e0)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H6b zenon_H10f zenon_H75 zenon_H10d zenon_H8c zenon_H3e zenon_H107 zenon_H109 zenon_H110 zenon_H62 zenon_Ha9 zenon_H67 zenon_H25. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H6b); [ zenon_intro zenon_H42 | zenon_intro zenon_H6c ]. % 3.14/3.35 apply (zenon_L82_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H6c); [ zenon_intro zenon_H53 | zenon_intro zenon_H6d ]. % 3.14/3.35 apply (zenon_L83_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H6d); [ zenon_intro zenon_H61 | zenon_intro zenon_H68 ]. % 3.14/3.35 apply (zenon_L85_); trivial. % 3.14/3.35 apply (zenon_L21_); trivial. % 3.14/3.35 (* end of lemma zenon_L86_ *) % 3.14/3.35 assert (zenon_L87_ : ((op (e1) (e3)) = (e0)) -> ((op (e1) (e1)) = (e2)) -> ((op (e3) (e3)) = (e1)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H119 zenon_H3e zenon_Ha9. % 3.14/3.35 apply (zenon_notand_s _ _ ax9); [ zenon_intro zenon_H7d | zenon_intro zenon_H11a ]. % 3.14/3.35 elim (classic ((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3)))); [ zenon_intro zenon_H7e | zenon_intro zenon_H7f ]. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3))) = ((e0) = (op (op (e3) (e3)) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H7d. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H7e. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H7f]. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H80]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e1) (e3)) = (e0)) = ((op (op (e3) (e3)) (e3)) = (e0))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H80. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H119. % 3.14/3.35 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 3.14/3.35 cut (((op (e1) (e3)) = (op (op (e3) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H11b]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3)))); [ zenon_intro zenon_H7e | zenon_intro zenon_H7f ]. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3))) = ((op (e1) (e3)) = (op (op (e3) (e3)) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H11b. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H7e. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H7f]. % 3.14/3.35 cut (((op (op (e3) (e3)) (e3)) = (op (e1) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H11c]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H27]. % 3.14/3.35 cut (((op (e3) (e3)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H2f]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H2f zenon_Ha9). % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 apply zenon_H7f. apply refl_equal. % 3.14/3.35 apply zenon_H7f. apply refl_equal. % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 apply zenon_H7f. apply refl_equal. % 3.14/3.35 apply zenon_H7f. apply refl_equal. % 3.14/3.35 apply (zenon_notand_s _ _ zenon_H11a); [ zenon_intro zenon_H11e | zenon_intro zenon_H11d ]. % 3.14/3.35 elim (classic ((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3))))); [ zenon_intro zenon_H84 | zenon_intro zenon_H85 ]. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3)))) = ((e2) = (op (op (e3) (e3)) (op (e3) (e3))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H11e. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H84. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H85]. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H11f]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e1) (e1)) = (e2)) = ((op (op (e3) (e3)) (op (e3) (e3))) = (e2))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H11f. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H3e. % 3.14/3.35 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 3.14/3.35 cut (((op (e1) (e1)) = (op (op (e3) (e3)) (op (e3) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H120]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3))))); [ zenon_intro zenon_H84 | zenon_intro zenon_H85 ]. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3)))) = ((op (e1) (e1)) = (op (op (e3) (e3)) (op (e3) (e3))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H120. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H84. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H85]. % 3.14/3.35 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (e1) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H121]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H2f]. % 3.14/3.35 cut (((op (e3) (e3)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H2f]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H2f zenon_Ha9). % 3.14/3.35 exact (zenon_H2f zenon_Ha9). % 3.14/3.35 apply zenon_H85. apply refl_equal. % 3.14/3.35 apply zenon_H85. apply refl_equal. % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 apply zenon_H85. apply refl_equal. % 3.14/3.35 apply zenon_H85. apply refl_equal. % 3.14/3.35 apply zenon_H11d. apply sym_equal. exact zenon_Ha9. % 3.14/3.35 (* end of lemma zenon_L87_ *) % 3.14/3.35 assert (zenon_L88_ : (((op (e0) (e0)) = (e3))/\(~((op (e3) (e3)) = (e0)))) -> (~((op (e0) (e0)) = (e3))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H21 zenon_H29. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H21). zenon_intro zenon_H25. zenon_intro zenon_H24. % 3.14/3.35 exact (zenon_H29 zenon_H25). % 3.14/3.35 (* end of lemma zenon_L88_ *) % 3.14/3.35 assert (zenon_L89_ : ((op (e1) (e1)) = (e2)) -> ((op (e1) (e0)) = (e2)) -> (~((op (e1) (e0)) = (op (e1) (e1)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H3e zenon_H122 zenon_H123. % 3.14/3.35 elim (classic ((op (e1) (e1)) = (op (e1) (e1)))); [ zenon_intro zenon_Hd3 | zenon_intro zenon_H4c ]. % 3.14/3.35 cut (((op (e1) (e1)) = (op (e1) (e1))) = ((op (e1) (e0)) = (op (e1) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H123. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hd3. % 3.14/3.35 cut (((op (e1) (e1)) = (op (e1) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 3.14/3.35 cut (((op (e1) (e1)) = (op (e1) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H124]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e1) (e1)) = (e2)) = ((op (e1) (e1)) = (op (e1) (e0)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H124. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H3e. % 3.14/3.35 cut (((e2) = (op (e1) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H125]. % 3.14/3.35 cut (((op (e1) (e1)) = (op (e1) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H4c. apply refl_equal. % 3.14/3.35 apply zenon_H125. apply sym_equal. exact zenon_H122. % 3.14/3.35 apply zenon_H4c. apply refl_equal. % 3.14/3.35 apply zenon_H4c. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L89_ *) % 3.14/3.35 assert (zenon_L90_ : ((op (e2) (e0)) = (e0)) -> ((op (e2) (e0)) = (e2)) -> (~((e0) = (e2))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H43 zenon_H9b zenon_H8c. % 3.14/3.35 elim (classic ((e2) = (e2))); [ zenon_intro zenon_Hcb | zenon_intro zenon_H20 ]. % 3.14/3.35 cut (((e2) = (e2)) = ((e0) = (e2))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H8c. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hcb. % 3.14/3.35 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 3.14/3.35 cut (((e2) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H126]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e2) (e0)) = (e0)) = ((e2) = (e0))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H126. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H43. % 3.14/3.35 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 3.14/3.35 cut (((op (e2) (e0)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H127]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H127 zenon_H9b). % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L90_ *) % 3.14/3.35 assert (zenon_L91_ : ((op (e2) (e1)) = (e0)) -> ((op (e1) (e1)) = (e2)) -> (~((e0) = (op (op (e1) (e1)) (e1)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H73 zenon_H3e zenon_Hd9. % 3.14/3.35 elim (classic ((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1)))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1))) = ((e0) = (op (op (e1) (e1)) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hd9. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hda. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_Hdc]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e2) (e1)) = (e0)) = ((op (op (e1) (e1)) (e1)) = (e0))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hdc. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H73. % 3.14/3.35 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 3.14/3.35 cut (((op (e2) (e1)) = (op (op (e1) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H128]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1)))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1))) = ((op (e2) (e1)) = (op (op (e1) (e1)) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H128. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hda. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (op (e2) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H129]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((op (e1) (e1)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H3c]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H3c zenon_H3e). % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 apply zenon_Hdb. apply refl_equal. % 3.14/3.35 apply zenon_Hdb. apply refl_equal. % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 apply zenon_Hdb. apply refl_equal. % 3.14/3.35 apply zenon_Hdb. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L91_ *) % 3.14/3.35 assert (zenon_L92_ : ((op (e2) (e1)) = (e0)) -> ((op (e2) (e2)) = (e3)) -> ((op (e1) (e1)) = (e2)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H73 zenon_H32 zenon_H3e. % 3.14/3.35 apply (zenon_notand_s _ _ ax10); [ zenon_intro zenon_Hd9 | zenon_intro zenon_H12a ]. % 3.14/3.35 apply (zenon_L91_); trivial. % 3.14/3.35 apply (zenon_notand_s _ _ zenon_H12a); [ zenon_intro zenon_H12c | zenon_intro zenon_H12b ]. % 3.14/3.35 elim (classic ((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1))))); [ zenon_intro zenon_He0 | zenon_intro zenon_He1 ]. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1)))) = ((e3) = (op (op (e1) (e1)) (op (e1) (e1))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H12c. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_He0. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1))))); [idtac | apply NNPP; zenon_intro zenon_He1]. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H12d]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e2) (e2)) = (e3)) = ((op (op (e1) (e1)) (op (e1) (e1))) = (e3))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H12d. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H32. % 3.14/3.35 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H27]. % 3.14/3.35 cut (((op (e2) (e2)) = (op (op (e1) (e1)) (op (e1) (e1))))); [idtac | apply NNPP; zenon_intro zenon_H12e]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1))))); [ zenon_intro zenon_He0 | zenon_intro zenon_He1 ]. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1)))) = ((op (e2) (e2)) = (op (op (e1) (e1)) (op (e1) (e1))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H12e. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_He0. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1))))); [idtac | apply NNPP; zenon_intro zenon_He1]. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (e2) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H12f]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e1) (e1)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H3c]. % 3.14/3.35 cut (((op (e1) (e1)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H3c]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H3c zenon_H3e). % 3.14/3.35 exact (zenon_H3c zenon_H3e). % 3.14/3.35 apply zenon_He1. apply refl_equal. % 3.14/3.35 apply zenon_He1. apply refl_equal. % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 apply zenon_He1. apply refl_equal. % 3.14/3.35 apply zenon_He1. apply refl_equal. % 3.14/3.35 apply zenon_H12b. apply sym_equal. exact zenon_H3e. % 3.14/3.35 (* end of lemma zenon_L92_ *) % 3.14/3.35 assert (zenon_L93_ : ((op (e3) (e3)) = (e0)) -> ((op (e2) (e3)) = (e0)) -> (~((op (e2) (e3)) = (op (e3) (e3)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H71 zenon_H7b zenon_Hb8. % 3.14/3.35 elim (classic ((op (e3) (e3)) = (op (e3) (e3)))); [ zenon_intro zenon_H63 | zenon_intro zenon_H64 ]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3))) = ((op (e2) (e3)) = (op (e3) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hb8. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H63. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hb9]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e0)) = ((op (e3) (e3)) = (op (e2) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hb9. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H71. % 3.14/3.35 cut (((e0) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hf4]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_Hf4. apply sym_equal. exact zenon_H7b. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L93_ *) % 3.14/3.35 assert (zenon_L94_ : ((op (e3) (e3)) = (e0)) -> ((op (e3) (e2)) = (e0)) -> (~((op (e3) (e2)) = (op (e3) (e3)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H71 zenon_H4e zenon_Hbc. % 3.14/3.35 elim (classic ((op (e3) (e3)) = (op (e3) (e3)))); [ zenon_intro zenon_H63 | zenon_intro zenon_H64 ]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3))) = ((op (e3) (e2)) = (op (e3) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hbc. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H63. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hbd]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e0)) = ((op (e3) (e3)) = (op (e3) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hbd. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H71. % 3.14/3.35 cut (((e0) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H4f]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_H4f. apply sym_equal. exact zenon_H4e. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L94_ *) % 3.14/3.35 assert (zenon_L95_ : ((op (e3) (e2)) = (e1)) -> ((op (e2) (e2)) = (e3)) -> (~((e1) = (op (op (e2) (e2)) (e2)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hbb zenon_H32 zenon_H130. % 3.14/3.35 elim (classic ((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2)))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2))) = ((e1) = (op (op (e2) (e2)) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H130. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hac. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H131]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e2)) = (e1)) = ((op (op (e2) (e2)) (e2)) = (e1))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H131. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hbb. % 3.14/3.35 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 3.14/3.35 cut (((op (e3) (e2)) = (op (op (e2) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Haf]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2)))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2))) = ((op (e3) (e2)) = (op (op (e2) (e2)) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Haf. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hac. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Ha7]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L39_); trivial. % 3.14/3.35 apply zenon_Had. apply refl_equal. % 3.14/3.35 apply zenon_Had. apply refl_equal. % 3.14/3.35 apply zenon_H30. apply refl_equal. % 3.14/3.35 apply zenon_Had. apply refl_equal. % 3.14/3.35 apply zenon_Had. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L95_ *) % 3.14/3.35 assert (zenon_L96_ : ((op (e3) (e2)) = (e1)) -> ((op (e3) (e3)) = (e0)) -> ((op (e2) (e2)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hbb zenon_H71 zenon_H32. % 3.14/3.35 apply (zenon_notand_s _ _ ax12); [ zenon_intro zenon_H130 | zenon_intro zenon_H132 ]. % 3.14/3.35 apply (zenon_L95_); trivial. % 3.14/3.35 apply (zenon_notand_s _ _ zenon_H132); [ zenon_intro zenon_H133 | zenon_intro zenon_Hb0 ]. % 3.14/3.35 elim (classic ((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2))))); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hb3 ]. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2)))) = ((e0) = (op (op (e2) (e2)) (op (e2) (e2))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H133. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hb2. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2))))); [idtac | apply NNPP; zenon_intro zenon_Hb3]. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H134]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e0)) = ((op (op (e2) (e2)) (op (e2) (e2))) = (e0))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H134. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H71. % 3.14/3.35 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (op (e2) (e2)) (op (e2) (e2))))); [idtac | apply NNPP; zenon_intro zenon_Hb5]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2))))); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hb3 ]. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2)))) = ((op (e3) (e3)) = (op (op (e2) (e2)) (op (e2) (e2))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hb5. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hb2. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2))))); [idtac | apply NNPP; zenon_intro zenon_Hb3]. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Ha8]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L40_); trivial. % 3.14/3.35 apply zenon_Hb3. apply refl_equal. % 3.14/3.35 apply zenon_Hb3. apply refl_equal. % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 apply zenon_Hb3. apply refl_equal. % 3.14/3.35 apply zenon_Hb3. apply refl_equal. % 3.14/3.35 apply zenon_Hb0. apply sym_equal. exact zenon_H32. % 3.14/3.35 (* end of lemma zenon_L96_ *) % 3.14/3.35 assert (zenon_L97_ : (~((op (e3) (e0)) = (op (e3) (e2)))) -> ((op (e3) (e0)) = (e2)) -> ((op (e3) (e2)) = (e2)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H4d zenon_H61 zenon_Hc1. % 3.14/3.35 cut (((op (e3) (e0)) = (e2)) = ((op (e3) (e0)) = (op (e3) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H4d. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H61. % 3.14/3.35 cut (((e2) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hc2]. % 3.14/3.35 cut (((op (e3) (e0)) = (op (e3) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H46]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H46. apply refl_equal. % 3.14/3.35 apply zenon_Hc2. apply sym_equal. exact zenon_Hc1. % 3.14/3.35 (* end of lemma zenon_L97_ *) % 3.14/3.35 assert (zenon_L98_ : (((op (e3) (e2)) = (e0))\/(((op (e3) (e2)) = (e1))\/(((op (e3) (e2)) = (e2))\/((op (e3) (e2)) = (e3))))) -> (~((op (e3) (e2)) = (op (e3) (e3)))) -> ((op (e3) (e3)) = (e0)) -> ((op (e3) (e0)) = (e2)) -> (~((op (e3) (e0)) = (op (e3) (e2)))) -> (~((op (e2) (e2)) = (op (e3) (e2)))) -> ((op (e2) (e2)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hc7 zenon_Hbc zenon_H71 zenon_H61 zenon_H4d zenon_Hc4 zenon_H32. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hc7); [ zenon_intro zenon_H4e | zenon_intro zenon_Hc8 ]. % 3.14/3.35 apply (zenon_L94_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hc8); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hc9 ]. % 3.14/3.35 apply (zenon_L96_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hc9); [ zenon_intro zenon_Hc1 | zenon_intro zenon_Hc5 ]. % 3.14/3.35 apply (zenon_L97_); trivial. % 3.14/3.35 apply (zenon_L48_); trivial. % 3.14/3.35 (* end of lemma zenon_L98_ *) % 3.14/3.35 assert (zenon_L99_ : ((op (e3) (e3)) = (e0)) -> ((op (e3) (e3)) = (e2)) -> (~((e0) = (e2))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H71 zenon_H54 zenon_H8c. % 3.14/3.35 elim (classic ((e2) = (e2))); [ zenon_intro zenon_Hcb | zenon_intro zenon_H20 ]. % 3.14/3.35 cut (((e2) = (e2)) = ((e0) = (e2))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H8c. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hcb. % 3.14/3.35 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 3.14/3.35 cut (((e2) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H126]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e0)) = ((e2) = (e0))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H126. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H71. % 3.14/3.35 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 3.14/3.35 cut (((op (e3) (e3)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H37]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H37 zenon_H54). % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L99_ *) % 3.14/3.35 assert (zenon_L100_ : (((op (e3) (e3)) = (e2))/\(~((op (e2) (e2)) = (e3)))) -> ((op (e3) (e3)) = (e0)) -> (~((e0) = (e2))) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hcd zenon_H71 zenon_H8c. % 3.14/3.35 apply (zenon_and_s _ _ zenon_Hcd). zenon_intro zenon_H54. zenon_intro zenon_H35. % 3.14/3.35 apply (zenon_L99_); trivial. % 3.14/3.35 (* end of lemma zenon_L100_ *) % 3.14/3.35 assert (zenon_L101_ : ((op (e0) (e2)) = (e0)) -> ((op (e0) (e1)) = (e0)) -> (~((op (e0) (e1)) = (op (e0) (e2)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H135 zenon_H108 zenon_H136. % 3.14/3.35 elim (classic ((op (e0) (e2)) = (op (e0) (e2)))); [ zenon_intro zenon_H137 | zenon_intro zenon_He7 ]. % 3.14/3.35 cut (((op (e0) (e2)) = (op (e0) (e2))) = ((op (e0) (e1)) = (op (e0) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H136. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H137. % 3.14/3.35 cut (((op (e0) (e2)) = (op (e0) (e2)))); [idtac | apply NNPP; zenon_intro zenon_He7]. % 3.14/3.35 cut (((op (e0) (e2)) = (op (e0) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H138]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e0) (e2)) = (e0)) = ((op (e0) (e2)) = (op (e0) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H138. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H135. % 3.14/3.35 cut (((e0) = (op (e0) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H10c]. % 3.14/3.35 cut (((op (e0) (e2)) = (op (e0) (e2)))); [idtac | apply NNPP; zenon_intro zenon_He7]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_He7. apply refl_equal. % 3.14/3.35 apply zenon_H10c. apply sym_equal. exact zenon_H108. % 3.14/3.35 apply zenon_He7. apply refl_equal. % 3.14/3.35 apply zenon_He7. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L101_ *) % 3.14/3.35 assert (zenon_L102_ : ((op (e3) (e3)) = (e0)) -> ((op (e3) (e1)) = (e0)) -> (~((op (e3) (e1)) = (op (e3) (e3)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H71 zenon_H4a zenon_He8. % 3.14/3.35 elim (classic ((op (e3) (e3)) = (op (e3) (e3)))); [ zenon_intro zenon_H63 | zenon_intro zenon_H64 ]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3))) = ((op (e3) (e1)) = (op (e3) (e3)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_He8. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H63. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e1)))); [idtac | apply NNPP; zenon_intro zenon_He9]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e0)) = ((op (e3) (e3)) = (op (e3) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_He9. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H71. % 3.14/3.35 cut (((e0) = (op (e3) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H4b]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_H4b. apply sym_equal. exact zenon_H4a. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 apply zenon_H64. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L102_ *) % 3.14/3.35 assert (zenon_L103_ : (~((op (e0) (e1)) = (op (e3) (e1)))) -> ((op (e0) (e1)) = (e1)) -> ((op (e3) (e1)) = (e1)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H139 zenon_H13a zenon_He4. % 3.14/3.35 cut (((op (e0) (e1)) = (e1)) = ((op (e0) (e1)) = (op (e3) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H139. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H13a. % 3.14/3.35 cut (((e1) = (op (e3) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H13b]. % 3.14/3.35 cut (((op (e0) (e1)) = (op (e0) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H13c]. % 3.14/3.35 congruence. % 3.14/3.35 apply zenon_H13c. apply refl_equal. % 3.14/3.35 apply zenon_H13b. apply sym_equal. exact zenon_He4. % 3.14/3.35 (* end of lemma zenon_L103_ *) % 3.14/3.35 assert (zenon_L104_ : ((op (e3) (e1)) = (e2)) -> ((op (e1) (e1)) = (e3)) -> (~((e2) = (op (op (e1) (e1)) (e1)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hc0 zenon_H2b zenon_H13d. % 3.14/3.35 elim (classic ((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1)))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1))) = ((e2) = (op (op (e1) (e1)) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H13d. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hda. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H13e]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e1)) = (e2)) = ((op (op (e1) (e1)) (e1)) = (e2))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H13e. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hc0. % 3.14/3.35 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 3.14/3.35 cut (((op (e3) (e1)) = (op (op (e1) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hdd]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1)))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1))) = ((op (e3) (e1)) = (op (op (e1) (e1)) (e1)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hdd. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hda. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 3.14/3.35 cut (((op (op (e1) (e1)) (e1)) = (op (e3) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hd6]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L61_); trivial. % 3.14/3.35 apply zenon_Hdb. apply refl_equal. % 3.14/3.35 apply zenon_Hdb. apply refl_equal. % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 apply zenon_Hdb. apply refl_equal. % 3.14/3.35 apply zenon_Hdb. apply refl_equal. % 3.14/3.35 (* end of lemma zenon_L104_ *) % 3.14/3.35 assert (zenon_L105_ : ((op (e3) (e1)) = (e2)) -> ((op (e3) (e3)) = (e0)) -> ((op (e1) (e1)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hc0 zenon_H71 zenon_H2b. % 3.14/3.35 apply (zenon_notand_s _ _ ax18); [ zenon_intro zenon_H13d | zenon_intro zenon_H13f ]. % 3.14/3.35 apply (zenon_L104_); trivial. % 3.14/3.35 apply (zenon_notand_s _ _ zenon_H13f); [ zenon_intro zenon_H140 | zenon_intro zenon_Hde ]. % 3.14/3.35 elim (classic ((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1))))); [ zenon_intro zenon_He0 | zenon_intro zenon_He1 ]. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1)))) = ((e0) = (op (op (e1) (e1)) (op (e1) (e1))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H140. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_He0. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1))))); [idtac | apply NNPP; zenon_intro zenon_He1]. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H141]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e3) (e3)) = (e0)) = ((op (op (e1) (e1)) (op (e1) (e1))) = (e0))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H141. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H71. % 3.14/3.35 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 3.14/3.35 cut (((op (e3) (e3)) = (op (op (e1) (e1)) (op (e1) (e1))))); [idtac | apply NNPP; zenon_intro zenon_He3]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1))))); [ zenon_intro zenon_He0 | zenon_intro zenon_He1 ]. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1)))) = ((op (e3) (e3)) = (op (op (e1) (e1)) (op (e1) (e1))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_He3. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_He0. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1))))); [idtac | apply NNPP; zenon_intro zenon_He1]. % 3.14/3.35 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hd7]. % 3.14/3.35 congruence. % 3.14/3.35 apply (zenon_L62_); trivial. % 3.14/3.35 apply zenon_He1. apply refl_equal. % 3.14/3.35 apply zenon_He1. apply refl_equal. % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 apply zenon_He1. apply refl_equal. % 3.14/3.35 apply zenon_He1. apply refl_equal. % 3.14/3.35 apply zenon_Hde. apply sym_equal. exact zenon_H2b. % 3.14/3.35 (* end of lemma zenon_L105_ *) % 3.14/3.35 assert (zenon_L106_ : (((op (e3) (e1)) = (e0))\/(((op (e3) (e1)) = (e1))\/(((op (e3) (e1)) = (e2))\/((op (e3) (e1)) = (e3))))) -> (~((op (e3) (e1)) = (op (e3) (e3)))) -> ((op (e0) (e1)) = (e1)) -> (~((op (e0) (e1)) = (op (e3) (e1)))) -> ((op (e3) (e3)) = (e0)) -> (~((op (e1) (e1)) = (op (e3) (e1)))) -> ((op (e1) (e1)) = (e3)) -> False). % 3.14/3.35 do 0 intro. intros zenon_Hed zenon_He8 zenon_H13a zenon_H139 zenon_H71 zenon_H49 zenon_H2b. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hed); [ zenon_intro zenon_H4a | zenon_intro zenon_Hee ]. % 3.14/3.35 apply (zenon_L102_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hee); [ zenon_intro zenon_He4 | zenon_intro zenon_Hef ]. % 3.14/3.35 apply (zenon_L103_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_Hef); [ zenon_intro zenon_Hc0 | zenon_intro zenon_Heb ]. % 3.14/3.35 apply (zenon_L105_); trivial. % 3.14/3.35 apply (zenon_L69_); trivial. % 3.14/3.35 (* end of lemma zenon_L106_ *) % 3.14/3.35 assert (zenon_L107_ : (((op (e0) (e1)) = (e0))\/(((op (e0) (e1)) = (e1))\/(((op (e0) (e1)) = (e2))\/((op (e0) (e1)) = (e3))))) -> (~((op (e0) (e1)) = (op (e0) (e2)))) -> ((op (e0) (e2)) = (e0)) -> (~((op (e1) (e1)) = (op (e3) (e1)))) -> ((op (e3) (e3)) = (e0)) -> (~((op (e0) (e1)) = (op (e3) (e1)))) -> (~((op (e3) (e1)) = (op (e3) (e3)))) -> (((op (e3) (e1)) = (e0))\/(((op (e3) (e1)) = (e1))\/(((op (e3) (e1)) = (e2))\/((op (e3) (e1)) = (e3))))) -> ((op (e0) (e0)) = (e2)) -> (~((op (e0) (e0)) = (op (e0) (e1)))) -> ((op (e1) (e1)) = (e3)) -> (~((op (e0) (e1)) = (op (e1) (e1)))) -> False). % 3.14/3.35 do 0 intro. intros zenon_H142 zenon_H136 zenon_H135 zenon_H49 zenon_H71 zenon_H139 zenon_He8 zenon_Hed zenon_H22 zenon_H89 zenon_H2b zenon_Hd2. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H142); [ zenon_intro zenon_H108 | zenon_intro zenon_H143 ]. % 3.14/3.35 apply (zenon_L101_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H143); [ zenon_intro zenon_H13a | zenon_intro zenon_H144 ]. % 3.14/3.35 apply (zenon_L106_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H144); [ zenon_intro zenon_H8a | zenon_intro zenon_Hd1 ]. % 3.14/3.35 apply (zenon_L31_); trivial. % 3.14/3.35 apply (zenon_L60_); trivial. % 3.14/3.35 (* end of lemma zenon_L107_ *) % 3.14/3.35 assert (zenon_L108_ : ((op (e1) (e2)) = (e0)) -> ((op (e1) (e1)) = (e3)) -> ((op (e2) (e2)) = (e1)) -> False). % 3.14/3.35 do 0 intro. intros zenon_H145 zenon_H2b zenon_H31. % 3.14/3.35 apply (zenon_notand_s _ _ ax11); [ zenon_intro zenon_Hab | zenon_intro zenon_H146 ]. % 3.14/3.35 elim (classic ((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2)))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2))) = ((e0) = (op (op (e2) (e2)) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hab. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hac. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e1) (e2)) = (e0)) = ((op (op (e2) (e2)) (e2)) = (e0))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_Hae. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H145. % 3.14/3.35 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 3.14/3.35 cut (((op (e1) (e2)) = (op (op (e2) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H147]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2)))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2))) = ((op (e1) (e2)) = (op (op (e2) (e2)) (e2)))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H147. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hac. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 3.14/3.35 cut (((op (op (e2) (e2)) (e2)) = (op (e1) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H148]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 3.14/3.35 cut (((op (e2) (e2)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H3d]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H3d zenon_H31). % 3.14/3.35 apply zenon_H20. apply refl_equal. % 3.14/3.35 apply zenon_Had. apply refl_equal. % 3.14/3.35 apply zenon_Had. apply refl_equal. % 3.14/3.35 apply zenon_H50. apply refl_equal. % 3.14/3.35 apply zenon_Had. apply refl_equal. % 3.14/3.35 apply zenon_Had. apply refl_equal. % 3.14/3.35 apply (zenon_notand_s _ _ zenon_H146); [ zenon_intro zenon_H14a | zenon_intro zenon_H149 ]. % 3.14/3.35 elim (classic ((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2))))); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hb3 ]. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2)))) = ((e3) = (op (op (e2) (e2)) (op (e2) (e2))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H14a. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hb2. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2))))); [idtac | apply NNPP; zenon_intro zenon_Hb3]. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H14b]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e1) (e1)) = (e3)) = ((op (op (e2) (e2)) (op (e2) (e2))) = (e3))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H14b. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_H2b. % 3.14/3.35 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H27]. % 3.14/3.35 cut (((op (e1) (e1)) = (op (op (e2) (e2)) (op (e2) (e2))))); [idtac | apply NNPP; zenon_intro zenon_H14c]. % 3.14/3.35 congruence. % 3.14/3.35 elim (classic ((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2))))); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hb3 ]. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2)))) = ((op (e1) (e1)) = (op (op (e2) (e2)) (op (e2) (e2))))). % 3.14/3.35 intro zenon_D_pnotp. % 3.14/3.35 apply zenon_H14c. % 3.14/3.35 rewrite <- zenon_D_pnotp. % 3.14/3.35 exact zenon_Hb2. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2))))); [idtac | apply NNPP; zenon_intro zenon_Hb3]. % 3.14/3.35 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (e1) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H14d]. % 3.14/3.35 congruence. % 3.14/3.35 cut (((op (e2) (e2)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H3d]. % 3.14/3.35 cut (((op (e2) (e2)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H3d]. % 3.14/3.35 congruence. % 3.14/3.35 exact (zenon_H3d zenon_H31). % 3.14/3.35 exact (zenon_H3d zenon_H31). % 3.14/3.35 apply zenon_Hb3. apply refl_equal. % 3.14/3.35 apply zenon_Hb3. apply refl_equal. % 3.14/3.35 apply zenon_H27. apply refl_equal. % 3.14/3.35 apply zenon_Hb3. apply refl_equal. % 3.14/3.35 apply zenon_Hb3. apply refl_equal. % 3.14/3.35 apply zenon_H149. apply sym_equal. exact zenon_H31. % 3.14/3.35 (* end of lemma zenon_L108_ *) % 3.14/3.35 apply (zenon_and_s _ _ ax1). zenon_intro zenon_H14f. zenon_intro zenon_H14e. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H14e). zenon_intro zenon_H142. zenon_intro zenon_H150. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H150). zenon_intro zenon_H152. zenon_intro zenon_H151. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H151). zenon_intro zenon_H154. zenon_intro zenon_H153. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H153). zenon_intro zenon_H156. zenon_intro zenon_H155. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H155). zenon_intro zenon_H158. zenon_intro zenon_H157. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H157). zenon_intro zenon_H15a. zenon_intro zenon_H159. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H159). zenon_intro zenon_H15c. zenon_intro zenon_H15b. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H15b). zenon_intro zenon_Ha4. zenon_intro zenon_H15d. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H15d). zenon_intro zenon_H15f. zenon_intro zenon_H15e. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H15e). zenon_intro zenon_H161. zenon_intro zenon_H160. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H160). zenon_intro zenon_Hfe. zenon_intro zenon_H162. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H162). zenon_intro zenon_H6b. zenon_intro zenon_H163. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H163). zenon_intro zenon_Hed. zenon_intro zenon_H164. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H164). zenon_intro zenon_Hc7. zenon_intro zenon_H165. % 3.14/3.35 apply (zenon_and_s _ _ ax2). zenon_intro zenon_H167. zenon_intro zenon_H166. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H166). zenon_intro zenon_H169. zenon_intro zenon_H168. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H168). zenon_intro zenon_H16b. zenon_intro zenon_H16a. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H16a). zenon_intro zenon_H16d. zenon_intro zenon_H16c. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H16c). zenon_intro zenon_H16f. zenon_intro zenon_H16e. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H16e). zenon_intro zenon_H171. zenon_intro zenon_H170. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H170). zenon_intro zenon_H173. zenon_intro zenon_H172. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H172). zenon_intro zenon_H175. zenon_intro zenon_H174. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H174). zenon_intro zenon_H177. zenon_intro zenon_H176. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H176). zenon_intro zenon_H110. zenon_intro zenon_H178. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H178). zenon_intro zenon_H17a. zenon_intro zenon_H179. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H179). zenon_intro zenon_H17c. zenon_intro zenon_H17b. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H17b). zenon_intro zenon_H17e. zenon_intro zenon_H17d. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H17d). zenon_intro zenon_H180. zenon_intro zenon_H17f. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H17f). zenon_intro zenon_H182. zenon_intro zenon_H181. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H181). zenon_intro zenon_H184. zenon_intro zenon_H183. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H183). zenon_intro zenon_H186. zenon_intro zenon_H185. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H185). zenon_intro zenon_H188. zenon_intro zenon_H187. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H187). zenon_intro zenon_H18a. zenon_intro zenon_H189. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H189). zenon_intro zenon_H18c. zenon_intro zenon_H18b. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H18b). zenon_intro zenon_H18e. zenon_intro zenon_H18d. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H18d). zenon_intro zenon_H190. zenon_intro zenon_H18f. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H18f). zenon_intro zenon_H192. zenon_intro zenon_H191. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H191). zenon_intro zenon_H194. zenon_intro zenon_H193. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H193). zenon_intro zenon_H6e. zenon_intro zenon_H195. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H195). zenon_intro zenon_H197. zenon_intro zenon_H196. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H196). zenon_intro zenon_H199. zenon_intro zenon_H198. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H198). zenon_intro zenon_H19b. zenon_intro zenon_H19a. % 3.14/3.35 apply (zenon_and_s _ _ ax3). zenon_intro zenon_H19d. zenon_intro zenon_H19c. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H19c). zenon_intro zenon_H19f. zenon_intro zenon_H19e. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H19e). zenon_intro zenon_H67. zenon_intro zenon_H1a0. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1a0). zenon_intro zenon_H1a2. zenon_intro zenon_H1a1. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1a1). zenon_intro zenon_H1a4. zenon_intro zenon_H1a3. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1a3). zenon_intro zenon_H44. zenon_intro zenon_H1a5. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1a5). zenon_intro zenon_Hd2. zenon_intro zenon_H1a6. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1a6). zenon_intro zenon_H1a8. zenon_intro zenon_H1a7. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1a7). zenon_intro zenon_H139. zenon_intro zenon_H1a9. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1a9). zenon_intro zenon_H72. zenon_intro zenon_H1aa. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1aa). zenon_intro zenon_H49. zenon_intro zenon_H1ab. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1ab). zenon_intro zenon_H1ad. zenon_intro zenon_H1ac. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1ac). zenon_intro zenon_H1af. zenon_intro zenon_H1ae. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1ae). zenon_intro zenon_H1b1. zenon_intro zenon_H1b0. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1b0). zenon_intro zenon_He5. zenon_intro zenon_H1b2. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1b2). zenon_intro zenon_H1b4. zenon_intro zenon_H1b3. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1b3). zenon_intro zenon_H1b6. zenon_intro zenon_H1b5. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1b5). zenon_intro zenon_Hc4. zenon_intro zenon_H1b7. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1b7). zenon_intro zenon_H1b9. zenon_intro zenon_H1b8. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1b8). zenon_intro zenon_Hfa. zenon_intro zenon_H1ba. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1ba). zenon_intro zenon_H1bc. zenon_intro zenon_H1bb. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1bb). zenon_intro zenon_Hf5. zenon_intro zenon_H1bd. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1bd). zenon_intro zenon_H1bf. zenon_intro zenon_H1be. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1be). zenon_intro zenon_Hb8. zenon_intro zenon_H1c0. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1c0). zenon_intro zenon_H89. zenon_intro zenon_H1c1. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1c1). zenon_intro zenon_H1c3. zenon_intro zenon_H1c2. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1c2). zenon_intro zenon_H1c5. zenon_intro zenon_H1c4. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1c4). zenon_intro zenon_H136. zenon_intro zenon_H1c6. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1c6). zenon_intro zenon_H109. zenon_intro zenon_H1c7. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1c7). zenon_intro zenon_H1c9. zenon_intro zenon_H1c8. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1c8). zenon_intro zenon_H123. zenon_intro zenon_H1ca. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1ca). zenon_intro zenon_H1cc. zenon_intro zenon_H1cb. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1cb). zenon_intro zenon_H1ce. zenon_intro zenon_H1cd. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1cd). zenon_intro zenon_H1d0. zenon_intro zenon_H1cf. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1cf). zenon_intro zenon_H1d2. zenon_intro zenon_H1d1. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1d1). zenon_intro zenon_H1d4. zenon_intro zenon_H1d3. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1d3). zenon_intro zenon_H97. zenon_intro zenon_H1d5. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1d5). zenon_intro zenon_H9f. zenon_intro zenon_H1d6. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1d6). zenon_intro zenon_H1d8. zenon_intro zenon_H1d7. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1d7). zenon_intro zenon_H10d. zenon_intro zenon_H1d9. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1d9). zenon_intro zenon_H1db. zenon_intro zenon_H1da. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1da). zenon_intro zenon_Hf3. zenon_intro zenon_H1dc. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1dc). zenon_intro zenon_H10f. zenon_intro zenon_H1dd. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1dd). zenon_intro zenon_H4d. zenon_intro zenon_H1de. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1de). zenon_intro zenon_H62. zenon_intro zenon_H1df. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1df). zenon_intro zenon_Hbf. zenon_intro zenon_H1e0. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1e0). zenon_intro zenon_He8. zenon_intro zenon_Hbc. % 3.14/3.35 apply (zenon_and_s _ _ ax4). zenon_intro zenon_H76. zenon_intro zenon_H1e1. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1e1). zenon_intro zenon_H8c. zenon_intro zenon_H1e2. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1e2). zenon_intro zenon_H2a. zenon_intro zenon_H1e3. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1e3). zenon_intro zenon_Hca. zenon_intro zenon_H1e4. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1e4). zenon_intro zenon_H33. zenon_intro zenon_H23. % 3.14/3.35 apply (zenon_and_s _ _ ax5). zenon_intro zenon_H1e6. zenon_intro zenon_H1e5. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1e5). zenon_intro zenon_H1e8. zenon_intro zenon_H1e7. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1e7). zenon_intro zenon_H1ea. zenon_intro zenon_H1e9. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1e6); [ zenon_intro zenon_H1ec | zenon_intro zenon_H1eb ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1ec). zenon_intro zenon_H1ee. zenon_intro zenon_H1ed. % 3.14/3.35 exact (zenon_H1ed zenon_H1ee). % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1eb); [ zenon_intro zenon_H1f0 | zenon_intro zenon_H1ef ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1f0). zenon_intro zenon_H2c. zenon_intro zenon_H1f1. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1e8); [ zenon_intro zenon_H1f3 | zenon_intro zenon_H1f2 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1f3). zenon_intro zenon_Hce. zenon_intro zenon_H2d. % 3.14/3.35 exact (zenon_H1f1 zenon_Hce). % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f2); [ zenon_intro zenon_H1d | zenon_intro zenon_H1f4 ]. % 3.14/3.35 apply (zenon_L1_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f4); [ zenon_intro zenon_H106 | zenon_intro zenon_Hb6 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H106). zenon_intro zenon_H31. zenon_intro zenon_H3c. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1ea); [ zenon_intro zenon_Hcf | zenon_intro zenon_H1f5 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_Hcf). zenon_intro zenon_H22. zenon_intro zenon_Hd0. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1e9); [ zenon_intro zenon_H21 | zenon_intro zenon_H1f6 ]. % 3.14/3.35 apply (zenon_L3_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f6); [ zenon_intro zenon_H2e | zenon_intro zenon_H1f7 ]. % 3.14/3.35 apply (zenon_L6_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f7); [ zenon_intro zenon_H36 | zenon_intro zenon_H38 ]. % 3.14/3.35 apply (zenon_L9_); trivial. % 3.14/3.35 apply (zenon_L10_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f5); [ zenon_intro zenon_H3b | zenon_intro zenon_H1f8 ]. % 3.14/3.35 apply (zenon_L11_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f8); [ zenon_intro zenon_H3f | zenon_intro zenon_Hcd ]. % 3.14/3.35 apply (zenon_L12_); trivial. % 3.14/3.35 apply (zenon_and_s _ _ zenon_Hcd). zenon_intro zenon_H54. zenon_intro zenon_H35. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1e9); [ zenon_intro zenon_H21 | zenon_intro zenon_H1f6 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H21). zenon_intro zenon_H25. zenon_intro zenon_H24. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H186); [ zenon_intro zenon_H43 | zenon_intro zenon_H1f9 ]. % 3.14/3.35 apply (zenon_L23_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f9); [ zenon_intro zenon_H73 | zenon_intro zenon_H1fa ]. % 3.14/3.35 apply (zenon_L24_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1fa); [ zenon_intro zenon_H75 | zenon_intro zenon_H7b ]. % 3.14/3.35 apply (zenon_L25_); trivial. % 3.14/3.35 apply (zenon_L28_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f6); [ zenon_intro zenon_H2e | zenon_intro zenon_H1f7 ]. % 3.14/3.35 apply (zenon_L6_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f7); [ zenon_intro zenon_H36 | zenon_intro zenon_H38 ]. % 3.14/3.35 apply (zenon_L29_); trivial. % 3.14/3.35 apply (zenon_L10_); trivial. % 3.14/3.35 apply (zenon_and_s _ _ zenon_Hb6). zenon_intro zenon_Ha9. zenon_intro zenon_H88. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1ea); [ zenon_intro zenon_Hcf | zenon_intro zenon_H1f5 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_Hcf). zenon_intro zenon_H22. zenon_intro zenon_Hd0. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1e9); [ zenon_intro zenon_H21 | zenon_intro zenon_H1f6 ]. % 3.14/3.35 apply (zenon_L3_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f6); [ zenon_intro zenon_H2e | zenon_intro zenon_H1f7 ]. % 3.14/3.35 apply (zenon_L30_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f7); [ zenon_intro zenon_H36 | zenon_intro zenon_H38 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H36). zenon_intro zenon_H32. zenon_intro zenon_H37. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H180); [ zenon_intro zenon_H8a | zenon_intro zenon_H1fb ]. % 3.14/3.35 apply (zenon_L31_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1fb); [ zenon_intro zenon_H3e | zenon_intro zenon_H1fc ]. % 3.14/3.35 apply (zenon_L32_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1fc); [ zenon_intro zenon_H9c | zenon_intro zenon_Hc0 ]. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H18a); [ zenon_intro zenon_H8d | zenon_intro zenon_H1fd ]. % 3.14/3.35 apply (zenon_L34_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1fd); [ zenon_intro zenon_H98 | zenon_intro zenon_H1fe ]. % 3.14/3.35 apply (zenon_L44_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1fe); [ zenon_intro zenon_H31 | zenon_intro zenon_Hb7 ]. % 3.14/3.35 apply (zenon_L9_); trivial. % 3.14/3.35 apply (zenon_L45_); trivial. % 3.14/3.35 apply (zenon_L49_); trivial. % 3.14/3.35 apply (zenon_L10_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f5); [ zenon_intro zenon_H3b | zenon_intro zenon_H1f8 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H3b). zenon_intro zenon_H3e. zenon_intro zenon_H3d. % 3.14/3.35 apply (zenon_L32_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f8); [ zenon_intro zenon_H3f | zenon_intro zenon_Hcd ]. % 3.14/3.35 apply (zenon_L12_); trivial. % 3.14/3.35 apply (zenon_L51_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1ef); [ zenon_intro zenon_H200 | zenon_intro zenon_H1ff ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H200). zenon_intro zenon_H75. zenon_intro zenon_H90. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1e8); [ zenon_intro zenon_H1f3 | zenon_intro zenon_H1f2 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1f3). zenon_intro zenon_Hce. zenon_intro zenon_H2d. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1ea); [ zenon_intro zenon_Hcf | zenon_intro zenon_H1f5 ]. % 3.14/3.35 apply (zenon_L53_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f5); [ zenon_intro zenon_H3b | zenon_intro zenon_H1f8 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H3b). zenon_intro zenon_H3e. zenon_intro zenon_H3d. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1e9); [ zenon_intro zenon_H21 | zenon_intro zenon_H1f6 ]. % 3.14/3.35 apply (zenon_L55_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f6); [ zenon_intro zenon_H2e | zenon_intro zenon_H1f7 ]. % 3.14/3.35 apply (zenon_L57_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f7); [ zenon_intro zenon_H36 | zenon_intro zenon_H38 ]. % 3.14/3.35 apply (zenon_L59_); trivial. % 3.14/3.35 apply (zenon_L10_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f8); [ zenon_intro zenon_H3f | zenon_intro zenon_Hcd ]. % 3.14/3.35 apply (zenon_L12_); trivial. % 3.14/3.35 apply (zenon_and_s _ _ zenon_Hcd). zenon_intro zenon_H54. zenon_intro zenon_H35. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1e9); [ zenon_intro zenon_H21 | zenon_intro zenon_H1f6 ]. % 3.14/3.35 apply (zenon_L55_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f6); [ zenon_intro zenon_H2e | zenon_intro zenon_H1f7 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H2e). zenon_intro zenon_H2b. zenon_intro zenon_H2f. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H173); [ zenon_intro zenon_H25 | zenon_intro zenon_H201 ]. % 3.14/3.35 apply (zenon_L54_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H201); [ zenon_intro zenon_Hd1 | zenon_intro zenon_H202 ]. % 3.14/3.35 apply (zenon_L60_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H202); [ zenon_intro zenon_He6 | zenon_intro zenon_Hf1 ]. % 3.14/3.35 apply (zenon_L70_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H19b); [ zenon_intro zenon_Hf0 | zenon_intro zenon_H203 ]. % 3.14/3.35 apply (zenon_L71_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H203); [ zenon_intro zenon_Hf6 | zenon_intro zenon_H204 ]. % 3.14/3.35 apply (zenon_L76_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H204); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Ha9 ]. % 3.14/3.35 apply (zenon_L77_); trivial. % 3.14/3.35 exact (zenon_H2f zenon_Ha9). % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f7); [ zenon_intro zenon_H36 | zenon_intro zenon_H38 ]. % 3.14/3.35 apply (zenon_L59_); trivial. % 3.14/3.35 apply (zenon_L10_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f2); [ zenon_intro zenon_H1d | zenon_intro zenon_H1f4 ]. % 3.14/3.35 apply (zenon_L1_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f4); [ zenon_intro zenon_H106 | zenon_intro zenon_Hb6 ]. % 3.14/3.35 apply (zenon_L78_); trivial. % 3.14/3.35 apply (zenon_and_s _ _ zenon_Hb6). zenon_intro zenon_Ha9. zenon_intro zenon_H88. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1ea); [ zenon_intro zenon_Hcf | zenon_intro zenon_H1f5 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_Hcf). zenon_intro zenon_H22. zenon_intro zenon_Hd0. % 3.14/3.35 exact (zenon_H90 zenon_H22). % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f5); [ zenon_intro zenon_H3b | zenon_intro zenon_H1f8 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H3b). zenon_intro zenon_H3e. zenon_intro zenon_H3d. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1e9); [ zenon_intro zenon_H21 | zenon_intro zenon_H1f6 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H21). zenon_intro zenon_H25. zenon_intro zenon_H24. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H197); [ zenon_intro zenon_H107 | zenon_intro zenon_H205 ]. % 3.14/3.35 apply (zenon_L86_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H205); [ zenon_intro zenon_H119 | zenon_intro zenon_H206 ]. % 3.14/3.35 apply (zenon_L87_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H206); [ zenon_intro zenon_H7b | zenon_intro zenon_H71 ]. % 3.14/3.35 apply (zenon_L72_); trivial. % 3.14/3.35 exact (zenon_H24 zenon_H71). % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f6); [ zenon_intro zenon_H2e | zenon_intro zenon_H1f7 ]. % 3.14/3.35 apply (zenon_L57_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f7); [ zenon_intro zenon_H36 | zenon_intro zenon_H38 ]. % 3.14/3.35 apply (zenon_L59_); trivial. % 3.14/3.35 apply (zenon_L10_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f8); [ zenon_intro zenon_H3f | zenon_intro zenon_Hcd ]. % 3.14/3.35 apply (zenon_L12_); trivial. % 3.14/3.35 apply (zenon_L51_); trivial. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1ff). zenon_intro zenon_H71. zenon_intro zenon_H29. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1e8); [ zenon_intro zenon_H1f3 | zenon_intro zenon_H1f2 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H1f3). zenon_intro zenon_Hce. zenon_intro zenon_H2d. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1ea); [ zenon_intro zenon_Hcf | zenon_intro zenon_H1f5 ]. % 3.14/3.35 apply (zenon_L53_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f5); [ zenon_intro zenon_H3b | zenon_intro zenon_H1f8 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H3b). zenon_intro zenon_H3e. zenon_intro zenon_H3d. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1e9); [ zenon_intro zenon_H21 | zenon_intro zenon_H1f6 ]. % 3.14/3.35 apply (zenon_L88_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f6); [ zenon_intro zenon_H2e | zenon_intro zenon_H1f7 ]. % 3.14/3.35 apply (zenon_L57_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f7); [ zenon_intro zenon_H36 | zenon_intro zenon_H38 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H36). zenon_intro zenon_H32. zenon_intro zenon_H37. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H171); [ zenon_intro zenon_H22 | zenon_intro zenon_H207 ]. % 3.14/3.35 apply (zenon_L52_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H207); [ zenon_intro zenon_H122 | zenon_intro zenon_H208 ]. % 3.14/3.35 apply (zenon_L89_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H208); [ zenon_intro zenon_H9b | zenon_intro zenon_H61 ]. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H186); [ zenon_intro zenon_H43 | zenon_intro zenon_H1f9 ]. % 3.14/3.35 apply (zenon_L90_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f9); [ zenon_intro zenon_H73 | zenon_intro zenon_H1fa ]. % 3.14/3.35 apply (zenon_L92_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1fa); [ zenon_intro zenon_H75 | zenon_intro zenon_H7b ]. % 3.14/3.35 apply (zenon_L58_); trivial. % 3.14/3.35 apply (zenon_L93_); trivial. % 3.14/3.35 apply (zenon_L98_); trivial. % 3.14/3.35 apply (zenon_L10_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f8); [ zenon_intro zenon_H3f | zenon_intro zenon_Hcd ]. % 3.14/3.35 apply (zenon_L12_); trivial. % 3.14/3.35 apply (zenon_L100_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f2); [ zenon_intro zenon_H1d | zenon_intro zenon_H1f4 ]. % 3.14/3.35 apply (zenon_L1_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f4); [ zenon_intro zenon_H106 | zenon_intro zenon_Hb6 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H106). zenon_intro zenon_H31. zenon_intro zenon_H3c. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1ea); [ zenon_intro zenon_Hcf | zenon_intro zenon_H1f5 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_Hcf). zenon_intro zenon_H22. zenon_intro zenon_Hd0. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1e9); [ zenon_intro zenon_H21 | zenon_intro zenon_H1f6 ]. % 3.14/3.35 apply (zenon_L88_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f6); [ zenon_intro zenon_H2e | zenon_intro zenon_H1f7 ]. % 3.14/3.35 apply (zenon_and_s _ _ zenon_H2e). zenon_intro zenon_H2b. zenon_intro zenon_H2f. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H188); [ zenon_intro zenon_H135 | zenon_intro zenon_H209 ]. % 3.14/3.35 apply (zenon_L107_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H209); [ zenon_intro zenon_H145 | zenon_intro zenon_H20a ]. % 3.14/3.35 apply (zenon_L108_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H20a); [ zenon_intro zenon_H75 | zenon_intro zenon_H4e ]. % 3.14/3.35 exact (zenon_Hd0 zenon_H75). % 3.14/3.35 apply (zenon_L94_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f7); [ zenon_intro zenon_H36 | zenon_intro zenon_H38 ]. % 3.14/3.35 apply (zenon_L9_); trivial. % 3.14/3.35 apply (zenon_L10_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f5); [ zenon_intro zenon_H3b | zenon_intro zenon_H1f8 ]. % 3.14/3.35 apply (zenon_L11_); trivial. % 3.14/3.35 apply (zenon_or_s _ _ zenon_H1f8); [ zenon_intro zenon_H3f | zenon_intro zenon_Hcd ]. % 3.14/3.35 apply (zenon_L12_); trivial. % 3.14/3.35 apply (zenon_L100_); trivial. % 3.14/3.35 apply (zenon_L43_); trivial. % 3.14/3.35 Qed. % 3.14/3.35 % SZS output end Proof % 3.14/3.35 (* END-PROOF *) % 3.14/3.35 nodes searched: 114549 % 3.14/3.35 max branch formulas: 284 % 3.14/3.35 proof nodes created: 5795 % 3.14/3.35 formulas created: 34338 % 3.14/3.35 %------------------------------------------------------------------------------