%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NUM860+1 : TPTP v8.1.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n010.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:04 EDT 2022 % Result : Theorem 47.46s 47.70s % Output : Proof 47.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM860+1 : TPTP v8.1.0. Released v4.1.0. % 0.03/0.13 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n010.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jul 7 02:14:01 EDT 2022 % 0.12/0.34 % CPUTime : % 47.46/47.70 (* PROOF-FOUND *) % 47.46/47.70 % SZS status Theorem % 47.46/47.70 (* BEGIN-PROOF *) % 47.46/47.70 % SZS output start Proof % 47.46/47.70 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))))). % 47.46/47.70 Proof. % 47.46/47.70 assert (zenon_L1_ : forall (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U), (~(model_max zenon_TX_r zenon_TY_q (summation (max zenon_TX_r zenon_TY_q)))) -> False). % 47.46/47.70 do 2 intro. intros zenon_Hf. % 47.46/47.70 generalize (model_max_3 zenon_TX_r). zenon_intro zenon_H12. % 47.46/47.70 generalize (zenon_H12 zenon_TY_q). zenon_intro zenon_H13. % 47.46/47.70 generalize (zenon_H13 (summation (max zenon_TX_r zenon_TY_q))). zenon_intro zenon_H14. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_H14); [ zenon_intro zenon_Hf; zenon_intro zenon_H17 | zenon_intro zenon_H16; zenon_intro zenon_H15 ]. % 47.46/47.70 generalize (lesseq_ref (summation (max zenon_TX_r zenon_TY_q))). zenon_intro zenon_H15. % 47.46/47.70 exact (zenon_H17 zenon_H15). % 47.46/47.70 exact (zenon_Hf zenon_H16). % 47.46/47.70 (* end of lemma zenon_L1_ *) % 47.46/47.70 assert (zenon_L2_ : forall (zenon_TX_r : zenon_U) (zenon_TY_q : zenon_U), (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (~(lesseq zenon_TY_q zenon_TX_r)) -> (~(lesseq zenon_TX_r zenon_TY_q)) -> False). % 47.46/47.70 do 2 intro. intros zenon_H18 zenon_H19 zenon_H1a. % 47.46/47.70 generalize (zenon_H18 zenon_TX_r). zenon_intro zenon_H1b. % 47.46/47.70 apply (zenon_or_s _ _ zenon_H1b); [ zenon_intro zenon_H1d | zenon_intro zenon_H1c ]. % 47.46/47.70 exact (zenon_H19 zenon_H1d). % 47.46/47.70 exact (zenon_H1a zenon_H1c). % 47.46/47.70 (* end of lemma zenon_L2_ *) % 47.46/47.70 assert (zenon_L3_ : forall (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U), (forall Y : zenon_U, (((max zenon_TX_r Y) = zenon_TX_r)\/(~(lesseq Y zenon_TX_r)))) -> (~((max zenon_TX_r zenon_TY_q) = zenon_TX_r)) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (~(lesseq zenon_TX_r zenon_TY_q)) -> False). % 47.46/47.70 do 2 intro. intros zenon_H1e zenon_H1f zenon_H18 zenon_H1a. % 47.46/47.70 generalize (zenon_H1e zenon_TY_q). zenon_intro zenon_H20. % 47.46/47.70 apply (zenon_or_s _ _ zenon_H20); [ zenon_intro zenon_H21 | zenon_intro zenon_H19 ]. % 47.46/47.70 exact (zenon_H1f zenon_H21). % 47.46/47.70 apply (zenon_L2_ zenon_TX_r zenon_TY_q); trivial. % 47.46/47.70 (* end of lemma zenon_L3_ *) % 47.46/47.70 assert (zenon_L4_ : forall (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U), (~((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TX_r))) -> (~(lesseq zenon_TX_r zenon_TY_q)) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (forall Y : zenon_U, (((max zenon_TX_r Y) = zenon_TX_r)\/(~(lesseq Y zenon_TX_r)))) -> False). % 47.46/47.70 do 2 intro. intros zenon_H22 zenon_H1a zenon_H18 zenon_H1e. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = zenon_TX_r)); [idtac | apply NNPP; zenon_intro zenon_H1f]. % 47.46/47.70 congruence. % 47.46/47.70 apply (zenon_L3_ zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 (* end of lemma zenon_L4_ *) % 47.46/47.70 assert (zenon_L5_ : forall (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U), (lesseq zenon_TX_r zenon_TY_q) -> (~((max zenon_TX_r zenon_TY_q) = zenon_TY_q)) -> False). % 47.46/47.70 do 2 intro. intros zenon_H1c zenon_H23. % 47.46/47.70 generalize (max_2 zenon_TX_r). zenon_intro zenon_H24. % 47.46/47.70 generalize (zenon_H24 zenon_TY_q). zenon_intro zenon_H25. % 47.46/47.70 apply (zenon_or_s _ _ zenon_H25); [ zenon_intro zenon_H26 | zenon_intro zenon_H1a ]. % 47.46/47.70 exact (zenon_H23 zenon_H26). % 47.46/47.70 exact (zenon_H1a zenon_H1c). % 47.46/47.70 (* end of lemma zenon_L5_ *) % 47.46/47.70 assert (zenon_L6_ : forall (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U), (forall Y : zenon_U, ((lesseq zenon_TX_r Y)\/(lesseq Y zenon_TX_r))) -> (~((max zenon_TX_r zenon_TY_q) = zenon_TY_q)) -> (~(lesseq zenon_TY_q zenon_TX_r)) -> False). % 47.46/47.70 do 2 intro. intros zenon_H27 zenon_H23 zenon_H19. % 47.46/47.70 generalize (zenon_H27 zenon_TY_q). zenon_intro zenon_H28. % 47.46/47.70 apply (zenon_or_s _ _ zenon_H28); [ zenon_intro zenon_H1c | zenon_intro zenon_H1d ]. % 47.46/47.70 apply (zenon_L5_ zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 exact (zenon_H19 zenon_H1d). % 47.46/47.70 (* end of lemma zenon_L6_ *) % 47.46/47.70 assert (zenon_L7_ : forall (zenon_TX_r : zenon_U) (zenon_TY_q : zenon_U), (lesseq zenon_TY_q zenon_TX_r) -> (~(ub zenon_TX_r zenon_TY_q zenon_TX_r)) -> False). % 47.46/47.70 do 2 intro. intros zenon_H1d zenon_H29. % 47.46/47.70 generalize (ub zenon_TX_r). zenon_intro zenon_H2a. % 47.46/47.70 generalize (zenon_H2a zenon_TY_q). zenon_intro zenon_H2b. % 47.46/47.70 generalize (zenon_H2b zenon_TX_r). zenon_intro zenon_H2c. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_H2c); [ zenon_intro zenon_H29; zenon_intro zenon_H2f | zenon_intro zenon_H2e; zenon_intro zenon_H2d ]. % 47.46/47.70 apply (zenon_notand_s _ _ zenon_H2f); [ zenon_intro zenon_H30 | zenon_intro zenon_H19 ]. % 47.46/47.70 generalize (lesseq_ref zenon_TX_r). zenon_intro zenon_H31. % 47.46/47.70 exact (zenon_H30 zenon_H31). % 47.46/47.70 exact (zenon_H19 zenon_H1d). % 47.46/47.70 exact (zenon_H29 zenon_H2e). % 47.46/47.70 (* end of lemma zenon_L7_ *) % 47.46/47.70 assert (zenon_L8_ : forall (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U), (forall Y : zenon_U, (forall Z : zenon_U, ((lesseq zenon_TX_r Y)<->(lesseq (sum Z zenon_TX_r) (sum Z Y))))) -> (~((max zenon_TX_r zenon_TY_q) = zenon_TY_q)) -> (forall Y : zenon_U, (((max zenon_TX_r Y) = zenon_TX_r)\/(~(lesseq Y zenon_TX_r)))) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (~((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TX_r))) -> False). % 47.46/47.70 do 2 intro. intros zenon_H32 zenon_H23 zenon_H1e zenon_H18 zenon_H22. % 47.46/47.70 generalize (zenon_H32 zenon_TY_q). zenon_intro zenon_H0. % 47.46/47.70 generalize (zenon_H0 zenon_E). zenon_intro zenon_H33. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_H33); [ zenon_intro zenon_H1a; zenon_intro zenon_H35 | zenon_intro zenon_H1c; zenon_intro zenon_H34 ]. % 47.46/47.70 apply (zenon_L4_ zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 apply (zenon_L5_ zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 (* end of lemma zenon_L8_ *) % 47.46/47.70 assert (zenon_L9_ : forall (zenon_TY_q : zenon_U) (zenon_TZ_ce : zenon_U) (zenon_TX_r : zenon_U), (~(lesseq (summation zenon_TX_r) zenon_TZ_ce)) -> (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (forall Y : zenon_U, (((max zenon_TX_r Y) = zenon_TX_r)\/(~(lesseq Y zenon_TX_r)))) -> (~((max zenon_TX_r zenon_TY_q) = zenon_TY_q)) -> (forall Y : zenon_U, (forall Z : zenon_U, ((lesseq zenon_TX_r Y)<->(lesseq (sum Z zenon_TX_r) (sum Z Y))))) -> False). % 47.46/47.70 do 3 intro. intros zenon_H36 zenon_H37 zenon_H18 zenon_H1e zenon_H23 zenon_H32. % 47.46/47.70 cut ((lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) = (lesseq (summation zenon_TX_r) zenon_TZ_ce)). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H36. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H37. % 47.46/47.70 cut ((zenon_TZ_ce = zenon_TZ_ce)); [idtac | apply NNPP; zenon_intro zenon_H39]. % 47.46/47.70 cut (((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TX_r))); [idtac | apply NNPP; zenon_intro zenon_H22]. % 47.46/47.70 congruence. % 47.46/47.70 apply (zenon_L8_ zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 apply zenon_H39. apply refl_equal. % 47.46/47.70 (* end of lemma zenon_L9_ *) % 47.46/47.70 assert (zenon_L10_ : forall (zenon_TZ_ce : zenon_U) (zenon_TX_r : zenon_U) (zenon_TY_q : zenon_U), (forall Y : zenon_U, ((lesseq zenon_TY_q Y)<->(lesseq (summation zenon_TY_q) (summation Y)))) -> (~((max zenon_TX_r zenon_TY_q) = zenon_TY_q)) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) -> (~(exists Z : zenon_U, ((ub zenon_TX_r zenon_TY_q Z)/\(lesseq (summation Z) zenon_TZ_ce)))) -> False). % 47.46/47.70 do 3 intro. intros zenon_H3a zenon_H23 zenon_H18 zenon_H37 zenon_H3b. % 47.46/47.70 generalize (max_1 zenon_TX_r). zenon_intro zenon_H1e. % 47.46/47.70 generalize (lesseq_total zenon_TX_r). zenon_intro zenon_H27. % 47.46/47.70 generalize (zenon_H3a zenon_TX_r). zenon_intro zenon_H3c. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_H3c); [ zenon_intro zenon_H19; zenon_intro zenon_H3e | zenon_intro zenon_H1d; zenon_intro zenon_H3d ]. % 47.46/47.70 apply (zenon_L6_ zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 generalize (sum_monotone_1 zenon_TX_r). zenon_intro zenon_H32. % 47.46/47.70 apply zenon_H3b. exists zenon_TX_r. apply NNPP. zenon_intro zenon_H3f. % 47.46/47.70 apply (zenon_notand_s _ _ zenon_H3f); [ zenon_intro zenon_H29 | zenon_intro zenon_H36 ]. % 47.46/47.70 apply (zenon_L7_ zenon_TX_r zenon_TY_q); trivial. % 47.46/47.70 apply (zenon_L9_ zenon_TY_q zenon_TZ_ce zenon_TX_r); trivial. % 47.46/47.70 (* end of lemma zenon_L10_ *) % 47.46/47.70 assert (zenon_L11_ : forall (zenon_TZ_ce : zenon_U) (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U), (~((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TY_q))) -> (~(exists Z : zenon_U, ((ub zenon_TX_r zenon_TY_q Z)/\(lesseq (summation Z) zenon_TZ_ce)))) -> (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)<->(lesseq (summation zenon_TY_q) (summation Y)))) -> False). % 47.46/47.70 do 3 intro. intros zenon_H40 zenon_H3b zenon_H37 zenon_H18 zenon_H3a. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = zenon_TY_q)); [idtac | apply NNPP; zenon_intro zenon_H23]. % 47.46/47.70 congruence. % 47.46/47.70 apply (zenon_L10_ zenon_TZ_ce zenon_TX_r zenon_TY_q); trivial. % 47.46/47.70 (* end of lemma zenon_L11_ *) % 47.46/47.70 assert (zenon_L12_ : forall (zenon_TX_r : zenon_U) (zenon_TY_q : zenon_U) (zenon_TZ_ce : zenon_U), (~(lesseq zenon_TZ_ce (summation zenon_TY_q))) -> (lesseq zenon_TZ_ce (summation (max zenon_TX_r zenon_TY_q))) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)<->(lesseq (summation zenon_TY_q) (summation Y)))) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) -> (~(exists Z : zenon_U, ((ub zenon_TX_r zenon_TY_q Z)/\(lesseq (summation Z) zenon_TZ_ce)))) -> False). % 47.46/47.70 do 3 intro. intros zenon_H41 zenon_H42 zenon_H3a zenon_H18 zenon_H37 zenon_H3b. % 47.46/47.70 cut ((lesseq zenon_TZ_ce (summation (max zenon_TX_r zenon_TY_q))) = (lesseq zenon_TZ_ce (summation zenon_TY_q))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H41. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H42. % 47.46/47.70 cut (((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_H40]. % 47.46/47.70 cut ((zenon_TZ_ce = zenon_TZ_ce)); [idtac | apply NNPP; zenon_intro zenon_H39]. % 47.46/47.70 congruence. % 47.46/47.70 apply zenon_H39. apply refl_equal. % 47.46/47.70 apply (zenon_L11_ zenon_TZ_ce zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 (* end of lemma zenon_L12_ *) % 47.46/47.70 assert (zenon_L13_ : forall (zenon_TZ_ce : zenon_U) (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> (~(lesseq (summation (max zenon_TX_r zenon_TY_q)) (summation zenon_TY_q))) -> (lesseq zenon_TZ_ce (summation (max zenon_TX_r zenon_TY_q))) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)<->(lesseq (summation zenon_TY_q) (summation Y)))) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) -> (~(exists Z : zenon_U, ((ub zenon_TX_r zenon_TY_q Z)/\(lesseq (summation Z) zenon_TZ_ce)))) -> False). % 47.46/47.70 do 3 intro. intros zenon_H43 zenon_H44 zenon_H42 zenon_H3a zenon_H18 zenon_H37 zenon_H3b. % 47.46/47.70 elim (classic (lesseq zenon_TZ_ce (summation zenon_TY_q))); [ zenon_intro zenon_H45 | zenon_intro zenon_H41 ]. % 47.46/47.70 generalize (zenon_H43 (summation (max zenon_TX_r zenon_TY_q))). zenon_intro zenon_H46. % 47.46/47.70 generalize (zenon_H46 zenon_TZ_ce). zenon_intro zenon_H47. % 47.46/47.70 generalize (zenon_H47 (summation zenon_TY_q)). zenon_intro zenon_H48. % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H48); [ zenon_intro zenon_H4a | zenon_intro zenon_H49 ]. % 47.46/47.70 exact (zenon_H4a zenon_H37). % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H49); [ zenon_intro zenon_H41 | zenon_intro zenon_H4b ]. % 47.46/47.70 exact (zenon_H41 zenon_H45). % 47.46/47.70 exact (zenon_H44 zenon_H4b). % 47.46/47.70 apply (zenon_L12_ zenon_TX_r zenon_TY_q zenon_TZ_ce); trivial. % 47.46/47.70 (* end of lemma zenon_L13_ *) % 47.46/47.70 assert (zenon_L14_ : forall (zenon_TX_r : zenon_U) (zenon_TZ_ce : zenon_U) (zenon_TY_q : zenon_U), (~(lesseq (summation zenon_TY_q) zenon_TZ_ce)) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)<->(lesseq (summation zenon_TY_q) (summation Y)))) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) -> (~(exists Z : zenon_U, ((ub zenon_TX_r zenon_TY_q Z)/\(lesseq (summation Z) zenon_TZ_ce)))) -> False). % 47.46/47.70 do 3 intro. intros zenon_H4c zenon_H3a zenon_H18 zenon_H37 zenon_H3b. % 47.46/47.70 cut ((lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) = (lesseq (summation zenon_TY_q) zenon_TZ_ce)). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H4c. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H37. % 47.46/47.70 cut ((zenon_TZ_ce = zenon_TZ_ce)); [idtac | apply NNPP; zenon_intro zenon_H39]. % 47.46/47.70 cut (((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_H40]. % 47.46/47.70 congruence. % 47.46/47.70 apply (zenon_L11_ zenon_TZ_ce zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 apply zenon_H39. apply refl_equal. % 47.46/47.70 (* end of lemma zenon_L14_ *) % 47.46/47.70 assert (zenon_L15_ : forall (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U), (forall Y : zenon_U, (((max zenon_TX_r Y) = zenon_TX_r)\/(~(lesseq Y zenon_TX_r)))) -> (~(zenon_TX_r = (max zenon_TX_r zenon_TY_q))) -> (lesseq zenon_TY_q zenon_TX_r) -> False). % 47.46/47.70 do 2 intro. intros zenon_H1e zenon_H4d zenon_H1d. % 47.46/47.70 generalize (zenon_H1e zenon_TY_q). zenon_intro zenon_H20. % 47.46/47.70 apply (zenon_or_s _ _ zenon_H20); [ zenon_intro zenon_H21 | zenon_intro zenon_H19 ]. % 47.46/47.70 apply zenon_H4d. apply sym_equal. exact zenon_H21. % 47.46/47.70 exact (zenon_H19 zenon_H1d). % 47.46/47.70 (* end of lemma zenon_L15_ *) % 47.46/47.70 assert (zenon_L16_ : forall (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U), (forall Y : zenon_U, (((max zenon_TX_r Y) = Y)\/(~(lesseq zenon_TX_r Y)))) -> (~(zenon_TY_q = (max zenon_TX_r zenon_TY_q))) -> (lesseq zenon_TX_r zenon_TY_q) -> False). % 47.46/47.70 do 2 intro. intros zenon_H24 zenon_H4e zenon_H1c. % 47.46/47.70 generalize (zenon_H24 zenon_TY_q). zenon_intro zenon_H25. % 47.46/47.70 apply (zenon_or_s _ _ zenon_H25); [ zenon_intro zenon_H26 | zenon_intro zenon_H1a ]. % 47.46/47.70 apply zenon_H4e. apply sym_equal. exact zenon_H26. % 47.46/47.70 exact (zenon_H1a zenon_H1c). % 47.46/47.70 (* end of lemma zenon_L16_ *) % 47.46/47.70 assert (zenon_L17_ : forall (zenon_TX_r : zenon_U) (zenon_TY_q : zenon_U), (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (forall Y : zenon_U, (((max zenon_TX_r Y) = zenon_TX_r)\/(~(lesseq Y zenon_TX_r)))) -> (~(zenon_TX_r = (max zenon_TX_r zenon_TY_q))) -> (forall Y : zenon_U, (((max zenon_TX_r Y) = Y)\/(~(lesseq zenon_TX_r Y)))) -> (~(zenon_TY_q = (max zenon_TX_r zenon_TY_q))) -> False). % 47.46/47.70 do 2 intro. intros zenon_H18 zenon_H1e zenon_H4d zenon_H24 zenon_H4e. % 47.46/47.70 generalize (zenon_H18 zenon_TX_r). zenon_intro zenon_H1b. % 47.46/47.70 apply (zenon_or_s _ _ zenon_H1b); [ zenon_intro zenon_H1d | zenon_intro zenon_H1c ]. % 47.46/47.70 apply (zenon_L15_ zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 apply (zenon_L16_ zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 (* end of lemma zenon_L17_ *) % 47.46/47.70 assert (zenon_L18_ : forall (zenon_TX_r : zenon_U) (zenon_TY_q : zenon_U), (~(zenon_TY_q = (max zenon_TX_r zenon_TY_q))) -> (forall Y : zenon_U, (((max zenon_TX_r Y) = Y)\/(~(lesseq zenon_TX_r Y)))) -> (~(zenon_TX_r = (max zenon_TX_r zenon_TY_q))) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> False). % 47.46/47.70 do 2 intro. intros zenon_H4e zenon_H24 zenon_H4d zenon_H18. % 47.46/47.70 generalize (max_1 zenon_TX_r). zenon_intro zenon_H1e. % 47.46/47.70 apply (zenon_L17_ zenon_TX_r zenon_TY_q); trivial. % 47.46/47.70 (* end of lemma zenon_L18_ *) % 47.46/47.70 assert (zenon_L19_ : forall (zenon_TZ_ce : zenon_U) (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U) (zenon_TZ_de : 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_TZ_de (summation (max zenon_TX_r zenon_TY_q)))) -> (lesseq zenon_TZ_de zenon_TZ_ce) -> (forall Z : zenon_U, ((model_max zenon_TX_r zenon_TY_q Z)->(lesseq zenon_TZ_ce Z))) -> False). % 47.46/47.70 do 4 intro. intros zenon_H43 zenon_H4f zenon_H50 zenon_H51. % 47.46/47.70 elim (classic (lesseq zenon_TZ_ce (summation (max zenon_TX_r zenon_TY_q)))); [ zenon_intro zenon_H42 | zenon_intro zenon_H53 ]. % 47.46/47.70 generalize (zenon_H43 zenon_TZ_de). zenon_intro zenon_H54. % 47.46/47.70 generalize (zenon_H54 zenon_TZ_ce). zenon_intro zenon_H55. % 47.46/47.70 generalize (zenon_H55 (summation (max zenon_TX_r zenon_TY_q))). zenon_intro zenon_H56. % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H56); [ zenon_intro zenon_H58 | zenon_intro zenon_H57 ]. % 47.46/47.70 exact (zenon_H58 zenon_H50). % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H57); [ zenon_intro zenon_H53 | zenon_intro zenon_H59 ]. % 47.46/47.70 exact (zenon_H53 zenon_H42). % 47.46/47.70 exact (zenon_H4f zenon_H59). % 47.46/47.70 generalize (zenon_H51 (summation (max zenon_TX_r zenon_TY_q))). zenon_intro zenon_H5a. % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_Hf | zenon_intro zenon_H42 ]. % 47.46/47.70 apply (zenon_L1_ zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 exact (zenon_H53 zenon_H42). % 47.46/47.70 (* end of lemma zenon_L19_ *) % 47.46/47.70 assert (zenon_L20_ : forall (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U) (zenon_TZ_de : zenon_U) (zenon_TZ_ce : 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_TZ_ce zenon_TZ_de)\/(lesseq zenon_TZ_de zenon_TZ_ce)) -> (forall Z : zenon_U, ((model_max zenon_TX_r zenon_TY_q Z)->(lesseq zenon_TZ_ce Z))) -> (~(lesseq zenon_TZ_de (summation (max zenon_TX_r zenon_TY_q)))) -> (~(lesseq zenon_TZ_ce zenon_TZ_de)) -> False). % 47.46/47.70 do 4 intro. intros zenon_H43 zenon_H5b zenon_H51 zenon_H4f zenon_H5c. % 47.46/47.70 apply (zenon_or_s _ _ zenon_H5b); [ zenon_intro zenon_H5d | zenon_intro zenon_H50 ]. % 47.46/47.70 exact (zenon_H5c zenon_H5d). % 47.46/47.70 apply (zenon_L19_ zenon_TZ_ce zenon_TY_q zenon_TX_r zenon_TZ_de); trivial. % 47.46/47.70 (* end of lemma zenon_L20_ *) % 47.46/47.70 assert (zenon_L21_ : forall (zenon_TZ_ce : zenon_U) (zenon_TZ_de : zenon_U) (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U) (zenon_TZ_ds : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> (~(lesseq (summation zenon_TZ_ds) (summation (max zenon_TX_r zenon_TY_q)))) -> (lesseq (summation zenon_TZ_ds) zenon_TZ_de) -> ((lesseq zenon_TZ_ce zenon_TZ_de)\/(lesseq zenon_TZ_de zenon_TZ_ce)) -> (forall Z : zenon_U, ((model_max zenon_TX_r zenon_TY_q Z)->(lesseq zenon_TZ_ce Z))) -> (~(lesseq zenon_TZ_ce zenon_TZ_de)) -> False). % 47.46/47.70 do 5 intro. intros zenon_H43 zenon_H5e zenon_H5f zenon_H5b zenon_H51 zenon_H5c. % 47.46/47.70 elim (classic (lesseq zenon_TZ_de (summation (max zenon_TX_r zenon_TY_q)))); [ zenon_intro zenon_H59 | zenon_intro zenon_H4f ]. % 47.46/47.70 generalize (zenon_H43 (summation zenon_TZ_ds)). zenon_intro zenon_H61. % 47.46/47.70 generalize (zenon_H61 zenon_TZ_de). zenon_intro zenon_H62. % 47.46/47.70 generalize (zenon_H62 (summation (max zenon_TX_r zenon_TY_q))). zenon_intro zenon_H63. % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H63); [ zenon_intro zenon_H65 | zenon_intro zenon_H64 ]. % 47.46/47.70 exact (zenon_H65 zenon_H5f). % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H64); [ zenon_intro zenon_H4f | zenon_intro zenon_H66 ]. % 47.46/47.70 exact (zenon_H4f zenon_H59). % 47.46/47.70 exact (zenon_H5e zenon_H66). % 47.46/47.70 apply (zenon_L20_ zenon_TY_q zenon_TX_r zenon_TZ_de zenon_TZ_ce); trivial. % 47.46/47.70 (* end of lemma zenon_L21_ *) % 47.46/47.70 assert (zenon_L22_ : forall (zenon_TZ_de : zenon_U) (zenon_TZ_ce : zenon_U) (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U) (zenon_TZ_ds : 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_TZ_ds zenon_TX_r)) -> (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) -> ((lesseq zenon_TZ_ce zenon_TZ_de)\/(lesseq zenon_TZ_de zenon_TZ_ce)) -> (forall Z : zenon_U, ((model_max zenon_TX_r zenon_TY_q Z)->(lesseq zenon_TZ_ce Z))) -> (~(lesseq zenon_TZ_ce zenon_TZ_de)) -> (lesseq (summation zenon_TZ_ds) zenon_TZ_de) -> (~(lesseq zenon_TX_r zenon_TY_q)) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (forall Y : zenon_U, ((lesseq zenon_TZ_ds Y)<->(lesseq (summation zenon_TZ_ds) (summation Y)))) -> False). % 47.46/47.70 do 5 intro. intros zenon_H43 zenon_H67 zenon_H37 zenon_H5b zenon_H51 zenon_H5c zenon_H5f zenon_H1a zenon_H18 zenon_H68. % 47.46/47.70 generalize (zenon_H51 (summation (max zenon_TX_r zenon_TY_q))). zenon_intro zenon_H5a. % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_Hf | zenon_intro zenon_H42 ]. % 47.46/47.70 apply (zenon_L1_ zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 generalize (max_1 zenon_TX_r). zenon_intro zenon_H1e. % 47.46/47.70 generalize (zenon_H68 zenon_TX_r). zenon_intro zenon_H69. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_H69); [ zenon_intro zenon_H67; zenon_intro zenon_H6c | zenon_intro zenon_H6b; zenon_intro zenon_H6a ]. % 47.46/47.70 elim (classic ((~((summation zenon_TZ_ds) = zenon_TZ_ce))/\(~(lesseq (summation zenon_TZ_ds) zenon_TZ_ce)))); [ zenon_intro zenon_H6d | zenon_intro zenon_H6e ]. % 47.46/47.70 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 47.46/47.70 elim (classic ((~((summation zenon_TZ_ds) = (summation (max zenon_TX_r zenon_TY_q))))/\(~(lesseq (summation zenon_TZ_ds) (summation (max zenon_TX_r zenon_TY_q)))))); [ zenon_intro zenon_H71 | zenon_intro zenon_H72 ]. % 47.46/47.70 apply (zenon_and_s _ _ zenon_H71). zenon_intro zenon_H73. zenon_intro zenon_H5e. % 47.46/47.70 apply (zenon_L21_ zenon_TZ_ce zenon_TZ_de zenon_TY_q zenon_TX_r zenon_TZ_ds); trivial. % 47.46/47.70 cut ((lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) = (lesseq (summation zenon_TZ_ds) zenon_TZ_ce)). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H6f. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H37. % 47.46/47.70 cut ((zenon_TZ_ce = zenon_TZ_ce)); [idtac | apply NNPP; zenon_intro zenon_H39]. % 47.46/47.70 cut (((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TZ_ds))); [idtac | apply NNPP; zenon_intro zenon_H74]. % 47.46/47.70 congruence. % 47.46/47.70 apply (zenon_notand_s _ _ zenon_H72); [ zenon_intro zenon_H76 | zenon_intro zenon_H75 ]. % 47.46/47.70 apply zenon_H76. zenon_intro zenon_H77. % 47.46/47.70 elim (classic ((summation zenon_TZ_ds) = (summation zenon_TZ_ds))); [ zenon_intro zenon_H78 | zenon_intro zenon_H79 ]. % 47.46/47.70 cut (((summation zenon_TZ_ds) = (summation zenon_TZ_ds)) = ((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TZ_ds))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H74. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H78. % 47.46/47.70 cut (((summation zenon_TZ_ds) = (summation zenon_TZ_ds))); [idtac | apply NNPP; zenon_intro zenon_H79]. % 47.46/47.70 cut (((summation zenon_TZ_ds) = (summation (max zenon_TX_r zenon_TY_q)))); [idtac | apply NNPP; zenon_intro zenon_H73]. % 47.46/47.70 congruence. % 47.46/47.70 exact (zenon_H73 zenon_H77). % 47.46/47.70 apply zenon_H79. apply refl_equal. % 47.46/47.70 apply zenon_H79. apply refl_equal. % 47.46/47.70 apply zenon_H75. zenon_intro zenon_H66. % 47.46/47.70 generalize (zenon_H43 (summation zenon_TZ_ds)). zenon_intro zenon_H61. % 47.46/47.70 generalize (zenon_H61 (summation (max zenon_TX_r zenon_TY_q))). zenon_intro zenon_H7a. % 47.46/47.70 generalize (zenon_H7a zenon_TZ_ce). zenon_intro zenon_H7b. % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H7b); [ zenon_intro zenon_H5e | zenon_intro zenon_H7c ]. % 47.46/47.70 exact (zenon_H5e zenon_H66). % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H7c); [ zenon_intro zenon_H4a | zenon_intro zenon_H7d ]. % 47.46/47.70 exact (zenon_H4a zenon_H37). % 47.46/47.70 exact (zenon_H6f zenon_H7d). % 47.46/47.70 apply zenon_H39. apply refl_equal. % 47.46/47.70 elim (classic ((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TX_r))); [ zenon_intro zenon_H7e | zenon_intro zenon_H22 ]. % 47.46/47.70 cut ((lesseq zenon_TZ_ce (summation (max zenon_TX_r zenon_TY_q))) = (lesseq (summation zenon_TZ_ds) (summation zenon_TX_r))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H6c. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H42. % 47.46/47.70 cut (((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TX_r))); [idtac | apply NNPP; zenon_intro zenon_H22]. % 47.46/47.70 cut ((zenon_TZ_ce = (summation zenon_TZ_ds))); [idtac | apply NNPP; zenon_intro zenon_H7f]. % 47.46/47.70 congruence. % 47.46/47.70 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_H81 | zenon_intro zenon_H80 ]. % 47.46/47.70 apply zenon_H81. zenon_intro zenon_H82. % 47.46/47.70 elim (classic ((summation zenon_TZ_ds) = (summation zenon_TZ_ds))); [ zenon_intro zenon_H78 | zenon_intro zenon_H79 ]. % 47.46/47.70 cut (((summation zenon_TZ_ds) = (summation zenon_TZ_ds)) = (zenon_TZ_ce = (summation zenon_TZ_ds))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H7f. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H78. % 47.46/47.70 cut (((summation zenon_TZ_ds) = (summation zenon_TZ_ds))); [idtac | apply NNPP; zenon_intro zenon_H79]. % 47.46/47.70 cut (((summation zenon_TZ_ds) = zenon_TZ_ce)); [idtac | apply NNPP; zenon_intro zenon_H70]. % 47.46/47.70 congruence. % 47.46/47.70 exact (zenon_H70 zenon_H82). % 47.46/47.70 apply zenon_H79. apply refl_equal. % 47.46/47.70 apply zenon_H79. apply refl_equal. % 47.46/47.70 apply zenon_H80. zenon_intro zenon_H7d. % 47.46/47.70 generalize (zenon_H43 (summation zenon_TZ_ds)). zenon_intro zenon_H61. % 47.46/47.70 generalize (zenon_H61 zenon_TZ_ce). zenon_intro zenon_H83. % 47.46/47.70 generalize (zenon_H83 (summation (max zenon_TX_r zenon_TY_q))). zenon_intro zenon_H84. % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H84); [ zenon_intro zenon_H6f | zenon_intro zenon_H85 ]. % 47.46/47.70 exact (zenon_H6f zenon_H7d). % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H85); [ zenon_intro zenon_H53 | zenon_intro zenon_H66 ]. % 47.46/47.70 exact (zenon_H53 zenon_H42). % 47.46/47.70 cut ((lesseq (summation zenon_TZ_ds) (summation (max zenon_TX_r zenon_TY_q))) = (lesseq (summation zenon_TZ_ds) (summation zenon_TX_r))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H6c. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H66. % 47.46/47.70 cut (((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TX_r))); [idtac | apply NNPP; zenon_intro zenon_H22]. % 47.46/47.70 cut (((summation zenon_TZ_ds) = (summation zenon_TZ_ds))); [idtac | apply NNPP; zenon_intro zenon_H79]. % 47.46/47.70 congruence. % 47.46/47.70 apply zenon_H79. apply refl_equal. % 47.46/47.70 exact (zenon_H22 zenon_H7e). % 47.46/47.70 exact (zenon_H22 zenon_H7e). % 47.46/47.70 apply (zenon_L4_ zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 exact (zenon_H67 zenon_H6b). % 47.46/47.70 (* end of lemma zenon_L22_ *) % 47.46/47.70 assert (zenon_L23_ : forall (zenon_TZ_de : zenon_U) (zenon_TZ_ce : zenon_U) (zenon_TZ_ds : zenon_U) (zenon_TY_q : zenon_U) (zenon_TX_r : 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, (((max zenon_TX_r Y) = Y)\/(~(lesseq zenon_TX_r Y)))) -> (~(zenon_TY_q = (max zenon_TX_r zenon_TY_q))) -> (~(lesseq zenon_TZ_ds zenon_TX_r)) -> (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) -> ((lesseq zenon_TZ_ce zenon_TZ_de)\/(lesseq zenon_TZ_de zenon_TZ_ce)) -> (forall Z : zenon_U, ((model_max zenon_TX_r zenon_TY_q Z)->(lesseq zenon_TZ_ce Z))) -> (~(lesseq zenon_TZ_ce zenon_TZ_de)) -> (lesseq (summation zenon_TZ_ds) zenon_TZ_de) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (forall Y : zenon_U, ((lesseq zenon_TZ_ds Y)<->(lesseq (summation zenon_TZ_ds) (summation Y)))) -> False). % 47.46/47.70 do 5 intro. intros zenon_H43 zenon_H24 zenon_H4e zenon_H67 zenon_H37 zenon_H5b zenon_H51 zenon_H5c zenon_H5f zenon_H18 zenon_H68. % 47.46/47.70 generalize (zenon_H24 zenon_TY_q). zenon_intro zenon_H25. % 47.46/47.70 apply (zenon_or_s _ _ zenon_H25); [ zenon_intro zenon_H26 | zenon_intro zenon_H1a ]. % 47.46/47.70 apply zenon_H4e. apply sym_equal. exact zenon_H26. % 47.46/47.70 apply (zenon_L22_ zenon_TZ_de zenon_TZ_ce zenon_TY_q zenon_TX_r zenon_TZ_ds); trivial. % 47.46/47.70 (* end of lemma zenon_L23_ *) % 47.46/47.70 assert (zenon_L24_ : forall (zenon_TZ_de : zenon_U) (zenon_TZ_ce : zenon_U) (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U) (zenon_TZ_ds : 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, (((max zenon_TZ_ds Y) = Y)\/(~(lesseq zenon_TZ_ds Y)))) -> (~(zenon_TX_r = (max zenon_TZ_ds zenon_TX_r))) -> (forall Y : zenon_U, (((max zenon_TX_r Y) = Y)\/(~(lesseq zenon_TX_r Y)))) -> (~(zenon_TY_q = (max zenon_TX_r zenon_TY_q))) -> (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) -> ((lesseq zenon_TZ_ce zenon_TZ_de)\/(lesseq zenon_TZ_de zenon_TZ_ce)) -> (forall Z : zenon_U, ((model_max zenon_TX_r zenon_TY_q Z)->(lesseq zenon_TZ_ce Z))) -> (~(lesseq zenon_TZ_ce zenon_TZ_de)) -> (lesseq (summation zenon_TZ_ds) zenon_TZ_de) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (forall Y : zenon_U, ((lesseq zenon_TZ_ds Y)<->(lesseq (summation zenon_TZ_ds) (summation Y)))) -> False). % 47.46/47.70 do 5 intro. intros zenon_H43 zenon_H86 zenon_H87 zenon_H24 zenon_H4e zenon_H37 zenon_H5b zenon_H51 zenon_H5c zenon_H5f zenon_H18 zenon_H68. % 47.46/47.70 generalize (zenon_H86 zenon_TX_r). zenon_intro zenon_H88. % 47.46/47.70 apply (zenon_or_s _ _ zenon_H88); [ zenon_intro zenon_H89 | zenon_intro zenon_H67 ]. % 47.46/47.70 apply zenon_H87. apply sym_equal. exact zenon_H89. % 47.46/47.70 apply (zenon_L23_ zenon_TZ_de zenon_TZ_ce zenon_TZ_ds zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 (* end of lemma zenon_L24_ *) % 47.46/47.70 assert (zenon_L25_ : forall (zenon_TX_r : zenon_U) (zenon_TZ_de : zenon_U) (zenon_TY_q : zenon_U) (zenon_TZ_ds : zenon_U) (zenon_TZ_ce : 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_ce Y)\/(lesseq Y zenon_TZ_ce))) -> (forall Y : zenon_U, ((lesseq zenon_TZ_ds Y)<->(lesseq (summation zenon_TZ_ds) (summation Y)))) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (lesseq (summation zenon_TZ_ds) zenon_TZ_de) -> (~(lesseq zenon_TZ_ce zenon_TZ_de)) -> (forall Z : zenon_U, ((model_max zenon_TX_r zenon_TY_q Z)->(lesseq zenon_TZ_ce Z))) -> (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) -> (~(zenon_TY_q = (max zenon_TX_r zenon_TY_q))) -> (forall Y : zenon_U, (((max zenon_TX_r Y) = Y)\/(~(lesseq zenon_TX_r Y)))) -> (~(zenon_TX_r = (max zenon_TZ_ds zenon_TX_r))) -> (forall Y : zenon_U, (((max zenon_TZ_ds Y) = Y)\/(~(lesseq zenon_TZ_ds Y)))) -> False). % 47.46/47.70 do 5 intro. intros zenon_H43 zenon_H8a zenon_H68 zenon_H18 zenon_H5f zenon_H5c zenon_H51 zenon_H37 zenon_H4e zenon_H24 zenon_H87 zenon_H86. % 47.46/47.70 generalize (zenon_H8a zenon_TZ_de). zenon_intro zenon_H5b. % 47.46/47.70 apply (zenon_L24_ zenon_TZ_de zenon_TZ_ce zenon_TY_q zenon_TX_r zenon_TZ_ds); trivial. % 47.46/47.70 (* end of lemma zenon_L25_ *) % 47.46/47.70 assert (zenon_L26_ : forall (zenon_TX_r : zenon_U) (zenon_TZ_de : zenon_U) (zenon_TY_q : zenon_U) (zenon_TZ_ds : zenon_U) (zenon_TZ_ce : 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_ce Y)\/(lesseq Y zenon_TZ_ce))) -> (forall Y : zenon_U, ((lesseq zenon_TZ_ds Y)<->(lesseq (summation zenon_TZ_ds) (summation Y)))) -> (forall Y : zenon_U, ((lesseq zenon_TY_q Y)\/(lesseq Y zenon_TY_q))) -> (lesseq (summation zenon_TZ_ds) zenon_TZ_de) -> (~(lesseq zenon_TZ_ce zenon_TZ_de)) -> (forall Z : zenon_U, ((model_max zenon_TX_r zenon_TY_q Z)->(lesseq zenon_TZ_ce Z))) -> (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) -> (~(lesseq zenon_TZ_ds zenon_TX_r)) -> (~(zenon_TY_q = (max zenon_TX_r zenon_TY_q))) -> (forall Y : zenon_U, (((max zenon_TX_r Y) = Y)\/(~(lesseq zenon_TX_r Y)))) -> False). % 47.46/47.70 do 5 intro. intros zenon_H43 zenon_H8a zenon_H68 zenon_H18 zenon_H5f zenon_H5c zenon_H51 zenon_H37 zenon_H67 zenon_H4e zenon_H24. % 47.46/47.70 generalize (zenon_H8a zenon_TZ_de). zenon_intro zenon_H5b. % 47.46/47.70 apply (zenon_L23_ zenon_TZ_de zenon_TZ_ce zenon_TZ_ds zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 (* end of lemma zenon_L26_ *) % 47.46/47.70 assert (zenon_L27_ : forall (zenon_TZ_de : zenon_U) (zenon_TZ_ce : zenon_U) (zenon_TZ_ds : zenon_U) (zenon_TX_r : zenon_U) (zenon_TY_q : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((lesseq x y)->((lesseq y z)->(lesseq x z)))))) -> (~((summation zenon_TY_q) = (summation (max zenon_TX_r zenon_TY_q)))) -> (~(zenon_TZ_ds = (max zenon_TX_r zenon_TY_q))) -> (lesseq zenon_TX_r zenon_TZ_ds) -> (lesseq zenon_TY_q zenon_TZ_ds) -> (forall Y : zenon_U, ((lesseq zenon_TZ_ce Y)\/(lesseq Y zenon_TZ_ce))) -> (lesseq (summation zenon_TZ_ds) zenon_TZ_de) -> (~(lesseq zenon_TZ_ce zenon_TZ_de)) -> (forall Z : zenon_U, ((model_max zenon_TX_r zenon_TY_q Z)->(lesseq zenon_TZ_ce Z))) -> (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) -> (forall Y : zenon_U, (((max zenon_TY_q Y) = Y)\/(~(lesseq zenon_TY_q Y)))) -> (forall Y : zenon_U, (((max zenon_TZ_ds Y) = zenon_TZ_ds)\/(~(lesseq Y zenon_TZ_ds)))) -> False). % 47.46/47.70 do 5 intro. intros zenon_H43 zenon_H8b zenon_H8c zenon_H8d zenon_H8e zenon_H8a zenon_H5f zenon_H5c zenon_H51 zenon_H37 zenon_H8f zenon_H90. % 47.46/47.70 cut ((zenon_TY_q = (max zenon_TX_r zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_H4e]. % 47.46/47.70 congruence. % 47.46/47.70 generalize (lesseq_total zenon_TY_q). zenon_intro zenon_H18. % 47.46/47.70 generalize (zenon_H90 zenon_TZ_ds). zenon_intro zenon_H91. % 47.46/47.70 apply (zenon_or_s _ _ zenon_H91); [ zenon_intro zenon_H93 | zenon_intro zenon_H92 ]. % 47.46/47.70 elim (classic ((max zenon_TX_r zenon_TY_q) = (max zenon_TX_r zenon_TY_q))); [ zenon_intro zenon_H94 | zenon_intro zenon_H95 ]. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = (max zenon_TX_r zenon_TY_q)) = (zenon_TZ_ds = (max zenon_TX_r zenon_TY_q))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H8c. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H94. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = (max zenon_TX_r zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_H95]. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = zenon_TZ_ds)); [idtac | apply NNPP; zenon_intro zenon_H96]. % 47.46/47.70 congruence. % 47.46/47.70 cut (((max zenon_TZ_ds zenon_TZ_ds) = zenon_TZ_ds) = ((max zenon_TX_r zenon_TY_q) = zenon_TZ_ds)). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H96. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H93. % 47.46/47.70 cut ((zenon_TZ_ds = zenon_TZ_ds)); [idtac | apply NNPP; zenon_intro zenon_H97]. % 47.46/47.70 cut (((max zenon_TZ_ds zenon_TZ_ds) = (max zenon_TX_r zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_H98]. % 47.46/47.70 congruence. % 47.46/47.70 elim (classic ((max zenon_TX_r zenon_TY_q) = (max zenon_TX_r zenon_TY_q))); [ zenon_intro zenon_H94 | zenon_intro zenon_H95 ]. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = (max zenon_TX_r zenon_TY_q)) = ((max zenon_TZ_ds zenon_TZ_ds) = (max zenon_TX_r zenon_TY_q))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H98. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H94. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = (max zenon_TX_r zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_H95]. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = (max zenon_TZ_ds zenon_TZ_ds))); [idtac | apply NNPP; zenon_intro zenon_H99]. % 47.46/47.70 congruence. % 47.46/47.70 generalize (summation_monotone zenon_TZ_ds). zenon_intro zenon_H68. % 47.46/47.70 generalize (max_2 zenon_TX_r). zenon_intro zenon_H24. % 47.46/47.70 generalize (zenon_H90 zenon_TX_r). zenon_intro zenon_H9a. % 47.46/47.70 apply (zenon_or_s _ _ zenon_H9a); [ zenon_intro zenon_H9c | zenon_intro zenon_H9b ]. % 47.46/47.70 cut (((max zenon_TZ_ds zenon_TX_r) = zenon_TZ_ds) = ((max zenon_TX_r zenon_TY_q) = (max zenon_TZ_ds zenon_TZ_ds))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H99. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H9c. % 47.46/47.70 cut ((zenon_TZ_ds = (max zenon_TZ_ds zenon_TZ_ds))); [idtac | apply NNPP; zenon_intro zenon_H9d]. % 47.46/47.70 cut (((max zenon_TZ_ds zenon_TX_r) = (max zenon_TX_r zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_H9e]. % 47.46/47.70 congruence. % 47.46/47.70 elim (classic ((max zenon_TX_r zenon_TY_q) = (max zenon_TX_r zenon_TY_q))); [ zenon_intro zenon_H94 | zenon_intro zenon_H95 ]. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = (max zenon_TX_r zenon_TY_q)) = ((max zenon_TZ_ds zenon_TX_r) = (max zenon_TX_r zenon_TY_q))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H9e. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H94. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = (max zenon_TX_r zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_H95]. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = (max zenon_TZ_ds zenon_TX_r))); [idtac | apply NNPP; zenon_intro zenon_H9f]. % 47.46/47.70 congruence. % 47.46/47.70 generalize (max_2 zenon_TZ_ds). zenon_intro zenon_H86. % 47.46/47.70 generalize (zenon_H8f zenon_TX_r). zenon_intro zenon_Ha0. % 47.46/47.70 apply (zenon_or_s _ _ zenon_Ha0); [ zenon_intro zenon_Ha1 | zenon_intro zenon_H19 ]. % 47.46/47.70 cut (((max zenon_TY_q zenon_TX_r) = zenon_TX_r) = ((max zenon_TX_r zenon_TY_q) = (max zenon_TZ_ds zenon_TX_r))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H9f. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_Ha1. % 47.46/47.70 cut ((zenon_TX_r = (max zenon_TZ_ds zenon_TX_r))); [idtac | apply NNPP; zenon_intro zenon_H87]. % 47.46/47.70 cut (((max zenon_TY_q zenon_TX_r) = (max zenon_TX_r zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_Ha2]. % 47.46/47.70 congruence. % 47.46/47.70 elim (classic ((max zenon_TX_r zenon_TY_q) = (max zenon_TX_r zenon_TY_q))); [ zenon_intro zenon_H94 | zenon_intro zenon_H95 ]. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = (max zenon_TX_r zenon_TY_q)) = ((max zenon_TY_q zenon_TX_r) = (max zenon_TX_r zenon_TY_q))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_Ha2. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H94. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = (max zenon_TX_r zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_H95]. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = (max zenon_TY_q zenon_TX_r))); [idtac | apply NNPP; zenon_intro zenon_Ha3]. % 47.46/47.70 congruence. % 47.46/47.70 elim (classic ((max zenon_TY_q zenon_TX_r) = (max zenon_TY_q zenon_TX_r))); [ zenon_intro zenon_Ha4 | zenon_intro zenon_Ha5 ]. % 47.46/47.70 cut (((max zenon_TY_q zenon_TX_r) = (max zenon_TY_q zenon_TX_r)) = ((max zenon_TX_r zenon_TY_q) = (max zenon_TY_q zenon_TX_r))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_Ha3. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_Ha4. % 47.46/47.70 cut (((max zenon_TY_q zenon_TX_r) = (max zenon_TY_q zenon_TX_r))); [idtac | apply NNPP; zenon_intro zenon_Ha5]. % 47.46/47.70 cut (((max zenon_TY_q zenon_TX_r) = (max zenon_TX_r zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_Ha2]. % 47.46/47.70 congruence. % 47.46/47.70 cut (((max zenon_TY_q zenon_TX_r) = zenon_TX_r) = ((max zenon_TY_q zenon_TX_r) = (max zenon_TX_r zenon_TY_q))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_Ha2. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_Ha1. % 47.46/47.70 cut ((zenon_TX_r = (max zenon_TX_r zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_H4d]. % 47.46/47.70 cut (((max zenon_TY_q zenon_TX_r) = (max zenon_TY_q zenon_TX_r))); [idtac | apply NNPP; zenon_intro zenon_Ha5]. % 47.46/47.70 congruence. % 47.46/47.70 apply zenon_Ha5. apply refl_equal. % 47.46/47.70 apply (zenon_L18_ zenon_TX_r zenon_TY_q); trivial. % 47.46/47.70 apply zenon_Ha5. apply refl_equal. % 47.46/47.70 apply zenon_Ha5. apply refl_equal. % 47.46/47.70 apply zenon_H95. apply refl_equal. % 47.46/47.70 apply zenon_H95. apply refl_equal. % 47.46/47.70 apply (zenon_L25_ zenon_TX_r zenon_TZ_de zenon_TY_q zenon_TZ_ds zenon_TZ_ce); trivial. % 47.46/47.70 elim (classic (lesseq zenon_TZ_ds zenon_TX_r)); [ zenon_intro zenon_H6b | zenon_intro zenon_H67 ]. % 47.46/47.70 generalize (zenon_H43 zenon_TY_q). zenon_intro zenon_Ha6. % 47.46/47.70 generalize (zenon_Ha6 zenon_TZ_ds). zenon_intro zenon_Ha7. % 47.46/47.70 generalize (zenon_Ha7 zenon_TX_r). zenon_intro zenon_Ha8. % 47.46/47.70 apply (zenon_imply_s _ _ zenon_Ha8); [ zenon_intro zenon_Haa | zenon_intro zenon_Ha9 ]. % 47.46/47.70 exact (zenon_Haa zenon_H8e). % 47.46/47.70 apply (zenon_imply_s _ _ zenon_Ha9); [ zenon_intro zenon_H67 | zenon_intro zenon_H1d ]. % 47.46/47.70 exact (zenon_H67 zenon_H6b). % 47.46/47.70 exact (zenon_H19 zenon_H1d). % 47.46/47.70 apply (zenon_L26_ zenon_TX_r zenon_TZ_de zenon_TY_q zenon_TZ_ds zenon_TZ_ce); trivial. % 47.46/47.70 apply zenon_H95. apply refl_equal. % 47.46/47.70 apply zenon_H95. apply refl_equal. % 47.46/47.70 apply zenon_H9d. apply sym_equal. exact zenon_H93. % 47.46/47.70 exact (zenon_H9b zenon_H8d). % 47.46/47.70 apply zenon_H95. apply refl_equal. % 47.46/47.70 apply zenon_H95. apply refl_equal. % 47.46/47.70 apply zenon_H97. apply refl_equal. % 47.46/47.70 apply zenon_H95. apply refl_equal. % 47.46/47.70 apply zenon_H95. apply refl_equal. % 47.46/47.70 generalize (lesseq_ref zenon_TZ_ds). zenon_intro zenon_Hab. % 47.46/47.70 exact (zenon_H92 zenon_Hab). % 47.46/47.70 (* end of lemma zenon_L27_ *) % 47.46/47.70 assert (zenon_L28_ : forall (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U), (~((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TX_r))) -> ((max zenon_TX_r zenon_TY_q) = zenon_TX_r) -> False). % 47.46/47.70 do 2 intro. intros zenon_H22 zenon_H21. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = zenon_TX_r)); [idtac | apply NNPP; zenon_intro zenon_H1f]. % 47.46/47.70 congruence. % 47.46/47.70 exact (zenon_H1f zenon_H21). % 47.46/47.70 (* end of lemma zenon_L28_ *) % 47.46/47.70 assert (zenon_L29_ : forall (zenon_TZ_gs : zenon_U) (zenon_TY_q : zenon_U) (zenon_TX_r : zenon_U), (forall Y : zenon_U, (((max zenon_TX_r Y) = Y)\/(~(lesseq zenon_TX_r Y)))) -> (lesseq zenon_TX_r zenon_TY_q) -> (~(exists Z : zenon_U, ((ub zenon_TX_r zenon_TY_q Z)/\(lesseq (summation Z) zenon_TZ_gs)))) -> (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_gs) -> False). % 47.46/47.70 do 3 intro. intros zenon_H24 zenon_H1c zenon_Hac zenon_Had. % 47.46/47.70 generalize (zenon_H24 zenon_TY_q). zenon_intro zenon_H25. % 47.46/47.70 apply (zenon_or_s _ _ zenon_H25); [ zenon_intro zenon_H26 | zenon_intro zenon_H1a ]. % 47.46/47.70 generalize (summation_monotone (summation zenon_TY_q)). zenon_intro zenon_Haf. % 47.46/47.70 generalize (zenon_Haf zenon_TZ_gs). zenon_intro zenon_Hb0. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_Hb0); [ zenon_intro zenon_Hb4; zenon_intro zenon_Hb3 | zenon_intro zenon_Hb2; zenon_intro zenon_Hb1 ]. % 47.46/47.70 cut ((lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_gs) = (lesseq (summation zenon_TY_q) zenon_TZ_gs)). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_Hb4. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_Had. % 47.46/47.70 cut ((zenon_TZ_gs = zenon_TZ_gs)); [idtac | apply NNPP; zenon_intro zenon_Hb5]. % 47.46/47.70 cut (((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_H40]. % 47.46/47.70 congruence. % 47.46/47.70 cut (((max zenon_TX_r zenon_TY_q) = zenon_TY_q)); [idtac | apply NNPP; zenon_intro zenon_H23]. % 47.46/47.70 congruence. % 47.46/47.70 exact (zenon_H23 zenon_H26). % 47.46/47.70 apply zenon_Hb5. apply refl_equal. % 47.46/47.70 apply zenon_Hac. exists zenon_TY_q. apply NNPP. zenon_intro zenon_Hb6. % 47.46/47.70 apply (zenon_notand_s _ _ zenon_Hb6); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb4 ]. % 47.46/47.70 generalize (ub zenon_TX_r). zenon_intro zenon_H2a. % 47.46/47.70 generalize (zenon_H2a zenon_TY_q). zenon_intro zenon_H2b. % 47.46/47.70 generalize (zenon_H2b zenon_TY_q). zenon_intro zenon_Hb8. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_Hb8); [ zenon_intro zenon_Hb7; zenon_intro zenon_Hbb | zenon_intro zenon_Hba; zenon_intro zenon_Hb9 ]. % 47.46/47.70 apply (zenon_notand_s _ _ zenon_Hbb); [ zenon_intro zenon_H1a | zenon_intro zenon_Hbc ]. % 47.46/47.70 exact (zenon_H1a zenon_H1c). % 47.46/47.70 generalize (lesseq_ref zenon_TY_q). zenon_intro zenon_Hbd. % 47.46/47.70 exact (zenon_Hbc zenon_Hbd). % 47.46/47.70 exact (zenon_Hb7 zenon_Hba). % 47.46/47.70 exact (zenon_Hb4 zenon_Hb2). % 47.46/47.70 exact (zenon_H1a zenon_H1c). % 47.46/47.70 (* end of lemma zenon_L29_ *) % 47.46/47.70 apply NNPP. intro zenon_G. % 47.46/47.70 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_H43 | zenon_intro zenon_Hbe ]. % 47.46/47.70 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_Hbf; idtac ]. % 47.46/47.70 elim zenon_Hbf. zenon_intro zenon_TX_r. zenon_intro zenon_Hc0. % 47.46/47.70 apply (zenon_notallex_s (fun Y : zenon_U => (forall Z : zenon_U, ((minsol_model_ub zenon_TX_r Y Z)<->(minsol_model_max zenon_TX_r Y Z)))) zenon_Hc0); [ zenon_intro zenon_Hc1; idtac ]. % 47.46/47.70 elim zenon_Hc1. zenon_intro zenon_TY_q. zenon_intro zenon_Hc2. % 47.46/47.70 apply (zenon_notallex_s (fun Z : zenon_U => ((minsol_model_ub zenon_TX_r zenon_TY_q Z)<->(minsol_model_max zenon_TX_r zenon_TY_q Z))) zenon_Hc2); [ zenon_intro zenon_Hc3; idtac ]. % 47.46/47.70 elim zenon_Hc3. zenon_intro zenon_TZ_ce. zenon_intro zenon_Hc4. % 47.46/47.70 apply (zenon_notequiv_s _ _ zenon_Hc4); [ zenon_intro zenon_Hc8; zenon_intro zenon_Hc7 | zenon_intro zenon_Hc6; zenon_intro zenon_Hc5 ]. % 47.46/47.70 generalize (minsol_model_ub zenon_TX_r). zenon_intro zenon_Hc9. % 47.46/47.70 generalize (zenon_Hc9 zenon_TY_q). zenon_intro zenon_Hca. % 47.46/47.70 generalize (zenon_Hca zenon_TZ_ce). zenon_intro zenon_Hcb. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_Hcb); [ zenon_intro zenon_Hc8; zenon_intro zenon_Hcd | zenon_intro zenon_Hc6; zenon_intro zenon_Hcc ]. % 47.46/47.70 generalize (minsol_model_max zenon_TX_r). zenon_intro zenon_Hce. % 47.46/47.70 generalize (zenon_Hce zenon_TY_q). zenon_intro zenon_Hcf. % 47.46/47.70 generalize (zenon_Hcf zenon_TZ_ce). zenon_intro zenon_Hd0. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_Hd0); [ zenon_intro zenon_Hc5; zenon_intro zenon_Hd2 | zenon_intro zenon_Hc7; zenon_intro zenon_Hd1 ]. % 47.46/47.70 exact (zenon_Hc5 zenon_Hc7). % 47.46/47.70 apply (zenon_and_s _ _ zenon_Hd1). zenon_intro zenon_Hd3. zenon_intro zenon_H51. % 47.46/47.70 generalize (model_max_3 zenon_TX_r). zenon_intro zenon_H12. % 47.46/47.70 generalize (zenon_H12 zenon_TY_q). zenon_intro zenon_H13. % 47.46/47.70 generalize (zenon_H13 zenon_TZ_ce). zenon_intro zenon_Hd4. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_Hd4); [ zenon_intro zenon_Hd5; zenon_intro zenon_H4a | zenon_intro zenon_Hd3; zenon_intro zenon_H37 ]. % 47.46/47.70 exact (zenon_Hd5 zenon_Hd3). % 47.46/47.70 apply (zenon_notand_s _ _ zenon_Hcd); [ zenon_intro zenon_Hd7 | zenon_intro zenon_Hd6 ]. % 47.46/47.70 generalize (model_ub_3 zenon_TX_r). zenon_intro zenon_Hd8. % 47.46/47.70 generalize (zenon_Hd8 zenon_TY_q). zenon_intro zenon_Hd9. % 47.46/47.70 generalize (zenon_Hd9 zenon_TZ_ce). zenon_intro zenon_Hda. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_Hda); [ zenon_intro zenon_Hd7; zenon_intro zenon_H3b | zenon_intro zenon_Hdc; zenon_intro zenon_Hdb ]. % 47.46/47.70 generalize (zenon_H51 (summation (max zenon_TX_r zenon_TY_q))). zenon_intro zenon_H5a. % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_Hf | zenon_intro zenon_H42 ]. % 47.46/47.70 apply (zenon_L1_ zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 generalize (lesseq_total zenon_TY_q). zenon_intro zenon_H18. % 47.46/47.70 generalize (summation_monotone zenon_TY_q). zenon_intro zenon_H3a. % 47.46/47.70 apply zenon_H3b. exists zenon_TY_q. apply NNPP. zenon_intro zenon_Hdd. % 47.46/47.70 apply (zenon_notand_s _ _ zenon_Hdd); [ zenon_intro zenon_Hb7 | zenon_intro zenon_H4c ]. % 47.46/47.70 generalize (ub zenon_TX_r). zenon_intro zenon_H2a. % 47.46/47.70 generalize (zenon_H2a zenon_TY_q). zenon_intro zenon_H2b. % 47.46/47.70 generalize (zenon_H2b zenon_TY_q). zenon_intro zenon_Hb8. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_Hb8); [ zenon_intro zenon_Hb7; zenon_intro zenon_Hbb | zenon_intro zenon_Hba; zenon_intro zenon_Hb9 ]. % 47.46/47.70 apply (zenon_notand_s _ _ zenon_Hbb); [ zenon_intro zenon_H1a | zenon_intro zenon_Hbc ]. % 47.46/47.70 generalize (summation_monotone zenon_TX_r). zenon_intro zenon_Hde. % 47.46/47.70 generalize (max_1 zenon_TX_r). zenon_intro zenon_H1e. % 47.46/47.70 generalize (zenon_Hde zenon_TY_q). zenon_intro zenon_Hdf. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_Hdf); [ zenon_intro zenon_H1a; zenon_intro zenon_He1 | zenon_intro zenon_H1c; zenon_intro zenon_He0 ]. % 47.46/47.70 elim (classic ((~((summation zenon_TX_r) = zenon_TZ_ce))/\(~(lesseq (summation zenon_TX_r) zenon_TZ_ce)))); [ zenon_intro zenon_He2 | zenon_intro zenon_He3 ]. % 47.46/47.70 apply (zenon_and_s _ _ zenon_He2). zenon_intro zenon_He4. zenon_intro zenon_H36. % 47.46/47.70 cut ((lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce) = (lesseq (summation zenon_TX_r) zenon_TZ_ce)). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H36. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H37. % 47.46/47.70 cut ((zenon_TZ_ce = zenon_TZ_ce)); [idtac | apply NNPP; zenon_intro zenon_H39]. % 47.46/47.70 cut (((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TX_r))); [idtac | apply NNPP; zenon_intro zenon_H22]. % 47.46/47.70 congruence. % 47.46/47.70 apply (zenon_L4_ zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 apply zenon_H39. apply refl_equal. % 47.46/47.70 elim (classic (lesseq (summation (max zenon_TX_r zenon_TY_q)) (summation zenon_TY_q))); [ zenon_intro zenon_H4b | zenon_intro zenon_H44 ]. % 47.46/47.70 generalize (zenon_H43 zenon_TZ_ce). zenon_intro zenon_He5. % 47.46/47.70 generalize (zenon_He5 (summation (max zenon_TX_r zenon_TY_q))). zenon_intro zenon_He6. % 47.46/47.70 generalize (zenon_He6 (summation zenon_TY_q)). zenon_intro zenon_He7. % 47.46/47.70 apply (zenon_imply_s _ _ zenon_He7); [ zenon_intro zenon_H53 | zenon_intro zenon_He8 ]. % 47.46/47.70 exact (zenon_H53 zenon_H42). % 47.46/47.70 apply (zenon_imply_s _ _ zenon_He8); [ zenon_intro zenon_H44 | zenon_intro zenon_H45 ]. % 47.46/47.70 exact (zenon_H44 zenon_H4b). % 47.46/47.70 cut ((lesseq zenon_TZ_ce (summation zenon_TY_q)) = (lesseq (summation zenon_TX_r) (summation zenon_TY_q))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_He1. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H45. % 47.46/47.70 cut (((summation zenon_TY_q) = (summation zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_He9]. % 47.46/47.70 cut ((zenon_TZ_ce = (summation zenon_TX_r))); [idtac | apply NNPP; zenon_intro zenon_Hea]. % 47.46/47.70 congruence. % 47.46/47.70 apply (zenon_notand_s _ _ zenon_He3); [ zenon_intro zenon_Hec | zenon_intro zenon_Heb ]. % 47.46/47.70 apply zenon_Hec. zenon_intro zenon_Hed. % 47.46/47.70 apply zenon_Hea. apply sym_equal. exact zenon_Hed. % 47.46/47.70 apply zenon_Heb. zenon_intro zenon_Hee. % 47.46/47.70 generalize (zenon_H43 (summation zenon_TX_r)). zenon_intro zenon_Hef. % 47.46/47.70 generalize (zenon_Hef zenon_TZ_ce). zenon_intro zenon_Hf0. % 47.46/47.70 generalize (zenon_Hf0 (summation zenon_TY_q)). zenon_intro zenon_Hf1. % 47.46/47.70 apply (zenon_imply_s _ _ zenon_Hf1); [ zenon_intro zenon_H36 | zenon_intro zenon_Hf2 ]. % 47.46/47.70 exact (zenon_H36 zenon_Hee). % 47.46/47.70 apply (zenon_imply_s _ _ zenon_Hf2); [ zenon_intro zenon_H41 | zenon_intro zenon_He0 ]. % 47.46/47.70 exact (zenon_H41 zenon_H45). % 47.46/47.70 exact (zenon_He1 zenon_He0). % 47.46/47.70 apply zenon_He9. apply refl_equal. % 47.46/47.70 apply (zenon_L13_ zenon_TZ_ce zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 exact (zenon_H1a zenon_H1c). % 47.46/47.70 generalize (lesseq_ref zenon_TY_q). zenon_intro zenon_Hbd. % 47.46/47.70 exact (zenon_Hbc zenon_Hbd). % 47.46/47.70 exact (zenon_Hb7 zenon_Hba). % 47.46/47.70 apply (zenon_L14_ zenon_TX_r zenon_TZ_ce zenon_TY_q); trivial. % 47.46/47.70 exact (zenon_Hd7 zenon_Hdc). % 47.46/47.70 apply (zenon_notallex_s (fun Z : zenon_U => ((model_ub zenon_TX_r zenon_TY_q Z)->(lesseq zenon_TZ_ce Z))) zenon_Hd6); [ zenon_intro zenon_Hf3; idtac ]. % 47.46/47.70 elim zenon_Hf3. zenon_intro zenon_TZ_de. zenon_intro zenon_Hf4. % 47.46/47.70 apply (zenon_notimply_s _ _ zenon_Hf4). zenon_intro zenon_Hf5. zenon_intro zenon_H5c. % 47.46/47.70 generalize (model_ub_3 zenon_TX_r). zenon_intro zenon_Hd8. % 47.46/47.70 generalize (zenon_Hd8 zenon_TY_q). zenon_intro zenon_Hd9. % 47.46/47.70 generalize (zenon_Hd9 zenon_TZ_de). zenon_intro zenon_Hf6. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_Hf6); [ zenon_intro zenon_Hf9; zenon_intro zenon_Hf8 | zenon_intro zenon_Hf5; zenon_intro zenon_Hf7 ]. % 47.46/47.70 exact (zenon_Hf9 zenon_Hf5). % 47.46/47.70 elim zenon_Hf7. zenon_intro zenon_TZ_ds. zenon_intro zenon_Hfa. % 47.46/47.70 apply (zenon_and_s _ _ zenon_Hfa). zenon_intro zenon_Hfb. zenon_intro zenon_H5f. % 47.46/47.70 generalize (ub zenon_TX_r). zenon_intro zenon_H2a. % 47.46/47.70 generalize (zenon_H2a zenon_TY_q). zenon_intro zenon_H2b. % 47.46/47.70 generalize (zenon_H2b zenon_TZ_ds). zenon_intro zenon_Hfc. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_Hfc); [ zenon_intro zenon_Hff; zenon_intro zenon_Hfe | zenon_intro zenon_Hfb; zenon_intro zenon_Hfd ]. % 47.46/47.70 exact (zenon_Hff zenon_Hfb). % 47.46/47.70 apply (zenon_and_s _ _ zenon_Hfd). zenon_intro zenon_H8d. zenon_intro zenon_H8e. % 47.46/47.70 generalize (max_1 zenon_TZ_ds). zenon_intro zenon_H90. % 47.46/47.70 generalize (zenon_H51 zenon_TZ_de). zenon_intro zenon_H100. % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H100); [ zenon_intro zenon_H101 | zenon_intro zenon_H5d ]. % 47.46/47.70 generalize (model_max_3 zenon_TX_r). zenon_intro zenon_H12. % 47.46/47.70 generalize (zenon_H12 zenon_TY_q). zenon_intro zenon_H13. % 47.46/47.70 generalize (zenon_H13 zenon_TZ_de). zenon_intro zenon_H102. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_H102); [ zenon_intro zenon_H101; zenon_intro zenon_H105 | zenon_intro zenon_H104; zenon_intro zenon_H103 ]. % 47.46/47.70 cut ((lesseq (summation zenon_TZ_ds) zenon_TZ_de) = (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_de)). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H105. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H5f. % 47.46/47.70 cut ((zenon_TZ_de = zenon_TZ_de)); [idtac | apply NNPP; zenon_intro zenon_H106]. % 47.46/47.70 cut (((summation zenon_TZ_ds) = (summation (max zenon_TX_r zenon_TY_q)))); [idtac | apply NNPP; zenon_intro zenon_H73]. % 47.46/47.70 congruence. % 47.46/47.70 cut ((zenon_TZ_ds = (max zenon_TX_r zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_H8c]. % 47.46/47.70 congruence. % 47.46/47.70 elim (classic ((~((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TZ_ds)))/\(~(lesseq (summation (max zenon_TX_r zenon_TY_q)) (summation zenon_TZ_ds))))); [ zenon_intro zenon_H107 | zenon_intro zenon_H108 ]. % 47.46/47.70 apply (zenon_and_s _ _ zenon_H107). zenon_intro zenon_H74. zenon_intro zenon_H109. % 47.46/47.70 generalize (lesseq_total zenon_TZ_ce). zenon_intro zenon_H8a. % 47.46/47.70 generalize (max_2 zenon_TY_q). zenon_intro zenon_H8f. % 47.46/47.70 generalize (summation_monotone zenon_TY_q). zenon_intro zenon_H3a. % 47.46/47.70 generalize (zenon_H3a zenon_TZ_ds). zenon_intro zenon_H10a. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_H10a); [ zenon_intro zenon_Haa; zenon_intro zenon_H10c | zenon_intro zenon_H8e; zenon_intro zenon_H10b ]. % 47.46/47.70 exact (zenon_Haa zenon_H8e). % 47.46/47.70 cut ((lesseq (summation zenon_TY_q) (summation zenon_TZ_ds)) = (lesseq (summation (max zenon_TX_r zenon_TY_q)) (summation zenon_TZ_ds))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H109. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H10b. % 47.46/47.70 cut (((summation zenon_TZ_ds) = (summation zenon_TZ_ds))); [idtac | apply NNPP; zenon_intro zenon_H79]. % 47.46/47.70 cut (((summation zenon_TY_q) = (summation (max zenon_TX_r zenon_TY_q)))); [idtac | apply NNPP; zenon_intro zenon_H8b]. % 47.46/47.70 congruence. % 47.46/47.70 apply (zenon_L27_ zenon_TZ_de zenon_TZ_ce zenon_TZ_ds zenon_TX_r zenon_TY_q); trivial. % 47.46/47.70 apply zenon_H79. apply refl_equal. % 47.46/47.70 cut ((lesseq (summation zenon_TZ_ds) zenon_TZ_de) = (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_de)). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H105. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H5f. % 47.46/47.70 cut ((zenon_TZ_de = zenon_TZ_de)); [idtac | apply NNPP; zenon_intro zenon_H106]. % 47.46/47.70 cut (((summation zenon_TZ_ds) = (summation (max zenon_TX_r zenon_TY_q)))); [idtac | apply NNPP; zenon_intro zenon_H73]. % 47.46/47.70 congruence. % 47.46/47.70 apply (zenon_notand_s _ _ zenon_H108); [ zenon_intro zenon_H10e | zenon_intro zenon_H10d ]. % 47.46/47.70 apply zenon_H10e. zenon_intro zenon_H10f. % 47.46/47.70 elim (classic ((summation (max zenon_TX_r zenon_TY_q)) = (summation (max zenon_TX_r zenon_TY_q)))); [ zenon_intro zenon_H110 | zenon_intro zenon_H111 ]. % 47.46/47.70 cut (((summation (max zenon_TX_r zenon_TY_q)) = (summation (max zenon_TX_r zenon_TY_q))) = ((summation zenon_TZ_ds) = (summation (max zenon_TX_r zenon_TY_q)))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H73. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H110. % 47.46/47.70 cut (((summation (max zenon_TX_r zenon_TY_q)) = (summation (max zenon_TX_r zenon_TY_q)))); [idtac | apply NNPP; zenon_intro zenon_H111]. % 47.46/47.70 cut (((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TZ_ds))); [idtac | apply NNPP; zenon_intro zenon_H74]. % 47.46/47.70 congruence. % 47.46/47.70 exact (zenon_H74 zenon_H10f). % 47.46/47.70 apply zenon_H111. apply refl_equal. % 47.46/47.70 apply zenon_H111. apply refl_equal. % 47.46/47.70 apply zenon_H10d. zenon_intro zenon_H112. % 47.46/47.70 generalize (zenon_H43 (summation (max zenon_TX_r zenon_TY_q))). zenon_intro zenon_H46. % 47.46/47.70 generalize (zenon_H46 (summation zenon_TZ_ds)). zenon_intro zenon_H113. % 47.46/47.70 generalize (zenon_H113 zenon_TZ_de). zenon_intro zenon_H114. % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H114); [ zenon_intro zenon_H109 | zenon_intro zenon_H115 ]. % 47.46/47.70 exact (zenon_H109 zenon_H112). % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H115); [ zenon_intro zenon_H65 | zenon_intro zenon_H103 ]. % 47.46/47.70 exact (zenon_H65 zenon_H5f). % 47.46/47.70 exact (zenon_H105 zenon_H103). % 47.46/47.70 apply zenon_H106. apply refl_equal. % 47.46/47.70 apply zenon_H106. apply refl_equal. % 47.46/47.70 exact (zenon_H101 zenon_H104). % 47.46/47.70 exact (zenon_H5c zenon_H5d). % 47.46/47.70 exact (zenon_Hc8 zenon_Hc6). % 47.46/47.70 generalize (minsol_model_ub zenon_TX_r). zenon_intro zenon_Hc9. % 47.46/47.70 generalize (zenon_Hc9 zenon_TY_q). zenon_intro zenon_Hca. % 47.46/47.70 generalize (zenon_Hca zenon_TZ_ce). zenon_intro zenon_Hcb. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_Hcb); [ zenon_intro zenon_Hc8; zenon_intro zenon_Hcd | zenon_intro zenon_Hc6; zenon_intro zenon_Hcc ]. % 47.46/47.70 exact (zenon_Hc8 zenon_Hc6). % 47.46/47.70 apply (zenon_and_s _ _ zenon_Hcc). zenon_intro zenon_Hdc. zenon_intro zenon_H116. % 47.46/47.70 generalize (model_ub_3 zenon_TX_r). zenon_intro zenon_Hd8. % 47.46/47.70 generalize (zenon_Hd8 zenon_TY_q). zenon_intro zenon_Hd9. % 47.46/47.70 generalize (zenon_Hd9 zenon_TZ_ce). zenon_intro zenon_Hda. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_Hda); [ zenon_intro zenon_Hd7; zenon_intro zenon_H3b | zenon_intro zenon_Hdc; zenon_intro zenon_Hdb ]. % 47.46/47.70 exact (zenon_Hd7 zenon_Hdc). % 47.46/47.70 elim zenon_Hdb. zenon_intro zenon_TZ_kt. zenon_intro zenon_H118. % 47.46/47.70 apply (zenon_and_s _ _ zenon_H118). zenon_intro zenon_H11a. zenon_intro zenon_H119. % 47.46/47.70 generalize (ub zenon_TX_r). zenon_intro zenon_H2a. % 47.46/47.70 generalize (zenon_H2a zenon_TY_q). zenon_intro zenon_H2b. % 47.46/47.70 generalize (zenon_H2b zenon_TZ_kt). zenon_intro zenon_H11b. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_H11b); [ zenon_intro zenon_H11e; zenon_intro zenon_H11d | zenon_intro zenon_H11a; zenon_intro zenon_H11c ]. % 47.46/47.70 exact (zenon_H11e zenon_H11a). % 47.46/47.70 apply (zenon_and_s _ _ zenon_H11c). zenon_intro zenon_H120. zenon_intro zenon_H11f. % 47.46/47.70 generalize (minsol_model_max zenon_TX_r). zenon_intro zenon_Hce. % 47.46/47.70 generalize (zenon_Hce zenon_TY_q). zenon_intro zenon_Hcf. % 47.46/47.70 generalize (zenon_Hcf zenon_TZ_ce). zenon_intro zenon_Hd0. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_Hd0); [ zenon_intro zenon_Hc5; zenon_intro zenon_Hd2 | zenon_intro zenon_Hc7; zenon_intro zenon_Hd1 ]. % 47.46/47.70 apply (zenon_notand_s _ _ zenon_Hd2); [ zenon_intro zenon_Hd5 | zenon_intro zenon_H121 ]. % 47.46/47.70 generalize (model_max_3 zenon_TX_r). zenon_intro zenon_H12. % 47.46/47.70 generalize (zenon_H12 zenon_TY_q). zenon_intro zenon_H13. % 47.46/47.70 generalize (zenon_H13 zenon_TZ_ce). zenon_intro zenon_Hd4. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_Hd4); [ zenon_intro zenon_Hd5; zenon_intro zenon_H4a | zenon_intro zenon_Hd3; zenon_intro zenon_H37 ]. % 47.46/47.70 elim (classic ((~((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TZ_kt)))/\(~(lesseq (summation (max zenon_TX_r zenon_TY_q)) (summation zenon_TZ_kt))))); [ zenon_intro zenon_H122 | zenon_intro zenon_H123 ]. % 47.46/47.70 apply (zenon_and_s _ _ zenon_H122). zenon_intro zenon_H125. zenon_intro zenon_H124. % 47.46/47.70 generalize (lesseq_total zenon_TY_q). zenon_intro zenon_H18. % 47.46/47.70 generalize (max_2 zenon_TX_r). zenon_intro zenon_H24. % 47.46/47.70 generalize (summation_monotone zenon_TY_q). zenon_intro zenon_H3a. % 47.46/47.70 generalize (summation_monotone zenon_TX_r). zenon_intro zenon_Hde. % 47.46/47.70 generalize (max_1 zenon_TX_r). zenon_intro zenon_H1e. % 47.46/47.70 generalize (zenon_H3a zenon_TZ_kt). zenon_intro zenon_H126. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_H126); [ zenon_intro zenon_H129; zenon_intro zenon_H128 | zenon_intro zenon_H11f; zenon_intro zenon_H127 ]. % 47.46/47.70 exact (zenon_H129 zenon_H11f). % 47.46/47.70 cut ((lesseq (summation zenon_TY_q) (summation zenon_TZ_kt)) = (lesseq (summation (max zenon_TX_r zenon_TY_q)) (summation zenon_TZ_kt))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H124. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H127. % 47.46/47.70 cut (((summation zenon_TZ_kt) = (summation zenon_TZ_kt))); [idtac | apply NNPP; zenon_intro zenon_H12a]. % 47.46/47.70 cut (((summation zenon_TY_q) = (summation (max zenon_TX_r zenon_TY_q)))); [idtac | apply NNPP; zenon_intro zenon_H8b]. % 47.46/47.70 congruence. % 47.46/47.70 cut ((zenon_TY_q = (max zenon_TX_r zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_H4e]. % 47.46/47.70 congruence. % 47.46/47.70 generalize (zenon_Hde zenon_TZ_kt). zenon_intro zenon_H12b. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_H12b); [ zenon_intro zenon_H12e; zenon_intro zenon_H12d | zenon_intro zenon_H120; zenon_intro zenon_H12c ]. % 47.46/47.70 exact (zenon_H12e zenon_H120). % 47.46/47.70 cut ((lesseq (summation zenon_TX_r) (summation zenon_TZ_kt)) = (lesseq (summation (max zenon_TX_r zenon_TY_q)) (summation zenon_TZ_kt))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H124. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H12c. % 47.46/47.70 cut (((summation zenon_TZ_kt) = (summation zenon_TZ_kt))); [idtac | apply NNPP; zenon_intro zenon_H12a]. % 47.46/47.70 cut (((summation zenon_TX_r) = (summation (max zenon_TX_r zenon_TY_q)))); [idtac | apply NNPP; zenon_intro zenon_H12f]. % 47.46/47.70 congruence. % 47.46/47.70 cut ((zenon_TX_r = (max zenon_TX_r zenon_TY_q))); [idtac | apply NNPP; zenon_intro zenon_H4d]. % 47.46/47.70 congruence. % 47.46/47.70 apply (zenon_L17_ zenon_TX_r zenon_TY_q); trivial. % 47.46/47.70 apply zenon_H12a. apply refl_equal. % 47.46/47.70 apply zenon_H12a. apply refl_equal. % 47.46/47.70 cut ((lesseq (summation zenon_TZ_kt) zenon_TZ_ce) = (lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_ce)). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H4a. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H119. % 47.46/47.70 cut ((zenon_TZ_ce = zenon_TZ_ce)); [idtac | apply NNPP; zenon_intro zenon_H39]. % 47.46/47.70 cut (((summation zenon_TZ_kt) = (summation (max zenon_TX_r zenon_TY_q)))); [idtac | apply NNPP; zenon_intro zenon_H130]. % 47.46/47.70 congruence. % 47.46/47.70 apply (zenon_notand_s _ _ zenon_H123); [ zenon_intro zenon_H132 | zenon_intro zenon_H131 ]. % 47.46/47.70 apply zenon_H132. zenon_intro zenon_H133. % 47.46/47.70 elim (classic ((summation (max zenon_TX_r zenon_TY_q)) = (summation (max zenon_TX_r zenon_TY_q)))); [ zenon_intro zenon_H110 | zenon_intro zenon_H111 ]. % 47.46/47.70 cut (((summation (max zenon_TX_r zenon_TY_q)) = (summation (max zenon_TX_r zenon_TY_q))) = ((summation zenon_TZ_kt) = (summation (max zenon_TX_r zenon_TY_q)))). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H130. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_H110. % 47.46/47.70 cut (((summation (max zenon_TX_r zenon_TY_q)) = (summation (max zenon_TX_r zenon_TY_q)))); [idtac | apply NNPP; zenon_intro zenon_H111]. % 47.46/47.70 cut (((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TZ_kt))); [idtac | apply NNPP; zenon_intro zenon_H125]. % 47.46/47.70 congruence. % 47.46/47.70 exact (zenon_H125 zenon_H133). % 47.46/47.70 apply zenon_H111. apply refl_equal. % 47.46/47.70 apply zenon_H111. apply refl_equal. % 47.46/47.70 apply zenon_H131. zenon_intro zenon_H134. % 47.46/47.70 generalize (zenon_H43 (summation (max zenon_TX_r zenon_TY_q))). zenon_intro zenon_H46. % 47.46/47.70 generalize (zenon_H46 (summation zenon_TZ_kt)). zenon_intro zenon_H135. % 47.46/47.70 generalize (zenon_H135 zenon_TZ_ce). zenon_intro zenon_H136. % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H136); [ zenon_intro zenon_H124 | zenon_intro zenon_H137 ]. % 47.46/47.70 exact (zenon_H124 zenon_H134). % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H137); [ zenon_intro zenon_H138 | zenon_intro zenon_H37 ]. % 47.46/47.70 exact (zenon_H138 zenon_H119). % 47.46/47.70 exact (zenon_H4a zenon_H37). % 47.46/47.70 apply zenon_H39. apply refl_equal. % 47.46/47.70 exact (zenon_Hd5 zenon_Hd3). % 47.46/47.70 apply (zenon_notallex_s (fun Z : zenon_U => ((model_max zenon_TX_r zenon_TY_q Z)->(lesseq zenon_TZ_ce Z))) zenon_H121); [ zenon_intro zenon_H139; idtac ]. % 47.46/47.70 elim zenon_H139. zenon_intro zenon_TZ_gs. zenon_intro zenon_H13a. % 47.46/47.70 apply (zenon_notimply_s _ _ zenon_H13a). zenon_intro zenon_H13c. zenon_intro zenon_H13b. % 47.46/47.70 generalize (model_max_3 zenon_TX_r). zenon_intro zenon_H12. % 47.46/47.70 generalize (zenon_H12 zenon_TY_q). zenon_intro zenon_H13. % 47.46/47.70 generalize (zenon_H13 zenon_TZ_gs). zenon_intro zenon_H13d. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_H13d); [ zenon_intro zenon_H13f; zenon_intro zenon_H13e | zenon_intro zenon_H13c; zenon_intro zenon_Had ]. % 47.46/47.70 exact (zenon_H13f zenon_H13c). % 47.46/47.70 generalize (zenon_H116 zenon_TZ_gs). zenon_intro zenon_H140. % 47.46/47.70 apply (zenon_imply_s _ _ zenon_H140); [ zenon_intro zenon_H142 | zenon_intro zenon_H141 ]. % 47.46/47.70 generalize (model_ub_3 zenon_TX_r). zenon_intro zenon_Hd8. % 47.46/47.70 generalize (zenon_Hd8 zenon_TY_q). zenon_intro zenon_Hd9. % 47.46/47.70 generalize (zenon_Hd9 zenon_TZ_gs). zenon_intro zenon_H143. % 47.46/47.70 apply (zenon_equiv_s _ _ zenon_H143); [ zenon_intro zenon_H142; zenon_intro zenon_Hac | zenon_intro zenon_H145; zenon_intro zenon_H144 ]. % 47.46/47.70 generalize (lesseq_total zenon_TY_q). zenon_intro zenon_H18. % 47.46/47.70 generalize (max_2 zenon_TX_r). zenon_intro zenon_H24. % 47.46/47.70 generalize (max_1 zenon_TX_r). zenon_intro zenon_H1e. % 47.46/47.70 generalize (zenon_H18 zenon_TX_r). zenon_intro zenon_H1b. % 47.46/47.70 apply (zenon_or_s _ _ zenon_H1b); [ zenon_intro zenon_H1d | zenon_intro zenon_H1c ]. % 47.46/47.70 generalize (zenon_H1e zenon_TY_q). zenon_intro zenon_H20. % 47.46/47.70 apply (zenon_or_s _ _ zenon_H20); [ zenon_intro zenon_H21 | zenon_intro zenon_H19 ]. % 47.46/47.70 apply zenon_Hac. exists zenon_TX_r. apply NNPP. zenon_intro zenon_H146. % 47.46/47.70 apply (zenon_notand_s _ _ zenon_H146); [ zenon_intro zenon_H29 | zenon_intro zenon_H147 ]. % 47.46/47.70 apply (zenon_L7_ zenon_TX_r zenon_TY_q); trivial. % 47.46/47.70 cut ((lesseq (summation (max zenon_TX_r zenon_TY_q)) zenon_TZ_gs) = (lesseq (summation zenon_TX_r) zenon_TZ_gs)). % 47.46/47.70 intro zenon_D_pnotp. % 47.46/47.70 apply zenon_H147. % 47.46/47.70 rewrite <- zenon_D_pnotp. % 47.46/47.70 exact zenon_Had. % 47.46/47.70 cut ((zenon_TZ_gs = zenon_TZ_gs)); [idtac | apply NNPP; zenon_intro zenon_Hb5]. % 47.46/47.70 cut (((summation (max zenon_TX_r zenon_TY_q)) = (summation zenon_TX_r))); [idtac | apply NNPP; zenon_intro zenon_H22]. % 47.46/47.70 congruence. % 47.46/47.70 apply (zenon_L28_ zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 apply zenon_Hb5. apply refl_equal. % 47.46/47.70 exact (zenon_H19 zenon_H1d). % 47.46/47.70 apply (zenon_L29_ zenon_TZ_gs zenon_TY_q zenon_TX_r); trivial. % 47.46/47.70 exact (zenon_H142 zenon_H145). % 47.46/47.70 exact (zenon_H13b zenon_H141). % 47.46/47.70 exact (zenon_Hc5 zenon_Hc7). % 47.46/47.70 apply zenon_Hbe. zenon_intro zenon_Tx_mq. apply NNPP. zenon_intro zenon_H149. % 47.46/47.70 apply zenon_H149. zenon_intro zenon_Ty_ms. apply NNPP. zenon_intro zenon_H14b. % 47.46/47.70 apply zenon_H14b. zenon_intro zenon_Tz_mu. apply NNPP. zenon_intro zenon_H14d. % 47.46/47.70 apply (zenon_notimply_s _ _ zenon_H14d). zenon_intro zenon_H14f. zenon_intro zenon_H14e. % 47.46/47.70 apply (zenon_notimply_s _ _ zenon_H14e). zenon_intro zenon_H151. zenon_intro zenon_H150. % 47.46/47.70 generalize (lesseq_trans zenon_Tx_mq). zenon_intro zenon_H152. % 47.46/47.71 generalize (zenon_H152 zenon_Ty_ms). zenon_intro zenon_H153. % 47.46/47.71 generalize (zenon_H153 zenon_Tz_mu). zenon_intro zenon_H154. % 47.46/47.71 apply (zenon_imply_s _ _ zenon_H154); [ zenon_intro zenon_H156 | zenon_intro zenon_H155 ]. % 47.46/47.71 apply (zenon_notand_s _ _ zenon_H156); [ zenon_intro zenon_H158 | zenon_intro zenon_H157 ]. % 47.46/47.71 exact (zenon_H158 zenon_H14f). % 47.46/47.71 exact (zenon_H157 zenon_H151). % 47.46/47.71 exact (zenon_H150 zenon_H155). % 47.46/47.71 Qed. % 47.46/47.71 % SZS output end Proof % 47.46/47.71 (* END-PROOF *) % 47.46/47.71 nodes searched: 4069361 % 47.46/47.71 max branch formulas: 12146 % 47.46/47.71 proof nodes created: 36582 % 47.46/47.71 formulas created: 1463137 % 47.46/47.71 %------------------------------------------------------------------------------