%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : PUZ078+1 : TPTP v8.1.0. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n026.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 : Mon Jul 18 18:33:42 EDT 2022 % Result : Theorem 4.24s 4.41s % Output : Proof 4.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : PUZ078+1 : TPTP v8.1.0. Released v3.5.0. % 0.10/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n026.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Sat May 28 21:49:24 EDT 2022 % 0.12/0.34 % CPUTime : % 4.24/4.41 (* PROOF-FOUND *) % 4.24/4.41 % SZS status Theorem % 4.24/4.41 (* BEGIN-PROOF *) % 4.24/4.41 % SZS output start Proof % 4.24/4.41 Theorem tuesday_leo_tells_truths : (truthday (tuesday)). % 4.24/4.41 Proof. % 4.24/4.41 assert (zenon_L1_ : forall (zenon_TX_z : zenon_U), (day3 (consecutive zenon_TX_z)) -> (~(day2 zenon_TX_z)) -> False). % 4.24/4.41 do 1 intro. intros zenon_H17 zenon_H18. % 4.24/4.41 generalize (day3_follows_day2 zenon_TX_z). zenon_intro zenon_H1a. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H1a); [ zenon_intro zenon_H18; zenon_intro zenon_H1c | zenon_intro zenon_H1b; zenon_intro zenon_H17 ]. % 4.24/4.41 exact (zenon_H1c zenon_H17). % 4.24/4.41 exact (zenon_H18 zenon_H1b). % 4.24/4.41 (* end of lemma zenon_L1_ *) % 4.24/4.41 assert (zenon_L2_ : forall (zenon_TX_bf : zenon_U), (day3 (consecutive (consecutive zenon_TX_bf))) -> (~(day2 (consecutive zenon_TX_bf))) -> False). % 4.24/4.41 do 1 intro. intros zenon_H1d zenon_H1e. % 4.24/4.41 generalize (day3_follows_day2 (consecutive zenon_TX_bf)). zenon_intro zenon_H20. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H20); [ zenon_intro zenon_H1e; zenon_intro zenon_H22 | zenon_intro zenon_H21; zenon_intro zenon_H1d ]. % 4.24/4.41 exact (zenon_H22 zenon_H1d). % 4.24/4.41 exact (zenon_H1e zenon_H21). % 4.24/4.41 (* end of lemma zenon_L2_ *) % 4.24/4.41 assert (zenon_L3_ : forall (zenon_TX_bf : zenon_U), (day3 (consecutive (consecutive zenon_TX_bf))) -> (~(day1 zenon_TX_bf)) -> False). % 4.24/4.41 do 1 intro. intros zenon_H1d zenon_H23. % 4.24/4.41 generalize (day2_follows_day1 zenon_TX_bf). zenon_intro zenon_H24. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H24); [ zenon_intro zenon_H23; zenon_intro zenon_H1e | zenon_intro zenon_H25; zenon_intro zenon_H21 ]. % 4.24/4.41 apply (zenon_L2_ zenon_TX_bf); trivial. % 4.24/4.41 exact (zenon_H23 zenon_H25). % 4.24/4.41 (* end of lemma zenon_L3_ *) % 4.24/4.41 assert (zenon_L4_ : (~((~(truthday (wednesday)))/\(~(truthday (friday))))) -> (~((monday) = (friday))) -> (~((monday) = (wednesday))) -> (truthday (monday)) -> False). % 4.24/4.41 do 0 intro. intros zenon_H26 zenon_H27 zenon_H28 zenon_H29. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H26); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 4.24/4.41 apply zenon_H2b. zenon_intro zenon_H2c. % 4.24/4.41 generalize (truth_unique (wednesday)). zenon_intro zenon_H2d. % 4.24/4.41 generalize (zenon_H2d (monday)). zenon_intro zenon_H2e. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H2e); [ zenon_intro zenon_H30 | zenon_intro zenon_H2f ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H30); [ zenon_intro zenon_H32 | zenon_intro zenon_H31 ]. % 4.24/4.41 exact (zenon_H32 zenon_H2c). % 4.24/4.41 exact (zenon_H31 zenon_H29). % 4.24/4.41 apply zenon_H28. apply sym_equal. exact zenon_H2f. % 4.24/4.41 apply zenon_H2a. zenon_intro zenon_H33. % 4.24/4.41 generalize (truth_unique (friday)). zenon_intro zenon_H34. % 4.24/4.41 generalize (zenon_H34 (monday)). zenon_intro zenon_H35. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H35); [ zenon_intro zenon_H37 | zenon_intro zenon_H36 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H37); [ zenon_intro zenon_H38 | zenon_intro zenon_H31 ]. % 4.24/4.41 exact (zenon_H38 zenon_H33). % 4.24/4.41 exact (zenon_H31 zenon_H29). % 4.24/4.41 apply zenon_H27. apply sym_equal. exact zenon_H36. % 4.24/4.41 (* end of lemma zenon_L4_ *) % 4.24/4.41 assert (zenon_L5_ : forall (zenon_TX_z : zenon_U), (day3 (consecutive zenon_TX_z)) -> (~(truthday (consecutive zenon_TX_z))) -> ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> False). % 4.24/4.41 do 1 intro. intros zenon_H17 zenon_H39 zenon_H3a. % 4.24/4.41 generalize (statement3 (consecutive zenon_TX_z)). zenon_intro zenon_H3b. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H3b); [ zenon_intro zenon_H1c | zenon_intro zenon_H3c ]. % 4.24/4.41 exact (zenon_H1c zenon_H17). % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H3c); [ zenon_intro zenon_H39; zenon_intro zenon_H26 | zenon_intro zenon_H3d; zenon_intro zenon_H3a ]. % 4.24/4.41 exact (zenon_H26 zenon_H3a). % 4.24/4.41 exact (zenon_H39 zenon_H3d). % 4.24/4.41 (* end of lemma zenon_L5_ *) % 4.24/4.41 assert (zenon_L6_ : forall (zenon_TX_z : zenon_U), (forall Y : zenon_U, (((truthday (monday))/\(truthday Y))->((monday) = Y))) -> (truthday (monday)) -> (day3 (consecutive zenon_TX_z)) -> ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> (~((monday) = (consecutive zenon_TX_z))) -> False). % 4.24/4.41 do 1 intro. intros zenon_H3e zenon_H29 zenon_H17 zenon_H3a zenon_H3f. % 4.24/4.41 generalize (zenon_H3e (consecutive zenon_TX_z)). zenon_intro zenon_H40. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H40); [ zenon_intro zenon_H42 | zenon_intro zenon_H41 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H42); [ zenon_intro zenon_H31 | zenon_intro zenon_H39 ]. % 4.24/4.41 exact (zenon_H31 zenon_H29). % 4.24/4.41 apply (zenon_L5_ zenon_TX_z); trivial. % 4.24/4.41 exact (zenon_H3f zenon_H41). % 4.24/4.41 (* end of lemma zenon_L6_ *) % 4.24/4.41 assert (zenon_L7_ : forall (zenon_TX_z : zenon_U), (~((monday) = (consecutive zenon_TX_z))) -> ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> (day3 (consecutive zenon_TX_z)) -> (truthday (monday)) -> False). % 4.24/4.41 do 1 intro. intros zenon_H3f zenon_H3a zenon_H17 zenon_H29. % 4.24/4.41 generalize (truth_unique (monday)). zenon_intro zenon_H3e. % 4.24/4.41 apply (zenon_L6_ zenon_TX_z); trivial. % 4.24/4.41 (* end of lemma zenon_L7_ *) % 4.24/4.41 assert (zenon_L8_ : forall (zenon_TX_z : zenon_U), ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> (day3 (consecutive zenon_TX_z)) -> (truthday (monday)) -> (~((consecutive zenon_TX_z) = (consecutive (sunday)))) -> False). % 4.24/4.41 do 1 intro. intros zenon_H3a zenon_H17 zenon_H29 zenon_H43. % 4.24/4.41 elim (classic ((consecutive (sunday)) = (consecutive (sunday)))); [ zenon_intro zenon_H44 | zenon_intro zenon_H45 ]. % 4.24/4.41 cut (((consecutive (sunday)) = (consecutive (sunday))) = ((consecutive zenon_TX_z) = (consecutive (sunday)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H43. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H44. % 4.24/4.41 cut (((consecutive (sunday)) = (consecutive (sunday)))); [idtac | apply NNPP; zenon_intro zenon_H45]. % 4.24/4.41 cut (((consecutive (sunday)) = (consecutive zenon_TX_z))); [idtac | apply NNPP; zenon_intro zenon_H46]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive (sunday)) = (monday)) = ((consecutive (sunday)) = (consecutive zenon_TX_z))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H46. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact monday_follows_sunday. % 4.24/4.41 cut (((monday) = (consecutive zenon_TX_z))); [idtac | apply NNPP; zenon_intro zenon_H3f]. % 4.24/4.41 cut (((consecutive (sunday)) = (consecutive (sunday)))); [idtac | apply NNPP; zenon_intro zenon_H45]. % 4.24/4.41 congruence. % 4.24/4.41 apply zenon_H45. apply refl_equal. % 4.24/4.41 apply (zenon_L7_ zenon_TX_z); trivial. % 4.24/4.41 apply zenon_H45. apply refl_equal. % 4.24/4.41 apply zenon_H45. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L8_ *) % 4.24/4.41 assert (zenon_L9_ : forall (zenon_TX_z : zenon_U) (zenon_TX_cv : zenon_U), (~((day2 (thursday))\/((day2 (saturday))\/(day2 (sunday))))) -> (day3 zenon_TX_cv) -> (day3 (consecutive zenon_TX_z)) -> (truthday (monday)) -> (~((monday) = (wednesday))) -> (~((monday) = (friday))) -> False). % 4.24/4.41 do 2 intro. intros zenon_H47 zenon_H48 zenon_H17 zenon_H29 zenon_H28 zenon_H27. % 4.24/4.41 apply (zenon_notor_s _ _ zenon_H47). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 4.24/4.41 apply (zenon_notor_s _ _ zenon_H4a). zenon_intro zenon_H4d. zenon_intro zenon_H4c. % 4.24/4.41 generalize (day3_follows_day2 (sunday)). zenon_intro zenon_H4e. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H4e); [ zenon_intro zenon_H4c; zenon_intro zenon_H51 | zenon_intro zenon_H50; zenon_intro zenon_H4f ]. % 4.24/4.41 cut ((day3 (consecutive zenon_TX_z)) = (day3 (consecutive (sunday)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H51. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H17. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive (sunday)))); [idtac | apply NNPP; zenon_intro zenon_H43]. % 4.24/4.41 congruence. % 4.24/4.41 generalize (statement3 zenon_TX_cv). zenon_intro zenon_H52. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H52); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 4.24/4.41 exact (zenon_H54 zenon_H48). % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H53); [ zenon_intro zenon_H56; zenon_intro zenon_H26 | zenon_intro zenon_H55; zenon_intro zenon_H3a ]. % 4.24/4.41 apply (zenon_L4_); trivial. % 4.24/4.41 apply (zenon_L8_ zenon_TX_z); trivial. % 4.24/4.41 exact (zenon_H4c zenon_H50). % 4.24/4.41 (* end of lemma zenon_L9_ *) % 4.24/4.41 assert (zenon_L10_ : (day3 (consecutive (thursday))) -> (~(day2 (thursday))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H57 zenon_H4b. % 4.24/4.41 generalize (day3_follows_day2 (thursday)). zenon_intro zenon_H58. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H58); [ zenon_intro zenon_H4b; zenon_intro zenon_H5a | zenon_intro zenon_H59; zenon_intro zenon_H57 ]. % 4.24/4.41 exact (zenon_H5a zenon_H57). % 4.24/4.41 exact (zenon_H4b zenon_H59). % 4.24/4.41 (* end of lemma zenon_L10_ *) % 4.24/4.41 assert (zenon_L11_ : (~((day2 (thursday))\/((day2 (saturday))\/(day2 (sunday))))) -> (day3 (consecutive (thursday))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H47 zenon_H57. % 4.24/4.41 apply (zenon_notor_s _ _ zenon_H47). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 4.24/4.41 apply (zenon_L10_); trivial. % 4.24/4.41 (* end of lemma zenon_L11_ *) % 4.24/4.41 assert (zenon_L12_ : forall (zenon_TX_dp : zenon_U) (zenon_TX_z : zenon_U), (~(zenon_TX_z = zenon_TX_dp)) -> (truthday zenon_TX_dp) -> (day3 (consecutive (thursday))) -> (day3 (consecutive zenon_TX_z)) -> False). % 4.24/4.41 do 2 intro. intros zenon_H5b zenon_H5c zenon_H57 zenon_H17. % 4.24/4.41 generalize (truth_unique zenon_TX_z). zenon_intro zenon_H5e. % 4.24/4.41 generalize (zenon_H5e zenon_TX_dp). zenon_intro zenon_H5f. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H5f); [ zenon_intro zenon_H61 | zenon_intro zenon_H60 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H61); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 4.24/4.41 generalize (statement2 zenon_TX_z). zenon_intro zenon_H64. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H64); [ zenon_intro zenon_H18 | zenon_intro zenon_H65 ]. % 4.24/4.41 apply (zenon_L1_ zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H65); [ zenon_intro zenon_H63; zenon_intro zenon_H47 | zenon_intro zenon_H67; zenon_intro zenon_H66 ]. % 4.24/4.41 apply (zenon_L11_); trivial. % 4.24/4.41 exact (zenon_H63 zenon_H67). % 4.24/4.41 exact (zenon_H62 zenon_H5c). % 4.24/4.41 exact (zenon_H5b zenon_H60). % 4.24/4.41 (* end of lemma zenon_L12_ *) % 4.24/4.41 assert (zenon_L13_ : (~((monday) = (monday))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H68. % 4.24/4.41 apply zenon_H68. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L13_ *) % 4.24/4.41 assert (zenon_L14_ : (day3 (consecutive (saturday))) -> (~(day2 (saturday))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H69 zenon_H4d. % 4.24/4.41 generalize (day3_follows_day2 (saturday)). zenon_intro zenon_H6a. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H6a); [ zenon_intro zenon_H4d; zenon_intro zenon_H6c | zenon_intro zenon_H6b; zenon_intro zenon_H69 ]. % 4.24/4.41 exact (zenon_H6c zenon_H69). % 4.24/4.41 exact (zenon_H4d zenon_H6b). % 4.24/4.41 (* end of lemma zenon_L14_ *) % 4.24/4.41 assert (zenon_L15_ : (~((day2 (thursday))\/((day2 (saturday))\/(day2 (sunday))))) -> (day3 (consecutive (saturday))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H47 zenon_H69. % 4.24/4.41 apply (zenon_notor_s _ _ zenon_H47). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 4.24/4.41 apply (zenon_notor_s _ _ zenon_H4a). zenon_intro zenon_H4d. zenon_intro zenon_H4c. % 4.24/4.41 apply (zenon_L14_); trivial. % 4.24/4.41 (* end of lemma zenon_L15_ *) % 4.24/4.41 assert (zenon_L16_ : forall (zenon_TX_dp : zenon_U) (zenon_TX_z : zenon_U), (~(zenon_TX_z = zenon_TX_dp)) -> (truthday zenon_TX_dp) -> (day3 (consecutive (saturday))) -> (day3 (consecutive zenon_TX_z)) -> False). % 4.24/4.41 do 2 intro. intros zenon_H5b zenon_H5c zenon_H69 zenon_H17. % 4.24/4.41 generalize (truth_unique zenon_TX_z). zenon_intro zenon_H5e. % 4.24/4.41 generalize (zenon_H5e zenon_TX_dp). zenon_intro zenon_H5f. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H5f); [ zenon_intro zenon_H61 | zenon_intro zenon_H60 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H61); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 4.24/4.41 generalize (statement2 zenon_TX_z). zenon_intro zenon_H64. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H64); [ zenon_intro zenon_H18 | zenon_intro zenon_H65 ]. % 4.24/4.41 apply (zenon_L1_ zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H65); [ zenon_intro zenon_H63; zenon_intro zenon_H47 | zenon_intro zenon_H67; zenon_intro zenon_H66 ]. % 4.24/4.41 apply (zenon_L15_); trivial. % 4.24/4.41 exact (zenon_H63 zenon_H67). % 4.24/4.41 exact (zenon_H62 zenon_H5c). % 4.24/4.41 exact (zenon_H5b zenon_H60). % 4.24/4.41 (* end of lemma zenon_L16_ *) % 4.24/4.41 assert (zenon_L17_ : forall (zenon_TX_z : zenon_U) (zenon_TX_dp : zenon_U), (~((saturday) = zenon_TX_dp)) -> (truthday zenon_TX_dp) -> (day3 (consecutive (saturday))) -> (day3 (consecutive zenon_TX_z)) -> False). % 4.24/4.41 do 2 intro. intros zenon_H6d zenon_H5c zenon_H69 zenon_H17. % 4.24/4.41 generalize (day2_unique zenon_TX_dp). zenon_intro zenon_H6e. % 4.24/4.41 generalize (zenon_H6e (saturday)). zenon_intro zenon_H6f. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H6f); [ zenon_intro zenon_H71 | zenon_intro zenon_H70 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H71); [ zenon_intro zenon_H72 | zenon_intro zenon_H4d ]. % 4.24/4.41 generalize (day3_follows_day2 zenon_TX_dp). zenon_intro zenon_H73. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H73); [ zenon_intro zenon_H72; zenon_intro zenon_H76 | zenon_intro zenon_H75; zenon_intro zenon_H74 ]. % 4.24/4.41 cut ((day3 (consecutive zenon_TX_z)) = (day3 (consecutive zenon_TX_dp))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H76. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H17. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive zenon_TX_dp))); [idtac | apply NNPP; zenon_intro zenon_H77]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_z = zenon_TX_dp)); [idtac | apply NNPP; zenon_intro zenon_H5b]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L16_ zenon_TX_dp zenon_TX_z); trivial. % 4.24/4.41 exact (zenon_H72 zenon_H75). % 4.24/4.41 apply (zenon_L14_); trivial. % 4.24/4.41 apply zenon_H6d. apply sym_equal. exact zenon_H70. % 4.24/4.41 (* end of lemma zenon_L17_ *) % 4.24/4.41 assert (zenon_L18_ : (day3 (consecutive (sunday))) -> (~(day2 (sunday))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H4f zenon_H4c. % 4.24/4.41 generalize (day3_follows_day2 (sunday)). zenon_intro zenon_H4e. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H4e); [ zenon_intro zenon_H4c; zenon_intro zenon_H51 | zenon_intro zenon_H50; zenon_intro zenon_H4f ]. % 4.24/4.41 exact (zenon_H51 zenon_H4f). % 4.24/4.41 exact (zenon_H4c zenon_H50). % 4.24/4.41 (* end of lemma zenon_L18_ *) % 4.24/4.41 assert (zenon_L19_ : (~((day2 (thursday))\/((day2 (saturday))\/(day2 (sunday))))) -> (day3 (consecutive (sunday))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H47 zenon_H4f. % 4.24/4.41 apply (zenon_notor_s _ _ zenon_H47). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 4.24/4.41 apply (zenon_notor_s _ _ zenon_H4a). zenon_intro zenon_H4d. zenon_intro zenon_H4c. % 4.24/4.41 apply (zenon_L18_); trivial. % 4.24/4.41 (* end of lemma zenon_L19_ *) % 4.24/4.41 assert (zenon_L20_ : forall (zenon_TX_z : zenon_U), (day3 (consecutive zenon_TX_z)) -> (~(truthday zenon_TX_z)) -> (day3 (consecutive (sunday))) -> False). % 4.24/4.41 do 1 intro. intros zenon_H17 zenon_H63 zenon_H4f. % 4.24/4.41 generalize (statement2 zenon_TX_z). zenon_intro zenon_H64. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H64); [ zenon_intro zenon_H18 | zenon_intro zenon_H65 ]. % 4.24/4.41 apply (zenon_L1_ zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H65); [ zenon_intro zenon_H63; zenon_intro zenon_H47 | zenon_intro zenon_H67; zenon_intro zenon_H66 ]. % 4.24/4.41 apply (zenon_L19_); trivial. % 4.24/4.41 exact (zenon_H63 zenon_H67). % 4.24/4.41 (* end of lemma zenon_L20_ *) % 4.24/4.41 assert (zenon_L21_ : forall (zenon_TX_z : zenon_U) (zenon_TX_dp : zenon_U), (~(day3 (consecutive (monday)))) -> (forall Y : zenon_U, (((truthday zenon_TX_dp)/\(truthday Y))->(zenon_TX_dp = Y))) -> (truthday zenon_TX_dp) -> (truthday (monday)) -> (day3 (consecutive zenon_TX_z)) -> (day3 (consecutive (sunday))) -> False). % 4.24/4.41 do 2 intro. intros zenon_H78 zenon_H79 zenon_H5c zenon_H29 zenon_H17 zenon_H4f. % 4.24/4.41 cut ((day3 (consecutive zenon_TX_z)) = (day3 (consecutive (monday)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H78. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H17. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive (monday)))); [idtac | apply NNPP; zenon_intro zenon_H7a]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_z = (monday))); [idtac | apply NNPP; zenon_intro zenon_H7b]. % 4.24/4.41 congruence. % 4.24/4.41 generalize (zenon_H79 (monday)). zenon_intro zenon_H7c. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H7c); [ zenon_intro zenon_H7e | zenon_intro zenon_H7d ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H7e); [ zenon_intro zenon_H62 | zenon_intro zenon_H31 ]. % 4.24/4.41 exact (zenon_H62 zenon_H5c). % 4.24/4.41 exact (zenon_H31 zenon_H29). % 4.24/4.41 cut ((zenon_TX_dp = (monday)) = (zenon_TX_z = (monday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H7b. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H7d. % 4.24/4.41 cut (((monday) = (monday))); [idtac | apply NNPP; zenon_intro zenon_H68]. % 4.24/4.41 cut ((zenon_TX_dp = zenon_TX_z)); [idtac | apply NNPP; zenon_intro zenon_H7f]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic (zenon_TX_z = zenon_TX_z)); [ zenon_intro zenon_H80 | zenon_intro zenon_H81 ]. % 4.24/4.41 cut ((zenon_TX_z = zenon_TX_z) = (zenon_TX_dp = zenon_TX_z)). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H7f. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H80. % 4.24/4.41 cut ((zenon_TX_z = zenon_TX_z)); [idtac | apply NNPP; zenon_intro zenon_H81]. % 4.24/4.41 cut ((zenon_TX_z = zenon_TX_dp)); [idtac | apply NNPP; zenon_intro zenon_H5b]. % 4.24/4.41 congruence. % 4.24/4.41 generalize (truth_unique zenon_TX_z). zenon_intro zenon_H5e. % 4.24/4.41 generalize (zenon_H5e zenon_TX_dp). zenon_intro zenon_H5f. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H5f); [ zenon_intro zenon_H61 | zenon_intro zenon_H60 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H61); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 4.24/4.41 apply (zenon_L20_ zenon_TX_z); trivial. % 4.24/4.41 exact (zenon_H62 zenon_H5c). % 4.24/4.41 exact (zenon_H5b zenon_H60). % 4.24/4.41 apply zenon_H81. apply refl_equal. % 4.24/4.41 apply zenon_H81. apply refl_equal. % 4.24/4.41 apply zenon_H68. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L21_ *) % 4.24/4.41 assert (zenon_L22_ : forall (zenon_TX_dp : zenon_U) (zenon_TX_z : zenon_U), ((day2 (thursday))\/((day2 (saturday))\/(day2 (sunday)))) -> (~((monday) = (thursday))) -> (~((monday) = (saturday))) -> (day3 (consecutive zenon_TX_z)) -> (truthday (monday)) -> (truthday zenon_TX_dp) -> (~((monday) = (sunday))) -> False). % 4.24/4.41 do 2 intro. intros zenon_H66 zenon_H82 zenon_H83 zenon_H17 zenon_H29 zenon_H5c zenon_H84. % 4.24/4.41 apply (zenon_or_s _ _ zenon_H66); [ zenon_intro zenon_H59 | zenon_intro zenon_H85 ]. % 4.24/4.41 generalize (day3_follows_day2 (thursday)). zenon_intro zenon_H58. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H58); [ zenon_intro zenon_H4b; zenon_intro zenon_H5a | zenon_intro zenon_H59; zenon_intro zenon_H57 ]. % 4.24/4.41 exact (zenon_H4b zenon_H59). % 4.24/4.41 generalize (truth_unique zenon_TX_dp). zenon_intro zenon_H79. % 4.24/4.41 generalize (zenon_H79 (monday)). zenon_intro zenon_H7c. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H7c); [ zenon_intro zenon_H7e | zenon_intro zenon_H7d ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H7e); [ zenon_intro zenon_H62 | zenon_intro zenon_H31 ]. % 4.24/4.41 exact (zenon_H62 zenon_H5c). % 4.24/4.41 exact (zenon_H31 zenon_H29). % 4.24/4.41 generalize (day2_unique zenon_TX_dp). zenon_intro zenon_H6e. % 4.24/4.41 elim (classic ((thursday) = (thursday))); [ zenon_intro zenon_H86 | zenon_intro zenon_H87 ]. % 4.24/4.41 cut (((thursday) = (thursday)) = ((monday) = (thursday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H82. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H86. % 4.24/4.41 cut (((thursday) = (thursday))); [idtac | apply NNPP; zenon_intro zenon_H87]. % 4.24/4.41 cut (((thursday) = (monday))); [idtac | apply NNPP; zenon_intro zenon_H88]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_dp = (monday)) = ((thursday) = (monday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H88. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H7d. % 4.24/4.41 cut (((monday) = (monday))); [idtac | apply NNPP; zenon_intro zenon_H68]. % 4.24/4.41 cut ((zenon_TX_dp = (thursday))); [idtac | apply NNPP; zenon_intro zenon_H89]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((thursday) = (thursday))); [ zenon_intro zenon_H86 | zenon_intro zenon_H87 ]. % 4.24/4.41 cut (((thursday) = (thursday)) = (zenon_TX_dp = (thursday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H89. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H86. % 4.24/4.41 cut (((thursday) = (thursday))); [idtac | apply NNPP; zenon_intro zenon_H87]. % 4.24/4.41 cut (((thursday) = zenon_TX_dp)); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 4.24/4.41 congruence. % 4.24/4.41 generalize (zenon_H6e (thursday)). zenon_intro zenon_H8b. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H8b); [ zenon_intro zenon_H8d | zenon_intro zenon_H8c ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H8d); [ zenon_intro zenon_H72 | zenon_intro zenon_H4b ]. % 4.24/4.41 generalize (day3_follows_day2 zenon_TX_dp). zenon_intro zenon_H73. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H73); [ zenon_intro zenon_H72; zenon_intro zenon_H76 | zenon_intro zenon_H75; zenon_intro zenon_H74 ]. % 4.24/4.41 cut ((day3 (consecutive zenon_TX_z)) = (day3 (consecutive zenon_TX_dp))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H76. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H17. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive zenon_TX_dp))); [idtac | apply NNPP; zenon_intro zenon_H77]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_z = zenon_TX_dp)); [idtac | apply NNPP; zenon_intro zenon_H5b]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L12_ zenon_TX_dp zenon_TX_z); trivial. % 4.24/4.41 exact (zenon_H72 zenon_H75). % 4.24/4.41 apply (zenon_L10_); trivial. % 4.24/4.41 apply zenon_H8a. apply sym_equal. exact zenon_H8c. % 4.24/4.41 apply zenon_H87. apply refl_equal. % 4.24/4.41 apply zenon_H87. apply refl_equal. % 4.24/4.41 apply zenon_H68. apply refl_equal. % 4.24/4.41 apply zenon_H87. apply refl_equal. % 4.24/4.41 apply zenon_H87. apply refl_equal. % 4.24/4.41 apply (zenon_or_s _ _ zenon_H85); [ zenon_intro zenon_H6b | zenon_intro zenon_H50 ]. % 4.24/4.41 generalize (day3_follows_day2 (saturday)). zenon_intro zenon_H6a. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H6a); [ zenon_intro zenon_H4d; zenon_intro zenon_H6c | zenon_intro zenon_H6b; zenon_intro zenon_H69 ]. % 4.24/4.41 exact (zenon_H4d zenon_H6b). % 4.24/4.41 generalize (truth_unique zenon_TX_dp). zenon_intro zenon_H79. % 4.24/4.41 generalize (zenon_H79 (monday)). zenon_intro zenon_H7c. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H7c); [ zenon_intro zenon_H7e | zenon_intro zenon_H7d ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H7e); [ zenon_intro zenon_H62 | zenon_intro zenon_H31 ]. % 4.24/4.41 exact (zenon_H62 zenon_H5c). % 4.24/4.41 exact (zenon_H31 zenon_H29). % 4.24/4.41 elim (classic ((saturday) = (saturday))); [ zenon_intro zenon_H8e | zenon_intro zenon_H8f ]. % 4.24/4.41 cut (((saturday) = (saturday)) = ((monday) = (saturday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H83. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H8e. % 4.24/4.41 cut (((saturday) = (saturday))); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 4.24/4.41 cut (((saturday) = (monday))); [idtac | apply NNPP; zenon_intro zenon_H90]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_dp = (monday)) = ((saturday) = (monday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H90. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H7d. % 4.24/4.41 cut (((monday) = (monday))); [idtac | apply NNPP; zenon_intro zenon_H68]. % 4.24/4.41 cut ((zenon_TX_dp = (saturday))); [idtac | apply NNPP; zenon_intro zenon_H91]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((saturday) = (saturday))); [ zenon_intro zenon_H8e | zenon_intro zenon_H8f ]. % 4.24/4.41 cut (((saturday) = (saturday)) = (zenon_TX_dp = (saturday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H91. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H8e. % 4.24/4.41 cut (((saturday) = (saturday))); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 4.24/4.41 cut (((saturday) = zenon_TX_dp)); [idtac | apply NNPP; zenon_intro zenon_H6d]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L17_ zenon_TX_z zenon_TX_dp); trivial. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 apply zenon_H68. apply refl_equal. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 generalize (day3_follows_day2 (sunday)). zenon_intro zenon_H4e. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H4e); [ zenon_intro zenon_H4c; zenon_intro zenon_H51 | zenon_intro zenon_H50; zenon_intro zenon_H4f ]. % 4.24/4.41 exact (zenon_H4c zenon_H50). % 4.24/4.41 generalize (truth_unique zenon_TX_dp). zenon_intro zenon_H79. % 4.24/4.41 generalize (day2_unique (monday)). zenon_intro zenon_H92. % 4.24/4.41 generalize (zenon_H92 (sunday)). zenon_intro zenon_H93. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H93); [ zenon_intro zenon_H95 | zenon_intro zenon_H94 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H95); [ zenon_intro zenon_H96 | zenon_intro zenon_H4c ]. % 4.24/4.41 generalize (day3_follows_day2 (monday)). zenon_intro zenon_H97. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H97); [ zenon_intro zenon_H96; zenon_intro zenon_H78 | zenon_intro zenon_H99; zenon_intro zenon_H98 ]. % 4.24/4.41 apply (zenon_L21_ zenon_TX_z zenon_TX_dp); trivial. % 4.24/4.41 exact (zenon_H96 zenon_H99). % 4.24/4.41 apply (zenon_L18_); trivial. % 4.24/4.41 exact (zenon_H84 zenon_H94). % 4.24/4.41 (* end of lemma zenon_L22_ *) % 4.24/4.41 assert (zenon_L23_ : forall (zenon_TX_cv : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_z : zenon_U), (~((~(truthday (monday)))/\(~(truthday (tuesday))))) -> (~(truthday (tuesday))) -> (day3 (consecutive zenon_TX_z)) -> (truthday zenon_TX_dp) -> (~((monday) = (thursday))) -> (~((monday) = (saturday))) -> (~((monday) = (sunday))) -> (day3 zenon_TX_cv) -> (~((monday) = (wednesday))) -> (~((monday) = (friday))) -> False). % 4.24/4.41 do 3 intro. intros zenon_H9a zenon_G zenon_H17 zenon_H5c zenon_H82 zenon_H83 zenon_H84 zenon_H48 zenon_H28 zenon_H27. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H9a); [ zenon_intro zenon_H9c | zenon_intro zenon_H9b ]. % 4.24/4.41 apply zenon_H9c. zenon_intro zenon_H29. % 4.24/4.41 generalize (statement2 zenon_TX_z). zenon_intro zenon_H64. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H64); [ zenon_intro zenon_H18 | zenon_intro zenon_H65 ]. % 4.24/4.41 apply (zenon_L1_ zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H65); [ zenon_intro zenon_H63; zenon_intro zenon_H47 | zenon_intro zenon_H67; zenon_intro zenon_H66 ]. % 4.24/4.41 apply (zenon_L9_ zenon_TX_z zenon_TX_cv); trivial. % 4.24/4.41 apply (zenon_L22_ zenon_TX_dp zenon_TX_z); trivial. % 4.24/4.41 exact (zenon_H9b zenon_G). % 4.24/4.41 (* end of lemma zenon_L23_ *) % 4.24/4.41 assert (zenon_L24_ : forall (zenon_TX_bf : zenon_U), (day3 (consecutive (consecutive zenon_TX_bf))) -> (~(truthday zenon_TX_bf)) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> False). % 4.24/4.41 do 1 intro. intros zenon_H1d zenon_H9d zenon_H9e. % 4.24/4.41 generalize (statement1 zenon_TX_bf). zenon_intro zenon_H9f. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H9f); [ zenon_intro zenon_H23 | zenon_intro zenon_Ha0 ]. % 4.24/4.41 apply (zenon_L3_ zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_Ha0); [ zenon_intro zenon_H9d; zenon_intro zenon_H9a | zenon_intro zenon_Ha1; zenon_intro zenon_H9e ]. % 4.24/4.41 exact (zenon_H9a zenon_H9e). % 4.24/4.41 exact (zenon_H9d zenon_Ha1). % 4.24/4.41 (* end of lemma zenon_L24_ *) % 4.24/4.41 assert (zenon_L25_ : forall (zenon_TX_bf : zenon_U), (~((consecutive zenon_TX_bf) = (consecutive (wednesday)))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (truthday (wednesday)) -> False). % 4.24/4.41 do 1 intro. intros zenon_Ha2 zenon_H1d zenon_H9e zenon_H2c. % 4.24/4.41 cut ((zenon_TX_bf = (wednesday))); [idtac | apply NNPP; zenon_intro zenon_Ha3]. % 4.24/4.41 congruence. % 4.24/4.41 generalize (truth_unique zenon_TX_bf). zenon_intro zenon_Ha4. % 4.24/4.41 generalize (zenon_Ha4 (wednesday)). zenon_intro zenon_Ha5. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_Ha5); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Ha6 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_Ha7); [ zenon_intro zenon_H9d | zenon_intro zenon_H32 ]. % 4.24/4.41 apply (zenon_L24_ zenon_TX_bf); trivial. % 4.24/4.41 exact (zenon_H32 zenon_H2c). % 4.24/4.41 exact (zenon_Ha3 zenon_Ha6). % 4.24/4.41 (* end of lemma zenon_L25_ *) % 4.24/4.41 assert (zenon_L26_ : (~((thursday) = (thursday))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H87. % 4.24/4.41 apply zenon_H87. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L26_ *) % 4.24/4.41 assert (zenon_L27_ : forall (zenon_TX_bf : zenon_U), (~((consecutive zenon_TX_bf) = (consecutive (friday)))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (truthday (friday)) -> False). % 4.24/4.41 do 1 intro. intros zenon_Ha8 zenon_H1d zenon_H9e zenon_H33. % 4.24/4.41 cut ((zenon_TX_bf = (friday))); [idtac | apply NNPP; zenon_intro zenon_Ha9]. % 4.24/4.41 congruence. % 4.24/4.41 generalize (truth_unique zenon_TX_bf). zenon_intro zenon_Ha4. % 4.24/4.41 generalize (zenon_Ha4 (friday)). zenon_intro zenon_Haa. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_Haa); [ zenon_intro zenon_Hac | zenon_intro zenon_Hab ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_Hac); [ zenon_intro zenon_H9d | zenon_intro zenon_H38 ]. % 4.24/4.41 apply (zenon_L24_ zenon_TX_bf); trivial. % 4.24/4.41 exact (zenon_H38 zenon_H33). % 4.24/4.41 exact (zenon_Ha9 zenon_Hab). % 4.24/4.41 (* end of lemma zenon_L27_ *) % 4.24/4.41 assert (zenon_L28_ : (~((saturday) = (saturday))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H8f. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L28_ *) % 4.24/4.41 assert (zenon_L29_ : forall (zenon_TX_bf : zenon_U), (~((~(truthday (wednesday)))/\(~(truthday (friday))))) -> (~((consecutive zenon_TX_bf) = (saturday))) -> (~((consecutive zenon_TX_bf) = (thursday))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> False). % 4.24/4.41 do 1 intro. intros zenon_H26 zenon_Had zenon_Hae zenon_H9e zenon_H1d. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H26); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 4.24/4.41 apply zenon_H2b. zenon_intro zenon_H2c. % 4.24/4.41 cut (((consecutive (wednesday)) = (thursday)) = ((consecutive zenon_TX_bf) = (thursday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Hae. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact thursday_follows_wednesday. % 4.24/4.41 cut (((thursday) = (thursday))); [idtac | apply NNPP; zenon_intro zenon_H87]. % 4.24/4.41 cut (((consecutive (wednesday)) = (consecutive zenon_TX_bf))); [idtac | apply NNPP; zenon_intro zenon_Haf]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((consecutive zenon_TX_bf) = (consecutive zenon_TX_bf))); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Hb1 ]. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive zenon_TX_bf)) = ((consecutive (wednesday)) = (consecutive zenon_TX_bf))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Haf. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_Hb0. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive zenon_TX_bf))); [idtac | apply NNPP; zenon_intro zenon_Hb1]. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive (wednesday)))); [idtac | apply NNPP; zenon_intro zenon_Ha2]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L25_ zenon_TX_bf); trivial. % 4.24/4.41 apply zenon_Hb1. apply refl_equal. % 4.24/4.41 apply zenon_Hb1. apply refl_equal. % 4.24/4.41 apply zenon_H87. apply refl_equal. % 4.24/4.41 apply zenon_H2a. zenon_intro zenon_H33. % 4.24/4.41 cut (((consecutive (friday)) = (saturday)) = ((consecutive zenon_TX_bf) = (saturday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Had. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact saturday_follows_friday. % 4.24/4.41 cut (((saturday) = (saturday))); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 4.24/4.41 cut (((consecutive (friday)) = (consecutive zenon_TX_bf))); [idtac | apply NNPP; zenon_intro zenon_Hb2]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((consecutive zenon_TX_bf) = (consecutive zenon_TX_bf))); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Hb1 ]. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive zenon_TX_bf)) = ((consecutive (friday)) = (consecutive zenon_TX_bf))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Hb2. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_Hb0. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive zenon_TX_bf))); [idtac | apply NNPP; zenon_intro zenon_Hb1]. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive (friday)))); [idtac | apply NNPP; zenon_intro zenon_Ha8]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L27_ zenon_TX_bf); trivial. % 4.24/4.41 apply zenon_Hb1. apply refl_equal. % 4.24/4.41 apply zenon_Hb1. apply refl_equal. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L29_ *) % 4.24/4.41 assert (zenon_L30_ : forall (zenon_TX_z : zenon_U), (~(day3 (consecutive (monday)))) -> (day3 (consecutive zenon_TX_z)) -> (zenon_TX_z = (monday)) -> False). % 4.24/4.41 do 1 intro. intros zenon_H78 zenon_H17 zenon_Hb3. % 4.24/4.41 cut ((day3 (consecutive zenon_TX_z)) = (day3 (consecutive (monday)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H78. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H17. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive (monday)))); [idtac | apply NNPP; zenon_intro zenon_H7a]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_z = (monday))); [idtac | apply NNPP; zenon_intro zenon_H7b]. % 4.24/4.41 congruence. % 4.24/4.41 exact (zenon_H7b zenon_Hb3). % 4.24/4.41 (* end of lemma zenon_L30_ *) % 4.24/4.41 assert (zenon_L31_ : forall (zenon_TX_z : zenon_U), (zenon_TX_z = (monday)) -> (day3 (consecutive zenon_TX_z)) -> (~(day2 (monday))) -> False). % 4.24/4.41 do 1 intro. intros zenon_Hb3 zenon_H17 zenon_H96. % 4.24/4.41 generalize (day3_follows_day2 (monday)). zenon_intro zenon_H97. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H97); [ zenon_intro zenon_H96; zenon_intro zenon_H78 | zenon_intro zenon_H99; zenon_intro zenon_H98 ]. % 4.24/4.41 apply (zenon_L30_ zenon_TX_z); trivial. % 4.24/4.41 exact (zenon_H96 zenon_H99). % 4.24/4.41 (* end of lemma zenon_L31_ *) % 4.24/4.41 assert (zenon_L32_ : (~((tuesday) = (tuesday))) -> False). % 4.24/4.41 do 0 intro. intros zenon_Hb4. % 4.24/4.41 apply zenon_Hb4. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L32_ *) % 4.24/4.41 assert (zenon_L33_ : forall (zenon_TX_bf : zenon_U), ((monday) = (consecutive zenon_TX_bf)) -> (~((tuesday) = (consecutive (consecutive zenon_TX_bf)))) -> False). % 4.24/4.41 do 1 intro. intros zenon_Hb5 zenon_Hb6. % 4.24/4.41 elim (classic ((consecutive (consecutive zenon_TX_bf)) = (consecutive (consecutive zenon_TX_bf)))); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb8 ]. % 4.24/4.41 cut (((consecutive (consecutive zenon_TX_bf)) = (consecutive (consecutive zenon_TX_bf))) = ((tuesday) = (consecutive (consecutive zenon_TX_bf)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Hb6. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_Hb7. % 4.24/4.41 cut (((consecutive (consecutive zenon_TX_bf)) = (consecutive (consecutive zenon_TX_bf)))); [idtac | apply NNPP; zenon_intro zenon_Hb8]. % 4.24/4.41 cut (((consecutive (consecutive zenon_TX_bf)) = (tuesday))); [idtac | apply NNPP; zenon_intro zenon_Hb9]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive (monday)) = (tuesday)) = ((consecutive (consecutive zenon_TX_bf)) = (tuesday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Hb9. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact tuesday_follows_monday. % 4.24/4.41 cut (((tuesday) = (tuesday))); [idtac | apply NNPP; zenon_intro zenon_Hb4]. % 4.24/4.41 cut (((consecutive (monday)) = (consecutive (consecutive zenon_TX_bf)))); [idtac | apply NNPP; zenon_intro zenon_Hba]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((consecutive (consecutive zenon_TX_bf)) = (consecutive (consecutive zenon_TX_bf)))); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb8 ]. % 4.24/4.41 cut (((consecutive (consecutive zenon_TX_bf)) = (consecutive (consecutive zenon_TX_bf))) = ((consecutive (monday)) = (consecutive (consecutive zenon_TX_bf)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Hba. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_Hb7. % 4.24/4.41 cut (((consecutive (consecutive zenon_TX_bf)) = (consecutive (consecutive zenon_TX_bf)))); [idtac | apply NNPP; zenon_intro zenon_Hb8]. % 4.24/4.41 cut (((consecutive (consecutive zenon_TX_bf)) = (consecutive (monday)))); [idtac | apply NNPP; zenon_intro zenon_Hbb]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (monday))); [idtac | apply NNPP; zenon_intro zenon_Hbc]. % 4.24/4.41 congruence. % 4.24/4.41 apply zenon_Hbc. apply sym_equal. exact zenon_Hb5. % 4.24/4.41 apply zenon_Hb8. apply refl_equal. % 4.24/4.41 apply zenon_Hb8. apply refl_equal. % 4.24/4.41 apply zenon_Hb4. apply refl_equal. % 4.24/4.41 apply zenon_Hb8. apply refl_equal. % 4.24/4.41 apply zenon_Hb8. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L33_ *) % 4.24/4.41 assert (zenon_L34_ : forall (zenon_TX_z : zenon_U) (zenon_TX_bf : zenon_U), (((day2 (monday))/\(day2 (consecutive zenon_TX_bf)))->((monday) = (consecutive zenon_TX_bf))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> (zenon_TX_z = (monday)) -> (day3 (consecutive zenon_TX_z)) -> (~((tuesday) = (consecutive (consecutive zenon_TX_bf)))) -> False). % 4.24/4.41 do 2 intro. intros zenon_Hbd zenon_H1d zenon_Hb3 zenon_H17 zenon_Hb6. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_Hbd); [ zenon_intro zenon_Hbe | zenon_intro zenon_Hb5 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_Hbe); [ zenon_intro zenon_H96 | zenon_intro zenon_H1e ]. % 4.24/4.41 apply (zenon_L31_ zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_L2_ zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_L33_ zenon_TX_bf); trivial. % 4.24/4.41 (* end of lemma zenon_L34_ *) % 4.24/4.41 assert (zenon_L35_ : forall (zenon_TX_bf : zenon_U) (zenon_TX_z : zenon_U), (forall Y : zenon_U, (((day2 (monday))/\(day2 Y))->((monday) = Y))) -> (zenon_TX_z = (monday)) -> (day3 (consecutive zenon_TX_z)) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> (~((tuesday) = (consecutive (consecutive zenon_TX_bf)))) -> False). % 4.24/4.41 do 2 intro. intros zenon_H92 zenon_Hb3 zenon_H17 zenon_H1d zenon_Hb6. % 4.24/4.41 generalize (zenon_H92 (consecutive zenon_TX_bf)). zenon_intro zenon_Hbd. % 4.24/4.41 apply (zenon_L34_ zenon_TX_z zenon_TX_bf); trivial. % 4.24/4.41 (* end of lemma zenon_L35_ *) % 4.24/4.41 assert (zenon_L36_ : forall (zenon_TX_z : zenon_U), (~(day3 (consecutive (tuesday)))) -> (day3 (consecutive zenon_TX_z)) -> (zenon_TX_z = (tuesday)) -> False). % 4.24/4.41 do 1 intro. intros zenon_Hbf zenon_H17 zenon_Hc0. % 4.24/4.41 cut ((day3 (consecutive zenon_TX_z)) = (day3 (consecutive (tuesday)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Hbf. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H17. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive (tuesday)))); [idtac | apply NNPP; zenon_intro zenon_Hc1]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_z = (tuesday))); [idtac | apply NNPP; zenon_intro zenon_Hc2]. % 4.24/4.41 congruence. % 4.24/4.41 exact (zenon_Hc2 zenon_Hc0). % 4.24/4.41 (* end of lemma zenon_L36_ *) % 4.24/4.41 assert (zenon_L37_ : forall (zenon_TX_bf : zenon_U), (~(zenon_TX_bf = (consecutive (tuesday)))) -> (truthday (consecutive (tuesday))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> False). % 4.24/4.41 do 1 intro. intros zenon_Hc3 zenon_Hc4 zenon_H9e zenon_H1d. % 4.24/4.41 generalize (truth_unique zenon_TX_bf). zenon_intro zenon_Ha4. % 4.24/4.41 generalize (zenon_Ha4 (consecutive (tuesday))). zenon_intro zenon_Hc5. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_Hc5); [ zenon_intro zenon_Hc7 | zenon_intro zenon_Hc6 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_Hc7); [ zenon_intro zenon_H9d | zenon_intro zenon_Hc8 ]. % 4.24/4.41 apply (zenon_L24_ zenon_TX_bf); trivial. % 4.24/4.41 exact (zenon_Hc8 zenon_Hc4). % 4.24/4.41 exact (zenon_Hc3 zenon_Hc6). % 4.24/4.41 (* end of lemma zenon_L37_ *) % 4.24/4.41 assert (zenon_L38_ : forall (zenon_TX_bf : zenon_U), ((truthday (consecutive (tuesday)))<->((~(truthday (wednesday)))/\(~(truthday (friday))))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (~(zenon_TX_bf = (consecutive (tuesday)))) -> ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> False). % 4.24/4.41 do 1 intro. intros zenon_Hc9 zenon_H1d zenon_H9e zenon_Hc3 zenon_H3a. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_Hc9); [ zenon_intro zenon_Hc8; zenon_intro zenon_H26 | zenon_intro zenon_Hc4; zenon_intro zenon_H3a ]. % 4.24/4.41 exact (zenon_H26 zenon_H3a). % 4.24/4.41 apply (zenon_L37_ zenon_TX_bf); trivial. % 4.24/4.41 (* end of lemma zenon_L38_ *) % 4.24/4.41 assert (zenon_L39_ : (~((wednesday) = (wednesday))) -> False). % 4.24/4.41 do 0 intro. intros zenon_Hca. % 4.24/4.41 apply zenon_Hca. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L39_ *) % 4.24/4.41 assert (zenon_L40_ : forall (zenon_TX_bf : zenon_U), ((truthday (consecutive (tuesday)))<->((~(truthday (monday)))/\(~(truthday (tuesday))))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> (~(zenon_TX_bf = (wednesday))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> False). % 4.24/4.41 do 1 intro. intros zenon_Hcb zenon_H1d zenon_Ha3 zenon_H9e. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_Hcb); [ zenon_intro zenon_Hc8; zenon_intro zenon_H9a | zenon_intro zenon_Hc4; zenon_intro zenon_H9e ]. % 4.24/4.41 exact (zenon_H9a zenon_H9e). % 4.24/4.41 cut (((consecutive (tuesday)) = (wednesday)) = (zenon_TX_bf = (wednesday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Ha3. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact wednesday_follows_tuesday. % 4.24/4.41 cut (((wednesday) = (wednesday))); [idtac | apply NNPP; zenon_intro zenon_Hca]. % 4.24/4.41 cut (((consecutive (tuesday)) = zenon_TX_bf)); [idtac | apply NNPP; zenon_intro zenon_Hcc]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic (zenon_TX_bf = zenon_TX_bf)); [ zenon_intro zenon_Hcd | zenon_intro zenon_Hce ]. % 4.24/4.41 cut ((zenon_TX_bf = zenon_TX_bf) = ((consecutive (tuesday)) = zenon_TX_bf)). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Hcc. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_Hcd. % 4.24/4.41 cut ((zenon_TX_bf = zenon_TX_bf)); [idtac | apply NNPP; zenon_intro zenon_Hce]. % 4.24/4.41 cut ((zenon_TX_bf = (consecutive (tuesday)))); [idtac | apply NNPP; zenon_intro zenon_Hc3]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L37_ zenon_TX_bf); trivial. % 4.24/4.41 apply zenon_Hce. apply refl_equal. % 4.24/4.41 apply zenon_Hce. apply refl_equal. % 4.24/4.41 apply zenon_Hca. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L40_ *) % 4.24/4.41 assert (zenon_L41_ : forall (zenon_TX_z : zenon_U) (zenon_TX_bf : zenon_U), ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> (zenon_TX_z = (tuesday)) -> (day3 (consecutive zenon_TX_z)) -> (~(zenon_TX_bf = (wednesday))) -> False). % 4.24/4.41 do 2 intro. intros zenon_H3a zenon_H9e zenon_H1d zenon_Hc0 zenon_H17 zenon_Ha3. % 4.24/4.41 generalize (statement1 (consecutive (tuesday))). zenon_intro zenon_Hcf. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_Hcf); [ zenon_intro zenon_Hd0 | zenon_intro zenon_Hcb ]. % 4.24/4.41 generalize (day2_follows_day1 (consecutive (tuesday))). zenon_intro zenon_Hd1. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_Hd1); [ zenon_intro zenon_Hd0; zenon_intro zenon_Hd4 | zenon_intro zenon_Hd3; zenon_intro zenon_Hd2 ]. % 4.24/4.41 generalize (day3_follows_day2 (consecutive (consecutive (tuesday)))). zenon_intro zenon_Hd5. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_Hd5); [ zenon_intro zenon_Hd4; zenon_intro zenon_Hd7 | zenon_intro zenon_Hd2; zenon_intro zenon_Hd6 ]. % 4.24/4.41 cut ((day3 (consecutive (consecutive zenon_TX_bf))) = (day3 (consecutive (consecutive (consecutive (tuesday)))))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Hd7. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H1d. % 4.24/4.41 cut (((consecutive (consecutive zenon_TX_bf)) = (consecutive (consecutive (consecutive (tuesday)))))); [idtac | apply NNPP; zenon_intro zenon_Hd8]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive (consecutive (tuesday))))); [idtac | apply NNPP; zenon_intro zenon_Hd9]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_bf = (consecutive (tuesday)))); [idtac | apply NNPP; zenon_intro zenon_Hc3]. % 4.24/4.41 congruence. % 4.24/4.41 generalize (statement3 (consecutive (tuesday))). zenon_intro zenon_Hda. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_Hda); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hc9 ]. % 4.24/4.41 apply (zenon_L36_ zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_L38_ zenon_TX_bf); trivial. % 4.24/4.41 exact (zenon_Hd4 zenon_Hd2). % 4.24/4.41 exact (zenon_Hd0 zenon_Hd3). % 4.24/4.41 apply (zenon_L40_ zenon_TX_bf); trivial. % 4.24/4.41 (* end of lemma zenon_L41_ *) % 4.24/4.41 assert (zenon_L42_ : (~((consecutive (consecutive (tuesday))) = (consecutive (wednesday)))) -> False). % 4.24/4.41 do 0 intro. intros zenon_Hdb. % 4.24/4.41 cut (((consecutive (tuesday)) = (wednesday))); [idtac | apply NNPP; zenon_intro zenon_Hdc]. % 4.24/4.41 congruence. % 4.24/4.41 exact (zenon_Hdc wednesday_follows_tuesday). % 4.24/4.41 (* end of lemma zenon_L42_ *) % 4.24/4.41 assert (zenon_L43_ : (~((thursday) = (consecutive (consecutive (tuesday))))) -> False). % 4.24/4.41 do 0 intro. intros zenon_Hdd. % 4.24/4.41 elim (classic ((consecutive (consecutive (tuesday))) = (consecutive (consecutive (tuesday))))); [ zenon_intro zenon_Hde | zenon_intro zenon_Hdf ]. % 4.24/4.41 cut (((consecutive (consecutive (tuesday))) = (consecutive (consecutive (tuesday)))) = ((thursday) = (consecutive (consecutive (tuesday))))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Hdd. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_Hde. % 4.24/4.41 cut (((consecutive (consecutive (tuesday))) = (consecutive (consecutive (tuesday))))); [idtac | apply NNPP; zenon_intro zenon_Hdf]. % 4.24/4.41 cut (((consecutive (consecutive (tuesday))) = (thursday))); [idtac | apply NNPP; zenon_intro zenon_He0]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive (wednesday)) = (thursday)) = ((consecutive (consecutive (tuesday))) = (thursday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_He0. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact thursday_follows_wednesday. % 4.24/4.41 cut (((thursday) = (thursday))); [idtac | apply NNPP; zenon_intro zenon_H87]. % 4.24/4.41 cut (((consecutive (wednesday)) = (consecutive (consecutive (tuesday))))); [idtac | apply NNPP; zenon_intro zenon_He1]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((consecutive (consecutive (tuesday))) = (consecutive (consecutive (tuesday))))); [ zenon_intro zenon_Hde | zenon_intro zenon_Hdf ]. % 4.24/4.41 cut (((consecutive (consecutive (tuesday))) = (consecutive (consecutive (tuesday)))) = ((consecutive (wednesday)) = (consecutive (consecutive (tuesday))))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_He1. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_Hde. % 4.24/4.41 cut (((consecutive (consecutive (tuesday))) = (consecutive (consecutive (tuesday))))); [idtac | apply NNPP; zenon_intro zenon_Hdf]. % 4.24/4.41 cut (((consecutive (consecutive (tuesday))) = (consecutive (wednesday)))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L42_); trivial. % 4.24/4.41 apply zenon_Hdf. apply refl_equal. % 4.24/4.41 apply zenon_Hdf. apply refl_equal. % 4.24/4.41 apply zenon_H87. apply refl_equal. % 4.24/4.41 apply zenon_Hdf. apply refl_equal. % 4.24/4.41 apply zenon_Hdf. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L43_ *) % 4.24/4.41 assert (zenon_L44_ : forall (zenon_TX_z : zenon_U), (~((consecutive zenon_TX_z) = (consecutive (consecutive (tuesday))))) -> (zenon_TX_z = (wednesday)) -> False). % 4.24/4.41 do 1 intro. intros zenon_He2 zenon_He3. % 4.24/4.41 cut (((consecutive (wednesday)) = (thursday)) = ((consecutive zenon_TX_z) = (consecutive (consecutive (tuesday))))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_He2. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact thursday_follows_wednesday. % 4.24/4.41 cut (((thursday) = (consecutive (consecutive (tuesday))))); [idtac | apply NNPP; zenon_intro zenon_Hdd]. % 4.24/4.41 cut (((consecutive (wednesday)) = (consecutive zenon_TX_z))); [idtac | apply NNPP; zenon_intro zenon_He4]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((consecutive zenon_TX_z) = (consecutive zenon_TX_z))); [ zenon_intro zenon_He5 | zenon_intro zenon_He6 ]. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive zenon_TX_z)) = ((consecutive (wednesday)) = (consecutive zenon_TX_z))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_He4. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_He5. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive zenon_TX_z))); [idtac | apply NNPP; zenon_intro zenon_He6]. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive (wednesday)))); [idtac | apply NNPP; zenon_intro zenon_He7]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_z = (wednesday))); [idtac | apply NNPP; zenon_intro zenon_He8]. % 4.24/4.41 congruence. % 4.24/4.41 exact (zenon_He8 zenon_He3). % 4.24/4.41 apply zenon_He6. apply refl_equal. % 4.24/4.41 apply zenon_He6. apply refl_equal. % 4.24/4.41 apply (zenon_L43_); trivial. % 4.24/4.41 (* end of lemma zenon_L44_ *) % 4.24/4.41 assert (zenon_L45_ : forall (zenon_TX_z : zenon_U), (~(day3 (consecutive (friday)))) -> (day3 (consecutive zenon_TX_z)) -> (zenon_TX_z = (friday)) -> False). % 4.24/4.41 do 1 intro. intros zenon_He9 zenon_H17 zenon_Hea. % 4.24/4.41 cut ((day3 (consecutive zenon_TX_z)) = (day3 (consecutive (friday)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_He9. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H17. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive (friday)))); [idtac | apply NNPP; zenon_intro zenon_Heb]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_z = (friday))); [idtac | apply NNPP; zenon_intro zenon_Hec]. % 4.24/4.41 congruence. % 4.24/4.41 exact (zenon_Hec zenon_Hea). % 4.24/4.41 (* end of lemma zenon_L45_ *) % 4.24/4.41 assert (zenon_L46_ : forall (zenon_TX_z : zenon_U) (zenon_TX_bf : zenon_U), (~(zenon_TX_bf = (saturday))) -> (day3 (consecutive zenon_TX_z)) -> (zenon_TX_z = (friday)) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> False). % 4.24/4.41 do 2 intro. intros zenon_Hed zenon_H17 zenon_Hea zenon_H9e zenon_H1d zenon_H3a. % 4.24/4.41 cut (((consecutive (friday)) = (saturday)) = (zenon_TX_bf = (saturday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Hed. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact saturday_follows_friday. % 4.24/4.41 cut (((saturday) = (saturday))); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 4.24/4.41 cut (((consecutive (friday)) = zenon_TX_bf)); [idtac | apply NNPP; zenon_intro zenon_Hee]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic (zenon_TX_bf = zenon_TX_bf)); [ zenon_intro zenon_Hcd | zenon_intro zenon_Hce ]. % 4.24/4.41 cut ((zenon_TX_bf = zenon_TX_bf) = ((consecutive (friday)) = zenon_TX_bf)). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Hee. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_Hcd. % 4.24/4.41 cut ((zenon_TX_bf = zenon_TX_bf)); [idtac | apply NNPP; zenon_intro zenon_Hce]. % 4.24/4.41 cut ((zenon_TX_bf = (consecutive (friday)))); [idtac | apply NNPP; zenon_intro zenon_Hef]. % 4.24/4.41 congruence. % 4.24/4.41 generalize (truth_unique zenon_TX_bf). zenon_intro zenon_Ha4. % 4.24/4.41 generalize (statement3 (consecutive (friday))). zenon_intro zenon_Hf0. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_Hf0); [ zenon_intro zenon_He9 | zenon_intro zenon_Hf1 ]. % 4.24/4.41 apply (zenon_L45_ zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_Hf1); [ zenon_intro zenon_Hf3; zenon_intro zenon_H26 | zenon_intro zenon_Hf2; zenon_intro zenon_H3a ]. % 4.24/4.41 exact (zenon_H26 zenon_H3a). % 4.24/4.41 generalize (zenon_Ha4 (consecutive (friday))). zenon_intro zenon_Hf4. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_Hf4); [ zenon_intro zenon_Hf6 | zenon_intro zenon_Hf5 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_Hf6); [ zenon_intro zenon_H9d | zenon_intro zenon_Hf3 ]. % 4.24/4.41 apply (zenon_L24_ zenon_TX_bf); trivial. % 4.24/4.41 exact (zenon_Hf3 zenon_Hf2). % 4.24/4.41 exact (zenon_Hef zenon_Hf5). % 4.24/4.41 apply zenon_Hce. apply refl_equal. % 4.24/4.41 apply zenon_Hce. apply refl_equal. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L46_ *) % 4.24/4.41 assert (zenon_L47_ : forall (zenon_TX_bf : zenon_U) (zenon_TX_z : zenon_U), (forall Y : zenon_U, (((day2 (monday))/\(day2 Y))->((monday) = Y))) -> (day3 (consecutive zenon_TX_z)) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> (~((tuesday) = (consecutive (consecutive zenon_TX_bf)))) -> ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (~(zenon_TX_bf = (wednesday))) -> (~((consecutive zenon_TX_z) = (consecutive (consecutive (tuesday))))) -> (~(zenon_TX_z = (thursday))) -> (~(zenon_TX_bf = (saturday))) -> (~(zenon_TX_z = (saturday))) -> (~(zenon_TX_z = (sunday))) -> False). % 4.24/4.41 do 2 intro. intros zenon_H92 zenon_H17 zenon_H1d zenon_Hb6 zenon_H3a zenon_H9e zenon_Ha3 zenon_He2 zenon_Hf7 zenon_Hed zenon_Hf8 zenon_Hf9. % 4.24/4.41 generalize (days_of_week zenon_TX_z). zenon_intro zenon_Hfa. % 4.24/4.41 apply (zenon_or_s _ _ zenon_Hfa); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hfb ]. % 4.24/4.41 apply (zenon_L35_ zenon_TX_bf zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_or_s _ _ zenon_Hfb); [ zenon_intro zenon_Hc0 | zenon_intro zenon_Hfc ]. % 4.24/4.41 apply (zenon_L41_ zenon_TX_z zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_or_s _ _ zenon_Hfc); [ zenon_intro zenon_He3 | zenon_intro zenon_Hfd ]. % 4.24/4.41 apply (zenon_L44_ zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_or_s _ _ zenon_Hfd); [ zenon_intro zenon_Hff | zenon_intro zenon_Hfe ]. % 4.24/4.41 exact (zenon_Hf7 zenon_Hff). % 4.24/4.41 apply (zenon_or_s _ _ zenon_Hfe); [ zenon_intro zenon_Hea | zenon_intro zenon_H100 ]. % 4.24/4.41 apply (zenon_L46_ zenon_TX_z zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_or_s _ _ zenon_H100); [ zenon_intro zenon_H102 | zenon_intro zenon_H101 ]. % 4.24/4.41 exact (zenon_Hf8 zenon_H102). % 4.24/4.41 exact (zenon_Hf9 zenon_H101). % 4.24/4.41 (* end of lemma zenon_L47_ *) % 4.24/4.41 assert (zenon_L48_ : forall (zenon_TX_bf : zenon_U) (zenon_TX_z : zenon_U), (~(zenon_TX_z = (sunday))) -> (~(zenon_TX_z = (saturday))) -> (~(zenon_TX_bf = (saturday))) -> (~(zenon_TX_z = (thursday))) -> (~((consecutive zenon_TX_z) = (consecutive (consecutive (tuesday))))) -> (~(zenon_TX_bf = (wednesday))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> (~((tuesday) = (consecutive (consecutive zenon_TX_bf)))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> (day3 (consecutive zenon_TX_z)) -> False). % 4.24/4.41 do 2 intro. intros zenon_Hf9 zenon_Hf8 zenon_Hed zenon_Hf7 zenon_He2 zenon_Ha3 zenon_H9e zenon_H3a zenon_Hb6 zenon_H1d zenon_H17. % 4.24/4.41 generalize (day2_unique (monday)). zenon_intro zenon_H92. % 4.24/4.41 apply (zenon_L47_ zenon_TX_bf zenon_TX_z); trivial. % 4.24/4.41 (* end of lemma zenon_L48_ *) % 4.24/4.41 assert (zenon_L49_ : ((truthday (tuesday))<->((~(truthday (monday)))/\(~(truthday (tuesday))))) -> (~(truthday (tuesday))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H103 zenon_G zenon_H9e. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H103); [ zenon_intro zenon_G; zenon_intro zenon_H9a | zenon_intro zenon_H104; zenon_intro zenon_H9e ]. % 4.24/4.41 exact (zenon_H9a zenon_H9e). % 4.24/4.41 exact (zenon_G zenon_H104). % 4.24/4.41 (* end of lemma zenon_L49_ *) % 4.24/4.41 assert (zenon_L50_ : forall (zenon_TX_bf : zenon_U) (zenon_TX_z : zenon_U), ((day1 (tuesday))->((truthday (tuesday))<->((~(truthday (monday)))/\(~(truthday (tuesday)))))) -> (~(truthday (tuesday))) -> (~(zenon_TX_z = (sunday))) -> (~(zenon_TX_z = (saturday))) -> (~(zenon_TX_bf = (saturday))) -> (~(zenon_TX_z = (thursday))) -> (~(zenon_TX_bf = (wednesday))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> (~((tuesday) = (consecutive (consecutive zenon_TX_bf)))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> (day3 (consecutive zenon_TX_z)) -> False). % 4.24/4.41 do 2 intro. intros zenon_H105 zenon_G zenon_Hf9 zenon_Hf8 zenon_Hed zenon_Hf7 zenon_Ha3 zenon_H9e zenon_H3a zenon_Hb6 zenon_H1d zenon_H17. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H105); [ zenon_intro zenon_H106 | zenon_intro zenon_H103 ]. % 4.24/4.41 generalize (day2_follows_day1 (tuesday)). zenon_intro zenon_H107. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H107); [ zenon_intro zenon_H106; zenon_intro zenon_H10a | zenon_intro zenon_H109; zenon_intro zenon_H108 ]. % 4.24/4.41 generalize (day3_follows_day2 (consecutive (tuesday))). zenon_intro zenon_H10b. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H10b); [ zenon_intro zenon_H10a; zenon_intro zenon_H10d | zenon_intro zenon_H108; zenon_intro zenon_H10c ]. % 4.24/4.41 cut ((day3 (consecutive zenon_TX_z)) = (day3 (consecutive (consecutive (tuesday))))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H10d. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H17. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive (consecutive (tuesday))))); [idtac | apply NNPP; zenon_intro zenon_He2]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L48_ zenon_TX_bf zenon_TX_z); trivial. % 4.24/4.41 exact (zenon_H10a zenon_H108). % 4.24/4.41 exact (zenon_H106 zenon_H109). % 4.24/4.41 apply (zenon_L49_); trivial. % 4.24/4.41 (* end of lemma zenon_L50_ *) % 4.24/4.41 assert (zenon_L51_ : (~((sunday) = (sunday))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H10e. % 4.24/4.41 apply zenon_H10e. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L51_ *) % 4.24/4.41 assert (zenon_L52_ : forall (zenon_TX_z : zenon_U) (zenon_TX_bf : zenon_U), (~((consecutive zenon_TX_bf) = (thursday))) -> (forall Y : zenon_U, (((day1 (sunday))/\(day1 Y))->((sunday) = Y))) -> (day3 (consecutive zenon_TX_z)) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (~(zenon_TX_z = (thursday))) -> (~(zenon_TX_bf = (saturday))) -> (~(zenon_TX_z = (saturday))) -> (~(zenon_TX_z = (sunday))) -> (~(truthday (tuesday))) -> (~((sunday) = (consecutive zenon_TX_z))) -> (truthday zenon_TX_bf) -> (forall Y : zenon_U, (((truthday zenon_TX_bf)/\(truthday Y))->(zenon_TX_bf = Y))) -> False). % 4.24/4.41 do 2 intro. intros zenon_Hae zenon_H10f zenon_H17 zenon_H1d zenon_H3a zenon_H9e zenon_Hf7 zenon_Hed zenon_Hf8 zenon_Hf9 zenon_G zenon_H110 zenon_Ha1 zenon_Ha4. % 4.24/4.41 cut (((consecutive (wednesday)) = (thursday)) = ((consecutive zenon_TX_bf) = (thursday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Hae. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact thursday_follows_wednesday. % 4.24/4.41 cut (((thursday) = (thursday))); [idtac | apply NNPP; zenon_intro zenon_H87]. % 4.24/4.41 cut (((consecutive (wednesday)) = (consecutive zenon_TX_bf))); [idtac | apply NNPP; zenon_intro zenon_Haf]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((consecutive zenon_TX_bf) = (consecutive zenon_TX_bf))); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Hb1 ]. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive zenon_TX_bf)) = ((consecutive (wednesday)) = (consecutive zenon_TX_bf))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_Haf. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_Hb0. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive zenon_TX_bf))); [idtac | apply NNPP; zenon_intro zenon_Hb1]. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive (wednesday)))); [idtac | apply NNPP; zenon_intro zenon_Ha2]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_bf = (wednesday))); [idtac | apply NNPP; zenon_intro zenon_Ha3]. % 4.24/4.41 congruence. % 4.24/4.41 generalize (zenon_H10f zenon_TX_bf). zenon_intro zenon_H111. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H111); [ zenon_intro zenon_H113 | zenon_intro zenon_H112 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H113); [ zenon_intro zenon_H114 | zenon_intro zenon_H23 ]. % 4.24/4.41 generalize (day2_follows_day1 (sunday)). zenon_intro zenon_H115. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H115); [ zenon_intro zenon_H114; zenon_intro zenon_H118 | zenon_intro zenon_H117; zenon_intro zenon_H116 ]. % 4.24/4.41 generalize (day3_follows_day2 (consecutive (sunday))). zenon_intro zenon_H119. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H119); [ zenon_intro zenon_H118; zenon_intro zenon_H11b | zenon_intro zenon_H116; zenon_intro zenon_H11a ]. % 4.24/4.41 cut ((day3 (consecutive (consecutive zenon_TX_bf))) = (day3 (consecutive (consecutive (sunday))))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H11b. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H1d. % 4.24/4.41 cut (((consecutive (consecutive zenon_TX_bf)) = (consecutive (consecutive (sunday))))); [idtac | apply NNPP; zenon_intro zenon_H11c]. % 4.24/4.41 congruence. % 4.24/4.41 generalize (statement1 (tuesday)). zenon_intro zenon_H105. % 4.24/4.41 elim (classic ((consecutive (consecutive (sunday))) = (consecutive (consecutive (sunday))))); [ zenon_intro zenon_H11d | zenon_intro zenon_H11e ]. % 4.24/4.41 cut (((consecutive (consecutive (sunday))) = (consecutive (consecutive (sunday)))) = ((consecutive (consecutive zenon_TX_bf)) = (consecutive (consecutive (sunday))))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H11c. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H11d. % 4.24/4.41 cut (((consecutive (consecutive (sunday))) = (consecutive (consecutive (sunday))))); [idtac | apply NNPP; zenon_intro zenon_H11e]. % 4.24/4.41 cut (((consecutive (consecutive (sunday))) = (consecutive (consecutive zenon_TX_bf)))); [idtac | apply NNPP; zenon_intro zenon_H11f]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive (monday)) = (tuesday)) = ((consecutive (consecutive (sunday))) = (consecutive (consecutive zenon_TX_bf)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H11f. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact tuesday_follows_monday. % 4.24/4.41 cut (((tuesday) = (consecutive (consecutive zenon_TX_bf)))); [idtac | apply NNPP; zenon_intro zenon_Hb6]. % 4.24/4.41 cut (((consecutive (monday)) = (consecutive (consecutive (sunday))))); [idtac | apply NNPP; zenon_intro zenon_H120]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((consecutive (consecutive (sunday))) = (consecutive (consecutive (sunday))))); [ zenon_intro zenon_H11d | zenon_intro zenon_H11e ]. % 4.24/4.41 cut (((consecutive (consecutive (sunday))) = (consecutive (consecutive (sunday)))) = ((consecutive (monday)) = (consecutive (consecutive (sunday))))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H120. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H11d. % 4.24/4.41 cut (((consecutive (consecutive (sunday))) = (consecutive (consecutive (sunday))))); [idtac | apply NNPP; zenon_intro zenon_H11e]. % 4.24/4.41 cut (((consecutive (consecutive (sunday))) = (consecutive (monday)))); [idtac | apply NNPP; zenon_intro zenon_H121]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive (sunday)) = (monday))); [idtac | apply NNPP; zenon_intro zenon_H122]. % 4.24/4.41 congruence. % 4.24/4.41 exact (zenon_H122 monday_follows_sunday). % 4.24/4.41 apply zenon_H11e. apply refl_equal. % 4.24/4.41 apply zenon_H11e. apply refl_equal. % 4.24/4.41 apply (zenon_L50_ zenon_TX_bf zenon_TX_z); trivial. % 4.24/4.41 apply zenon_H11e. apply refl_equal. % 4.24/4.41 apply zenon_H11e. apply refl_equal. % 4.24/4.41 exact (zenon_H118 zenon_H116). % 4.24/4.41 exact (zenon_H114 zenon_H117). % 4.24/4.41 apply (zenon_L3_ zenon_TX_bf); trivial. % 4.24/4.41 generalize (statement3 (consecutive zenon_TX_z)). zenon_intro zenon_H3b. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H3b); [ zenon_intro zenon_H1c | zenon_intro zenon_H3c ]. % 4.24/4.41 exact (zenon_H1c zenon_H17). % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H3c); [ zenon_intro zenon_H39; zenon_intro zenon_H26 | zenon_intro zenon_H3d; zenon_intro zenon_H3a ]. % 4.24/4.41 exact (zenon_H26 zenon_H3a). % 4.24/4.41 generalize (zenon_Ha4 (consecutive zenon_TX_z)). zenon_intro zenon_H123. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H123); [ zenon_intro zenon_H125 | zenon_intro zenon_H124 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H125); [ zenon_intro zenon_H9d | zenon_intro zenon_H39 ]. % 4.24/4.41 exact (zenon_H9d zenon_Ha1). % 4.24/4.41 exact (zenon_H39 zenon_H3d). % 4.24/4.41 cut (((sunday) = zenon_TX_bf) = ((sunday) = (consecutive zenon_TX_z))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H110. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H112. % 4.24/4.41 cut ((zenon_TX_bf = (consecutive zenon_TX_z))); [idtac | apply NNPP; zenon_intro zenon_H126]. % 4.24/4.41 cut (((sunday) = (sunday))); [idtac | apply NNPP; zenon_intro zenon_H10e]. % 4.24/4.41 congruence. % 4.24/4.41 apply zenon_H10e. apply refl_equal. % 4.24/4.41 exact (zenon_H126 zenon_H124). % 4.24/4.41 apply zenon_Hb1. apply refl_equal. % 4.24/4.41 apply zenon_Hb1. apply refl_equal. % 4.24/4.41 apply zenon_H87. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L52_ *) % 4.24/4.41 assert (zenon_L53_ : forall (zenon_TX_z : zenon_U) (zenon_TX_bf : zenon_U), (~((consecutive zenon_TX_bf) = (sunday))) -> (~((consecutive zenon_TX_bf) = (thursday))) -> (forall Y : zenon_U, (((day1 (sunday))/\(day1 Y))->((sunday) = Y))) -> (day3 (consecutive zenon_TX_z)) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (~(zenon_TX_z = (thursday))) -> (~(zenon_TX_z = (saturday))) -> (~(zenon_TX_z = (sunday))) -> (~(truthday (tuesday))) -> (~((sunday) = (consecutive zenon_TX_z))) -> (truthday zenon_TX_bf) -> (forall Y : zenon_U, (((truthday zenon_TX_bf)/\(truthday Y))->(zenon_TX_bf = Y))) -> False). % 4.24/4.41 do 2 intro. intros zenon_H127 zenon_Hae zenon_H10f zenon_H17 zenon_H1d zenon_H3a zenon_H9e zenon_Hf7 zenon_Hf8 zenon_Hf9 zenon_G zenon_H110 zenon_Ha1 zenon_Ha4. % 4.24/4.41 cut (((consecutive (saturday)) = (sunday)) = ((consecutive zenon_TX_bf) = (sunday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H127. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact sunday_follows_saturday. % 4.24/4.41 cut (((sunday) = (sunday))); [idtac | apply NNPP; zenon_intro zenon_H10e]. % 4.24/4.41 cut (((consecutive (saturday)) = (consecutive zenon_TX_bf))); [idtac | apply NNPP; zenon_intro zenon_H128]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((consecutive zenon_TX_bf) = (consecutive zenon_TX_bf))); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Hb1 ]. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive zenon_TX_bf)) = ((consecutive (saturday)) = (consecutive zenon_TX_bf))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H128. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_Hb0. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive zenon_TX_bf))); [idtac | apply NNPP; zenon_intro zenon_Hb1]. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive (saturday)))); [idtac | apply NNPP; zenon_intro zenon_H129]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_bf = (saturday))); [idtac | apply NNPP; zenon_intro zenon_Hed]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L52_ zenon_TX_z zenon_TX_bf); trivial. % 4.24/4.41 apply zenon_Hb1. apply refl_equal. % 4.24/4.41 apply zenon_Hb1. apply refl_equal. % 4.24/4.41 apply zenon_H10e. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L53_ *) % 4.24/4.41 assert (zenon_L54_ : forall (zenon_TX_bf : zenon_U) (zenon_TX_cv : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_z : zenon_U), (~((day2 (thursday))\/((day2 (saturday))\/(day2 (sunday))))) -> (~(truthday (tuesday))) -> (day3 (consecutive zenon_TX_z)) -> (truthday zenon_TX_dp) -> (~((monday) = (thursday))) -> (~((monday) = (saturday))) -> (~((monday) = (sunday))) -> (day3 zenon_TX_cv) -> (~((monday) = (wednesday))) -> (~((monday) = (friday))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> False). % 4.24/4.41 do 4 intro. intros zenon_H47 zenon_G zenon_H17 zenon_H5c zenon_H82 zenon_H83 zenon_H84 zenon_H48 zenon_H28 zenon_H27 zenon_H1d. % 4.24/4.41 apply (zenon_notor_s _ _ zenon_H47). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 4.24/4.41 apply (zenon_notor_s _ _ zenon_H4a). zenon_intro zenon_H4d. zenon_intro zenon_H4c. % 4.24/4.41 generalize (day3_follows_day2 (thursday)). zenon_intro zenon_H58. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H58); [ zenon_intro zenon_H4b; zenon_intro zenon_H5a | zenon_intro zenon_H59; zenon_intro zenon_H57 ]. % 4.24/4.41 generalize (day3_follows_day2 (saturday)). zenon_intro zenon_H6a. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H6a); [ zenon_intro zenon_H4d; zenon_intro zenon_H6c | zenon_intro zenon_H6b; zenon_intro zenon_H69 ]. % 4.24/4.41 generalize (day3_follows_day2 (sunday)). zenon_intro zenon_H4e. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H4e); [ zenon_intro zenon_H4c; zenon_intro zenon_H51 | zenon_intro zenon_H50; zenon_intro zenon_H4f ]. % 4.24/4.41 cut ((day3 (consecutive (consecutive zenon_TX_bf))) = (day3 (consecutive (sunday)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H51. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H1d. % 4.24/4.41 cut (((consecutive (consecutive zenon_TX_bf)) = (consecutive (sunday)))); [idtac | apply NNPP; zenon_intro zenon_H12a]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (sunday))); [idtac | apply NNPP; zenon_intro zenon_H127]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((day3 (consecutive zenon_TX_z)) = (day3 (consecutive (sunday)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H51. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H17. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive (sunday)))); [idtac | apply NNPP; zenon_intro zenon_H43]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_z = (sunday))); [idtac | apply NNPP; zenon_intro zenon_Hf9]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((day3 (consecutive (consecutive zenon_TX_bf))) = (day3 (consecutive (saturday)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H6c. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H1d. % 4.24/4.41 cut (((consecutive (consecutive zenon_TX_bf)) = (consecutive (saturday)))); [idtac | apply NNPP; zenon_intro zenon_H12b]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (saturday))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((day3 (consecutive zenon_TX_z)) = (day3 (consecutive (saturday)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H6c. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H17. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive (saturday)))); [idtac | apply NNPP; zenon_intro zenon_H12c]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_z = (saturday))); [idtac | apply NNPP; zenon_intro zenon_Hf8]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((day3 (consecutive (consecutive zenon_TX_bf))) = (day3 (consecutive (thursday)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H5a. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H1d. % 4.24/4.41 cut (((consecutive (consecutive zenon_TX_bf)) = (consecutive (thursday)))); [idtac | apply NNPP; zenon_intro zenon_H12d]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (thursday))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((day3 (consecutive zenon_TX_z)) = (day3 (consecutive (thursday)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H5a. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H17. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive (thursday)))); [idtac | apply NNPP; zenon_intro zenon_H12e]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_z = (thursday))); [idtac | apply NNPP; zenon_intro zenon_Hf7]. % 4.24/4.41 congruence. % 4.24/4.41 generalize (statement1 zenon_TX_bf). zenon_intro zenon_H9f. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H9f); [ zenon_intro zenon_H23 | zenon_intro zenon_Ha0 ]. % 4.24/4.41 apply (zenon_L3_ zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_Ha0); [ zenon_intro zenon_H9d; zenon_intro zenon_H9a | zenon_intro zenon_Ha1; zenon_intro zenon_H9e ]. % 4.24/4.41 apply (zenon_L23_ zenon_TX_cv zenon_TX_dp zenon_TX_z); trivial. % 4.24/4.41 generalize (statement3 zenon_TX_cv). zenon_intro zenon_H52. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H52); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 4.24/4.41 exact (zenon_H54 zenon_H48). % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H53); [ zenon_intro zenon_H56; zenon_intro zenon_H26 | zenon_intro zenon_H55; zenon_intro zenon_H3a ]. % 4.24/4.41 apply (zenon_L29_ zenon_TX_bf); trivial. % 4.24/4.41 generalize (day1_unique (sunday)). zenon_intro zenon_H10f. % 4.24/4.41 generalize (truth_unique zenon_TX_bf). zenon_intro zenon_Ha4. % 4.24/4.41 elim (classic ((consecutive (saturday)) = (consecutive (saturday)))); [ zenon_intro zenon_H12f | zenon_intro zenon_H130 ]. % 4.24/4.41 cut (((consecutive (saturday)) = (consecutive (saturday))) = ((consecutive zenon_TX_z) = (consecutive (saturday)))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H12c. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H12f. % 4.24/4.41 cut (((consecutive (saturday)) = (consecutive (saturday)))); [idtac | apply NNPP; zenon_intro zenon_H130]. % 4.24/4.41 cut (((consecutive (saturday)) = (consecutive zenon_TX_z))); [idtac | apply NNPP; zenon_intro zenon_H131]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive (saturday)) = (sunday)) = ((consecutive (saturday)) = (consecutive zenon_TX_z))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H131. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact sunday_follows_saturday. % 4.24/4.41 cut (((sunday) = (consecutive zenon_TX_z))); [idtac | apply NNPP; zenon_intro zenon_H110]. % 4.24/4.41 cut (((consecutive (saturday)) = (consecutive (saturday)))); [idtac | apply NNPP; zenon_intro zenon_H130]. % 4.24/4.41 congruence. % 4.24/4.41 apply zenon_H130. apply refl_equal. % 4.24/4.41 apply (zenon_L53_ zenon_TX_z zenon_TX_bf); trivial. % 4.24/4.41 apply zenon_H130. apply refl_equal. % 4.24/4.41 apply zenon_H130. apply refl_equal. % 4.24/4.41 exact (zenon_H4c zenon_H50). % 4.24/4.41 exact (zenon_H4d zenon_H6b). % 4.24/4.41 exact (zenon_H4b zenon_H59). % 4.24/4.41 (* end of lemma zenon_L54_ *) % 4.24/4.41 assert (zenon_L55_ : forall (zenon_TX_z : zenon_U) (zenon_TX_dp : zenon_U), (truthday zenon_TX_dp) -> (truthday (wednesday)) -> (day3 (consecutive zenon_TX_z)) -> (day3 (consecutive (thursday))) -> (~(truthday (tuesday))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> False). % 4.24/4.41 do 2 intro. intros zenon_H5c zenon_H2c zenon_H17 zenon_H57 zenon_G zenon_H9e. % 4.24/4.41 generalize (statement1 (tuesday)). zenon_intro zenon_H105. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H105); [ zenon_intro zenon_H106 | zenon_intro zenon_H103 ]. % 4.24/4.41 generalize (day2_follows_day1 (tuesday)). zenon_intro zenon_H107. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H107); [ zenon_intro zenon_H106; zenon_intro zenon_H10a | zenon_intro zenon_H109; zenon_intro zenon_H108 ]. % 4.24/4.41 generalize (day3_follows_day2 (consecutive (tuesday))). zenon_intro zenon_H10b. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H10b); [ zenon_intro zenon_H10a; zenon_intro zenon_H10d | zenon_intro zenon_H108; zenon_intro zenon_H10c ]. % 4.24/4.41 cut ((day3 (consecutive zenon_TX_z)) = (day3 (consecutive (consecutive (tuesday))))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H10d. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H17. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive (consecutive (tuesday))))); [idtac | apply NNPP; zenon_intro zenon_He2]. % 4.24/4.41 congruence. % 4.24/4.41 generalize (truth_unique zenon_TX_dp). zenon_intro zenon_H79. % 4.24/4.41 generalize (zenon_H79 (wednesday)). zenon_intro zenon_H132. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H132); [ zenon_intro zenon_H134 | zenon_intro zenon_H133 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H134); [ zenon_intro zenon_H62 | zenon_intro zenon_H32 ]. % 4.24/4.41 exact (zenon_H62 zenon_H5c). % 4.24/4.41 exact (zenon_H32 zenon_H2c). % 4.24/4.41 cut (((consecutive (wednesday)) = (thursday)) = ((consecutive zenon_TX_z) = (consecutive (consecutive (tuesday))))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_He2. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact thursday_follows_wednesday. % 4.24/4.41 cut (((thursday) = (consecutive (consecutive (tuesday))))); [idtac | apply NNPP; zenon_intro zenon_Hdd]. % 4.24/4.41 cut (((consecutive (wednesday)) = (consecutive zenon_TX_z))); [idtac | apply NNPP; zenon_intro zenon_He4]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((consecutive zenon_TX_z) = (consecutive zenon_TX_z))); [ zenon_intro zenon_He5 | zenon_intro zenon_He6 ]. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive zenon_TX_z)) = ((consecutive (wednesday)) = (consecutive zenon_TX_z))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_He4. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_He5. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive zenon_TX_z))); [idtac | apply NNPP; zenon_intro zenon_He6]. % 4.24/4.41 cut (((consecutive zenon_TX_z) = (consecutive (wednesday)))); [idtac | apply NNPP; zenon_intro zenon_He7]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_z = (wednesday))); [idtac | apply NNPP; zenon_intro zenon_He8]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_dp = (wednesday)) = (zenon_TX_z = (wednesday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_He8. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H133. % 4.24/4.41 cut (((wednesday) = (wednesday))); [idtac | apply NNPP; zenon_intro zenon_Hca]. % 4.24/4.41 cut ((zenon_TX_dp = zenon_TX_z)); [idtac | apply NNPP; zenon_intro zenon_H7f]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic (zenon_TX_z = zenon_TX_z)); [ zenon_intro zenon_H80 | zenon_intro zenon_H81 ]. % 4.24/4.41 cut ((zenon_TX_z = zenon_TX_z) = (zenon_TX_dp = zenon_TX_z)). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H7f. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H80. % 4.24/4.41 cut ((zenon_TX_z = zenon_TX_z)); [idtac | apply NNPP; zenon_intro zenon_H81]. % 4.24/4.41 cut ((zenon_TX_z = zenon_TX_dp)); [idtac | apply NNPP; zenon_intro zenon_H5b]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L12_ zenon_TX_dp zenon_TX_z); trivial. % 4.24/4.41 apply zenon_H81. apply refl_equal. % 4.24/4.41 apply zenon_H81. apply refl_equal. % 4.24/4.41 apply zenon_Hca. apply refl_equal. % 4.24/4.41 apply zenon_He6. apply refl_equal. % 4.24/4.41 apply zenon_He6. apply refl_equal. % 4.24/4.41 apply (zenon_L43_); trivial. % 4.24/4.41 exact (zenon_H10a zenon_H108). % 4.24/4.41 exact (zenon_H106 zenon_H109). % 4.24/4.41 apply (zenon_L49_); trivial. % 4.24/4.41 (* end of lemma zenon_L55_ *) % 4.24/4.41 assert (zenon_L56_ : forall (zenon_TX_bf : zenon_U), (truthday (friday)) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> (~(day2 (consecutive (friday)))) -> False). % 4.24/4.41 do 1 intro. intros zenon_H33 zenon_H9e zenon_H1d zenon_H135. % 4.24/4.41 generalize (day3_follows_day2 (consecutive (friday))). zenon_intro zenon_H136. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H136); [ zenon_intro zenon_H135; zenon_intro zenon_H139 | zenon_intro zenon_H138; zenon_intro zenon_H137 ]. % 4.24/4.41 cut ((day3 (consecutive (consecutive zenon_TX_bf))) = (day3 (consecutive (consecutive (friday))))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H139. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H1d. % 4.24/4.41 cut (((consecutive (consecutive zenon_TX_bf)) = (consecutive (consecutive (friday))))); [idtac | apply NNPP; zenon_intro zenon_H13a]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive (friday)))); [idtac | apply NNPP; zenon_intro zenon_Ha8]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L27_ zenon_TX_bf); trivial. % 4.24/4.41 exact (zenon_H135 zenon_H138). % 4.24/4.41 (* end of lemma zenon_L56_ *) % 4.24/4.41 assert (zenon_L57_ : forall (zenon_TX_bf : zenon_U), (~((thursday) = (consecutive (friday)))) -> (day3 (consecutive (thursday))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (truthday (friday)) -> False). % 4.24/4.41 do 1 intro. intros zenon_H13b zenon_H57 zenon_H1d zenon_H9e zenon_H33. % 4.24/4.41 generalize (day2_unique (consecutive (friday))). zenon_intro zenon_H13c. % 4.24/4.41 generalize (zenon_H13c (thursday)). zenon_intro zenon_H13d. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H13d); [ zenon_intro zenon_H13f | zenon_intro zenon_H13e ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H13f); [ zenon_intro zenon_H135 | zenon_intro zenon_H4b ]. % 4.24/4.41 apply (zenon_L56_ zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_L10_); trivial. % 4.24/4.41 apply zenon_H13b. apply sym_equal. exact zenon_H13e. % 4.24/4.41 (* end of lemma zenon_L57_ *) % 4.24/4.41 assert (zenon_L58_ : forall (zenon_TX_z : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_cv : zenon_U) (zenon_TX_bf : zenon_U), (~((~(truthday (wednesday)))/\(~(truthday (friday))))) -> (~((thursday) = (saturday))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> (day3 (consecutive (thursday))) -> (~((monday) = (friday))) -> (~((monday) = (wednesday))) -> (day3 zenon_TX_cv) -> (~((monday) = (sunday))) -> (~((monday) = (saturday))) -> (~((monday) = (thursday))) -> (truthday zenon_TX_dp) -> (day3 (consecutive zenon_TX_z)) -> (~(truthday (tuesday))) -> False). % 4.24/4.41 do 4 intro. intros zenon_H26 zenon_H140 zenon_H1d zenon_H57 zenon_H27 zenon_H28 zenon_H48 zenon_H84 zenon_H83 zenon_H82 zenon_H5c zenon_H17 zenon_G. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H26); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 4.24/4.41 apply zenon_H2b. zenon_intro zenon_H2c. % 4.24/4.41 generalize (statement1 zenon_TX_bf). zenon_intro zenon_H9f. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H9f); [ zenon_intro zenon_H23 | zenon_intro zenon_Ha0 ]. % 4.24/4.41 apply (zenon_L3_ zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_Ha0); [ zenon_intro zenon_H9d; zenon_intro zenon_H9a | zenon_intro zenon_Ha1; zenon_intro zenon_H9e ]. % 4.24/4.41 apply (zenon_L23_ zenon_TX_cv zenon_TX_dp zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_L55_ zenon_TX_z zenon_TX_dp); trivial. % 4.24/4.41 apply zenon_H2a. zenon_intro zenon_H33. % 4.24/4.41 cut (((consecutive (friday)) = (saturday)) = ((thursday) = (saturday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H140. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact saturday_follows_friday. % 4.24/4.41 cut (((saturday) = (saturday))); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 4.24/4.41 cut (((consecutive (friday)) = (thursday))); [idtac | apply NNPP; zenon_intro zenon_H141]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((thursday) = (thursday))); [ zenon_intro zenon_H86 | zenon_intro zenon_H87 ]. % 4.24/4.41 cut (((thursday) = (thursday)) = ((consecutive (friday)) = (thursday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H141. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H86. % 4.24/4.41 cut (((thursday) = (thursday))); [idtac | apply NNPP; zenon_intro zenon_H87]. % 4.24/4.41 cut (((thursday) = (consecutive (friday)))); [idtac | apply NNPP; zenon_intro zenon_H13b]. % 4.24/4.41 congruence. % 4.24/4.41 generalize (statement1 zenon_TX_bf). zenon_intro zenon_H9f. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H9f); [ zenon_intro zenon_H23 | zenon_intro zenon_Ha0 ]. % 4.24/4.41 apply (zenon_L3_ zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_Ha0); [ zenon_intro zenon_H9d; zenon_intro zenon_H9a | zenon_intro zenon_Ha1; zenon_intro zenon_H9e ]. % 4.24/4.41 apply (zenon_L23_ zenon_TX_cv zenon_TX_dp zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_L57_ zenon_TX_bf); trivial. % 4.24/4.41 apply zenon_H87. apply refl_equal. % 4.24/4.41 apply zenon_H87. apply refl_equal. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L58_ *) % 4.24/4.41 assert (zenon_L59_ : ((truthday (wednesday))<->((~(truthday (monday)))/\(~(truthday (tuesday))))) -> (~(truthday (wednesday))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H142 zenon_H32 zenon_H9e. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H142); [ zenon_intro zenon_H32; zenon_intro zenon_H9a | zenon_intro zenon_H2c; zenon_intro zenon_H9e ]. % 4.24/4.41 exact (zenon_H9a zenon_H9e). % 4.24/4.41 exact (zenon_H32 zenon_H2c). % 4.24/4.41 (* end of lemma zenon_L59_ *) % 4.24/4.41 assert (zenon_L60_ : (day3 (consecutive (thursday))) -> (~(truthday (wednesday))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H57 zenon_H32 zenon_H9e. % 4.24/4.41 generalize (statement1 (wednesday)). zenon_intro zenon_H143. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H143); [ zenon_intro zenon_H144 | zenon_intro zenon_H142 ]. % 4.24/4.41 generalize (day2_follows_day1 (wednesday)). zenon_intro zenon_H145. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H145); [ zenon_intro zenon_H144; zenon_intro zenon_H148 | zenon_intro zenon_H147; zenon_intro zenon_H146 ]. % 4.24/4.41 generalize (day3_follows_day2 (consecutive (wednesday))). zenon_intro zenon_H149. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H149); [ zenon_intro zenon_H148; zenon_intro zenon_H14b | zenon_intro zenon_H146; zenon_intro zenon_H14a ]. % 4.24/4.41 cut ((day3 (consecutive (thursday))) = (day3 (consecutive (consecutive (wednesday))))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H14b. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H57. % 4.24/4.41 cut (((consecutive (thursday)) = (consecutive (consecutive (wednesday))))); [idtac | apply NNPP; zenon_intro zenon_H14c]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((thursday) = (consecutive (wednesday)))); [idtac | apply NNPP; zenon_intro zenon_H14d]. % 4.24/4.41 congruence. % 4.24/4.41 apply zenon_H14d. apply sym_equal. exact thursday_follows_wednesday. % 4.24/4.41 exact (zenon_H148 zenon_H146). % 4.24/4.41 exact (zenon_H144 zenon_H147). % 4.24/4.41 apply (zenon_L59_); trivial. % 4.24/4.41 (* end of lemma zenon_L60_ *) % 4.24/4.41 assert (zenon_L61_ : forall (zenon_TX_bf : zenon_U), (truthday (wednesday)) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> (~(day2 (consecutive (wednesday)))) -> False). % 4.24/4.41 do 1 intro. intros zenon_H2c zenon_H9e zenon_H1d zenon_H148. % 4.24/4.41 generalize (day3_follows_day2 (consecutive (wednesday))). zenon_intro zenon_H149. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H149); [ zenon_intro zenon_H148; zenon_intro zenon_H14b | zenon_intro zenon_H146; zenon_intro zenon_H14a ]. % 4.24/4.41 cut ((day3 (consecutive (consecutive zenon_TX_bf))) = (day3 (consecutive (consecutive (wednesday))))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H14b. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H1d. % 4.24/4.41 cut (((consecutive (consecutive zenon_TX_bf)) = (consecutive (consecutive (wednesday))))); [idtac | apply NNPP; zenon_intro zenon_H14e]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive (wednesday)))); [idtac | apply NNPP; zenon_intro zenon_Ha2]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L25_ zenon_TX_bf); trivial. % 4.24/4.41 exact (zenon_H148 zenon_H146). % 4.24/4.41 (* end of lemma zenon_L61_ *) % 4.24/4.41 assert (zenon_L62_ : forall (zenon_TX_bf : zenon_U), (~((saturday) = (consecutive (wednesday)))) -> (day3 (consecutive (saturday))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (truthday (wednesday)) -> False). % 4.24/4.41 do 1 intro. intros zenon_H14f zenon_H69 zenon_H1d zenon_H9e zenon_H2c. % 4.24/4.41 generalize (day2_unique (consecutive (wednesday))). zenon_intro zenon_H150. % 4.24/4.41 generalize (zenon_H150 (saturday)). zenon_intro zenon_H151. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H151); [ zenon_intro zenon_H153 | zenon_intro zenon_H152 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H153); [ zenon_intro zenon_H148 | zenon_intro zenon_H4d ]. % 4.24/4.41 apply (zenon_L61_ zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_L14_); trivial. % 4.24/4.41 apply zenon_H14f. apply sym_equal. exact zenon_H152. % 4.24/4.41 (* end of lemma zenon_L62_ *) % 4.24/4.41 assert (zenon_L63_ : (~((friday) = (friday))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H154. % 4.24/4.41 apply zenon_H154. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L63_ *) % 4.24/4.41 assert (zenon_L64_ : forall (zenon_TX_z : zenon_U) (zenon_TX_dp : zenon_U), (~(~(truthday (friday)))) -> (truthday zenon_TX_dp) -> (~((friday) = (saturday))) -> (day3 (consecutive zenon_TX_z)) -> (day3 (consecutive (saturday))) -> False). % 4.24/4.41 do 2 intro. intros zenon_H2a zenon_H5c zenon_H155 zenon_H17 zenon_H69. % 4.24/4.41 apply zenon_H2a. zenon_intro zenon_H33. % 4.24/4.41 generalize (truth_unique zenon_TX_dp). zenon_intro zenon_H79. % 4.24/4.41 generalize (zenon_H79 (friday)). zenon_intro zenon_H156. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H156); [ zenon_intro zenon_H158 | zenon_intro zenon_H157 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H158); [ zenon_intro zenon_H62 | zenon_intro zenon_H38 ]. % 4.24/4.41 exact (zenon_H62 zenon_H5c). % 4.24/4.41 exact (zenon_H38 zenon_H33). % 4.24/4.41 elim (classic ((saturday) = (saturday))); [ zenon_intro zenon_H8e | zenon_intro zenon_H8f ]. % 4.24/4.41 cut (((saturday) = (saturday)) = ((friday) = (saturday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H155. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H8e. % 4.24/4.41 cut (((saturday) = (saturday))); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 4.24/4.41 cut (((saturday) = (friday))); [idtac | apply NNPP; zenon_intro zenon_H159]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_dp = (friday)) = ((saturday) = (friday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H159. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H157. % 4.24/4.41 cut (((friday) = (friday))); [idtac | apply NNPP; zenon_intro zenon_H154]. % 4.24/4.41 cut ((zenon_TX_dp = (saturday))); [idtac | apply NNPP; zenon_intro zenon_H91]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((saturday) = (saturday))); [ zenon_intro zenon_H8e | zenon_intro zenon_H8f ]. % 4.24/4.41 cut (((saturday) = (saturday)) = (zenon_TX_dp = (saturday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H91. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H8e. % 4.24/4.41 cut (((saturday) = (saturday))); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 4.24/4.41 cut (((saturday) = zenon_TX_dp)); [idtac | apply NNPP; zenon_intro zenon_H6d]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L17_ zenon_TX_z zenon_TX_dp); trivial. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 apply zenon_H154. apply refl_equal. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L64_ *) % 4.24/4.41 assert (zenon_L65_ : forall (zenon_TX_bf : zenon_U) (zenon_TX_cv : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_z : zenon_U), (~((~(truthday (wednesday)))/\(~(truthday (friday))))) -> (~((friday) = (saturday))) -> (~((thursday) = (saturday))) -> (~(truthday (tuesday))) -> (day3 (consecutive zenon_TX_z)) -> (truthday zenon_TX_dp) -> (~((monday) = (thursday))) -> (~((monday) = (saturday))) -> (~((monday) = (sunday))) -> (day3 zenon_TX_cv) -> (~((monday) = (wednesday))) -> (~((monday) = (friday))) -> (day3 (consecutive (saturday))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> False). % 4.24/4.41 do 4 intro. intros zenon_H26 zenon_H155 zenon_H140 zenon_G zenon_H17 zenon_H5c zenon_H82 zenon_H83 zenon_H84 zenon_H48 zenon_H28 zenon_H27 zenon_H69 zenon_H1d. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H26); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 4.24/4.41 apply zenon_H2b. zenon_intro zenon_H2c. % 4.24/4.41 elim (classic ((saturday) = (saturday))); [ zenon_intro zenon_H8e | zenon_intro zenon_H8f ]. % 4.24/4.41 cut (((saturday) = (saturday)) = ((thursday) = (saturday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H140. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H8e. % 4.24/4.41 cut (((saturday) = (saturday))); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 4.24/4.41 cut (((saturday) = (thursday))); [idtac | apply NNPP; zenon_intro zenon_H15a]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive (wednesday)) = (thursday)) = ((saturday) = (thursday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H15a. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact thursday_follows_wednesday. % 4.24/4.41 cut (((thursday) = (thursday))); [idtac | apply NNPP; zenon_intro zenon_H87]. % 4.24/4.41 cut (((consecutive (wednesday)) = (saturday))); [idtac | apply NNPP; zenon_intro zenon_H15b]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((saturday) = (saturday))); [ zenon_intro zenon_H8e | zenon_intro zenon_H8f ]. % 4.24/4.41 cut (((saturday) = (saturday)) = ((consecutive (wednesday)) = (saturday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H15b. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H8e. % 4.24/4.41 cut (((saturday) = (saturday))); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 4.24/4.41 cut (((saturday) = (consecutive (wednesday)))); [idtac | apply NNPP; zenon_intro zenon_H14f]. % 4.24/4.41 congruence. % 4.24/4.41 generalize (statement1 zenon_TX_bf). zenon_intro zenon_H9f. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H9f); [ zenon_intro zenon_H23 | zenon_intro zenon_Ha0 ]. % 4.24/4.41 apply (zenon_L3_ zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_Ha0); [ zenon_intro zenon_H9d; zenon_intro zenon_H9a | zenon_intro zenon_Ha1; zenon_intro zenon_H9e ]. % 4.24/4.41 apply (zenon_L23_ zenon_TX_cv zenon_TX_dp zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_L62_ zenon_TX_bf); trivial. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 apply zenon_H87. apply refl_equal. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 apply (zenon_L64_ zenon_TX_z zenon_TX_dp); trivial. % 4.24/4.41 (* end of lemma zenon_L65_ *) % 4.24/4.41 assert (zenon_L66_ : ((truthday (friday))<->((~(truthday (monday)))/\(~(truthday (tuesday))))) -> (~(truthday (friday))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H15c zenon_H38 zenon_H9e. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H15c); [ zenon_intro zenon_H38; zenon_intro zenon_H9a | zenon_intro zenon_H33; zenon_intro zenon_H9e ]. % 4.24/4.41 exact (zenon_H9a zenon_H9e). % 4.24/4.41 exact (zenon_H38 zenon_H33). % 4.24/4.41 (* end of lemma zenon_L66_ *) % 4.24/4.41 assert (zenon_L67_ : (day3 (consecutive (saturday))) -> (~(truthday (friday))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H69 zenon_H38 zenon_H9e. % 4.24/4.41 generalize (statement1 (friday)). zenon_intro zenon_H15d. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H15d); [ zenon_intro zenon_H15e | zenon_intro zenon_H15c ]. % 4.24/4.41 generalize (day2_follows_day1 (friday)). zenon_intro zenon_H15f. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H15f); [ zenon_intro zenon_H15e; zenon_intro zenon_H135 | zenon_intro zenon_H160; zenon_intro zenon_H138 ]. % 4.24/4.41 generalize (day3_follows_day2 (consecutive (friday))). zenon_intro zenon_H136. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H136); [ zenon_intro zenon_H135; zenon_intro zenon_H139 | zenon_intro zenon_H138; zenon_intro zenon_H137 ]. % 4.24/4.41 cut ((day3 (consecutive (saturday))) = (day3 (consecutive (consecutive (friday))))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H139. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H69. % 4.24/4.41 cut (((consecutive (saturday)) = (consecutive (consecutive (friday))))); [idtac | apply NNPP; zenon_intro zenon_H161]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((saturday) = (consecutive (friday)))); [idtac | apply NNPP; zenon_intro zenon_H162]. % 4.24/4.41 congruence. % 4.24/4.41 apply zenon_H162. apply sym_equal. exact saturday_follows_friday. % 4.24/4.41 exact (zenon_H135 zenon_H138). % 4.24/4.41 exact (zenon_H15e zenon_H160). % 4.24/4.41 apply (zenon_L66_); trivial. % 4.24/4.41 (* end of lemma zenon_L67_ *) % 4.24/4.41 assert (zenon_L68_ : forall (zenon_TX_bf : zenon_U) (zenon_TX_cv : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_z : zenon_U), ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> (~(truthday (tuesday))) -> (day3 (consecutive zenon_TX_z)) -> (truthday zenon_TX_dp) -> (~((monday) = (thursday))) -> (~((monday) = (saturday))) -> (~((monday) = (sunday))) -> (day3 zenon_TX_cv) -> (~((monday) = (wednesday))) -> (~((monday) = (friday))) -> (day3 (consecutive (saturday))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> False). % 4.24/4.41 do 4 intro. intros zenon_H3a zenon_G zenon_H17 zenon_H5c zenon_H82 zenon_H83 zenon_H84 zenon_H48 zenon_H28 zenon_H27 zenon_H69 zenon_H1d. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H3a). zenon_intro zenon_H32. zenon_intro zenon_H38. % 4.24/4.41 generalize (statement1 zenon_TX_bf). zenon_intro zenon_H9f. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H9f); [ zenon_intro zenon_H23 | zenon_intro zenon_Ha0 ]. % 4.24/4.41 apply (zenon_L3_ zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_Ha0); [ zenon_intro zenon_H9d; zenon_intro zenon_H9a | zenon_intro zenon_Ha1; zenon_intro zenon_H9e ]. % 4.24/4.41 apply (zenon_L23_ zenon_TX_cv zenon_TX_dp zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_L67_); trivial. % 4.24/4.41 (* end of lemma zenon_L68_ *) % 4.24/4.41 assert (zenon_L69_ : forall (zenon_TX_bf : zenon_U), (~((sunday) = (consecutive (wednesday)))) -> (day3 (consecutive (sunday))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (truthday (wednesday)) -> False). % 4.24/4.41 do 1 intro. intros zenon_H163 zenon_H4f zenon_H1d zenon_H9e zenon_H2c. % 4.24/4.41 generalize (day2_unique (consecutive (wednesday))). zenon_intro zenon_H150. % 4.24/4.41 generalize (zenon_H150 (sunday)). zenon_intro zenon_H164. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H164); [ zenon_intro zenon_H166 | zenon_intro zenon_H165 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H166); [ zenon_intro zenon_H148 | zenon_intro zenon_H4c ]. % 4.24/4.41 apply (zenon_L61_ zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_L18_); trivial. % 4.24/4.41 apply zenon_H163. apply sym_equal. exact zenon_H165. % 4.24/4.41 (* end of lemma zenon_L69_ *) % 4.24/4.41 assert (zenon_L70_ : forall (zenon_TX_bf : zenon_U), (~((sunday) = (consecutive (friday)))) -> (day3 (consecutive (sunday))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (truthday (friday)) -> False). % 4.24/4.41 do 1 intro. intros zenon_H167 zenon_H4f zenon_H1d zenon_H9e zenon_H33. % 4.24/4.41 generalize (day2_unique (consecutive (friday))). zenon_intro zenon_H13c. % 4.24/4.41 generalize (zenon_H13c (sunday)). zenon_intro zenon_H168. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H168); [ zenon_intro zenon_H16a | zenon_intro zenon_H169 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H16a); [ zenon_intro zenon_H135 | zenon_intro zenon_H4c ]. % 4.24/4.41 apply (zenon_L56_ zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_L18_); trivial. % 4.24/4.41 apply zenon_H167. apply sym_equal. exact zenon_H169. % 4.24/4.41 (* end of lemma zenon_L70_ *) % 4.24/4.41 assert (zenon_L71_ : forall (zenon_TX_bf : zenon_U), (~((~(truthday (wednesday)))/\(~(truthday (friday))))) -> (~((saturday) = (sunday))) -> (~((thursday) = (sunday))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> (day3 (consecutive (sunday))) -> False). % 4.24/4.41 do 1 intro. intros zenon_H26 zenon_H16b zenon_H16c zenon_H9e zenon_H1d zenon_H4f. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H26); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 4.24/4.41 apply zenon_H2b. zenon_intro zenon_H2c. % 4.24/4.41 elim (classic ((sunday) = (sunday))); [ zenon_intro zenon_H16d | zenon_intro zenon_H10e ]. % 4.24/4.41 cut (((sunday) = (sunday)) = ((thursday) = (sunday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H16c. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H16d. % 4.24/4.41 cut (((sunday) = (sunday))); [idtac | apply NNPP; zenon_intro zenon_H10e]. % 4.24/4.41 cut (((sunday) = (thursday))); [idtac | apply NNPP; zenon_intro zenon_H16e]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive (wednesday)) = (thursday)) = ((sunday) = (thursday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H16e. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact thursday_follows_wednesday. % 4.24/4.41 cut (((thursday) = (thursday))); [idtac | apply NNPP; zenon_intro zenon_H87]. % 4.24/4.41 cut (((consecutive (wednesday)) = (sunday))); [idtac | apply NNPP; zenon_intro zenon_H16f]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((sunday) = (sunday))); [ zenon_intro zenon_H16d | zenon_intro zenon_H10e ]. % 4.24/4.41 cut (((sunday) = (sunday)) = ((consecutive (wednesday)) = (sunday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H16f. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H16d. % 4.24/4.41 cut (((sunday) = (sunday))); [idtac | apply NNPP; zenon_intro zenon_H10e]. % 4.24/4.41 cut (((sunday) = (consecutive (wednesday)))); [idtac | apply NNPP; zenon_intro zenon_H163]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L69_ zenon_TX_bf); trivial. % 4.24/4.41 apply zenon_H10e. apply refl_equal. % 4.24/4.41 apply zenon_H10e. apply refl_equal. % 4.24/4.41 apply zenon_H87. apply refl_equal. % 4.24/4.41 apply zenon_H10e. apply refl_equal. % 4.24/4.41 apply zenon_H10e. apply refl_equal. % 4.24/4.41 apply zenon_H2a. zenon_intro zenon_H33. % 4.24/4.41 elim (classic ((sunday) = (sunday))); [ zenon_intro zenon_H16d | zenon_intro zenon_H10e ]. % 4.24/4.41 cut (((sunday) = (sunday)) = ((saturday) = (sunday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H16b. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H16d. % 4.24/4.41 cut (((sunday) = (sunday))); [idtac | apply NNPP; zenon_intro zenon_H10e]. % 4.24/4.41 cut (((sunday) = (saturday))); [idtac | apply NNPP; zenon_intro zenon_H170]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive (friday)) = (saturday)) = ((sunday) = (saturday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H170. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact saturday_follows_friday. % 4.24/4.41 cut (((saturday) = (saturday))); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 4.24/4.41 cut (((consecutive (friday)) = (sunday))); [idtac | apply NNPP; zenon_intro zenon_H171]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic ((sunday) = (sunday))); [ zenon_intro zenon_H16d | zenon_intro zenon_H10e ]. % 4.24/4.41 cut (((sunday) = (sunday)) = ((consecutive (friday)) = (sunday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H171. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H16d. % 4.24/4.41 cut (((sunday) = (sunday))); [idtac | apply NNPP; zenon_intro zenon_H10e]. % 4.24/4.41 cut (((sunday) = (consecutive (friday)))); [idtac | apply NNPP; zenon_intro zenon_H167]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L70_ zenon_TX_bf); trivial. % 4.24/4.41 apply zenon_H10e. apply refl_equal. % 4.24/4.41 apply zenon_H10e. apply refl_equal. % 4.24/4.41 apply zenon_H8f. apply refl_equal. % 4.24/4.41 apply zenon_H10e. apply refl_equal. % 4.24/4.41 apply zenon_H10e. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L71_ *) % 4.24/4.41 assert (zenon_L72_ : forall (zenon_TX_bf : zenon_U), (~(zenon_TX_bf = (consecutive (sunday)))) -> (truthday (consecutive (sunday))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> False). % 4.24/4.41 do 1 intro. intros zenon_H172 zenon_H173 zenon_H9e zenon_H1d. % 4.24/4.41 generalize (truth_unique zenon_TX_bf). zenon_intro zenon_Ha4. % 4.24/4.41 generalize (zenon_Ha4 (consecutive (sunday))). zenon_intro zenon_H174. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H174); [ zenon_intro zenon_H176 | zenon_intro zenon_H175 ]. % 4.24/4.41 apply (zenon_notand_s _ _ zenon_H176); [ zenon_intro zenon_H9d | zenon_intro zenon_H177 ]. % 4.24/4.41 apply (zenon_L24_ zenon_TX_bf); trivial. % 4.24/4.41 exact (zenon_H177 zenon_H173). % 4.24/4.41 exact (zenon_H172 zenon_H175). % 4.24/4.41 (* end of lemma zenon_L72_ *) % 4.24/4.41 assert (zenon_L73_ : forall (zenon_TX_bf : zenon_U), (~(zenon_TX_bf = (monday))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (truthday (consecutive (sunday))) -> False). % 4.24/4.41 do 1 intro. intros zenon_H178 zenon_H1d zenon_H9e zenon_H173. % 4.24/4.41 cut (((consecutive (sunday)) = (monday)) = (zenon_TX_bf = (monday))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H178. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact monday_follows_sunday. % 4.24/4.41 cut (((monday) = (monday))); [idtac | apply NNPP; zenon_intro zenon_H68]. % 4.24/4.41 cut (((consecutive (sunday)) = zenon_TX_bf)); [idtac | apply NNPP; zenon_intro zenon_H179]. % 4.24/4.41 congruence. % 4.24/4.41 elim (classic (zenon_TX_bf = zenon_TX_bf)); [ zenon_intro zenon_Hcd | zenon_intro zenon_Hce ]. % 4.24/4.41 cut ((zenon_TX_bf = zenon_TX_bf) = ((consecutive (sunday)) = zenon_TX_bf)). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H179. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_Hcd. % 4.24/4.41 cut ((zenon_TX_bf = zenon_TX_bf)); [idtac | apply NNPP; zenon_intro zenon_Hce]. % 4.24/4.41 cut ((zenon_TX_bf = (consecutive (sunday)))); [idtac | apply NNPP; zenon_intro zenon_H172]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L72_ zenon_TX_bf); trivial. % 4.24/4.41 apply zenon_Hce. apply refl_equal. % 4.24/4.41 apply zenon_Hce. apply refl_equal. % 4.24/4.41 apply zenon_H68. apply refl_equal. % 4.24/4.41 (* end of lemma zenon_L73_ *) % 4.24/4.41 assert (zenon_L74_ : forall (zenon_TX_bf : zenon_U), (day3 (consecutive (sunday))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> (~(zenon_TX_bf = (monday))) -> ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> False). % 4.24/4.41 do 1 intro. intros zenon_H4f zenon_H9e zenon_H1d zenon_H178 zenon_H3a. % 4.24/4.41 generalize (statement3 (consecutive (sunday))). zenon_intro zenon_H17a. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H17a); [ zenon_intro zenon_H51 | zenon_intro zenon_H17b ]. % 4.24/4.41 exact (zenon_H51 zenon_H4f). % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H17b); [ zenon_intro zenon_H177; zenon_intro zenon_H26 | zenon_intro zenon_H173; zenon_intro zenon_H3a ]. % 4.24/4.41 exact (zenon_H26 zenon_H3a). % 4.24/4.41 apply (zenon_L73_ zenon_TX_bf); trivial. % 4.24/4.41 (* end of lemma zenon_L74_ *) % 4.24/4.41 assert (zenon_L75_ : forall (zenon_TX_bf : zenon_U), ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (day3 (consecutive (sunday))) -> (~(day1 (monday))) -> False). % 4.24/4.41 do 1 intro. intros zenon_H3a zenon_H1d zenon_H9e zenon_H4f zenon_H17c. % 4.24/4.41 generalize (day2_follows_day1 (monday)). zenon_intro zenon_H17d. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H17d); [ zenon_intro zenon_H17c; zenon_intro zenon_H180 | zenon_intro zenon_H17f; zenon_intro zenon_H17e ]. % 4.24/4.41 generalize (day3_follows_day2 (consecutive (monday))). zenon_intro zenon_H181. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H181); [ zenon_intro zenon_H180; zenon_intro zenon_H183 | zenon_intro zenon_H17e; zenon_intro zenon_H182 ]. % 4.24/4.41 cut ((day3 (consecutive (consecutive zenon_TX_bf))) = (day3 (consecutive (consecutive (monday))))). % 4.24/4.41 intro zenon_D_pnotp. % 4.24/4.41 apply zenon_H183. % 4.24/4.41 rewrite <- zenon_D_pnotp. % 4.24/4.41 exact zenon_H1d. % 4.24/4.41 cut (((consecutive (consecutive zenon_TX_bf)) = (consecutive (consecutive (monday))))); [idtac | apply NNPP; zenon_intro zenon_H184]. % 4.24/4.41 congruence. % 4.24/4.41 cut (((consecutive zenon_TX_bf) = (consecutive (monday)))); [idtac | apply NNPP; zenon_intro zenon_H185]. % 4.24/4.41 congruence. % 4.24/4.41 cut ((zenon_TX_bf = (monday))); [idtac | apply NNPP; zenon_intro zenon_H178]. % 4.24/4.41 congruence. % 4.24/4.41 apply (zenon_L74_ zenon_TX_bf); trivial. % 4.24/4.41 exact (zenon_H180 zenon_H17e). % 4.24/4.41 exact (zenon_H17c zenon_H17f). % 4.24/4.41 (* end of lemma zenon_L75_ *) % 4.24/4.41 assert (zenon_L76_ : ((truthday (monday))<->((~(truthday (monday)))/\(~(truthday (tuesday))))) -> (~(truthday (monday))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> False). % 4.24/4.41 do 0 intro. intros zenon_H186 zenon_H31 zenon_H9e. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H186); [ zenon_intro zenon_H31; zenon_intro zenon_H9a | zenon_intro zenon_H29; zenon_intro zenon_H9e ]. % 4.24/4.41 exact (zenon_H9a zenon_H9e). % 4.24/4.41 exact (zenon_H31 zenon_H29). % 4.24/4.41 (* end of lemma zenon_L76_ *) % 4.24/4.41 assert (zenon_L77_ : forall (zenon_TX_bf : zenon_U), ((~(truthday (wednesday)))/\(~(truthday (friday)))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (day3 (consecutive (sunday))) -> (~(truthday (monday))) -> False). % 4.24/4.41 do 1 intro. intros zenon_H3a zenon_H1d zenon_H9e zenon_H4f zenon_H31. % 4.24/4.41 generalize (statement1 (monday)). zenon_intro zenon_H187. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H187); [ zenon_intro zenon_H17c | zenon_intro zenon_H186 ]. % 4.24/4.41 apply (zenon_L75_ zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_L76_); trivial. % 4.24/4.41 (* end of lemma zenon_L77_ *) % 4.24/4.41 assert (zenon_L78_ : forall (zenon_TX_bf : zenon_U) (zenon_TX_cv : zenon_U), (day2 (sunday)) -> (day3 zenon_TX_cv) -> (~(truthday (monday))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> ((~(truthday (monday)))/\(~(truthday (tuesday)))) -> (~((thursday) = (sunday))) -> (~((saturday) = (sunday))) -> False). % 4.24/4.41 do 2 intro. intros zenon_H50 zenon_H48 zenon_H31 zenon_H1d zenon_H9e zenon_H16c zenon_H16b. % 4.24/4.41 generalize (day3_follows_day2 (sunday)). zenon_intro zenon_H4e. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H4e); [ zenon_intro zenon_H4c; zenon_intro zenon_H51 | zenon_intro zenon_H50; zenon_intro zenon_H4f ]. % 4.24/4.41 exact (zenon_H4c zenon_H50). % 4.24/4.41 generalize (statement3 zenon_TX_cv). zenon_intro zenon_H52. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H52); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 4.24/4.41 exact (zenon_H54 zenon_H48). % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H53); [ zenon_intro zenon_H56; zenon_intro zenon_H26 | zenon_intro zenon_H55; zenon_intro zenon_H3a ]. % 4.24/4.41 apply (zenon_L71_ zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_L77_ zenon_TX_bf); trivial. % 4.24/4.41 (* end of lemma zenon_L78_ *) % 4.24/4.41 assert (zenon_L79_ : forall (zenon_TX_z : zenon_U) (zenon_TX_dp : zenon_U) (zenon_TX_cv : zenon_U) (zenon_TX_bf : zenon_U), ((day2 (thursday))\/((day2 (saturday))\/(day2 (sunday)))) -> (~((friday) = (saturday))) -> (~((thursday) = (saturday))) -> (day3 (consecutive (consecutive zenon_TX_bf))) -> (~((saturday) = (sunday))) -> (~((thursday) = (sunday))) -> (~((monday) = (friday))) -> (~((monday) = (wednesday))) -> (day3 zenon_TX_cv) -> (~((monday) = (sunday))) -> (~((monday) = (saturday))) -> (~((monday) = (thursday))) -> (truthday zenon_TX_dp) -> (day3 (consecutive zenon_TX_z)) -> (~(truthday (tuesday))) -> False). % 4.24/4.41 do 4 intro. intros zenon_H66 zenon_H155 zenon_H140 zenon_H1d zenon_H16b zenon_H16c zenon_H27 zenon_H28 zenon_H48 zenon_H84 zenon_H83 zenon_H82 zenon_H5c zenon_H17 zenon_G. % 4.24/4.41 apply (zenon_or_s _ _ zenon_H66); [ zenon_intro zenon_H59 | zenon_intro zenon_H85 ]. % 4.24/4.41 generalize (day3_follows_day2 (thursday)). zenon_intro zenon_H58. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H58); [ zenon_intro zenon_H4b; zenon_intro zenon_H5a | zenon_intro zenon_H59; zenon_intro zenon_H57 ]. % 4.24/4.41 exact (zenon_H4b zenon_H59). % 4.24/4.41 generalize (statement3 zenon_TX_cv). zenon_intro zenon_H52. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H52); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 4.24/4.41 exact (zenon_H54 zenon_H48). % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H53); [ zenon_intro zenon_H56; zenon_intro zenon_H26 | zenon_intro zenon_H55; zenon_intro zenon_H3a ]. % 4.24/4.41 apply (zenon_L58_ zenon_TX_z zenon_TX_dp zenon_TX_cv zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H3a). zenon_intro zenon_H32. zenon_intro zenon_H38. % 4.24/4.41 generalize (statement1 zenon_TX_bf). zenon_intro zenon_H9f. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H9f); [ zenon_intro zenon_H23 | zenon_intro zenon_Ha0 ]. % 4.24/4.41 apply (zenon_L3_ zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_Ha0); [ zenon_intro zenon_H9d; zenon_intro zenon_H9a | zenon_intro zenon_Ha1; zenon_intro zenon_H9e ]. % 4.24/4.41 apply (zenon_L23_ zenon_TX_cv zenon_TX_dp zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_L60_); trivial. % 4.24/4.41 apply (zenon_or_s _ _ zenon_H85); [ zenon_intro zenon_H6b | zenon_intro zenon_H50 ]. % 4.24/4.41 generalize (day3_follows_day2 (saturday)). zenon_intro zenon_H6a. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H6a); [ zenon_intro zenon_H4d; zenon_intro zenon_H6c | zenon_intro zenon_H6b; zenon_intro zenon_H69 ]. % 4.24/4.41 exact (zenon_H4d zenon_H6b). % 4.24/4.41 generalize (statement3 zenon_TX_cv). zenon_intro zenon_H52. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H52); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 4.24/4.41 exact (zenon_H54 zenon_H48). % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H53); [ zenon_intro zenon_H56; zenon_intro zenon_H26 | zenon_intro zenon_H55; zenon_intro zenon_H3a ]. % 4.24/4.41 apply (zenon_L65_ zenon_TX_bf zenon_TX_cv zenon_TX_dp zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_L68_ zenon_TX_bf zenon_TX_cv zenon_TX_dp zenon_TX_z); trivial. % 4.24/4.41 generalize (statement1 zenon_TX_bf). zenon_intro zenon_H9f. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H9f); [ zenon_intro zenon_H23 | zenon_intro zenon_Ha0 ]. % 4.24/4.41 apply (zenon_L3_ zenon_TX_bf); trivial. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_Ha0); [ zenon_intro zenon_H9d; zenon_intro zenon_H9a | zenon_intro zenon_Ha1; zenon_intro zenon_H9e ]. % 4.24/4.41 apply (zenon_L23_ zenon_TX_cv zenon_TX_dp zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H9e). zenon_intro zenon_H31. zenon_intro zenon_G. % 4.24/4.41 apply (zenon_L78_ zenon_TX_bf zenon_TX_cv); trivial. % 4.24/4.41 (* end of lemma zenon_L79_ *) % 4.24/4.41 apply NNPP. intro zenon_G. % 4.24/4.41 apply (zenon_and_s _ _ uniquenames). zenon_intro zenon_H189. zenon_intro zenon_H188. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H188). zenon_intro zenon_H28. zenon_intro zenon_H18a. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H18a). zenon_intro zenon_H82. zenon_intro zenon_H18b. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H18b). zenon_intro zenon_H27. zenon_intro zenon_H18c. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H18c). zenon_intro zenon_H83. zenon_intro zenon_H18d. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H18d). zenon_intro zenon_H84. zenon_intro zenon_H18e. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H18e). zenon_intro zenon_H190. zenon_intro zenon_H18f. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H18f). zenon_intro zenon_H192. zenon_intro zenon_H191. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H191). zenon_intro zenon_H194. zenon_intro zenon_H193. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H193). zenon_intro zenon_H196. zenon_intro zenon_H195. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H195). zenon_intro zenon_H198. zenon_intro zenon_H197. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H197). zenon_intro zenon_H19a. zenon_intro zenon_H199. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H199). zenon_intro zenon_H19c. zenon_intro zenon_H19b. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H19b). zenon_intro zenon_H19e. zenon_intro zenon_H19d. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H19d). zenon_intro zenon_H1a0. zenon_intro zenon_H19f. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H19f). zenon_intro zenon_H1a2. zenon_intro zenon_H1a1. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H1a1). zenon_intro zenon_H140. zenon_intro zenon_H1a3. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H1a3). zenon_intro zenon_H16c. zenon_intro zenon_H1a4. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H1a4). zenon_intro zenon_H155. zenon_intro zenon_H1a5. % 4.24/4.41 apply (zenon_and_s _ _ zenon_H1a5). zenon_intro zenon_H1a6. zenon_intro zenon_H16b. % 4.24/4.41 elim truth_once. zenon_intro zenon_TX_dp. zenon_intro zenon_H5c. % 4.24/4.41 elim day1_once. zenon_intro zenon_TX_bf. zenon_intro zenon_H25. % 4.24/4.41 generalize (day2_follows_day1 zenon_TX_bf). zenon_intro zenon_H24. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H24); [ zenon_intro zenon_H23; zenon_intro zenon_H1e | zenon_intro zenon_H25; zenon_intro zenon_H21 ]. % 4.24/4.41 exact (zenon_H23 zenon_H25). % 4.24/4.41 generalize (day3_follows_day2 (consecutive zenon_TX_bf)). zenon_intro zenon_H20. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H20); [ zenon_intro zenon_H1e; zenon_intro zenon_H22 | zenon_intro zenon_H21; zenon_intro zenon_H1d ]. % 4.24/4.41 exact (zenon_H1e zenon_H21). % 4.24/4.41 elim day2_once. zenon_intro zenon_TX_z. zenon_intro zenon_H1b. % 4.24/4.41 generalize (day3_follows_day2 zenon_TX_z). zenon_intro zenon_H1a. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H1a); [ zenon_intro zenon_H18; zenon_intro zenon_H1c | zenon_intro zenon_H1b; zenon_intro zenon_H17 ]. % 4.24/4.41 exact (zenon_H18 zenon_H1b). % 4.24/4.41 elim day3_once. zenon_intro zenon_TX_cv. zenon_intro zenon_H48. % 4.24/4.41 generalize (statement2 zenon_TX_z). zenon_intro zenon_H64. % 4.24/4.41 apply (zenon_imply_s _ _ zenon_H64); [ zenon_intro zenon_H18 | zenon_intro zenon_H65 ]. % 4.24/4.41 apply (zenon_L1_ zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_equiv_s _ _ zenon_H65); [ zenon_intro zenon_H63; zenon_intro zenon_H47 | zenon_intro zenon_H67; zenon_intro zenon_H66 ]. % 4.24/4.41 apply (zenon_L54_ zenon_TX_bf zenon_TX_cv zenon_TX_dp zenon_TX_z); trivial. % 4.24/4.41 apply (zenon_L79_ zenon_TX_z zenon_TX_dp zenon_TX_cv zenon_TX_bf); trivial. % 4.24/4.41 Qed. % 4.24/4.41 % SZS output end Proof % 4.24/4.41 (* END-PROOF *) % 4.24/4.41 nodes searched: 139047 % 4.24/4.41 max branch formulas: 971 % 4.24/4.41 proof nodes created: 2848 % 4.24/4.41 formulas created: 152506 % 4.24/4.41 %------------------------------------------------------------------------------