%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NUM859+1 : TPTP v8.1.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n025.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 16:00:03 EDT 2022 % Result : Theorem 4.25s 4.40s % Output : Proof 4.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM859+1 : TPTP v8.1.0. Released v4.1.0. % 0.11/0.13 % Command : run_zenon %s %d % 0.14/0.34 % Computer : n025.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Tue Jul 5 13:29:27 EDT 2022 % 0.14/0.34 % CPUTime : % 4.25/4.40 (* PROOF-FOUND *) % 4.25/4.40 % SZS status Theorem % 4.25/4.40 (* BEGIN-PROOF *) % 4.25/4.40 % SZS output start Proof % 4.25/4.40 Theorem max_is_ub_1 : (forall X : zenon_U, (forall Y : zenon_U, (forall Z : zenon_U, ((minsol_model_ub X Y Z)<->(minsol_model_max X Y Z))))). % 4.25/4.40 Proof. % 4.25/4.40 assert (zenon_L1_ : forall (zenon_TY_s : zenon_U) (zenon_TX_t : zenon_U), (forall Y : zenon_U, (((max zenon_TX_t Y) = zenon_TX_t)\/(~(lesseq Y zenon_TX_t)))) -> (~(zenon_TX_t = (max zenon_TX_t zenon_TY_s))) -> (lesseq zenon_TY_s zenon_TX_t) -> False). % 4.25/4.40 do 2 intro. intros zenon_Hf zenon_H10 zenon_H11. % 4.25/4.40 generalize (zenon_Hf zenon_TY_s). zenon_intro zenon_H14. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H14); [ zenon_intro zenon_H16 | zenon_intro zenon_H15 ]. % 4.25/4.40 apply zenon_H10. apply sym_equal. exact zenon_H16. % 4.25/4.40 exact (zenon_H15 zenon_H11). % 4.25/4.40 (* end of lemma zenon_L1_ *) % 4.25/4.40 assert (zenon_L2_ : forall (zenon_TX_t : zenon_U) (zenon_TY_s : zenon_U), (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (~(zenon_TX_t = (max zenon_TX_t zenon_TY_s))) -> (~(lesseq zenon_TX_t zenon_TY_s)) -> False). % 4.25/4.40 do 2 intro. intros zenon_H17 zenon_H10 zenon_H18. % 4.25/4.40 generalize (zenon_H17 zenon_TX_t). zenon_intro zenon_H19. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H19); [ zenon_intro zenon_H11 | zenon_intro zenon_H1a ]. % 4.25/4.40 generalize (max_1 zenon_TX_t). zenon_intro zenon_Hf. % 4.25/4.40 apply (zenon_L1_ zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 exact (zenon_H18 zenon_H1a). % 4.25/4.40 (* end of lemma zenon_L2_ *) % 4.25/4.40 assert (zenon_L3_ : forall (zenon_TY_s : zenon_U) (zenon_TX_t : zenon_U), (forall Y : zenon_U, (((max zenon_TX_t Y) = Y)\/(~(lesseq zenon_TX_t Y)))) -> (~(zenon_TY_s = (max zenon_TX_t zenon_TY_s))) -> (lesseq zenon_TX_t zenon_TY_s) -> False). % 4.25/4.40 do 2 intro. intros zenon_H1b zenon_H1c zenon_H1a. % 4.25/4.40 generalize (zenon_H1b zenon_TY_s). zenon_intro zenon_H1d. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H1d); [ zenon_intro zenon_H1e | zenon_intro zenon_H18 ]. % 4.25/4.40 apply zenon_H1c. apply sym_equal. exact zenon_H1e. % 4.25/4.40 exact (zenon_H18 zenon_H1a). % 4.25/4.40 (* end of lemma zenon_L3_ *) % 4.25/4.40 assert (zenon_L4_ : forall (zenon_TY_s : zenon_U) (zenon_TX_t : zenon_U), (lesseq zenon_TX_t zenon_TY_s) -> (~(zenon_TY_s = (max zenon_TX_t zenon_TY_s))) -> False). % 4.25/4.40 do 2 intro. intros zenon_H1a zenon_H1c. % 4.25/4.40 generalize (max_2 zenon_TX_t). zenon_intro zenon_H1b. % 4.25/4.40 apply (zenon_L3_ zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 (* end of lemma zenon_L4_ *) % 4.25/4.40 assert (zenon_L5_ : forall (zenon_TX_t : zenon_U) (zenon_TY_s : zenon_U), (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (~(lesseq zenon_TY_s zenon_TX_t)) -> (~(zenon_TY_s = (max zenon_TX_t zenon_TY_s))) -> False). % 4.25/4.40 do 2 intro. intros zenon_H17 zenon_H15 zenon_H1c. % 4.25/4.40 generalize (zenon_H17 zenon_TX_t). zenon_intro zenon_H19. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H19); [ zenon_intro zenon_H11 | zenon_intro zenon_H1a ]. % 4.25/4.40 exact (zenon_H15 zenon_H11). % 4.25/4.40 apply (zenon_L4_ zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 (* end of lemma zenon_L5_ *) % 4.25/4.40 assert (zenon_L6_ : forall (zenon_TZ_bi : zenon_U) (zenon_TX_t : zenon_U) (zenon_TY_s : zenon_U), (~(zenon_TY_s = (max zenon_TX_t zenon_TY_s))) -> (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> (~(lesseq zenon_TX_t zenon_TZ_bi)) -> (lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_bi) -> False). % 4.25/4.40 do 3 intro. intros zenon_H1c zenon_H17 zenon_H1f zenon_H20 zenon_H21. % 4.25/4.40 elim (classic ((~(zenon_TX_t = (max zenon_TX_t zenon_TY_s)))/\(~(lesseq zenon_TX_t (max zenon_TX_t zenon_TY_s))))); [ zenon_intro zenon_H23 | zenon_intro zenon_H24 ]. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H23). zenon_intro zenon_H10. zenon_intro zenon_H25. % 4.25/4.40 generalize (sum_monotone_1 zenon_TX_t). zenon_intro zenon_H26. % 4.25/4.40 generalize (zenon_H26 zenon_TY_s). zenon_intro zenon_H0. % 4.25/4.40 generalize (zenon_H0 zenon_E). zenon_intro zenon_H27. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H27); [ zenon_intro zenon_H18; zenon_intro zenon_H29 | zenon_intro zenon_H1a; zenon_intro zenon_H28 ]. % 4.25/4.40 apply (zenon_L2_ zenon_TX_t zenon_TY_s); trivial. % 4.25/4.40 apply (zenon_L4_ zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 cut ((lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_bi) = (lesseq zenon_TX_t zenon_TZ_bi)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H20. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H21. % 4.25/4.40 cut ((zenon_TZ_bi = zenon_TZ_bi)); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_H2b]. % 4.25/4.40 congruence. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H24); [ zenon_intro zenon_H2d | zenon_intro zenon_H2c ]. % 4.25/4.40 apply zenon_H2d. zenon_intro zenon_H2e. % 4.25/4.40 elim (classic (zenon_TX_t = zenon_TX_t)); [ zenon_intro zenon_H2f | zenon_intro zenon_H30 ]. % 4.25/4.40 cut ((zenon_TX_t = zenon_TX_t) = ((max zenon_TX_t zenon_TY_s) = zenon_TX_t)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H2b. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H2f. % 4.25/4.40 cut ((zenon_TX_t = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_H30]. % 4.25/4.40 cut ((zenon_TX_t = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H10]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H10 zenon_H2e). % 4.25/4.40 apply zenon_H30. apply refl_equal. % 4.25/4.40 apply zenon_H30. apply refl_equal. % 4.25/4.40 apply zenon_H2c. zenon_intro zenon_H31. % 4.25/4.40 generalize (zenon_H1f zenon_TX_t). zenon_intro zenon_H32. % 4.25/4.40 generalize (zenon_H32 (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_H33. % 4.25/4.40 generalize (zenon_H33 zenon_TZ_bi). zenon_intro zenon_H34. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H34); [ zenon_intro zenon_H25 | zenon_intro zenon_H35 ]. % 4.25/4.40 exact (zenon_H25 zenon_H31). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H35); [ zenon_intro zenon_H37 | zenon_intro zenon_H36 ]. % 4.25/4.40 exact (zenon_H37 zenon_H21). % 4.25/4.40 exact (zenon_H20 zenon_H36). % 4.25/4.40 apply zenon_H2a. apply refl_equal. % 4.25/4.40 (* end of lemma zenon_L6_ *) % 4.25/4.40 assert (zenon_L7_ : forall (zenon_TX_t : zenon_U) (zenon_TZ_bi : zenon_U) (zenon_TY_s : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> (~(lesseq zenon_TY_s zenon_TZ_bi)) -> (lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_bi) -> False). % 4.25/4.40 do 3 intro. intros zenon_H1f zenon_H38 zenon_H21. % 4.25/4.40 elim (classic ((~(zenon_TY_s = (max zenon_TX_t zenon_TY_s)))/\(~(lesseq zenon_TY_s (max zenon_TX_t zenon_TY_s))))); [ zenon_intro zenon_H39 | zenon_intro zenon_H3a ]. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H39). zenon_intro zenon_H1c. zenon_intro zenon_H3b. % 4.25/4.40 generalize (summation_monotone zenon_TY_s). zenon_intro zenon_H3c. % 4.25/4.40 generalize (lesseq_total zenon_TY_s). zenon_intro zenon_H17. % 4.25/4.40 generalize (zenon_H3c zenon_TX_t). zenon_intro zenon_H3d. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H3d); [ zenon_intro zenon_H15; zenon_intro zenon_H3f | zenon_intro zenon_H11; zenon_intro zenon_H3e ]. % 4.25/4.40 apply (zenon_L5_ zenon_TX_t zenon_TY_s); trivial. % 4.25/4.40 elim (classic (lesseq zenon_TX_t zenon_TZ_bi)); [ zenon_intro zenon_H36 | zenon_intro zenon_H20 ]. % 4.25/4.40 generalize (zenon_H1f zenon_TY_s). zenon_intro zenon_H40. % 4.25/4.40 generalize (zenon_H40 zenon_TX_t). zenon_intro zenon_H41. % 4.25/4.40 generalize (zenon_H41 zenon_TZ_bi). zenon_intro zenon_H42. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H42); [ zenon_intro zenon_H15 | zenon_intro zenon_H43 ]. % 4.25/4.40 exact (zenon_H15 zenon_H11). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H43); [ zenon_intro zenon_H20 | zenon_intro zenon_H44 ]. % 4.25/4.40 exact (zenon_H20 zenon_H36). % 4.25/4.40 exact (zenon_H38 zenon_H44). % 4.25/4.40 apply (zenon_L6_ zenon_TZ_bi zenon_TX_t zenon_TY_s); trivial. % 4.25/4.40 cut ((lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_bi) = (lesseq zenon_TY_s zenon_TZ_bi)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H38. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H21. % 4.25/4.40 cut ((zenon_TZ_bi = zenon_TZ_bi)); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_H45]. % 4.25/4.40 congruence. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H3a); [ zenon_intro zenon_H47 | zenon_intro zenon_H46 ]. % 4.25/4.40 apply zenon_H47. zenon_intro zenon_H48. % 4.25/4.40 elim (classic (zenon_TY_s = zenon_TY_s)); [ zenon_intro zenon_H49 | zenon_intro zenon_H4a ]. % 4.25/4.40 cut ((zenon_TY_s = zenon_TY_s) = ((max zenon_TX_t zenon_TY_s) = zenon_TY_s)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H45. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H49. % 4.25/4.40 cut ((zenon_TY_s = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_H4a]. % 4.25/4.40 cut ((zenon_TY_s = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H1c]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H1c zenon_H48). % 4.25/4.40 apply zenon_H4a. apply refl_equal. % 4.25/4.40 apply zenon_H4a. apply refl_equal. % 4.25/4.40 apply zenon_H46. zenon_intro zenon_H4b. % 4.25/4.40 generalize (zenon_H1f zenon_TY_s). zenon_intro zenon_H40. % 4.25/4.40 generalize (zenon_H40 (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_H4c. % 4.25/4.40 generalize (zenon_H4c zenon_TZ_bi). zenon_intro zenon_H4d. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H4d); [ zenon_intro zenon_H3b | zenon_intro zenon_H4e ]. % 4.25/4.40 exact (zenon_H3b zenon_H4b). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H4e); [ zenon_intro zenon_H37 | zenon_intro zenon_H44 ]. % 4.25/4.40 exact (zenon_H37 zenon_H21). % 4.25/4.40 exact (zenon_H38 zenon_H44). % 4.25/4.40 apply zenon_H2a. apply refl_equal. % 4.25/4.40 (* end of lemma zenon_L7_ *) % 4.25/4.40 assert (zenon_L8_ : forall (zenon_TY_s : zenon_U) (zenon_TX_t : zenon_U), (forall Y : zenon_U, (((max zenon_TX_t Y) = Y)\/(~(lesseq zenon_TX_t Y)))) -> (~((max zenon_TX_t zenon_TY_s) = zenon_TY_s)) -> (lesseq zenon_TX_t zenon_TY_s) -> False). % 4.25/4.40 do 2 intro. intros zenon_H1b zenon_H45 zenon_H1a. % 4.25/4.40 generalize (zenon_H1b zenon_TY_s). zenon_intro zenon_H1d. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H1d); [ zenon_intro zenon_H1e | zenon_intro zenon_H18 ]. % 4.25/4.40 exact (zenon_H45 zenon_H1e). % 4.25/4.40 exact (zenon_H18 zenon_H1a). % 4.25/4.40 (* end of lemma zenon_L8_ *) % 4.25/4.40 assert (zenon_L9_ : forall (zenon_TZ_bi : zenon_U) (zenon_TY_s : zenon_U) (zenon_TX_t : zenon_U), (forall Z : zenon_U, ((model_ub zenon_TX_t zenon_TY_s Z)->(lesseq zenon_TZ_bi Z))) -> (lesseq zenon_TY_s zenon_TX_t) -> (~(lesseq zenon_TZ_bi zenon_TX_t)) -> False). % 4.25/4.40 do 3 intro. intros zenon_H4f zenon_H11 zenon_H50. % 4.25/4.40 generalize (zenon_H4f zenon_TX_t). zenon_intro zenon_H51. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H51); [ zenon_intro zenon_H53 | zenon_intro zenon_H52 ]. % 4.25/4.40 generalize (model_ub_2 zenon_TX_t). zenon_intro zenon_H54. % 4.25/4.40 generalize (zenon_H54 zenon_TY_s). zenon_intro zenon_H55. % 4.25/4.40 generalize (zenon_H55 zenon_TX_t). zenon_intro zenon_H56. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H56); [ zenon_intro zenon_H53; zenon_intro zenon_H59 | zenon_intro zenon_H58; zenon_intro zenon_H57 ]. % 4.25/4.40 apply zenon_H59. exists zenon_TX_t. apply NNPP. zenon_intro zenon_H5a. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H5a); [ zenon_intro zenon_H5c | zenon_intro zenon_H5b ]. % 4.25/4.40 generalize (ub zenon_TX_t). zenon_intro zenon_H5d. % 4.25/4.40 generalize (zenon_H5d zenon_TY_s). zenon_intro zenon_H5e. % 4.25/4.40 generalize (zenon_H5e zenon_TX_t). zenon_intro zenon_H5f. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H5f); [ zenon_intro zenon_H5c; zenon_intro zenon_H62 | zenon_intro zenon_H61; zenon_intro zenon_H60 ]. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H62); [ zenon_intro zenon_H5b | zenon_intro zenon_H15 ]. % 4.25/4.40 generalize (lesseq_ref zenon_TX_t). zenon_intro zenon_H63. % 4.25/4.40 exact (zenon_H5b zenon_H63). % 4.25/4.40 exact (zenon_H15 zenon_H11). % 4.25/4.40 exact (zenon_H5c zenon_H61). % 4.25/4.40 generalize (lesseq_ref zenon_TX_t). zenon_intro zenon_H63. % 4.25/4.40 exact (zenon_H5b zenon_H63). % 4.25/4.40 exact (zenon_H53 zenon_H58). % 4.25/4.40 exact (zenon_H50 zenon_H52). % 4.25/4.40 (* end of lemma zenon_L9_ *) % 4.25/4.40 assert (zenon_L10_ : forall (zenon_TZ_bi : zenon_U) (zenon_TZ_dy : zenon_U) (zenon_TX_t : zenon_U), (lesseq zenon_TX_t zenon_TZ_dy) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> (~(lesseq zenon_TX_t zenon_TZ_bi)) -> (lesseq zenon_TZ_dy zenon_TZ_bi) -> False). % 4.25/4.40 do 3 intro. intros zenon_H64 zenon_H1f zenon_H20 zenon_H65. % 4.25/4.40 elim (classic ((~(zenon_TX_t = zenon_TZ_dy))/\(~(lesseq zenon_TX_t zenon_TZ_dy)))); [ zenon_intro zenon_H67 | zenon_intro zenon_H68 ]. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H67). zenon_intro zenon_H6a. zenon_intro zenon_H69. % 4.25/4.40 exact (zenon_H69 zenon_H64). % 4.25/4.40 cut ((lesseq zenon_TZ_dy zenon_TZ_bi) = (lesseq zenon_TX_t zenon_TZ_bi)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H20. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H65. % 4.25/4.40 cut ((zenon_TZ_bi = zenon_TZ_bi)); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 4.25/4.40 cut ((zenon_TZ_dy = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_H6b]. % 4.25/4.40 congruence. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H68); [ zenon_intro zenon_H6d | zenon_intro zenon_H6c ]. % 4.25/4.40 apply zenon_H6d. zenon_intro zenon_H6e. % 4.25/4.40 elim (classic (zenon_TX_t = zenon_TX_t)); [ zenon_intro zenon_H2f | zenon_intro zenon_H30 ]. % 4.25/4.40 cut ((zenon_TX_t = zenon_TX_t) = (zenon_TZ_dy = zenon_TX_t)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H6b. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H2f. % 4.25/4.40 cut ((zenon_TX_t = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_H30]. % 4.25/4.40 cut ((zenon_TX_t = zenon_TZ_dy)); [idtac | apply NNPP; zenon_intro zenon_H6a]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H6a zenon_H6e). % 4.25/4.40 apply zenon_H30. apply refl_equal. % 4.25/4.40 apply zenon_H30. apply refl_equal. % 4.25/4.40 apply zenon_H6c. zenon_intro zenon_H64. % 4.25/4.40 generalize (zenon_H1f zenon_TX_t). zenon_intro zenon_H32. % 4.25/4.40 generalize (zenon_H32 zenon_TZ_dy). zenon_intro zenon_H6f. % 4.25/4.40 generalize (zenon_H6f zenon_TZ_bi). zenon_intro zenon_H70. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H70); [ zenon_intro zenon_H69 | zenon_intro zenon_H71 ]. % 4.25/4.40 exact (zenon_H69 zenon_H64). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H71); [ zenon_intro zenon_H72 | zenon_intro zenon_H36 ]. % 4.25/4.40 exact (zenon_H72 zenon_H65). % 4.25/4.40 exact (zenon_H20 zenon_H36). % 4.25/4.40 apply zenon_H2a. apply refl_equal. % 4.25/4.40 (* end of lemma zenon_L10_ *) % 4.25/4.40 assert (zenon_L11_ : forall (zenon_TZ_bi : zenon_U) (zenon_TZ_dy : zenon_U) (zenon_TY_s : zenon_U), (lesseq zenon_TY_s zenon_TZ_dy) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> (~(lesseq zenon_TY_s zenon_TZ_bi)) -> (lesseq zenon_TZ_dy zenon_TZ_bi) -> False). % 4.25/4.40 do 3 intro. intros zenon_H73 zenon_H1f zenon_H38 zenon_H65. % 4.25/4.40 elim (classic ((~(zenon_TY_s = zenon_TZ_dy))/\(~(lesseq zenon_TY_s zenon_TZ_dy)))); [ zenon_intro zenon_H74 | zenon_intro zenon_H75 ]. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H74). zenon_intro zenon_H77. zenon_intro zenon_H76. % 4.25/4.40 exact (zenon_H76 zenon_H73). % 4.25/4.40 cut ((lesseq zenon_TZ_dy zenon_TZ_bi) = (lesseq zenon_TY_s zenon_TZ_bi)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H38. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H65. % 4.25/4.40 cut ((zenon_TZ_bi = zenon_TZ_bi)); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 4.25/4.40 cut ((zenon_TZ_dy = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_H78]. % 4.25/4.40 congruence. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H75); [ zenon_intro zenon_H7a | zenon_intro zenon_H79 ]. % 4.25/4.40 apply zenon_H7a. zenon_intro zenon_H7b. % 4.25/4.40 elim (classic (zenon_TY_s = zenon_TY_s)); [ zenon_intro zenon_H49 | zenon_intro zenon_H4a ]. % 4.25/4.40 cut ((zenon_TY_s = zenon_TY_s) = (zenon_TZ_dy = zenon_TY_s)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H78. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H49. % 4.25/4.40 cut ((zenon_TY_s = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_H4a]. % 4.25/4.40 cut ((zenon_TY_s = zenon_TZ_dy)); [idtac | apply NNPP; zenon_intro zenon_H77]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H77 zenon_H7b). % 4.25/4.40 apply zenon_H4a. apply refl_equal. % 4.25/4.40 apply zenon_H4a. apply refl_equal. % 4.25/4.40 apply zenon_H79. zenon_intro zenon_H73. % 4.25/4.40 generalize (zenon_H1f zenon_TY_s). zenon_intro zenon_H40. % 4.25/4.40 generalize (zenon_H40 zenon_TZ_dy). zenon_intro zenon_H7c. % 4.25/4.40 generalize (zenon_H7c zenon_TZ_bi). zenon_intro zenon_H7d. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H7d); [ zenon_intro zenon_H76 | zenon_intro zenon_H7e ]. % 4.25/4.40 exact (zenon_H76 zenon_H73). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H7e); [ zenon_intro zenon_H72 | zenon_intro zenon_H44 ]. % 4.25/4.40 exact (zenon_H72 zenon_H65). % 4.25/4.40 exact (zenon_H38 zenon_H44). % 4.25/4.40 apply zenon_H2a. apply refl_equal. % 4.25/4.40 (* end of lemma zenon_L11_ *) % 4.25/4.40 assert (zenon_L12_ : forall (zenon_TX_t : zenon_U) (zenon_TY_s : zenon_U), (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = zenon_TX_t)\/(~(lesseq Y zenon_TX_t)))) -> (~(zenon_TX_t = (max zenon_TX_t zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = Y)\/(~(lesseq zenon_TX_t Y)))) -> (~(zenon_TY_s = (max zenon_TX_t zenon_TY_s))) -> False). % 4.25/4.40 do 2 intro. intros zenon_H17 zenon_Hf zenon_H10 zenon_H1b zenon_H1c. % 4.25/4.40 generalize (zenon_H17 zenon_TX_t). zenon_intro zenon_H19. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H19); [ zenon_intro zenon_H11 | zenon_intro zenon_H1a ]. % 4.25/4.40 apply (zenon_L1_ zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 apply (zenon_L3_ zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 (* end of lemma zenon_L12_ *) % 4.25/4.40 assert (zenon_L13_ : forall (zenon_TY_s : zenon_U) (zenon_TX_t : zenon_U) (zenon_TZ_ez : zenon_U), (~(lesseq zenon_TZ_ez (max zenon_TX_t zenon_TY_s))) -> (lesseq zenon_TZ_ez zenon_TY_s) -> (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = zenon_TX_t)\/(~(lesseq Y zenon_TX_t)))) -> (~(zenon_TX_t = (max zenon_TX_t zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = Y)\/(~(lesseq zenon_TX_t Y)))) -> False). % 4.25/4.40 do 3 intro. intros zenon_H7f zenon_H80 zenon_H17 zenon_Hf zenon_H10 zenon_H1b. % 4.25/4.40 elim (classic (zenon_TY_s = (max zenon_TX_t zenon_TY_s))); [ zenon_intro zenon_H48 | zenon_intro zenon_H1c ]. % 4.25/4.40 cut ((lesseq zenon_TZ_ez zenon_TY_s) = (lesseq zenon_TZ_ez (max zenon_TX_t zenon_TY_s))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H7f. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H80. % 4.25/4.40 cut ((zenon_TY_s = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H1c]. % 4.25/4.40 cut ((zenon_TZ_ez = zenon_TZ_ez)); [idtac | apply NNPP; zenon_intro zenon_H82]. % 4.25/4.40 congruence. % 4.25/4.40 apply zenon_H82. apply refl_equal. % 4.25/4.40 exact (zenon_H1c zenon_H48). % 4.25/4.40 apply (zenon_L12_ zenon_TX_t zenon_TY_s); trivial. % 4.25/4.40 (* end of lemma zenon_L13_ *) % 4.25/4.40 assert (zenon_L14_ : forall (zenon_TX_t : zenon_U) (zenon_TY_s : zenon_U), (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = zenon_TX_t)\/(~(lesseq Y zenon_TX_t)))) -> (~(zenon_TX_t = (max zenon_TX_t zenon_TY_s))) -> (~(lesseq zenon_TX_t zenon_TY_s)) -> False). % 4.25/4.40 do 2 intro. intros zenon_H17 zenon_Hf zenon_H10 zenon_H18. % 4.25/4.40 generalize (zenon_H17 zenon_TX_t). zenon_intro zenon_H19. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H19); [ zenon_intro zenon_H11 | zenon_intro zenon_H1a ]. % 4.25/4.40 apply (zenon_L1_ zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 exact (zenon_H18 zenon_H1a). % 4.25/4.40 (* end of lemma zenon_L14_ *) % 4.25/4.40 assert (zenon_L15_ : forall (zenon_TZ_ez : zenon_U) (zenon_TY_s : zenon_U) (zenon_TX_t : zenon_U), (~(zenon_TX_t = (max zenon_TX_t zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = zenon_TX_t)\/(~(lesseq Y zenon_TX_t)))) -> (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> (~(lesseq zenon_TX_t zenon_TZ_ez)) -> (lesseq zenon_TY_s zenon_TZ_ez) -> False). % 4.25/4.40 do 3 intro. intros zenon_H10 zenon_Hf zenon_H17 zenon_H1f zenon_H83 zenon_H84. % 4.25/4.40 elim (classic ((~(zenon_TX_t = zenon_TY_s))/\(~(lesseq zenon_TX_t zenon_TY_s)))); [ zenon_intro zenon_H85 | zenon_intro zenon_H86 ]. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H85). zenon_intro zenon_H87. zenon_intro zenon_H18. % 4.25/4.40 apply (zenon_L14_ zenon_TX_t zenon_TY_s); trivial. % 4.25/4.40 cut ((lesseq zenon_TY_s zenon_TZ_ez) = (lesseq zenon_TX_t zenon_TZ_ez)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H83. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H84. % 4.25/4.40 cut ((zenon_TZ_ez = zenon_TZ_ez)); [idtac | apply NNPP; zenon_intro zenon_H82]. % 4.25/4.40 cut ((zenon_TY_s = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_H88]. % 4.25/4.40 congruence. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H86); [ zenon_intro zenon_H8a | zenon_intro zenon_H89 ]. % 4.25/4.40 apply zenon_H8a. zenon_intro zenon_H8b. % 4.25/4.40 elim (classic (zenon_TX_t = zenon_TX_t)); [ zenon_intro zenon_H2f | zenon_intro zenon_H30 ]. % 4.25/4.40 cut ((zenon_TX_t = zenon_TX_t) = (zenon_TY_s = zenon_TX_t)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H88. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H2f. % 4.25/4.40 cut ((zenon_TX_t = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_H30]. % 4.25/4.40 cut ((zenon_TX_t = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_H87]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H87 zenon_H8b). % 4.25/4.40 apply zenon_H30. apply refl_equal. % 4.25/4.40 apply zenon_H30. apply refl_equal. % 4.25/4.40 apply zenon_H89. zenon_intro zenon_H1a. % 4.25/4.40 generalize (zenon_H1f zenon_TX_t). zenon_intro zenon_H32. % 4.25/4.40 generalize (zenon_H32 zenon_TY_s). zenon_intro zenon_H8c. % 4.25/4.40 generalize (zenon_H8c zenon_TZ_ez). zenon_intro zenon_H8d. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H8d); [ zenon_intro zenon_H18 | zenon_intro zenon_H8e ]. % 4.25/4.40 exact (zenon_H18 zenon_H1a). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H8e); [ zenon_intro zenon_H90 | zenon_intro zenon_H8f ]. % 4.25/4.40 exact (zenon_H90 zenon_H84). % 4.25/4.40 exact (zenon_H83 zenon_H8f). % 4.25/4.40 apply zenon_H82. apply refl_equal. % 4.25/4.40 (* end of lemma zenon_L15_ *) % 4.25/4.40 assert (zenon_L16_ : forall (zenon_TY_s : zenon_U) (zenon_TX_t : zenon_U) (zenon_TZ_ez : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> (forall Y : zenon_U, ((lesseq zenon_TZ_ez Y)\/(lesseq Y zenon_TZ_ez))) -> (~(lesseq zenon_TZ_ez (max zenon_TX_t zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = Y)\/(~(lesseq zenon_TX_t Y)))) -> (~(zenon_TX_t = (max zenon_TX_t zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = zenon_TX_t)\/(~(lesseq Y zenon_TX_t)))) -> (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (~(lesseq zenon_TX_t zenon_TZ_ez)) -> False). % 4.25/4.40 do 3 intro. intros zenon_H1f zenon_H91 zenon_H7f zenon_H1b zenon_H10 zenon_Hf zenon_H17 zenon_H83. % 4.25/4.40 generalize (zenon_H91 zenon_TY_s). zenon_intro zenon_H92. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H92); [ zenon_intro zenon_H80 | zenon_intro zenon_H84 ]. % 4.25/4.40 apply (zenon_L13_ zenon_TY_s zenon_TX_t zenon_TZ_ez); trivial. % 4.25/4.40 apply (zenon_L15_ zenon_TZ_ez zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 (* end of lemma zenon_L16_ *) % 4.25/4.40 assert (zenon_L17_ : forall (zenon_TZ_ez : zenon_U) (zenon_TY_s : zenon_U) (zenon_TX_t : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> (~(exists Z : zenon_U, ((ub zenon_TX_t zenon_TY_s Z)/\(lesseq Z zenon_TZ_ez)))) -> (forall Y : zenon_U, ((lesseq zenon_TZ_ez Y)\/(lesseq Y zenon_TZ_ez))) -> (~(lesseq zenon_TZ_ez (max zenon_TX_t zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = Y)\/(~(lesseq zenon_TX_t Y)))) -> (~(zenon_TX_t = (max zenon_TX_t zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = zenon_TX_t)\/(~(lesseq Y zenon_TX_t)))) -> (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_ez) -> False). % 4.25/4.40 do 3 intro. intros zenon_H1f zenon_H93 zenon_H91 zenon_H7f zenon_H1b zenon_H10 zenon_Hf zenon_H17 zenon_H94. % 4.25/4.40 apply zenon_H93. exists zenon_TZ_ez. apply NNPP. zenon_intro zenon_H95. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H95); [ zenon_intro zenon_H97 | zenon_intro zenon_H96 ]. % 4.25/4.40 generalize (ub zenon_TX_t). zenon_intro zenon_H5d. % 4.25/4.40 generalize (zenon_H5d zenon_TY_s). zenon_intro zenon_H5e. % 4.25/4.40 generalize (zenon_H5e zenon_TZ_ez). zenon_intro zenon_H98. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H97; zenon_intro zenon_H9b | zenon_intro zenon_H9a; zenon_intro zenon_H99 ]. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H9b); [ zenon_intro zenon_H83 | zenon_intro zenon_H90 ]. % 4.25/4.40 apply (zenon_L16_ zenon_TY_s zenon_TX_t zenon_TZ_ez); trivial. % 4.25/4.40 elim (classic ((~(zenon_TY_s = (max zenon_TX_t zenon_TY_s)))/\(~(lesseq zenon_TY_s (max zenon_TX_t zenon_TY_s))))); [ zenon_intro zenon_H39 | zenon_intro zenon_H3a ]. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H39). zenon_intro zenon_H1c. zenon_intro zenon_H3b. % 4.25/4.40 apply (zenon_L12_ zenon_TX_t zenon_TY_s); trivial. % 4.25/4.40 cut ((lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_ez) = (lesseq zenon_TY_s zenon_TZ_ez)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H90. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H94. % 4.25/4.40 cut ((zenon_TZ_ez = zenon_TZ_ez)); [idtac | apply NNPP; zenon_intro zenon_H82]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_H45]. % 4.25/4.40 congruence. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H3a); [ zenon_intro zenon_H47 | zenon_intro zenon_H46 ]. % 4.25/4.40 apply zenon_H47. zenon_intro zenon_H48. % 4.25/4.40 elim (classic (zenon_TY_s = zenon_TY_s)); [ zenon_intro zenon_H49 | zenon_intro zenon_H4a ]. % 4.25/4.40 cut ((zenon_TY_s = zenon_TY_s) = ((max zenon_TX_t zenon_TY_s) = zenon_TY_s)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H45. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H49. % 4.25/4.40 cut ((zenon_TY_s = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_H4a]. % 4.25/4.40 cut ((zenon_TY_s = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H1c]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H1c zenon_H48). % 4.25/4.40 apply zenon_H4a. apply refl_equal. % 4.25/4.40 apply zenon_H4a. apply refl_equal. % 4.25/4.40 apply zenon_H46. zenon_intro zenon_H4b. % 4.25/4.40 generalize (zenon_H1f zenon_TY_s). zenon_intro zenon_H40. % 4.25/4.40 generalize (zenon_H40 (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_H4c. % 4.25/4.40 generalize (zenon_H4c zenon_TZ_ez). zenon_intro zenon_H9c. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H9c); [ zenon_intro zenon_H3b | zenon_intro zenon_H9d ]. % 4.25/4.40 exact (zenon_H3b zenon_H4b). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H9d); [ zenon_intro zenon_H9e | zenon_intro zenon_H84 ]. % 4.25/4.40 exact (zenon_H9e zenon_H94). % 4.25/4.40 exact (zenon_H90 zenon_H84). % 4.25/4.40 apply zenon_H82. apply refl_equal. % 4.25/4.40 exact (zenon_H97 zenon_H9a). % 4.25/4.40 generalize (lesseq_ref zenon_TZ_ez). zenon_intro zenon_H9f. % 4.25/4.40 exact (zenon_H96 zenon_H9f). % 4.25/4.40 (* end of lemma zenon_L17_ *) % 4.25/4.40 assert (zenon_L18_ : forall (zenon_TZ_ez : zenon_U) (zenon_TY_s : zenon_U) (zenon_TX_t : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> (~(exists Z : zenon_U, ((ub zenon_TX_t zenon_TY_s Z)/\(lesseq Z zenon_TZ_ez)))) -> (forall Y : zenon_U, ((lesseq zenon_TZ_ez Y)\/(lesseq Y zenon_TZ_ez))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = Y)\/(~(lesseq zenon_TX_t Y)))) -> (~(zenon_TX_t = (max zenon_TX_t zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = zenon_TX_t)\/(~(lesseq Y zenon_TX_t)))) -> (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_ez) -> ((max zenon_TZ_ez zenon_TZ_ez) = zenon_TZ_ez) -> (~(lesseq (max zenon_TZ_ez zenon_TZ_ez) (max zenon_TX_t zenon_TY_s))) -> False). % 4.25/4.40 do 3 intro. intros zenon_H1f zenon_H93 zenon_H91 zenon_H1b zenon_H10 zenon_Hf zenon_H17 zenon_H94 zenon_Ha0 zenon_Ha1. % 4.25/4.40 elim (classic (lesseq (max zenon_TZ_ez zenon_TZ_ez) (max zenon_TZ_ez zenon_TZ_ez))); [ zenon_intro zenon_Ha2 | zenon_intro zenon_Ha3 ]. % 4.25/4.40 elim (classic (lesseq (max zenon_TZ_ez zenon_TZ_ez) zenon_TZ_ez)); [ zenon_intro zenon_Ha4 | zenon_intro zenon_Ha5 ]. % 4.25/4.40 elim (classic (lesseq zenon_TZ_ez (max zenon_TX_t zenon_TY_s))); [ zenon_intro zenon_Ha6 | zenon_intro zenon_H7f ]. % 4.25/4.40 generalize (zenon_H1f (max zenon_TZ_ez zenon_TZ_ez)). zenon_intro zenon_Ha7. % 4.25/4.40 generalize (zenon_Ha7 zenon_TZ_ez). zenon_intro zenon_Ha8. % 4.25/4.40 generalize (zenon_Ha8 (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_Ha9. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_Ha9); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Haa ]. % 4.25/4.40 exact (zenon_Ha5 zenon_Ha4). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_Haa); [ zenon_intro zenon_H7f | zenon_intro zenon_Hab ]. % 4.25/4.40 exact (zenon_H7f zenon_Ha6). % 4.25/4.40 exact (zenon_Ha1 zenon_Hab). % 4.25/4.40 apply (zenon_L17_ zenon_TZ_ez zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 cut ((lesseq (max zenon_TZ_ez zenon_TZ_ez) (max zenon_TZ_ez zenon_TZ_ez)) = (lesseq (max zenon_TZ_ez zenon_TZ_ez) zenon_TZ_ez)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Ha5. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_Ha2. % 4.25/4.40 cut (((max zenon_TZ_ez zenon_TZ_ez) = zenon_TZ_ez)); [idtac | apply NNPP; zenon_intro zenon_Hac]. % 4.25/4.40 cut (((max zenon_TZ_ez zenon_TZ_ez) = (max zenon_TZ_ez zenon_TZ_ez))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 4.25/4.40 congruence. % 4.25/4.40 apply zenon_Had. apply refl_equal. % 4.25/4.40 exact (zenon_Hac zenon_Ha0). % 4.25/4.40 generalize (lesseq_ref (max zenon_TZ_ez zenon_TZ_ez)). zenon_intro zenon_Ha2. % 4.25/4.40 exact (zenon_Ha3 zenon_Ha2). % 4.25/4.40 (* end of lemma zenon_L18_ *) % 4.25/4.40 assert (zenon_L19_ : forall (zenon_TZ_ez : zenon_U) (zenon_TX_t : zenon_U) (zenon_TY_s : zenon_U), (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = zenon_TX_t)\/(~(lesseq Y zenon_TX_t)))) -> (~(zenon_TX_t = (max zenon_TX_t zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = Y)\/(~(lesseq zenon_TX_t Y)))) -> ((max zenon_TZ_ez zenon_TY_s) = zenon_TY_s) -> (~(lesseq (max zenon_TZ_ez zenon_TY_s) (max zenon_TX_t zenon_TY_s))) -> False). % 4.25/4.40 do 3 intro. intros zenon_H17 zenon_Hf zenon_H10 zenon_H1b zenon_Hae zenon_Haf. % 4.25/4.40 elim (classic (lesseq (max zenon_TZ_ez zenon_TY_s) (max zenon_TZ_ez zenon_TY_s))); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Hb1 ]. % 4.25/4.40 elim (classic (lesseq (max zenon_TZ_ez zenon_TY_s) zenon_TY_s)); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hb3 ]. % 4.25/4.40 cut ((lesseq (max zenon_TZ_ez zenon_TY_s) zenon_TY_s) = (lesseq (max zenon_TZ_ez zenon_TY_s) (max zenon_TX_t zenon_TY_s))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Haf. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_Hb2. % 4.25/4.40 cut ((zenon_TY_s = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H1c]. % 4.25/4.40 cut (((max zenon_TZ_ez zenon_TY_s) = (max zenon_TZ_ez zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_Hb4]. % 4.25/4.40 congruence. % 4.25/4.40 apply zenon_Hb4. apply refl_equal. % 4.25/4.40 apply (zenon_L12_ zenon_TX_t zenon_TY_s); trivial. % 4.25/4.40 cut ((lesseq (max zenon_TZ_ez zenon_TY_s) (max zenon_TZ_ez zenon_TY_s)) = (lesseq (max zenon_TZ_ez zenon_TY_s) zenon_TY_s)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Hb3. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_Hb0. % 4.25/4.40 cut (((max zenon_TZ_ez zenon_TY_s) = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_Hb5]. % 4.25/4.40 cut (((max zenon_TZ_ez zenon_TY_s) = (max zenon_TZ_ez zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_Hb4]. % 4.25/4.40 congruence. % 4.25/4.40 apply zenon_Hb4. apply refl_equal. % 4.25/4.40 exact (zenon_Hb5 zenon_Hae). % 4.25/4.40 generalize (lesseq_ref (max zenon_TZ_ez zenon_TY_s)). zenon_intro zenon_Hb0. % 4.25/4.40 exact (zenon_Hb1 zenon_Hb0). % 4.25/4.40 (* end of lemma zenon_L19_ *) % 4.25/4.40 assert (zenon_L20_ : forall (zenon_TX_t : zenon_U) (zenon_TY_s : zenon_U) (zenon_TZ_ez : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> ((max zenon_TZ_ez zenon_TY_s) = zenon_TY_s) -> (~(zenon_TX_t = (max zenon_TX_t zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = zenon_TX_t)\/(~(lesseq Y zenon_TX_t)))) -> (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> ((max zenon_TX_t zenon_TX_t) = zenon_TX_t) -> (~(lesseq (max zenon_TX_t zenon_TX_t) (max zenon_TZ_ez zenon_TY_s))) -> False). % 4.25/4.40 do 3 intro. intros zenon_H1f zenon_Hae zenon_H10 zenon_Hf zenon_H17 zenon_Hb6 zenon_Hb7. % 4.25/4.40 elim (classic (lesseq (max zenon_TX_t zenon_TX_t) (max zenon_TX_t zenon_TX_t))); [ zenon_intro zenon_Hb8 | zenon_intro zenon_Hb9 ]. % 4.25/4.40 elim (classic (lesseq (max zenon_TX_t zenon_TX_t) zenon_TX_t)); [ zenon_intro zenon_Hba | zenon_intro zenon_Hbb ]. % 4.25/4.40 elim (classic (lesseq zenon_TX_t (max zenon_TZ_ez zenon_TY_s))); [ zenon_intro zenon_Hbc | zenon_intro zenon_Hbd ]. % 4.25/4.40 generalize (zenon_H1f (max zenon_TX_t zenon_TX_t)). zenon_intro zenon_Hbe. % 4.25/4.40 generalize (zenon_Hbe zenon_TX_t). zenon_intro zenon_Hbf. % 4.25/4.40 generalize (zenon_Hbf (max zenon_TZ_ez zenon_TY_s)). zenon_intro zenon_Hc0. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_Hc0); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hc1 ]. % 4.25/4.40 exact (zenon_Hbb zenon_Hba). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_Hc1); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hc2 ]. % 4.25/4.40 exact (zenon_Hbd zenon_Hbc). % 4.25/4.40 exact (zenon_Hb7 zenon_Hc2). % 4.25/4.40 elim (classic (zenon_TY_s = (max zenon_TZ_ez zenon_TY_s))); [ zenon_intro zenon_Hc3 | zenon_intro zenon_Hc4 ]. % 4.25/4.40 elim (classic (lesseq zenon_TX_t zenon_TY_s)); [ zenon_intro zenon_H1a | zenon_intro zenon_H18 ]. % 4.25/4.40 cut ((lesseq zenon_TX_t zenon_TY_s) = (lesseq zenon_TX_t (max zenon_TZ_ez zenon_TY_s))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Hbd. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H1a. % 4.25/4.40 cut ((zenon_TY_s = (max zenon_TZ_ez zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 4.25/4.40 cut ((zenon_TX_t = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_H30]. % 4.25/4.40 congruence. % 4.25/4.40 apply zenon_H30. apply refl_equal. % 4.25/4.40 exact (zenon_Hc4 zenon_Hc3). % 4.25/4.40 apply (zenon_L14_ zenon_TX_t zenon_TY_s); trivial. % 4.25/4.40 elim (classic ((max zenon_TZ_ez zenon_TY_s) = (max zenon_TZ_ez zenon_TY_s))); [ zenon_intro zenon_Hc5 | zenon_intro zenon_Hb4 ]. % 4.25/4.40 cut (((max zenon_TZ_ez zenon_TY_s) = (max zenon_TZ_ez zenon_TY_s)) = (zenon_TY_s = (max zenon_TZ_ez zenon_TY_s))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Hc4. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_Hc5. % 4.25/4.40 cut (((max zenon_TZ_ez zenon_TY_s) = (max zenon_TZ_ez zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_Hb4]. % 4.25/4.40 cut (((max zenon_TZ_ez zenon_TY_s) = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_Hb5]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_Hb5 zenon_Hae). % 4.25/4.40 apply zenon_Hb4. apply refl_equal. % 4.25/4.40 apply zenon_Hb4. apply refl_equal. % 4.25/4.40 cut ((lesseq (max zenon_TX_t zenon_TX_t) (max zenon_TX_t zenon_TX_t)) = (lesseq (max zenon_TX_t zenon_TX_t) zenon_TX_t)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Hbb. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_Hb8. % 4.25/4.40 cut (((max zenon_TX_t zenon_TX_t) = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_Hc6]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TX_t) = (max zenon_TX_t zenon_TX_t))); [idtac | apply NNPP; zenon_intro zenon_Hc7]. % 4.25/4.40 congruence. % 4.25/4.40 apply zenon_Hc7. apply refl_equal. % 4.25/4.40 exact (zenon_Hc6 zenon_Hb6). % 4.25/4.40 generalize (lesseq_ref (max zenon_TX_t zenon_TX_t)). zenon_intro zenon_Hb8. % 4.25/4.40 exact (zenon_Hb9 zenon_Hb8). % 4.25/4.40 (* end of lemma zenon_L20_ *) % 4.25/4.40 assert (zenon_L21_ : forall (zenon_TZ_ez : zenon_U) (zenon_TY_s : zenon_U) (zenon_TX_t : zenon_U), (~(exists Z : zenon_U, ((ub zenon_TX_t zenon_TY_s Z)/\(lesseq Z zenon_TZ_ez)))) -> (forall Y : zenon_U, ((lesseq zenon_TZ_ez Y)\/(lesseq Y zenon_TZ_ez))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = Y)\/(~(lesseq zenon_TX_t Y)))) -> (~(zenon_TX_t = (max zenon_TX_t zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = zenon_TX_t)\/(~(lesseq Y zenon_TX_t)))) -> (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_ez) -> ((max zenon_TX_t zenon_TX_t) = zenon_TX_t) -> (~(lesseq (max zenon_TX_t zenon_TX_t) (max zenon_TX_t zenon_TY_s))) -> (~(lesseq zenon_TX_t (max zenon_TX_t zenon_TY_s))) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> ((max zenon_TZ_ez zenon_TZ_ez) = zenon_TZ_ez) -> False). % 4.25/4.40 do 3 intro. intros zenon_H93 zenon_H91 zenon_H1b zenon_H10 zenon_Hf zenon_H17 zenon_H94 zenon_Hb6 zenon_Hc8 zenon_H25 zenon_H1f zenon_Ha0. % 4.25/4.40 elim (classic (zenon_TZ_ez = (max zenon_TZ_ez zenon_TZ_ez))); [ zenon_intro zenon_Hc9 | zenon_intro zenon_Hca ]. % 4.25/4.40 elim (classic (lesseq zenon_TX_t zenon_TZ_ez)); [ zenon_intro zenon_H8f | zenon_intro zenon_H83 ]. % 4.25/4.40 elim (classic (lesseq zenon_TX_t (max zenon_TZ_ez zenon_TZ_ez))); [ zenon_intro zenon_Hcb | zenon_intro zenon_Hcc ]. % 4.25/4.40 elim (classic (lesseq (max zenon_TZ_ez zenon_TZ_ez) (max zenon_TX_t zenon_TY_s))); [ zenon_intro zenon_Hab | zenon_intro zenon_Ha1 ]. % 4.25/4.40 generalize (zenon_H1f zenon_TX_t). zenon_intro zenon_H32. % 4.25/4.40 generalize (zenon_H32 (max zenon_TZ_ez zenon_TZ_ez)). zenon_intro zenon_Hcd. % 4.25/4.40 generalize (zenon_Hcd (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_Hce. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_Hce); [ zenon_intro zenon_Hcc | zenon_intro zenon_Hcf ]. % 4.25/4.40 exact (zenon_Hcc zenon_Hcb). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_Hcf); [ zenon_intro zenon_Ha1 | zenon_intro zenon_H31 ]. % 4.25/4.40 exact (zenon_Ha1 zenon_Hab). % 4.25/4.40 exact (zenon_H25 zenon_H31). % 4.25/4.40 apply (zenon_L18_ zenon_TZ_ez zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 cut ((lesseq zenon_TX_t zenon_TZ_ez) = (lesseq zenon_TX_t (max zenon_TZ_ez zenon_TZ_ez))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Hcc. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H8f. % 4.25/4.40 cut ((zenon_TZ_ez = (max zenon_TZ_ez zenon_TZ_ez))); [idtac | apply NNPP; zenon_intro zenon_Hca]. % 4.25/4.40 cut ((zenon_TX_t = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_H30]. % 4.25/4.40 congruence. % 4.25/4.40 apply zenon_H30. apply refl_equal. % 4.25/4.40 exact (zenon_Hca zenon_Hc9). % 4.25/4.40 generalize (max_2 zenon_TZ_ez). zenon_intro zenon_Hd0. % 4.25/4.40 generalize (zenon_H91 zenon_TY_s). zenon_intro zenon_H92. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H92); [ zenon_intro zenon_H80 | zenon_intro zenon_H84 ]. % 4.25/4.40 generalize (zenon_Hd0 zenon_TY_s). zenon_intro zenon_Hd1. % 4.25/4.40 apply (zenon_or_s _ _ zenon_Hd1); [ zenon_intro zenon_Hae | zenon_intro zenon_Hd2 ]. % 4.25/4.40 elim (classic (zenon_TY_s = (max zenon_TZ_ez zenon_TY_s))); [ zenon_intro zenon_Hc3 | zenon_intro zenon_Hc4 ]. % 4.25/4.40 elim (classic (lesseq (max zenon_TX_t zenon_TX_t) zenon_TY_s)); [ zenon_intro zenon_Hd3 | zenon_intro zenon_Hd4 ]. % 4.25/4.40 elim (classic (lesseq (max zenon_TX_t zenon_TX_t) (max zenon_TZ_ez zenon_TY_s))); [ zenon_intro zenon_Hc2 | zenon_intro zenon_Hb7 ]. % 4.25/4.40 elim (classic (lesseq (max zenon_TZ_ez zenon_TY_s) (max zenon_TX_t zenon_TY_s))); [ zenon_intro zenon_Hd5 | zenon_intro zenon_Haf ]. % 4.25/4.40 generalize (zenon_H1f (max zenon_TX_t zenon_TX_t)). zenon_intro zenon_Hbe. % 4.25/4.40 generalize (zenon_Hbe (max zenon_TZ_ez zenon_TY_s)). zenon_intro zenon_Hd6. % 4.25/4.40 generalize (zenon_Hd6 (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_Hd7. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_Hd7); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hd8 ]. % 4.25/4.40 exact (zenon_Hb7 zenon_Hc2). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_Hd8); [ zenon_intro zenon_Haf | zenon_intro zenon_Hd9 ]. % 4.25/4.40 exact (zenon_Haf zenon_Hd5). % 4.25/4.40 exact (zenon_Hc8 zenon_Hd9). % 4.25/4.40 apply (zenon_L19_ zenon_TZ_ez zenon_TX_t zenon_TY_s); trivial. % 4.25/4.40 cut ((lesseq (max zenon_TX_t zenon_TX_t) zenon_TY_s) = (lesseq (max zenon_TX_t zenon_TX_t) (max zenon_TZ_ez zenon_TY_s))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Hb7. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_Hd3. % 4.25/4.40 cut ((zenon_TY_s = (max zenon_TZ_ez zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TX_t) = (max zenon_TX_t zenon_TX_t))); [idtac | apply NNPP; zenon_intro zenon_Hc7]. % 4.25/4.40 congruence. % 4.25/4.40 apply zenon_Hc7. apply refl_equal. % 4.25/4.40 exact (zenon_Hc4 zenon_Hc3). % 4.25/4.40 elim (classic (lesseq (max zenon_TX_t zenon_TX_t) (max zenon_TZ_ez zenon_TY_s))); [ zenon_intro zenon_Hc2 | zenon_intro zenon_Hb7 ]. % 4.25/4.40 cut ((lesseq (max zenon_TX_t zenon_TX_t) (max zenon_TZ_ez zenon_TY_s)) = (lesseq (max zenon_TX_t zenon_TX_t) zenon_TY_s)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Hd4. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_Hc2. % 4.25/4.40 cut (((max zenon_TZ_ez zenon_TY_s) = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_Hb5]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TX_t) = (max zenon_TX_t zenon_TX_t))); [idtac | apply NNPP; zenon_intro zenon_Hc7]. % 4.25/4.40 congruence. % 4.25/4.40 apply zenon_Hc7. apply refl_equal. % 4.25/4.40 exact (zenon_Hb5 zenon_Hae). % 4.25/4.40 apply (zenon_L20_ zenon_TX_t zenon_TY_s zenon_TZ_ez); trivial. % 4.25/4.40 elim (classic ((max zenon_TZ_ez zenon_TY_s) = (max zenon_TZ_ez zenon_TY_s))); [ zenon_intro zenon_Hc5 | zenon_intro zenon_Hb4 ]. % 4.25/4.40 cut (((max zenon_TZ_ez zenon_TY_s) = (max zenon_TZ_ez zenon_TY_s)) = (zenon_TY_s = (max zenon_TZ_ez zenon_TY_s))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Hc4. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_Hc5. % 4.25/4.40 cut (((max zenon_TZ_ez zenon_TY_s) = (max zenon_TZ_ez zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_Hb4]. % 4.25/4.40 cut (((max zenon_TZ_ez zenon_TY_s) = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_Hb5]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_Hb5 zenon_Hae). % 4.25/4.40 apply zenon_Hb4. apply refl_equal. % 4.25/4.40 apply zenon_Hb4. apply refl_equal. % 4.25/4.40 exact (zenon_Hd2 zenon_H80). % 4.25/4.40 apply (zenon_L15_ zenon_TZ_ez zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 elim (classic ((max zenon_TZ_ez zenon_TZ_ez) = (max zenon_TZ_ez zenon_TZ_ez))); [ zenon_intro zenon_Hda | zenon_intro zenon_Had ]. % 4.25/4.40 cut (((max zenon_TZ_ez zenon_TZ_ez) = (max zenon_TZ_ez zenon_TZ_ez)) = (zenon_TZ_ez = (max zenon_TZ_ez zenon_TZ_ez))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Hca. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_Hda. % 4.25/4.40 cut (((max zenon_TZ_ez zenon_TZ_ez) = (max zenon_TZ_ez zenon_TZ_ez))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 4.25/4.40 cut (((max zenon_TZ_ez zenon_TZ_ez) = zenon_TZ_ez)); [idtac | apply NNPP; zenon_intro zenon_Hac]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_Hac zenon_Ha0). % 4.25/4.40 apply zenon_Had. apply refl_equal. % 4.25/4.40 apply zenon_Had. apply refl_equal. % 4.25/4.40 (* end of lemma zenon_L21_ *) % 4.25/4.40 assert (zenon_L22_ : forall (zenon_TZ_ez : zenon_U) (zenon_TY_s : zenon_U) (zenon_TX_t : zenon_U), (~(lesseq zenon_TX_t (max zenon_TX_t zenon_TY_s))) -> (~(zenon_TX_t = (max zenon_TX_t zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = zenon_TX_t)\/(~(lesseq Y zenon_TX_t)))) -> (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = Y)\/(~(lesseq zenon_TX_t Y)))) -> (forall Y : zenon_U, ((lesseq zenon_TZ_ez Y)\/(lesseq Y zenon_TZ_ez))) -> ((max zenon_TZ_ez zenon_TZ_ez) = zenon_TZ_ez) -> (lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_ez) -> (~(exists Z : zenon_U, ((ub zenon_TX_t zenon_TY_s Z)/\(lesseq Z zenon_TZ_ez)))) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> ((max zenon_TX_t zenon_TX_t) = zenon_TX_t) -> False). % 4.25/4.40 do 3 intro. intros zenon_H25 zenon_H10 zenon_Hf zenon_H17 zenon_H1b zenon_H91 zenon_Ha0 zenon_H94 zenon_H93 zenon_H1f zenon_Hb6. % 4.25/4.40 elim (classic (zenon_TX_t = (max zenon_TX_t zenon_TX_t))); [ zenon_intro zenon_Hdb | zenon_intro zenon_Hdc ]. % 4.25/4.40 elim (classic (lesseq zenon_TX_t zenon_TX_t)); [ zenon_intro zenon_H63 | zenon_intro zenon_H5b ]. % 4.25/4.40 elim (classic (lesseq zenon_TX_t (max zenon_TX_t zenon_TX_t))); [ zenon_intro zenon_Hdd | zenon_intro zenon_Hde ]. % 4.25/4.40 elim (classic (lesseq (max zenon_TX_t zenon_TX_t) (max zenon_TX_t zenon_TY_s))); [ zenon_intro zenon_Hd9 | zenon_intro zenon_Hc8 ]. % 4.25/4.40 generalize (zenon_H1f zenon_TX_t). zenon_intro zenon_H32. % 4.25/4.40 generalize (zenon_H32 (max zenon_TX_t zenon_TX_t)). zenon_intro zenon_Hdf. % 4.25/4.40 generalize (zenon_Hdf (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_He0. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_He0); [ zenon_intro zenon_Hde | zenon_intro zenon_He1 ]. % 4.25/4.40 exact (zenon_Hde zenon_Hdd). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_He1); [ zenon_intro zenon_Hc8 | zenon_intro zenon_H31 ]. % 4.25/4.40 exact (zenon_Hc8 zenon_Hd9). % 4.25/4.40 exact (zenon_H25 zenon_H31). % 4.25/4.40 apply (zenon_L21_ zenon_TZ_ez zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 cut ((lesseq zenon_TX_t zenon_TX_t) = (lesseq zenon_TX_t (max zenon_TX_t zenon_TX_t))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Hde. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H63. % 4.25/4.40 cut ((zenon_TX_t = (max zenon_TX_t zenon_TX_t))); [idtac | apply NNPP; zenon_intro zenon_Hdc]. % 4.25/4.40 cut ((zenon_TX_t = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_H30]. % 4.25/4.40 congruence. % 4.25/4.40 apply zenon_H30. apply refl_equal. % 4.25/4.40 exact (zenon_Hdc zenon_Hdb). % 4.25/4.40 generalize (lesseq_ref zenon_TX_t). zenon_intro zenon_H63. % 4.25/4.40 exact (zenon_H5b zenon_H63). % 4.25/4.40 elim (classic ((max zenon_TX_t zenon_TX_t) = (max zenon_TX_t zenon_TX_t))); [ zenon_intro zenon_He2 | zenon_intro zenon_Hc7 ]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TX_t) = (max zenon_TX_t zenon_TX_t)) = (zenon_TX_t = (max zenon_TX_t zenon_TX_t))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Hdc. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_He2. % 4.25/4.40 cut (((max zenon_TX_t zenon_TX_t) = (max zenon_TX_t zenon_TX_t))); [idtac | apply NNPP; zenon_intro zenon_Hc7]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TX_t) = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_Hc6]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_Hc6 zenon_Hb6). % 4.25/4.40 apply zenon_Hc7. apply refl_equal. % 4.25/4.40 apply zenon_Hc7. apply refl_equal. % 4.25/4.40 (* end of lemma zenon_L22_ *) % 4.25/4.40 assert (zenon_L23_ : forall (zenon_TZ_ez : zenon_U) (zenon_TY_s : zenon_U) (zenon_TX_t : zenon_U), (~(exists Z : zenon_U, ((ub zenon_TX_t zenon_TY_s Z)/\(lesseq Z zenon_TZ_ez)))) -> ((max zenon_TZ_ez zenon_TZ_ez) = zenon_TZ_ez) -> (forall Y : zenon_U, ((lesseq zenon_TZ_ez Y)\/(lesseq Y zenon_TZ_ez))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = Y)\/(~(lesseq zenon_TX_t Y)))) -> ((max zenon_TX_t zenon_TX_t) = zenon_TX_t) -> (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = zenon_TX_t)\/(~(lesseq Y zenon_TX_t)))) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> (~(lesseq zenon_TX_t zenon_TZ_ez)) -> (lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_ez) -> False). % 4.25/4.40 do 3 intro. intros zenon_H93 zenon_Ha0 zenon_H91 zenon_H1b zenon_Hb6 zenon_H17 zenon_Hf zenon_H1f zenon_H83 zenon_H94. % 4.25/4.40 elim (classic ((~(zenon_TX_t = (max zenon_TX_t zenon_TY_s)))/\(~(lesseq zenon_TX_t (max zenon_TX_t zenon_TY_s))))); [ zenon_intro zenon_H23 | zenon_intro zenon_H24 ]. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H23). zenon_intro zenon_H10. zenon_intro zenon_H25. % 4.25/4.40 apply (zenon_L22_ zenon_TZ_ez zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 cut ((lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_ez) = (lesseq zenon_TX_t zenon_TZ_ez)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H83. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H94. % 4.25/4.40 cut ((zenon_TZ_ez = zenon_TZ_ez)); [idtac | apply NNPP; zenon_intro zenon_H82]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_H2b]. % 4.25/4.40 congruence. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H24); [ zenon_intro zenon_H2d | zenon_intro zenon_H2c ]. % 4.25/4.40 apply zenon_H2d. zenon_intro zenon_H2e. % 4.25/4.40 elim (classic (zenon_TX_t = zenon_TX_t)); [ zenon_intro zenon_H2f | zenon_intro zenon_H30 ]. % 4.25/4.40 cut ((zenon_TX_t = zenon_TX_t) = ((max zenon_TX_t zenon_TY_s) = zenon_TX_t)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H2b. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H2f. % 4.25/4.40 cut ((zenon_TX_t = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_H30]. % 4.25/4.40 cut ((zenon_TX_t = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H10]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H10 zenon_H2e). % 4.25/4.40 apply zenon_H30. apply refl_equal. % 4.25/4.40 apply zenon_H30. apply refl_equal. % 4.25/4.40 apply zenon_H2c. zenon_intro zenon_H31. % 4.25/4.40 generalize (zenon_H1f zenon_TX_t). zenon_intro zenon_H32. % 4.25/4.40 generalize (zenon_H32 (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_H33. % 4.25/4.40 generalize (zenon_H33 zenon_TZ_ez). zenon_intro zenon_He3. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_He3); [ zenon_intro zenon_H25 | zenon_intro zenon_He4 ]. % 4.25/4.40 exact (zenon_H25 zenon_H31). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_He4); [ zenon_intro zenon_H9e | zenon_intro zenon_H8f ]. % 4.25/4.40 exact (zenon_H9e zenon_H94). % 4.25/4.40 exact (zenon_H83 zenon_H8f). % 4.25/4.40 apply zenon_H82. apply refl_equal. % 4.25/4.40 (* end of lemma zenon_L23_ *) % 4.25/4.40 assert (zenon_L24_ : forall (zenon_TZ_ez : zenon_U) (zenon_TY_s : zenon_U) (zenon_TX_t : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> (~(exists Z : zenon_U, ((ub zenon_TX_t zenon_TY_s Z)/\(lesseq Z zenon_TZ_ez)))) -> (lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_ez) -> ((max zenon_TZ_ez zenon_TZ_ez) = zenon_TZ_ez) -> (forall Y : zenon_U, ((lesseq zenon_TZ_ez Y)\/(lesseq Y zenon_TZ_ez))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = Y)\/(~(lesseq zenon_TX_t Y)))) -> (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = zenon_TX_t)\/(~(lesseq Y zenon_TX_t)))) -> ((max zenon_TX_t zenon_TX_t) = zenon_TX_t) -> (~(lesseq (max zenon_TX_t zenon_TX_t) (max zenon_TX_t zenon_TY_s))) -> False). % 4.25/4.40 do 3 intro. intros zenon_H1f zenon_H93 zenon_H94 zenon_Ha0 zenon_H91 zenon_H1b zenon_H17 zenon_Hf zenon_Hb6 zenon_Hc8. % 4.25/4.40 elim (classic (lesseq (max zenon_TX_t zenon_TX_t) (max zenon_TX_t zenon_TX_t))); [ zenon_intro zenon_Hb8 | zenon_intro zenon_Hb9 ]. % 4.25/4.40 elim (classic (lesseq (max zenon_TX_t zenon_TX_t) zenon_TX_t)); [ zenon_intro zenon_Hba | zenon_intro zenon_Hbb ]. % 4.25/4.40 cut ((lesseq (max zenon_TX_t zenon_TX_t) zenon_TX_t) = (lesseq (max zenon_TX_t zenon_TX_t) (max zenon_TX_t zenon_TY_s))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Hc8. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_Hba. % 4.25/4.40 cut ((zenon_TX_t = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H10]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TX_t) = (max zenon_TX_t zenon_TX_t))); [idtac | apply NNPP; zenon_intro zenon_Hc7]. % 4.25/4.40 congruence. % 4.25/4.40 apply zenon_Hc7. apply refl_equal. % 4.25/4.40 elim (classic (lesseq zenon_TX_t (max zenon_TX_t zenon_TY_s))); [ zenon_intro zenon_H31 | zenon_intro zenon_H25 ]. % 4.25/4.40 generalize (zenon_H1f (max zenon_TX_t zenon_TX_t)). zenon_intro zenon_Hbe. % 4.25/4.40 generalize (zenon_Hbe zenon_TX_t). zenon_intro zenon_Hbf. % 4.25/4.40 generalize (zenon_Hbf (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_He5. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_He5); [ zenon_intro zenon_Hbb | zenon_intro zenon_He6 ]. % 4.25/4.40 exact (zenon_Hbb zenon_Hba). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_He6); [ zenon_intro zenon_H25 | zenon_intro zenon_Hd9 ]. % 4.25/4.40 exact (zenon_H25 zenon_H31). % 4.25/4.40 exact (zenon_Hc8 zenon_Hd9). % 4.25/4.40 apply (zenon_L21_ zenon_TZ_ez zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 cut ((lesseq (max zenon_TX_t zenon_TX_t) (max zenon_TX_t zenon_TX_t)) = (lesseq (max zenon_TX_t zenon_TX_t) zenon_TX_t)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Hbb. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_Hb8. % 4.25/4.40 cut (((max zenon_TX_t zenon_TX_t) = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_Hc6]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TX_t) = (max zenon_TX_t zenon_TX_t))); [idtac | apply NNPP; zenon_intro zenon_Hc7]. % 4.25/4.40 congruence. % 4.25/4.40 apply zenon_Hc7. apply refl_equal. % 4.25/4.40 exact (zenon_Hc6 zenon_Hb6). % 4.25/4.40 generalize (lesseq_ref (max zenon_TX_t zenon_TX_t)). zenon_intro zenon_Hb8. % 4.25/4.40 exact (zenon_Hb9 zenon_Hb8). % 4.25/4.40 (* end of lemma zenon_L24_ *) % 4.25/4.40 assert (zenon_L25_ : forall (zenon_TX_t : zenon_U) (zenon_TY_s : zenon_U), (forall Y : zenon_U, ((lesseq zenon_TY_s Y)\/(lesseq Y zenon_TY_s))) -> (~(lesseq zenon_TY_s zenon_TX_t)) -> (forall Y : zenon_U, (((max zenon_TX_t Y) = Y)\/(~(lesseq zenon_TX_t Y)))) -> (~(zenon_TY_s = (max zenon_TX_t zenon_TY_s))) -> False). % 4.25/4.40 do 2 intro. intros zenon_H17 zenon_H15 zenon_H1b zenon_H1c. % 4.25/4.40 generalize (zenon_H17 zenon_TX_t). zenon_intro zenon_H19. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H19); [ zenon_intro zenon_H11 | zenon_intro zenon_H1a ]. % 4.25/4.40 exact (zenon_H15 zenon_H11). % 4.25/4.40 apply (zenon_L3_ zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 (* end of lemma zenon_L25_ *) % 4.25/4.40 apply NNPP. intro zenon_G. % 4.25/4.40 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z))))))); [ zenon_intro zenon_H1f | zenon_intro zenon_He7 ]. % 4.25/4.40 apply (zenon_notallex_s (fun X : zenon_U => (forall Y : zenon_U, (forall Z : zenon_U, ((minsol_model_ub X Y Z)<->(minsol_model_max X Y Z))))) zenon_G); [ zenon_intro zenon_He8; idtac ]. % 4.25/4.40 elim zenon_He8. zenon_intro zenon_TX_t. zenon_intro zenon_He9. % 4.25/4.40 apply (zenon_notallex_s (fun Y : zenon_U => (forall Z : zenon_U, ((minsol_model_ub zenon_TX_t Y Z)<->(minsol_model_max zenon_TX_t Y Z)))) zenon_He9); [ zenon_intro zenon_Hea; idtac ]. % 4.25/4.40 elim zenon_Hea. zenon_intro zenon_TY_s. zenon_intro zenon_Heb. % 4.25/4.40 apply (zenon_notallex_s (fun Z : zenon_U => ((minsol_model_ub zenon_TX_t zenon_TY_s Z)<->(minsol_model_max zenon_TX_t zenon_TY_s Z))) zenon_Heb); [ zenon_intro zenon_Hec; idtac ]. % 4.25/4.40 elim zenon_Hec. zenon_intro zenon_TZ_bi. zenon_intro zenon_Hed. % 4.25/4.40 apply (zenon_notequiv_s _ _ zenon_Hed); [ zenon_intro zenon_Hf1; zenon_intro zenon_Hf0 | zenon_intro zenon_Hef; zenon_intro zenon_Hee ]. % 4.25/4.40 generalize (minsol_model_ub zenon_TX_t). zenon_intro zenon_Hf2. % 4.25/4.40 generalize (zenon_Hf2 zenon_TY_s). zenon_intro zenon_Hf3. % 4.25/4.40 generalize (zenon_Hf3 zenon_TZ_bi). zenon_intro zenon_Hf4. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_Hf4); [ zenon_intro zenon_Hf1; zenon_intro zenon_Hf6 | zenon_intro zenon_Hef; zenon_intro zenon_Hf5 ]. % 4.25/4.40 generalize (minsol_model_max zenon_TX_t). zenon_intro zenon_Hf7. % 4.25/4.40 generalize (zenon_Hf7 zenon_TY_s). zenon_intro zenon_Hf8. % 4.25/4.40 generalize (zenon_Hf8 zenon_TZ_bi). zenon_intro zenon_Hf9. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_Hf9); [ zenon_intro zenon_Hee; zenon_intro zenon_Hfb | zenon_intro zenon_Hf0; zenon_intro zenon_Hfa ]. % 4.25/4.40 exact (zenon_Hee zenon_Hf0). % 4.25/4.40 apply (zenon_and_s _ _ zenon_Hfa). zenon_intro zenon_Hfd. zenon_intro zenon_Hfc. % 4.25/4.40 generalize (model_max_2 zenon_TX_t). zenon_intro zenon_Hfe. % 4.25/4.40 generalize (zenon_Hfe zenon_TY_s). zenon_intro zenon_Hff. % 4.25/4.40 generalize (zenon_Hff zenon_TZ_bi). zenon_intro zenon_H100. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H100); [ zenon_intro zenon_H101; zenon_intro zenon_H37 | zenon_intro zenon_Hfd; zenon_intro zenon_H21 ]. % 4.25/4.40 exact (zenon_H101 zenon_Hfd). % 4.25/4.40 apply (zenon_notand_s _ _ zenon_Hf6); [ zenon_intro zenon_H103 | zenon_intro zenon_H102 ]. % 4.25/4.40 generalize (model_ub_2 zenon_TX_t). zenon_intro zenon_H54. % 4.25/4.40 generalize (zenon_H54 zenon_TY_s). zenon_intro zenon_H55. % 4.25/4.40 generalize (zenon_H55 zenon_TZ_bi). zenon_intro zenon_H104. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H104); [ zenon_intro zenon_H103; zenon_intro zenon_H107 | zenon_intro zenon_H106; zenon_intro zenon_H105 ]. % 4.25/4.40 apply zenon_H107. exists zenon_TZ_bi. apply NNPP. zenon_intro zenon_H108. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H108); [ zenon_intro zenon_H10a | zenon_intro zenon_H109 ]. % 4.25/4.40 generalize (ub zenon_TX_t). zenon_intro zenon_H5d. % 4.25/4.40 generalize (zenon_H5d zenon_TY_s). zenon_intro zenon_H5e. % 4.25/4.40 generalize (zenon_H5e zenon_TZ_bi). zenon_intro zenon_H10b. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H10b); [ zenon_intro zenon_H10a; zenon_intro zenon_H10e | zenon_intro zenon_H10d; zenon_intro zenon_H10c ]. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H10e); [ zenon_intro zenon_H20 | zenon_intro zenon_H38 ]. % 4.25/4.40 elim (classic ((~(zenon_TX_t = (max zenon_TX_t zenon_TY_s)))/\(~(lesseq zenon_TX_t (max zenon_TX_t zenon_TY_s))))); [ zenon_intro zenon_H23 | zenon_intro zenon_H24 ]. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H23). zenon_intro zenon_H10. zenon_intro zenon_H25. % 4.25/4.40 generalize (summation_monotone zenon_TX_t). zenon_intro zenon_H10f. % 4.25/4.40 generalize (lesseq_total zenon_TY_s). zenon_intro zenon_H17. % 4.25/4.40 generalize (zenon_H10f zenon_TY_s). zenon_intro zenon_H110. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H110); [ zenon_intro zenon_H18; zenon_intro zenon_H112 | zenon_intro zenon_H1a; zenon_intro zenon_H111 ]. % 4.25/4.40 apply (zenon_L2_ zenon_TX_t zenon_TY_s); trivial. % 4.25/4.40 elim (classic (lesseq zenon_TY_s zenon_TZ_bi)); [ zenon_intro zenon_H44 | zenon_intro zenon_H38 ]. % 4.25/4.40 generalize (zenon_H1f zenon_TX_t). zenon_intro zenon_H32. % 4.25/4.40 generalize (zenon_H32 zenon_TY_s). zenon_intro zenon_H8c. % 4.25/4.40 generalize (zenon_H8c zenon_TZ_bi). zenon_intro zenon_H113. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H113); [ zenon_intro zenon_H18 | zenon_intro zenon_H114 ]. % 4.25/4.40 exact (zenon_H18 zenon_H1a). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H114); [ zenon_intro zenon_H38 | zenon_intro zenon_H36 ]. % 4.25/4.40 exact (zenon_H38 zenon_H44). % 4.25/4.40 exact (zenon_H20 zenon_H36). % 4.25/4.40 apply (zenon_L7_ zenon_TX_t zenon_TZ_bi zenon_TY_s); trivial. % 4.25/4.40 cut ((lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_bi) = (lesseq zenon_TX_t zenon_TZ_bi)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H20. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H21. % 4.25/4.40 cut ((zenon_TZ_bi = zenon_TZ_bi)); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_H2b]. % 4.25/4.40 congruence. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H24); [ zenon_intro zenon_H2d | zenon_intro zenon_H2c ]. % 4.25/4.40 apply zenon_H2d. zenon_intro zenon_H2e. % 4.25/4.40 elim (classic (zenon_TX_t = zenon_TX_t)); [ zenon_intro zenon_H2f | zenon_intro zenon_H30 ]. % 4.25/4.40 cut ((zenon_TX_t = zenon_TX_t) = ((max zenon_TX_t zenon_TY_s) = zenon_TX_t)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H2b. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H2f. % 4.25/4.40 cut ((zenon_TX_t = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_H30]. % 4.25/4.40 cut ((zenon_TX_t = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H10]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H10 zenon_H2e). % 4.25/4.40 apply zenon_H30. apply refl_equal. % 4.25/4.40 apply zenon_H30. apply refl_equal. % 4.25/4.40 apply zenon_H2c. zenon_intro zenon_H31. % 4.25/4.40 generalize (zenon_H1f zenon_TX_t). zenon_intro zenon_H32. % 4.25/4.40 generalize (zenon_H32 (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_H33. % 4.25/4.40 generalize (zenon_H33 zenon_TZ_bi). zenon_intro zenon_H34. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H34); [ zenon_intro zenon_H25 | zenon_intro zenon_H35 ]. % 4.25/4.40 exact (zenon_H25 zenon_H31). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H35); [ zenon_intro zenon_H37 | zenon_intro zenon_H36 ]. % 4.25/4.40 exact (zenon_H37 zenon_H21). % 4.25/4.40 exact (zenon_H20 zenon_H36). % 4.25/4.40 apply zenon_H2a. apply refl_equal. % 4.25/4.40 apply (zenon_L7_ zenon_TX_t zenon_TZ_bi zenon_TY_s); trivial. % 4.25/4.40 exact (zenon_H10a zenon_H10d). % 4.25/4.40 generalize (lesseq_ref zenon_TZ_bi). zenon_intro zenon_H115. % 4.25/4.40 exact (zenon_H109 zenon_H115). % 4.25/4.40 exact (zenon_H103 zenon_H106). % 4.25/4.40 apply (zenon_notallex_s (fun Z : zenon_U => ((model_ub zenon_TX_t zenon_TY_s Z)->(lesseq zenon_TZ_bi Z))) zenon_H102); [ zenon_intro zenon_H116; idtac ]. % 4.25/4.40 elim zenon_H116. zenon_intro zenon_TZ_kt. zenon_intro zenon_H118. % 4.25/4.40 apply (zenon_notimply_s _ _ zenon_H118). zenon_intro zenon_H11a. zenon_intro zenon_H119. % 4.25/4.40 generalize (model_ub_2 zenon_TX_t). zenon_intro zenon_H54. % 4.25/4.40 generalize (zenon_H54 zenon_TY_s). zenon_intro zenon_H55. % 4.25/4.40 generalize (zenon_H55 zenon_TZ_kt). zenon_intro zenon_H11b. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H11b); [ zenon_intro zenon_H11e; zenon_intro zenon_H11d | zenon_intro zenon_H11a; zenon_intro zenon_H11c ]. % 4.25/4.40 exact (zenon_H11e zenon_H11a). % 4.25/4.40 elim zenon_H11c. zenon_intro zenon_TZ_lb. zenon_intro zenon_H120. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H120). zenon_intro zenon_H122. zenon_intro zenon_H121. % 4.25/4.40 generalize (ub zenon_TX_t). zenon_intro zenon_H5d. % 4.25/4.40 generalize (zenon_H5d zenon_TY_s). zenon_intro zenon_H5e. % 4.25/4.40 generalize (zenon_H5e zenon_TZ_lb). zenon_intro zenon_H123. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H123); [ zenon_intro zenon_H126; zenon_intro zenon_H125 | zenon_intro zenon_H122; zenon_intro zenon_H124 ]. % 4.25/4.40 exact (zenon_H126 zenon_H122). % 4.25/4.40 apply (zenon_and_s _ _ zenon_H124). zenon_intro zenon_H128. zenon_intro zenon_H127. % 4.25/4.40 generalize (lesseq_total zenon_TX_t). zenon_intro zenon_H129. % 4.25/4.40 generalize (zenon_Hfc zenon_TZ_kt). zenon_intro zenon_H12a. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H12a); [ zenon_intro zenon_H12c | zenon_intro zenon_H12b ]. % 4.25/4.40 generalize (model_max_2 zenon_TX_t). zenon_intro zenon_Hfe. % 4.25/4.40 generalize (zenon_Hfe zenon_TY_s). zenon_intro zenon_Hff. % 4.25/4.40 generalize (zenon_Hff zenon_TZ_kt). zenon_intro zenon_H12d. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H12d); [ zenon_intro zenon_H12c; zenon_intro zenon_H130 | zenon_intro zenon_H12f; zenon_intro zenon_H12e ]. % 4.25/4.40 elim (classic ((~((max zenon_TX_t zenon_TY_s) = zenon_TZ_lb))/\(~(lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_lb)))); [ zenon_intro zenon_H131 | zenon_intro zenon_H132 ]. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H131). zenon_intro zenon_H134. zenon_intro zenon_H133. % 4.25/4.40 elim (classic ((~((max zenon_TX_t zenon_TY_s) = zenon_TY_s))/\(~(lesseq (max zenon_TX_t zenon_TY_s) zenon_TY_s)))); [ zenon_intro zenon_H135 | zenon_intro zenon_H136 ]. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H135). zenon_intro zenon_H45. zenon_intro zenon_H137. % 4.25/4.40 elim (classic ((~((max zenon_TX_t zenon_TY_s) = zenon_TX_t))/\(~(lesseq (max zenon_TX_t zenon_TY_s) zenon_TX_t)))); [ zenon_intro zenon_H138 | zenon_intro zenon_H139 ]. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H138). zenon_intro zenon_H2b. zenon_intro zenon_H13a. % 4.25/4.40 generalize (max_2 zenon_TX_t). zenon_intro zenon_H1b. % 4.25/4.40 generalize (zenon_H129 zenon_TY_s). zenon_intro zenon_H13b. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H13b); [ zenon_intro zenon_H1a | zenon_intro zenon_H11 ]. % 4.25/4.40 apply (zenon_L8_ zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 generalize (max_1 zenon_TX_t). zenon_intro zenon_Hf. % 4.25/4.40 generalize (zenon_Hf zenon_TY_s). zenon_intro zenon_H14. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H14); [ zenon_intro zenon_H16 | zenon_intro zenon_H15 ]. % 4.25/4.40 exact (zenon_H2b zenon_H16). % 4.25/4.40 exact (zenon_H15 zenon_H11). % 4.25/4.40 cut ((lesseq zenon_TX_t zenon_TZ_lb) = (lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_lb)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H133. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H128. % 4.25/4.40 cut ((zenon_TZ_lb = zenon_TZ_lb)); [idtac | apply NNPP; zenon_intro zenon_H13c]. % 4.25/4.40 cut ((zenon_TX_t = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H10]. % 4.25/4.40 congruence. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H139); [ zenon_intro zenon_H13e | zenon_intro zenon_H13d ]. % 4.25/4.40 apply zenon_H13e. zenon_intro zenon_H16. % 4.25/4.40 elim (classic ((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s))); [ zenon_intro zenon_H13f | zenon_intro zenon_H140 ]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s)) = (zenon_TX_t = (max zenon_TX_t zenon_TY_s))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H10. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H13f. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H140]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_H2b]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H2b zenon_H16). % 4.25/4.40 apply zenon_H140. apply refl_equal. % 4.25/4.40 apply zenon_H140. apply refl_equal. % 4.25/4.40 apply zenon_H13d. zenon_intro zenon_H141. % 4.25/4.40 generalize (zenon_H1f (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_H142. % 4.25/4.40 generalize (zenon_H142 zenon_TX_t). zenon_intro zenon_H143. % 4.25/4.40 generalize (zenon_H143 zenon_TZ_lb). zenon_intro zenon_H144. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H144); [ zenon_intro zenon_H13a | zenon_intro zenon_H145 ]. % 4.25/4.40 exact (zenon_H13a zenon_H141). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H145); [ zenon_intro zenon_H147 | zenon_intro zenon_H146 ]. % 4.25/4.40 exact (zenon_H147 zenon_H128). % 4.25/4.40 exact (zenon_H133 zenon_H146). % 4.25/4.40 apply zenon_H13c. apply refl_equal. % 4.25/4.40 cut ((lesseq zenon_TY_s zenon_TZ_lb) = (lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_lb)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H133. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H127. % 4.25/4.40 cut ((zenon_TZ_lb = zenon_TZ_lb)); [idtac | apply NNPP; zenon_intro zenon_H13c]. % 4.25/4.40 cut ((zenon_TY_s = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H1c]. % 4.25/4.40 congruence. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H136); [ zenon_intro zenon_H149 | zenon_intro zenon_H148 ]. % 4.25/4.40 apply zenon_H149. zenon_intro zenon_H1e. % 4.25/4.40 elim (classic ((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s))); [ zenon_intro zenon_H13f | zenon_intro zenon_H140 ]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s)) = (zenon_TY_s = (max zenon_TX_t zenon_TY_s))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H1c. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H13f. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H140]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_H45]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H45 zenon_H1e). % 4.25/4.40 apply zenon_H140. apply refl_equal. % 4.25/4.40 apply zenon_H140. apply refl_equal. % 4.25/4.40 apply zenon_H148. zenon_intro zenon_H14a. % 4.25/4.40 generalize (zenon_H1f (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_H142. % 4.25/4.40 generalize (zenon_H142 zenon_TY_s). zenon_intro zenon_H14b. % 4.25/4.40 generalize (zenon_H14b zenon_TZ_lb). zenon_intro zenon_H14c. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H14c); [ zenon_intro zenon_H137 | zenon_intro zenon_H14d ]. % 4.25/4.40 exact (zenon_H137 zenon_H14a). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H14d); [ zenon_intro zenon_H14e | zenon_intro zenon_H146 ]. % 4.25/4.40 exact (zenon_H14e zenon_H127). % 4.25/4.40 exact (zenon_H133 zenon_H146). % 4.25/4.40 apply zenon_H13c. apply refl_equal. % 4.25/4.40 cut ((lesseq zenon_TZ_lb zenon_TZ_kt) = (lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_kt)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H130. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H121. % 4.25/4.40 cut ((zenon_TZ_kt = zenon_TZ_kt)); [idtac | apply NNPP; zenon_intro zenon_H14f]. % 4.25/4.40 cut ((zenon_TZ_lb = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H150]. % 4.25/4.40 congruence. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H132); [ zenon_intro zenon_H152 | zenon_intro zenon_H151 ]. % 4.25/4.40 apply zenon_H152. zenon_intro zenon_H153. % 4.25/4.40 elim (classic ((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s))); [ zenon_intro zenon_H13f | zenon_intro zenon_H140 ]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s)) = (zenon_TZ_lb = (max zenon_TX_t zenon_TY_s))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H150. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H13f. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H140]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = zenon_TZ_lb)); [idtac | apply NNPP; zenon_intro zenon_H134]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H134 zenon_H153). % 4.25/4.40 apply zenon_H140. apply refl_equal. % 4.25/4.40 apply zenon_H140. apply refl_equal. % 4.25/4.40 apply zenon_H151. zenon_intro zenon_H146. % 4.25/4.40 generalize (zenon_H1f (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_H142. % 4.25/4.40 generalize (zenon_H142 zenon_TZ_lb). zenon_intro zenon_H154. % 4.25/4.40 generalize (zenon_H154 zenon_TZ_kt). zenon_intro zenon_H155. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H155); [ zenon_intro zenon_H133 | zenon_intro zenon_H156 ]. % 4.25/4.40 exact (zenon_H133 zenon_H146). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H156); [ zenon_intro zenon_H157 | zenon_intro zenon_H12e ]. % 4.25/4.40 exact (zenon_H157 zenon_H121). % 4.25/4.40 exact (zenon_H130 zenon_H12e). % 4.25/4.40 apply zenon_H14f. apply refl_equal. % 4.25/4.40 exact (zenon_H12c zenon_H12f). % 4.25/4.40 exact (zenon_H119 zenon_H12b). % 4.25/4.40 exact (zenon_Hf1 zenon_Hef). % 4.25/4.40 generalize (minsol_model_ub zenon_TX_t). zenon_intro zenon_Hf2. % 4.25/4.40 generalize (zenon_Hf2 zenon_TY_s). zenon_intro zenon_Hf3. % 4.25/4.40 generalize (zenon_Hf3 zenon_TZ_bi). zenon_intro zenon_Hf4. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_Hf4); [ zenon_intro zenon_Hf1; zenon_intro zenon_Hf6 | zenon_intro zenon_Hef; zenon_intro zenon_Hf5 ]. % 4.25/4.40 exact (zenon_Hf1 zenon_Hef). % 4.25/4.40 apply (zenon_and_s _ _ zenon_Hf5). zenon_intro zenon_H106. zenon_intro zenon_H4f. % 4.25/4.40 generalize (model_ub_2 zenon_TX_t). zenon_intro zenon_H54. % 4.25/4.40 generalize (zenon_H54 zenon_TY_s). zenon_intro zenon_H55. % 4.25/4.40 generalize (zenon_H55 zenon_TZ_bi). zenon_intro zenon_H104. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H104); [ zenon_intro zenon_H103; zenon_intro zenon_H107 | zenon_intro zenon_H106; zenon_intro zenon_H105 ]. % 4.25/4.40 exact (zenon_H103 zenon_H106). % 4.25/4.40 elim zenon_H105. zenon_intro zenon_TZ_dy. zenon_intro zenon_H158. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H158). zenon_intro zenon_H159. zenon_intro zenon_H65. % 4.25/4.40 generalize (ub zenon_TX_t). zenon_intro zenon_H5d. % 4.25/4.40 generalize (zenon_H5d zenon_TY_s). zenon_intro zenon_H5e. % 4.25/4.40 generalize (zenon_H5e zenon_TZ_dy). zenon_intro zenon_H15a. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H15a); [ zenon_intro zenon_H15d; zenon_intro zenon_H15c | zenon_intro zenon_H159; zenon_intro zenon_H15b ]. % 4.25/4.40 exact (zenon_H15d zenon_H159). % 4.25/4.40 apply (zenon_and_s _ _ zenon_H15b). zenon_intro zenon_H64. zenon_intro zenon_H73. % 4.25/4.40 generalize (minsol_model_max zenon_TX_t). zenon_intro zenon_Hf7. % 4.25/4.40 generalize (zenon_Hf7 zenon_TY_s). zenon_intro zenon_Hf8. % 4.25/4.40 generalize (zenon_Hf8 zenon_TZ_bi). zenon_intro zenon_Hf9. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_Hf9); [ zenon_intro zenon_Hee; zenon_intro zenon_Hfb | zenon_intro zenon_Hf0; zenon_intro zenon_Hfa ]. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_Hfb); [ zenon_intro zenon_H101 | zenon_intro zenon_H15e ]. % 4.25/4.40 generalize (model_max_2 zenon_TX_t). zenon_intro zenon_Hfe. % 4.25/4.40 generalize (zenon_Hfe zenon_TY_s). zenon_intro zenon_Hff. % 4.25/4.40 generalize (zenon_Hff zenon_TZ_bi). zenon_intro zenon_H100. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H100); [ zenon_intro zenon_H101; zenon_intro zenon_H37 | zenon_intro zenon_Hfd; zenon_intro zenon_H21 ]. % 4.25/4.40 elim (classic ((~((max zenon_TX_t zenon_TY_s) = zenon_TZ_dy))/\(~(lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_dy)))); [ zenon_intro zenon_H15f | zenon_intro zenon_H160 ]. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H15f). zenon_intro zenon_H162. zenon_intro zenon_H161. % 4.25/4.40 elim (classic ((~((max zenon_TX_t zenon_TY_s) = zenon_TY_s))/\(~(lesseq (max zenon_TX_t zenon_TY_s) zenon_TY_s)))); [ zenon_intro zenon_H135 | zenon_intro zenon_H136 ]. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H135). zenon_intro zenon_H45. zenon_intro zenon_H137. % 4.25/4.40 generalize (max_1 zenon_TZ_bi). zenon_intro zenon_H163. % 4.25/4.40 generalize (lesseq_total zenon_TY_s). zenon_intro zenon_H17. % 4.25/4.40 generalize (lesseq_antisymmetric zenon_TZ_bi). zenon_intro zenon_H164. % 4.25/4.40 generalize (max_2 zenon_TX_t). zenon_intro zenon_H1b. % 4.25/4.40 generalize (zenon_H163 zenon_TZ_bi). zenon_intro zenon_H165. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H165); [ zenon_intro zenon_H166 | zenon_intro zenon_H109 ]. % 4.25/4.40 elim (classic (lesseq zenon_TZ_bi zenon_TZ_bi)); [ zenon_intro zenon_H115 | zenon_intro zenon_H109 ]. % 4.25/4.40 elim (classic (lesseq (max zenon_TZ_bi zenon_TZ_bi) zenon_TZ_bi)); [ zenon_intro zenon_H167 | zenon_intro zenon_H168 ]. % 4.25/4.40 cut ((lesseq (max zenon_TZ_bi zenon_TZ_bi) zenon_TZ_bi) = (lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_bi)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H37. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H167. % 4.25/4.40 cut ((zenon_TZ_bi = zenon_TZ_bi)); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 4.25/4.40 cut (((max zenon_TZ_bi zenon_TZ_bi) = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H169]. % 4.25/4.40 congruence. % 4.25/4.40 elim (classic ((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s))); [ zenon_intro zenon_H13f | zenon_intro zenon_H140 ]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s)) = ((max zenon_TZ_bi zenon_TZ_bi) = (max zenon_TX_t zenon_TY_s))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H169. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H13f. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H140]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TZ_bi zenon_TZ_bi))); [idtac | apply NNPP; zenon_intro zenon_H16a]. % 4.25/4.40 congruence. % 4.25/4.40 cut ((zenon_TY_s = zenon_TZ_bi)); [idtac | apply NNPP; zenon_intro zenon_H16b]. % 4.25/4.40 cut ((zenon_TX_t = zenon_TZ_bi)); [idtac | apply NNPP; zenon_intro zenon_H16c]. % 4.25/4.40 congruence. % 4.25/4.40 generalize (zenon_H17 zenon_TX_t). zenon_intro zenon_H19. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H19); [ zenon_intro zenon_H11 | zenon_intro zenon_H1a ]. % 4.25/4.40 generalize (zenon_H164 zenon_TX_t). zenon_intro zenon_H16d. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H16d); [ zenon_intro zenon_H16f | zenon_intro zenon_H16e ]. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H16f); [ zenon_intro zenon_H50 | zenon_intro zenon_H20 ]. % 4.25/4.40 apply (zenon_L9_ zenon_TZ_bi zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 apply (zenon_L10_ zenon_TZ_bi zenon_TZ_dy zenon_TX_t); trivial. % 4.25/4.40 apply zenon_H16c. apply sym_equal. exact zenon_H16e. % 4.25/4.40 apply (zenon_L8_ zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 generalize (zenon_H17 zenon_TX_t). zenon_intro zenon_H19. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H19); [ zenon_intro zenon_H11 | zenon_intro zenon_H1a ]. % 4.25/4.40 generalize (zenon_H164 zenon_TX_t). zenon_intro zenon_H16d. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H16d); [ zenon_intro zenon_H16f | zenon_intro zenon_H16e ]. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H16f); [ zenon_intro zenon_H50 | zenon_intro zenon_H20 ]. % 4.25/4.40 apply (zenon_L9_ zenon_TZ_bi zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 apply (zenon_L10_ zenon_TZ_bi zenon_TZ_dy zenon_TX_t); trivial. % 4.25/4.40 generalize (zenon_H164 zenon_TY_s). zenon_intro zenon_H170. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H170); [ zenon_intro zenon_H172 | zenon_intro zenon_H171 ]. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H172); [ zenon_intro zenon_H173 | zenon_intro zenon_H38 ]. % 4.25/4.40 generalize (zenon_H17 zenon_TZ_bi). zenon_intro zenon_H174. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H174); [ zenon_intro zenon_H44 | zenon_intro zenon_H175 ]. % 4.25/4.40 generalize (zenon_H163 zenon_TY_s). zenon_intro zenon_H176. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H176); [ zenon_intro zenon_H177 | zenon_intro zenon_H38 ]. % 4.25/4.40 elim (classic (lesseq zenon_TZ_bi zenon_TZ_bi)); [ zenon_intro zenon_H115 | zenon_intro zenon_H109 ]. % 4.25/4.40 elim (classic (lesseq (max zenon_TZ_bi zenon_TY_s) zenon_TZ_bi)); [ zenon_intro zenon_H178 | zenon_intro zenon_H179 ]. % 4.25/4.40 cut ((lesseq (max zenon_TZ_bi zenon_TY_s) zenon_TZ_bi) = (lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_bi)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H37. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H178. % 4.25/4.40 cut ((zenon_TZ_bi = zenon_TZ_bi)); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 4.25/4.40 cut (((max zenon_TZ_bi zenon_TY_s) = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H17a]. % 4.25/4.40 congruence. % 4.25/4.40 elim (classic ((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s))); [ zenon_intro zenon_H13f | zenon_intro zenon_H140 ]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s)) = ((max zenon_TZ_bi zenon_TY_s) = (max zenon_TX_t zenon_TY_s))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H17a. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H13f. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H140]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TZ_bi zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H17b]. % 4.25/4.40 congruence. % 4.25/4.40 cut ((zenon_TY_s = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_H4a]. % 4.25/4.40 cut ((zenon_TX_t = zenon_TZ_bi)); [idtac | apply NNPP; zenon_intro zenon_H16c]. % 4.25/4.40 congruence. % 4.25/4.40 apply zenon_H16c. apply sym_equal. exact zenon_H16e. % 4.25/4.40 apply zenon_H4a. apply refl_equal. % 4.25/4.40 apply zenon_H140. apply refl_equal. % 4.25/4.40 apply zenon_H140. apply refl_equal. % 4.25/4.40 apply zenon_H2a. apply refl_equal. % 4.25/4.40 cut ((lesseq zenon_TZ_bi zenon_TZ_bi) = (lesseq (max zenon_TZ_bi zenon_TY_s) zenon_TZ_bi)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H179. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H115. % 4.25/4.40 cut ((zenon_TZ_bi = zenon_TZ_bi)); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 4.25/4.40 cut ((zenon_TZ_bi = (max zenon_TZ_bi zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H17c]. % 4.25/4.40 congruence. % 4.25/4.40 elim (classic ((max zenon_TZ_bi zenon_TY_s) = (max zenon_TZ_bi zenon_TY_s))); [ zenon_intro zenon_H17d | zenon_intro zenon_H17e ]. % 4.25/4.40 cut (((max zenon_TZ_bi zenon_TY_s) = (max zenon_TZ_bi zenon_TY_s)) = (zenon_TZ_bi = (max zenon_TZ_bi zenon_TY_s))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H17c. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H17d. % 4.25/4.40 cut (((max zenon_TZ_bi zenon_TY_s) = (max zenon_TZ_bi zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H17e]. % 4.25/4.40 cut (((max zenon_TZ_bi zenon_TY_s) = zenon_TZ_bi)); [idtac | apply NNPP; zenon_intro zenon_H17f]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H17f zenon_H177). % 4.25/4.40 apply zenon_H17e. apply refl_equal. % 4.25/4.40 apply zenon_H17e. apply refl_equal. % 4.25/4.40 apply zenon_H2a. apply refl_equal. % 4.25/4.40 generalize (lesseq_ref zenon_TZ_bi). zenon_intro zenon_H115. % 4.25/4.40 exact (zenon_H109 zenon_H115). % 4.25/4.40 exact (zenon_H38 zenon_H44). % 4.25/4.40 exact (zenon_H173 zenon_H175). % 4.25/4.40 apply (zenon_L11_ zenon_TZ_bi zenon_TZ_dy zenon_TY_s); trivial. % 4.25/4.40 apply zenon_H16b. apply sym_equal. exact zenon_H171. % 4.25/4.40 apply (zenon_L8_ zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 apply zenon_H140. apply refl_equal. % 4.25/4.40 apply zenon_H140. apply refl_equal. % 4.25/4.40 apply zenon_H2a. apply refl_equal. % 4.25/4.40 cut ((lesseq zenon_TZ_bi zenon_TZ_bi) = (lesseq (max zenon_TZ_bi zenon_TZ_bi) zenon_TZ_bi)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H168. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H115. % 4.25/4.40 cut ((zenon_TZ_bi = zenon_TZ_bi)); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 4.25/4.40 cut ((zenon_TZ_bi = (max zenon_TZ_bi zenon_TZ_bi))); [idtac | apply NNPP; zenon_intro zenon_H180]. % 4.25/4.40 congruence. % 4.25/4.40 elim (classic ((max zenon_TZ_bi zenon_TZ_bi) = (max zenon_TZ_bi zenon_TZ_bi))); [ zenon_intro zenon_H181 | zenon_intro zenon_H182 ]. % 4.25/4.40 cut (((max zenon_TZ_bi zenon_TZ_bi) = (max zenon_TZ_bi zenon_TZ_bi)) = (zenon_TZ_bi = (max zenon_TZ_bi zenon_TZ_bi))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H180. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H181. % 4.25/4.40 cut (((max zenon_TZ_bi zenon_TZ_bi) = (max zenon_TZ_bi zenon_TZ_bi))); [idtac | apply NNPP; zenon_intro zenon_H182]. % 4.25/4.40 cut (((max zenon_TZ_bi zenon_TZ_bi) = zenon_TZ_bi)); [idtac | apply NNPP; zenon_intro zenon_H183]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H183 zenon_H166). % 4.25/4.40 apply zenon_H182. apply refl_equal. % 4.25/4.40 apply zenon_H182. apply refl_equal. % 4.25/4.40 apply zenon_H2a. apply refl_equal. % 4.25/4.40 generalize (lesseq_ref zenon_TZ_bi). zenon_intro zenon_H115. % 4.25/4.40 exact (zenon_H109 zenon_H115). % 4.25/4.40 generalize (lesseq_ref zenon_TZ_bi). zenon_intro zenon_H115. % 4.25/4.40 exact (zenon_H109 zenon_H115). % 4.25/4.40 cut ((lesseq zenon_TY_s zenon_TZ_dy) = (lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_dy)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H161. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H73. % 4.25/4.40 cut ((zenon_TZ_dy = zenon_TZ_dy)); [idtac | apply NNPP; zenon_intro zenon_H184]. % 4.25/4.40 cut ((zenon_TY_s = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H1c]. % 4.25/4.40 congruence. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H136); [ zenon_intro zenon_H149 | zenon_intro zenon_H148 ]. % 4.25/4.40 apply zenon_H149. zenon_intro zenon_H1e. % 4.25/4.40 elim (classic ((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s))); [ zenon_intro zenon_H13f | zenon_intro zenon_H140 ]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s)) = (zenon_TY_s = (max zenon_TX_t zenon_TY_s))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H1c. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H13f. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H140]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_H45]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H45 zenon_H1e). % 4.25/4.40 apply zenon_H140. apply refl_equal. % 4.25/4.40 apply zenon_H140. apply refl_equal. % 4.25/4.40 apply zenon_H148. zenon_intro zenon_H14a. % 4.25/4.40 generalize (zenon_H1f (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_H142. % 4.25/4.40 generalize (zenon_H142 zenon_TY_s). zenon_intro zenon_H14b. % 4.25/4.40 generalize (zenon_H14b zenon_TZ_dy). zenon_intro zenon_H185. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H185); [ zenon_intro zenon_H137 | zenon_intro zenon_H186 ]. % 4.25/4.40 exact (zenon_H137 zenon_H14a). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H186); [ zenon_intro zenon_H76 | zenon_intro zenon_H187 ]. % 4.25/4.40 exact (zenon_H76 zenon_H73). % 4.25/4.40 exact (zenon_H161 zenon_H187). % 4.25/4.40 apply zenon_H184. apply refl_equal. % 4.25/4.40 cut ((lesseq zenon_TZ_dy zenon_TZ_bi) = (lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_bi)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H37. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H65. % 4.25/4.40 cut ((zenon_TZ_bi = zenon_TZ_bi)); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 4.25/4.40 cut ((zenon_TZ_dy = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H188]. % 4.25/4.40 congruence. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H160); [ zenon_intro zenon_H18a | zenon_intro zenon_H189 ]. % 4.25/4.40 apply zenon_H18a. zenon_intro zenon_H18b. % 4.25/4.40 elim (classic ((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s))); [ zenon_intro zenon_H13f | zenon_intro zenon_H140 ]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s)) = (zenon_TZ_dy = (max zenon_TX_t zenon_TY_s))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H188. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H13f. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H140]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = zenon_TZ_dy)); [idtac | apply NNPP; zenon_intro zenon_H162]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H162 zenon_H18b). % 4.25/4.40 apply zenon_H140. apply refl_equal. % 4.25/4.40 apply zenon_H140. apply refl_equal. % 4.25/4.40 apply zenon_H189. zenon_intro zenon_H187. % 4.25/4.40 generalize (zenon_H1f (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_H142. % 4.25/4.40 generalize (zenon_H142 zenon_TZ_dy). zenon_intro zenon_H18c. % 4.25/4.40 generalize (zenon_H18c zenon_TZ_bi). zenon_intro zenon_H18d. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H18d); [ zenon_intro zenon_H161 | zenon_intro zenon_H18e ]. % 4.25/4.40 exact (zenon_H161 zenon_H187). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H18e); [ zenon_intro zenon_H72 | zenon_intro zenon_H21 ]. % 4.25/4.40 exact (zenon_H72 zenon_H65). % 4.25/4.40 exact (zenon_H37 zenon_H21). % 4.25/4.40 apply zenon_H2a. apply refl_equal. % 4.25/4.40 exact (zenon_H101 zenon_Hfd). % 4.25/4.40 apply (zenon_notallex_s (fun Z : zenon_U => ((model_max zenon_TX_t zenon_TY_s Z)->(lesseq zenon_TZ_bi Z))) zenon_H15e); [ zenon_intro zenon_H18f; idtac ]. % 4.25/4.40 elim zenon_H18f. zenon_intro zenon_TZ_ez. zenon_intro zenon_H190. % 4.25/4.40 apply (zenon_notimply_s _ _ zenon_H190). zenon_intro zenon_H192. zenon_intro zenon_H191. % 4.25/4.40 generalize (model_max_2 zenon_TX_t). zenon_intro zenon_Hfe. % 4.25/4.40 generalize (zenon_Hfe zenon_TY_s). zenon_intro zenon_Hff. % 4.25/4.40 generalize (zenon_Hff zenon_TZ_ez). zenon_intro zenon_H193. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H193); [ zenon_intro zenon_H194; zenon_intro zenon_H9e | zenon_intro zenon_H192; zenon_intro zenon_H94 ]. % 4.25/4.40 exact (zenon_H194 zenon_H192). % 4.25/4.40 generalize (max_1 zenon_TZ_ez). zenon_intro zenon_H195. % 4.25/4.40 generalize (lesseq_total zenon_TZ_ez). zenon_intro zenon_H91. % 4.25/4.40 generalize (max_2 zenon_TX_t). zenon_intro zenon_H1b. % 4.25/4.40 generalize (zenon_H4f zenon_TZ_ez). zenon_intro zenon_H196. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H196); [ zenon_intro zenon_H198 | zenon_intro zenon_H197 ]. % 4.25/4.40 generalize (model_ub_2 zenon_TX_t). zenon_intro zenon_H54. % 4.25/4.40 generalize (zenon_H54 zenon_TY_s). zenon_intro zenon_H55. % 4.25/4.40 generalize (zenon_H55 zenon_TZ_ez). zenon_intro zenon_H199. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H199); [ zenon_intro zenon_H198; zenon_intro zenon_H93 | zenon_intro zenon_H19b; zenon_intro zenon_H19a ]. % 4.25/4.40 generalize (lesseq_total zenon_TY_s). zenon_intro zenon_H17. % 4.25/4.40 generalize (max_1 zenon_TX_t). zenon_intro zenon_Hf. % 4.25/4.40 generalize (zenon_H195 zenon_TZ_ez). zenon_intro zenon_H19c. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H19c); [ zenon_intro zenon_Ha0 | zenon_intro zenon_H96 ]. % 4.25/4.40 generalize (zenon_H1b zenon_TX_t). zenon_intro zenon_H19d. % 4.25/4.40 apply (zenon_or_s _ _ zenon_H19d); [ zenon_intro zenon_Hb6 | zenon_intro zenon_H5b ]. % 4.25/4.40 apply zenon_H93. exists zenon_TZ_ez. apply NNPP. zenon_intro zenon_H95. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H95); [ zenon_intro zenon_H97 | zenon_intro zenon_H96 ]. % 4.25/4.40 generalize (ub zenon_TX_t). zenon_intro zenon_H5d. % 4.25/4.40 generalize (zenon_H5d zenon_TY_s). zenon_intro zenon_H5e. % 4.25/4.40 generalize (zenon_H5e zenon_TZ_ez). zenon_intro zenon_H98. % 4.25/4.40 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H97; zenon_intro zenon_H9b | zenon_intro zenon_H9a; zenon_intro zenon_H99 ]. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H9b); [ zenon_intro zenon_H83 | zenon_intro zenon_H90 ]. % 4.25/4.40 apply (zenon_L23_ zenon_TZ_ez zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 elim (classic ((~(zenon_TY_s = (max zenon_TX_t zenon_TY_s)))/\(~(lesseq zenon_TY_s (max zenon_TX_t zenon_TY_s))))); [ zenon_intro zenon_H39 | zenon_intro zenon_H3a ]. % 4.25/4.40 apply (zenon_and_s _ _ zenon_H39). zenon_intro zenon_H1c. zenon_intro zenon_H3b. % 4.25/4.40 elim (classic (zenon_TX_t = (max zenon_TX_t zenon_TX_t))); [ zenon_intro zenon_Hdb | zenon_intro zenon_Hdc ]. % 4.25/4.40 elim (classic (lesseq zenon_TY_s zenon_TX_t)); [ zenon_intro zenon_H11 | zenon_intro zenon_H15 ]. % 4.25/4.40 elim (classic (lesseq zenon_TY_s (max zenon_TX_t zenon_TX_t))); [ zenon_intro zenon_H19e | zenon_intro zenon_H19f ]. % 4.25/4.40 elim (classic (lesseq (max zenon_TX_t zenon_TX_t) (max zenon_TX_t zenon_TY_s))); [ zenon_intro zenon_Hd9 | zenon_intro zenon_Hc8 ]. % 4.25/4.40 generalize (zenon_H1f zenon_TY_s). zenon_intro zenon_H40. % 4.25/4.40 generalize (zenon_H40 (max zenon_TX_t zenon_TX_t)). zenon_intro zenon_H1a0. % 4.25/4.40 generalize (zenon_H1a0 (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_H1a1. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H1a1); [ zenon_intro zenon_H19f | zenon_intro zenon_H1a2 ]. % 4.25/4.40 exact (zenon_H19f zenon_H19e). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H1a2); [ zenon_intro zenon_Hc8 | zenon_intro zenon_H4b ]. % 4.25/4.40 exact (zenon_Hc8 zenon_Hd9). % 4.25/4.40 exact (zenon_H3b zenon_H4b). % 4.25/4.40 apply (zenon_L24_ zenon_TZ_ez zenon_TY_s zenon_TX_t); trivial. % 4.25/4.40 cut ((lesseq zenon_TY_s zenon_TX_t) = (lesseq zenon_TY_s (max zenon_TX_t zenon_TX_t))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H19f. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H11. % 4.25/4.40 cut ((zenon_TX_t = (max zenon_TX_t zenon_TX_t))); [idtac | apply NNPP; zenon_intro zenon_Hdc]. % 4.25/4.40 cut ((zenon_TY_s = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_H4a]. % 4.25/4.40 congruence. % 4.25/4.40 apply zenon_H4a. apply refl_equal. % 4.25/4.40 exact (zenon_Hdc zenon_Hdb). % 4.25/4.40 apply (zenon_L25_ zenon_TX_t zenon_TY_s); trivial. % 4.25/4.40 elim (classic ((max zenon_TX_t zenon_TX_t) = (max zenon_TX_t zenon_TX_t))); [ zenon_intro zenon_He2 | zenon_intro zenon_Hc7 ]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TX_t) = (max zenon_TX_t zenon_TX_t)) = (zenon_TX_t = (max zenon_TX_t zenon_TX_t))). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_Hdc. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_He2. % 4.25/4.40 cut (((max zenon_TX_t zenon_TX_t) = (max zenon_TX_t zenon_TX_t))); [idtac | apply NNPP; zenon_intro zenon_Hc7]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TX_t) = zenon_TX_t)); [idtac | apply NNPP; zenon_intro zenon_Hc6]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_Hc6 zenon_Hb6). % 4.25/4.40 apply zenon_Hc7. apply refl_equal. % 4.25/4.40 apply zenon_Hc7. apply refl_equal. % 4.25/4.40 cut ((lesseq (max zenon_TX_t zenon_TY_s) zenon_TZ_ez) = (lesseq zenon_TY_s zenon_TZ_ez)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H90. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H94. % 4.25/4.40 cut ((zenon_TZ_ez = zenon_TZ_ez)); [idtac | apply NNPP; zenon_intro zenon_H82]. % 4.25/4.40 cut (((max zenon_TX_t zenon_TY_s) = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_H45]. % 4.25/4.40 congruence. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H3a); [ zenon_intro zenon_H47 | zenon_intro zenon_H46 ]. % 4.25/4.40 apply zenon_H47. zenon_intro zenon_H48. % 4.25/4.40 elim (classic (zenon_TY_s = zenon_TY_s)); [ zenon_intro zenon_H49 | zenon_intro zenon_H4a ]. % 4.25/4.40 cut ((zenon_TY_s = zenon_TY_s) = ((max zenon_TX_t zenon_TY_s) = zenon_TY_s)). % 4.25/4.40 intro zenon_D_pnotp. % 4.25/4.40 apply zenon_H45. % 4.25/4.40 rewrite <- zenon_D_pnotp. % 4.25/4.40 exact zenon_H49. % 4.25/4.40 cut ((zenon_TY_s = zenon_TY_s)); [idtac | apply NNPP; zenon_intro zenon_H4a]. % 4.25/4.40 cut ((zenon_TY_s = (max zenon_TX_t zenon_TY_s))); [idtac | apply NNPP; zenon_intro zenon_H1c]. % 4.25/4.40 congruence. % 4.25/4.40 exact (zenon_H1c zenon_H48). % 4.25/4.40 apply zenon_H4a. apply refl_equal. % 4.25/4.40 apply zenon_H4a. apply refl_equal. % 4.25/4.40 apply zenon_H46. zenon_intro zenon_H4b. % 4.25/4.40 generalize (zenon_H1f zenon_TY_s). zenon_intro zenon_H40. % 4.25/4.40 generalize (zenon_H40 (max zenon_TX_t zenon_TY_s)). zenon_intro zenon_H4c. % 4.25/4.40 generalize (zenon_H4c zenon_TZ_ez). zenon_intro zenon_H9c. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H9c); [ zenon_intro zenon_H3b | zenon_intro zenon_H9d ]. % 4.25/4.40 exact (zenon_H3b zenon_H4b). % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H9d); [ zenon_intro zenon_H9e | zenon_intro zenon_H84 ]. % 4.25/4.40 exact (zenon_H9e zenon_H94). % 4.25/4.40 exact (zenon_H90 zenon_H84). % 4.25/4.40 apply zenon_H82. apply refl_equal. % 4.25/4.40 exact (zenon_H97 zenon_H9a). % 4.25/4.40 generalize (lesseq_ref zenon_TZ_ez). zenon_intro zenon_H9f. % 4.25/4.40 exact (zenon_H96 zenon_H9f). % 4.25/4.40 generalize (lesseq_ref zenon_TX_t). zenon_intro zenon_H63. % 4.25/4.40 exact (zenon_H5b zenon_H63). % 4.25/4.40 generalize (lesseq_ref zenon_TZ_ez). zenon_intro zenon_H9f. % 4.25/4.40 exact (zenon_H96 zenon_H9f). % 4.25/4.40 exact (zenon_H198 zenon_H19b). % 4.25/4.40 exact (zenon_H191 zenon_H197). % 4.25/4.40 exact (zenon_Hee zenon_Hf0). % 4.25/4.40 apply zenon_He7. zenon_intro zenon_Tx_qd. apply NNPP. zenon_intro zenon_H1a4. % 4.25/4.40 apply zenon_H1a4. zenon_intro zenon_Ty_qf. apply NNPP. zenon_intro zenon_H1a6. % 4.25/4.40 apply zenon_H1a6. zenon_intro zenon_Tz_qh. apply NNPP. zenon_intro zenon_H1a8. % 4.25/4.40 apply (zenon_notimply_s _ _ zenon_H1a8). zenon_intro zenon_H1aa. zenon_intro zenon_H1a9. % 4.25/4.40 apply (zenon_notimply_s _ _ zenon_H1a9). zenon_intro zenon_H1ac. zenon_intro zenon_H1ab. % 4.25/4.40 generalize (lesseq_trans zenon_Tx_qd). zenon_intro zenon_H1ad. % 4.25/4.40 generalize (zenon_H1ad zenon_Ty_qf). zenon_intro zenon_H1ae. % 4.25/4.40 generalize (zenon_H1ae zenon_Tz_qh). zenon_intro zenon_H1af. % 4.25/4.40 apply (zenon_imply_s _ _ zenon_H1af); [ zenon_intro zenon_H1b1 | zenon_intro zenon_H1b0 ]. % 4.25/4.40 apply (zenon_notand_s _ _ zenon_H1b1); [ zenon_intro zenon_H1b3 | zenon_intro zenon_H1b2 ]. % 4.25/4.40 exact (zenon_H1b3 zenon_H1aa). % 4.25/4.40 exact (zenon_H1b2 zenon_H1ac). % 4.25/4.40 exact (zenon_H1ab zenon_H1b0). % 4.25/4.40 Qed. % 4.25/4.40 % SZS output end Proof % 4.25/4.40 (* END-PROOF *) % 4.25/4.40 nodes searched: 325053 % 4.25/4.40 max branch formulas: 3553 % 4.25/4.40 proof nodes created: 7664 % 4.25/4.40 formulas created: 216661 % 4.25/4.40 %------------------------------------------------------------------------------