%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT027+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:24:19 AM UTC 2026 % Result : Theorem 0.44s 0.71s % Output : Proof 0.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT027+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : run_zenon %s %d % 0.10/0.36 % Computer : n017.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Mon Sep 7 12:08:39 UTC 2026 % 0.10/0.36 % CPUTime : % 0.44/0.71 (* PROOF-FOUND *) % 0.44/0.71 % SZS status Theorem % 0.44/0.71 (* BEGIN-PROOF *) % 0.44/0.71 % SZS output start Proof % 0.44/0.71 Theorem prove_l9 : (forall E : zenon_U, (((environment E)/\(stable E))->(exists To : zenon_U, ((greater To (appear (efficient_producers) E))/\(contracts_from To (first_movers)))))). % 0.44/0.71 Proof. % 0.44/0.71 assert (zenon_L1_ : forall (zenon_TE_m : zenon_U), (environment zenon_TE_m) -> (stable zenon_TE_m) -> (~(in_environment zenon_TE_m (appear (efficient_producers) zenon_TE_m))) -> False). % 0.44/0.71 do 1 intro. intros zenon_H9 zenon_Ha zenon_Hb. % 0.44/0.71 generalize (mp_EP_in_stable_environments zenon_TE_m). zenon_intro zenon_Hd. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_Hd); [ zenon_intro zenon_Hf | zenon_intro zenon_He ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_Hf); [ zenon_intro zenon_H11 | zenon_intro zenon_H10 ]. % 0.44/0.71 exact (zenon_H11 zenon_H9). % 0.44/0.71 exact (zenon_H10 zenon_Ha). % 0.44/0.71 exact (zenon_Hb zenon_He). % 0.44/0.71 (* end of lemma zenon_L1_ *) % 0.44/0.71 assert (zenon_L2_ : forall (zenon_TE_m : zenon_U) (zenon_TTo_w : zenon_U) (zenon_TT_x : zenon_U), (greater zenon_TT_x zenon_TTo_w) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater zenon_TT_x (appear (efficient_producers) zenon_TE_m))) -> (greater zenon_TTo_w (appear (efficient_producers) zenon_TE_m)) -> False). % 0.44/0.71 do 3 intro. intros zenon_H12 zenon_H13 zenon_H14 zenon_H15. % 0.44/0.71 elim (classic ((~(zenon_TT_x = zenon_TTo_w))/\(~(greater zenon_TT_x zenon_TTo_w)))); [ zenon_intro zenon_H18 | zenon_intro zenon_H19 ]. % 0.44/0.71 apply (zenon_and_s _ _ zenon_H18). zenon_intro zenon_H1b. zenon_intro zenon_H1a. % 0.44/0.71 exact (zenon_H1a zenon_H12). % 0.44/0.71 cut ((greater zenon_TTo_w (appear (efficient_producers) zenon_TE_m)) = (greater zenon_TT_x (appear (efficient_producers) zenon_TE_m))). % 0.44/0.71 intro zenon_D_pnotp. % 0.44/0.71 apply zenon_H14. % 0.44/0.71 rewrite <- zenon_D_pnotp. % 0.44/0.71 exact zenon_H15. % 0.44/0.71 cut (((appear (efficient_producers) zenon_TE_m) = (appear (efficient_producers) zenon_TE_m))); [idtac | apply NNPP; zenon_intro zenon_H1c]. % 0.44/0.71 cut ((zenon_TTo_w = zenon_TT_x)); [idtac | apply NNPP; zenon_intro zenon_H1d]. % 0.44/0.71 congruence. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H19); [ zenon_intro zenon_H1f | zenon_intro zenon_H1e ]. % 0.44/0.71 apply zenon_H1f. zenon_intro zenon_H20. % 0.44/0.71 elim (classic (zenon_TT_x = zenon_TT_x)); [ zenon_intro zenon_H21 | zenon_intro zenon_H22 ]. % 0.44/0.71 cut ((zenon_TT_x = zenon_TT_x) = (zenon_TTo_w = zenon_TT_x)). % 0.44/0.71 intro zenon_D_pnotp. % 0.44/0.71 apply zenon_H1d. % 0.44/0.71 rewrite <- zenon_D_pnotp. % 0.44/0.71 exact zenon_H21. % 0.44/0.71 cut ((zenon_TT_x = zenon_TT_x)); [idtac | apply NNPP; zenon_intro zenon_H22]. % 0.44/0.71 cut ((zenon_TT_x = zenon_TTo_w)); [idtac | apply NNPP; zenon_intro zenon_H1b]. % 0.44/0.71 congruence. % 0.44/0.71 exact (zenon_H1b zenon_H20). % 0.44/0.71 apply zenon_H22. apply refl_equal. % 0.44/0.71 apply zenon_H22. apply refl_equal. % 0.44/0.71 apply zenon_H1e. zenon_intro zenon_H12. % 0.44/0.71 generalize (zenon_H13 zenon_TT_x). zenon_intro zenon_H23. % 0.44/0.71 generalize (zenon_H23 zenon_TTo_w). zenon_intro zenon_H24. % 0.44/0.71 generalize (zenon_H24 (appear (efficient_producers) zenon_TE_m)). zenon_intro zenon_H25. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H25); [ zenon_intro zenon_H1a | zenon_intro zenon_H26 ]. % 0.44/0.71 exact (zenon_H1a zenon_H12). % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H26); [ zenon_intro zenon_H28 | zenon_intro zenon_H27 ]. % 0.44/0.71 exact (zenon_H28 zenon_H15). % 0.44/0.71 exact (zenon_H14 zenon_H27). % 0.44/0.71 apply zenon_H1c. apply refl_equal. % 0.44/0.71 (* end of lemma zenon_L2_ *) % 0.44/0.71 assert (zenon_L3_ : forall (zenon_TTo_w : zenon_U) (zenon_TT_x : zenon_U) (zenon_TT_br : zenon_U), (greater zenon_TT_br zenon_TT_x) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater zenon_TT_br zenon_TTo_w)) -> (greater zenon_TT_x zenon_TTo_w) -> False). % 0.44/0.71 do 3 intro. intros zenon_H29 zenon_H13 zenon_H2a zenon_H12. % 0.44/0.71 elim (classic ((~(zenon_TT_br = zenon_TT_x))/\(~(greater zenon_TT_br zenon_TT_x)))); [ zenon_intro zenon_H2c | zenon_intro zenon_H2d ]. % 0.44/0.71 apply (zenon_and_s _ _ zenon_H2c). zenon_intro zenon_H2f. zenon_intro zenon_H2e. % 0.44/0.71 exact (zenon_H2e zenon_H29). % 0.44/0.71 cut ((greater zenon_TT_x zenon_TTo_w) = (greater zenon_TT_br zenon_TTo_w)). % 0.44/0.71 intro zenon_D_pnotp. % 0.44/0.71 apply zenon_H2a. % 0.44/0.71 rewrite <- zenon_D_pnotp. % 0.44/0.71 exact zenon_H12. % 0.44/0.71 cut ((zenon_TTo_w = zenon_TTo_w)); [idtac | apply NNPP; zenon_intro zenon_H30]. % 0.44/0.71 cut ((zenon_TT_x = zenon_TT_br)); [idtac | apply NNPP; zenon_intro zenon_H31]. % 0.44/0.71 congruence. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H2d); [ zenon_intro zenon_H33 | zenon_intro zenon_H32 ]. % 0.44/0.71 apply zenon_H33. zenon_intro zenon_H34. % 0.44/0.71 elim (classic (zenon_TT_br = zenon_TT_br)); [ zenon_intro zenon_H35 | zenon_intro zenon_H36 ]. % 0.44/0.71 cut ((zenon_TT_br = zenon_TT_br) = (zenon_TT_x = zenon_TT_br)). % 0.44/0.71 intro zenon_D_pnotp. % 0.44/0.71 apply zenon_H31. % 0.44/0.71 rewrite <- zenon_D_pnotp. % 0.44/0.71 exact zenon_H35. % 0.44/0.71 cut ((zenon_TT_br = zenon_TT_br)); [idtac | apply NNPP; zenon_intro zenon_H36]. % 0.44/0.71 cut ((zenon_TT_br = zenon_TT_x)); [idtac | apply NNPP; zenon_intro zenon_H2f]. % 0.44/0.71 congruence. % 0.44/0.71 exact (zenon_H2f zenon_H34). % 0.44/0.71 apply zenon_H36. apply refl_equal. % 0.44/0.71 apply zenon_H36. apply refl_equal. % 0.44/0.71 apply zenon_H32. zenon_intro zenon_H29. % 0.44/0.71 generalize (zenon_H13 zenon_TT_br). zenon_intro zenon_H37. % 0.44/0.71 generalize (zenon_H37 zenon_TT_x). zenon_intro zenon_H38. % 0.44/0.71 generalize (zenon_H38 zenon_TTo_w). zenon_intro zenon_H39. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H39); [ zenon_intro zenon_H2e | zenon_intro zenon_H3a ]. % 0.44/0.71 exact (zenon_H2e zenon_H29). % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H3a); [ zenon_intro zenon_H1a | zenon_intro zenon_H3b ]. % 0.44/0.71 exact (zenon_H1a zenon_H12). % 0.44/0.71 exact (zenon_H2a zenon_H3b). % 0.44/0.71 apply zenon_H30. apply refl_equal. % 0.44/0.71 (* end of lemma zenon_L3_ *) % 0.44/0.71 assert (zenon_L4_ : forall (zenon_TE_m : zenon_U) (zenon_TTo_w : zenon_U) (zenon_TT_x : zenon_U) (zenon_TT_br : zenon_U), (greater zenon_TT_br zenon_TT_x) -> (greater zenon_TT_x zenon_TTo_w) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater zenon_TT_br (appear (efficient_producers) zenon_TE_m))) -> (greater zenon_TTo_w (appear (efficient_producers) zenon_TE_m)) -> False). % 0.44/0.71 do 4 intro. intros zenon_H29 zenon_H12 zenon_H13 zenon_H3c zenon_H15. % 0.44/0.71 elim (classic ((~(zenon_TT_br = zenon_TTo_w))/\(~(greater zenon_TT_br zenon_TTo_w)))); [ zenon_intro zenon_H3d | zenon_intro zenon_H3e ]. % 0.44/0.71 apply (zenon_and_s _ _ zenon_H3d). zenon_intro zenon_H3f. zenon_intro zenon_H2a. % 0.44/0.71 apply (zenon_L3_ zenon_TTo_w zenon_TT_x zenon_TT_br); trivial. % 0.44/0.71 cut ((greater zenon_TTo_w (appear (efficient_producers) zenon_TE_m)) = (greater zenon_TT_br (appear (efficient_producers) zenon_TE_m))). % 0.44/0.71 intro zenon_D_pnotp. % 0.44/0.71 apply zenon_H3c. % 0.44/0.71 rewrite <- zenon_D_pnotp. % 0.44/0.71 exact zenon_H15. % 0.44/0.71 cut (((appear (efficient_producers) zenon_TE_m) = (appear (efficient_producers) zenon_TE_m))); [idtac | apply NNPP; zenon_intro zenon_H1c]. % 0.44/0.71 cut ((zenon_TTo_w = zenon_TT_br)); [idtac | apply NNPP; zenon_intro zenon_H40]. % 0.44/0.71 congruence. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H3e); [ zenon_intro zenon_H42 | zenon_intro zenon_H41 ]. % 0.44/0.71 apply zenon_H42. zenon_intro zenon_H43. % 0.44/0.71 elim (classic (zenon_TT_br = zenon_TT_br)); [ zenon_intro zenon_H35 | zenon_intro zenon_H36 ]. % 0.44/0.71 cut ((zenon_TT_br = zenon_TT_br) = (zenon_TTo_w = zenon_TT_br)). % 0.44/0.71 intro zenon_D_pnotp. % 0.44/0.71 apply zenon_H40. % 0.44/0.71 rewrite <- zenon_D_pnotp. % 0.44/0.71 exact zenon_H35. % 0.44/0.71 cut ((zenon_TT_br = zenon_TT_br)); [idtac | apply NNPP; zenon_intro zenon_H36]. % 0.44/0.71 cut ((zenon_TT_br = zenon_TTo_w)); [idtac | apply NNPP; zenon_intro zenon_H3f]. % 0.44/0.71 congruence. % 0.44/0.71 exact (zenon_H3f zenon_H43). % 0.44/0.71 apply zenon_H36. apply refl_equal. % 0.44/0.71 apply zenon_H36. apply refl_equal. % 0.44/0.71 apply zenon_H41. zenon_intro zenon_H3b. % 0.44/0.71 generalize (zenon_H13 zenon_TT_br). zenon_intro zenon_H37. % 0.44/0.71 generalize (zenon_H37 zenon_TTo_w). zenon_intro zenon_H44. % 0.44/0.71 generalize (zenon_H44 (appear (efficient_producers) zenon_TE_m)). zenon_intro zenon_H45. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H45); [ zenon_intro zenon_H2a | zenon_intro zenon_H46 ]. % 0.44/0.71 exact (zenon_H2a zenon_H3b). % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H46); [ zenon_intro zenon_H28 | zenon_intro zenon_H47 ]. % 0.44/0.71 exact (zenon_H28 zenon_H15). % 0.44/0.71 exact (zenon_H3c zenon_H47). % 0.44/0.71 apply zenon_H1c. apply refl_equal. % 0.44/0.71 (* end of lemma zenon_L4_ *) % 0.44/0.71 assert (zenon_L5_ : forall (zenon_TTo_w : zenon_U) (zenon_TT_x : zenon_U) (zenon_TT_br : zenon_U), (zenon_TT_br = zenon_TT_x) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater zenon_TT_br zenon_TTo_w)) -> (greater zenon_TT_x zenon_TTo_w) -> False). % 0.44/0.71 do 3 intro. intros zenon_H34 zenon_H13 zenon_H2a zenon_H12. % 0.44/0.71 elim (classic ((~(zenon_TT_br = zenon_TT_x))/\(~(greater zenon_TT_br zenon_TT_x)))); [ zenon_intro zenon_H2c | zenon_intro zenon_H2d ]. % 0.44/0.71 apply (zenon_and_s _ _ zenon_H2c). zenon_intro zenon_H2f. zenon_intro zenon_H2e. % 0.44/0.71 exact (zenon_H2f zenon_H34). % 0.44/0.71 cut ((greater zenon_TT_x zenon_TTo_w) = (greater zenon_TT_br zenon_TTo_w)). % 0.44/0.71 intro zenon_D_pnotp. % 0.44/0.71 apply zenon_H2a. % 0.44/0.71 rewrite <- zenon_D_pnotp. % 0.44/0.71 exact zenon_H12. % 0.44/0.71 cut ((zenon_TTo_w = zenon_TTo_w)); [idtac | apply NNPP; zenon_intro zenon_H30]. % 0.44/0.71 cut ((zenon_TT_x = zenon_TT_br)); [idtac | apply NNPP; zenon_intro zenon_H31]. % 0.44/0.71 congruence. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H2d); [ zenon_intro zenon_H33 | zenon_intro zenon_H32 ]. % 0.44/0.71 apply zenon_H33. zenon_intro zenon_H34. % 0.44/0.71 elim (classic (zenon_TT_br = zenon_TT_br)); [ zenon_intro zenon_H35 | zenon_intro zenon_H36 ]. % 0.44/0.71 cut ((zenon_TT_br = zenon_TT_br) = (zenon_TT_x = zenon_TT_br)). % 0.44/0.71 intro zenon_D_pnotp. % 0.44/0.71 apply zenon_H31. % 0.44/0.71 rewrite <- zenon_D_pnotp. % 0.44/0.71 exact zenon_H35. % 0.44/0.71 cut ((zenon_TT_br = zenon_TT_br)); [idtac | apply NNPP; zenon_intro zenon_H36]. % 0.44/0.71 cut ((zenon_TT_br = zenon_TT_x)); [idtac | apply NNPP; zenon_intro zenon_H2f]. % 0.44/0.71 congruence. % 0.44/0.71 exact (zenon_H2f zenon_H34). % 0.44/0.71 apply zenon_H36. apply refl_equal. % 0.44/0.71 apply zenon_H36. apply refl_equal. % 0.44/0.71 apply zenon_H32. zenon_intro zenon_H29. % 0.44/0.71 generalize (zenon_H13 zenon_TT_br). zenon_intro zenon_H37. % 0.44/0.71 generalize (zenon_H37 zenon_TT_x). zenon_intro zenon_H38. % 0.44/0.71 generalize (zenon_H38 zenon_TTo_w). zenon_intro zenon_H39. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H39); [ zenon_intro zenon_H2e | zenon_intro zenon_H3a ]. % 0.44/0.71 exact (zenon_H2e zenon_H29). % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H3a); [ zenon_intro zenon_H1a | zenon_intro zenon_H3b ]. % 0.44/0.71 exact (zenon_H1a zenon_H12). % 0.44/0.71 exact (zenon_H2a zenon_H3b). % 0.44/0.71 apply zenon_H30. apply refl_equal. % 0.44/0.71 (* end of lemma zenon_L5_ *) % 0.44/0.71 assert (zenon_L6_ : forall (zenon_TE_m : zenon_U) (zenon_TTo_w : zenon_U) (zenon_TT_x : zenon_U) (zenon_TT_br : zenon_U), (zenon_TT_br = zenon_TT_x) -> (greater zenon_TT_x zenon_TTo_w) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater zenon_TT_br (appear (efficient_producers) zenon_TE_m))) -> (greater zenon_TTo_w (appear (efficient_producers) zenon_TE_m)) -> False). % 0.44/0.71 do 4 intro. intros zenon_H34 zenon_H12 zenon_H13 zenon_H3c zenon_H15. % 0.44/0.71 elim (classic ((~(zenon_TT_br = zenon_TTo_w))/\(~(greater zenon_TT_br zenon_TTo_w)))); [ zenon_intro zenon_H3d | zenon_intro zenon_H3e ]. % 0.44/0.71 apply (zenon_and_s _ _ zenon_H3d). zenon_intro zenon_H3f. zenon_intro zenon_H2a. % 0.44/0.71 apply (zenon_L5_ zenon_TTo_w zenon_TT_x zenon_TT_br); trivial. % 0.44/0.71 cut ((greater zenon_TTo_w (appear (efficient_producers) zenon_TE_m)) = (greater zenon_TT_br (appear (efficient_producers) zenon_TE_m))). % 0.44/0.71 intro zenon_D_pnotp. % 0.44/0.71 apply zenon_H3c. % 0.44/0.71 rewrite <- zenon_D_pnotp. % 0.44/0.71 exact zenon_H15. % 0.44/0.71 cut (((appear (efficient_producers) zenon_TE_m) = (appear (efficient_producers) zenon_TE_m))); [idtac | apply NNPP; zenon_intro zenon_H1c]. % 0.44/0.71 cut ((zenon_TTo_w = zenon_TT_br)); [idtac | apply NNPP; zenon_intro zenon_H40]. % 0.44/0.71 congruence. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H3e); [ zenon_intro zenon_H42 | zenon_intro zenon_H41 ]. % 0.44/0.71 apply zenon_H42. zenon_intro zenon_H43. % 0.44/0.71 elim (classic (zenon_TT_br = zenon_TT_br)); [ zenon_intro zenon_H35 | zenon_intro zenon_H36 ]. % 0.44/0.71 cut ((zenon_TT_br = zenon_TT_br) = (zenon_TTo_w = zenon_TT_br)). % 0.44/0.71 intro zenon_D_pnotp. % 0.44/0.71 apply zenon_H40. % 0.44/0.71 rewrite <- zenon_D_pnotp. % 0.44/0.71 exact zenon_H35. % 0.44/0.71 cut ((zenon_TT_br = zenon_TT_br)); [idtac | apply NNPP; zenon_intro zenon_H36]. % 0.44/0.71 cut ((zenon_TT_br = zenon_TTo_w)); [idtac | apply NNPP; zenon_intro zenon_H3f]. % 0.44/0.71 congruence. % 0.44/0.71 exact (zenon_H3f zenon_H43). % 0.44/0.71 apply zenon_H36. apply refl_equal. % 0.44/0.71 apply zenon_H36. apply refl_equal. % 0.44/0.71 apply zenon_H41. zenon_intro zenon_H3b. % 0.44/0.71 generalize (zenon_H13 zenon_TT_br). zenon_intro zenon_H37. % 0.44/0.71 generalize (zenon_H37 zenon_TTo_w). zenon_intro zenon_H44. % 0.44/0.71 generalize (zenon_H44 (appear (efficient_producers) zenon_TE_m)). zenon_intro zenon_H45. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H45); [ zenon_intro zenon_H2a | zenon_intro zenon_H46 ]. % 0.44/0.71 exact (zenon_H2a zenon_H3b). % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H46); [ zenon_intro zenon_H28 | zenon_intro zenon_H47 ]. % 0.44/0.71 exact (zenon_H28 zenon_H15). % 0.44/0.71 exact (zenon_H3c zenon_H47). % 0.44/0.71 apply zenon_H1c. apply refl_equal. % 0.44/0.71 (* end of lemma zenon_L6_ *) % 0.44/0.71 assert (zenon_L7_ : forall (zenon_TE_m : zenon_U) (zenon_TTo_w : zenon_U) (zenon_TT_x : zenon_U), (zenon_TT_x = zenon_TTo_w) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater zenon_TT_x (appear (efficient_producers) zenon_TE_m))) -> (greater zenon_TTo_w (appear (efficient_producers) zenon_TE_m)) -> False). % 0.44/0.71 do 3 intro. intros zenon_H20 zenon_H13 zenon_H14 zenon_H15. % 0.44/0.71 elim (classic ((~(zenon_TT_x = zenon_TTo_w))/\(~(greater zenon_TT_x zenon_TTo_w)))); [ zenon_intro zenon_H18 | zenon_intro zenon_H19 ]. % 0.44/0.71 apply (zenon_and_s _ _ zenon_H18). zenon_intro zenon_H1b. zenon_intro zenon_H1a. % 0.44/0.71 exact (zenon_H1b zenon_H20). % 0.44/0.71 cut ((greater zenon_TTo_w (appear (efficient_producers) zenon_TE_m)) = (greater zenon_TT_x (appear (efficient_producers) zenon_TE_m))). % 0.44/0.71 intro zenon_D_pnotp. % 0.44/0.71 apply zenon_H14. % 0.44/0.71 rewrite <- zenon_D_pnotp. % 0.44/0.71 exact zenon_H15. % 0.44/0.71 cut (((appear (efficient_producers) zenon_TE_m) = (appear (efficient_producers) zenon_TE_m))); [idtac | apply NNPP; zenon_intro zenon_H1c]. % 0.44/0.71 cut ((zenon_TTo_w = zenon_TT_x)); [idtac | apply NNPP; zenon_intro zenon_H1d]. % 0.44/0.71 congruence. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H19); [ zenon_intro zenon_H1f | zenon_intro zenon_H1e ]. % 0.44/0.71 apply zenon_H1f. zenon_intro zenon_H20. % 0.44/0.71 elim (classic (zenon_TT_x = zenon_TT_x)); [ zenon_intro zenon_H21 | zenon_intro zenon_H22 ]. % 0.44/0.71 cut ((zenon_TT_x = zenon_TT_x) = (zenon_TTo_w = zenon_TT_x)). % 0.44/0.71 intro zenon_D_pnotp. % 0.44/0.71 apply zenon_H1d. % 0.44/0.71 rewrite <- zenon_D_pnotp. % 0.44/0.71 exact zenon_H21. % 0.44/0.71 cut ((zenon_TT_x = zenon_TT_x)); [idtac | apply NNPP; zenon_intro zenon_H22]. % 0.44/0.71 cut ((zenon_TT_x = zenon_TTo_w)); [idtac | apply NNPP; zenon_intro zenon_H1b]. % 0.44/0.71 congruence. % 0.44/0.71 exact (zenon_H1b zenon_H20). % 0.44/0.71 apply zenon_H22. apply refl_equal. % 0.44/0.71 apply zenon_H22. apply refl_equal. % 0.44/0.71 apply zenon_H1e. zenon_intro zenon_H12. % 0.44/0.71 generalize (zenon_H13 zenon_TT_x). zenon_intro zenon_H23. % 0.44/0.71 generalize (zenon_H23 zenon_TTo_w). zenon_intro zenon_H24. % 0.44/0.71 generalize (zenon_H24 (appear (efficient_producers) zenon_TE_m)). zenon_intro zenon_H25. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H25); [ zenon_intro zenon_H1a | zenon_intro zenon_H26 ]. % 0.44/0.71 exact (zenon_H1a zenon_H12). % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H26); [ zenon_intro zenon_H28 | zenon_intro zenon_H27 ]. % 0.44/0.71 exact (zenon_H28 zenon_H15). % 0.44/0.71 exact (zenon_H14 zenon_H27). % 0.44/0.71 apply zenon_H1c. apply refl_equal. % 0.44/0.71 (* end of lemma zenon_L7_ *) % 0.44/0.71 apply NNPP. intro zenon_G. % 0.44/0.71 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z))))))); [ zenon_intro zenon_H13 | zenon_intro zenon_H48 ]. % 0.44/0.71 apply (zenon_notallex_s (fun E : zenon_U => (((environment E)/\(stable E))->(exists To : zenon_U, ((greater To (appear (efficient_producers) E))/\(contracts_from To (first_movers)))))) zenon_G); [ zenon_intro zenon_H49; idtac ]. % 0.44/0.71 elim zenon_H49. zenon_intro zenon_TE_m. zenon_intro zenon_H4a. % 0.44/0.71 apply (zenon_notimply_s _ _ zenon_H4a). zenon_intro zenon_H4c. zenon_intro zenon_H4b. % 0.44/0.71 apply (zenon_and_s _ _ zenon_H4c). zenon_intro zenon_H9. zenon_intro zenon_Ha. % 0.44/0.71 generalize (mp_long_stable_environments zenon_TE_m). zenon_intro zenon_H4d. % 0.44/0.71 generalize (l10 zenon_TE_m). zenon_intro zenon_H4e. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H4e); [ zenon_intro zenon_Hf | zenon_intro zenon_H4f ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_Hf); [ zenon_intro zenon_H11 | zenon_intro zenon_H10 ]. % 0.44/0.71 exact (zenon_H11 zenon_H9). % 0.44/0.71 exact (zenon_H10 zenon_Ha). % 0.44/0.71 elim zenon_H4f. zenon_intro zenon_TTo_w. zenon_intro zenon_H50. % 0.44/0.71 apply (zenon_and_s _ _ zenon_H50). zenon_intro zenon_H15. zenon_intro zenon_H51. % 0.44/0.71 generalize (mp_contracts_from zenon_TE_m). zenon_intro zenon_H52. % 0.44/0.71 generalize (zenon_H4d (appear (efficient_producers) zenon_TE_m)). zenon_intro zenon_H53. % 0.44/0.71 generalize (zenon_H53 zenon_TTo_w). zenon_intro zenon_H54. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H54); [ zenon_intro zenon_H56 | zenon_intro zenon_H55 ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H56); [ zenon_intro zenon_H11 | zenon_intro zenon_H57 ]. % 0.44/0.71 exact (zenon_H11 zenon_H9). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H57); [ zenon_intro zenon_H10 | zenon_intro zenon_H58 ]. % 0.44/0.71 exact (zenon_H10 zenon_Ha). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H58); [ zenon_intro zenon_Hb | zenon_intro zenon_H28 ]. % 0.44/0.71 apply (zenon_L1_ zenon_TE_m); trivial. % 0.44/0.71 exact (zenon_H28 zenon_H15). % 0.44/0.71 apply zenon_H4b. exists zenon_TTo_w. apply NNPP. zenon_intro zenon_H59. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H59); [ zenon_intro zenon_H28 | zenon_intro zenon_H5a ]. % 0.44/0.71 exact (zenon_H28 zenon_H15). % 0.44/0.71 generalize (zenon_H52 zenon_TTo_w). zenon_intro zenon_H5b. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H5b); [ zenon_intro zenon_H5d | zenon_intro zenon_H5c ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H5d); [ zenon_intro zenon_H11 | zenon_intro zenon_H5e ]. % 0.44/0.71 exact (zenon_H11 zenon_H9). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H5e); [ zenon_intro zenon_H10 | zenon_intro zenon_H5f ]. % 0.44/0.71 exact (zenon_H10 zenon_Ha). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H5f); [ zenon_intro zenon_H61 | zenon_intro zenon_H60 ]. % 0.44/0.71 exact (zenon_H61 zenon_H55). % 0.44/0.71 apply (zenon_notallex_s (fun T : zenon_U => (((greater (cardinality_at_time (first_movers) T) (zero))/\(greater_or_equal T zenon_TTo_w))->(greater (zero) (growth_rate (first_movers) T)))) zenon_H60); [ zenon_intro zenon_H62; idtac ]. % 0.44/0.71 elim zenon_H62. zenon_intro zenon_TT_x. zenon_intro zenon_H63. % 0.44/0.71 apply (zenon_notimply_s _ _ zenon_H63). zenon_intro zenon_H65. zenon_intro zenon_H64. % 0.44/0.71 apply (zenon_and_s _ _ zenon_H65). zenon_intro zenon_H67. zenon_intro zenon_H66. % 0.44/0.71 generalize (mp_greater_or_equal zenon_TT_x). zenon_intro zenon_H68. % 0.44/0.71 generalize (zenon_H68 zenon_TTo_w). zenon_intro zenon_H69. % 0.44/0.71 apply (zenon_equiv_s _ _ zenon_H69); [ zenon_intro zenon_H6c; zenon_intro zenon_H6b | zenon_intro zenon_H66; zenon_intro zenon_H6a ]. % 0.44/0.71 exact (zenon_H6c zenon_H66). % 0.44/0.71 apply (zenon_or_s _ _ zenon_H6a); [ zenon_intro zenon_H12 | zenon_intro zenon_H20 ]. % 0.44/0.71 generalize (zenon_H53 zenon_TT_x). zenon_intro zenon_H6d. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H6d); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H6f); [ zenon_intro zenon_H11 | zenon_intro zenon_H70 ]. % 0.44/0.71 exact (zenon_H11 zenon_H9). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H70); [ zenon_intro zenon_H10 | zenon_intro zenon_H71 ]. % 0.44/0.71 exact (zenon_H10 zenon_Ha). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H71); [ zenon_intro zenon_Hb | zenon_intro zenon_H14 ]. % 0.44/0.71 apply (zenon_L1_ zenon_TE_m); trivial. % 0.44/0.71 apply (zenon_L2_ zenon_TE_m zenon_TTo_w zenon_TT_x); trivial. % 0.44/0.71 apply zenon_H4b. exists zenon_TT_x. apply NNPP. zenon_intro zenon_H72. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H72); [ zenon_intro zenon_H14 | zenon_intro zenon_H73 ]. % 0.44/0.71 apply (zenon_L2_ zenon_TE_m zenon_TTo_w zenon_TT_x); trivial. % 0.44/0.71 generalize (zenon_H52 zenon_TT_x). zenon_intro zenon_H74. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H74); [ zenon_intro zenon_H76 | zenon_intro zenon_H75 ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H76); [ zenon_intro zenon_H11 | zenon_intro zenon_H77 ]. % 0.44/0.71 exact (zenon_H11 zenon_H9). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H77); [ zenon_intro zenon_H10 | zenon_intro zenon_H78 ]. % 0.44/0.71 exact (zenon_H10 zenon_Ha). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H78); [ zenon_intro zenon_H7a | zenon_intro zenon_H79 ]. % 0.44/0.71 exact (zenon_H7a zenon_H6e). % 0.44/0.71 apply (zenon_notallex_s (fun T : zenon_U => (((greater (cardinality_at_time (first_movers) T) (zero))/\(greater_or_equal T zenon_TT_x))->(greater (zero) (growth_rate (first_movers) T)))) zenon_H79); [ zenon_intro zenon_H7b; idtac ]. % 0.44/0.71 elim zenon_H7b. zenon_intro zenon_TT_br. zenon_intro zenon_H7c. % 0.44/0.71 apply (zenon_notimply_s _ _ zenon_H7c). zenon_intro zenon_H7e. zenon_intro zenon_H7d. % 0.44/0.71 apply (zenon_and_s _ _ zenon_H7e). zenon_intro zenon_H80. zenon_intro zenon_H7f. % 0.44/0.71 generalize (mp_greater_or_equal zenon_TT_br). zenon_intro zenon_H81. % 0.44/0.71 generalize (zenon_H81 zenon_TT_x). zenon_intro zenon_H82. % 0.44/0.71 apply (zenon_equiv_s _ _ zenon_H82); [ zenon_intro zenon_H85; zenon_intro zenon_H84 | zenon_intro zenon_H7f; zenon_intro zenon_H83 ]. % 0.44/0.71 exact (zenon_H85 zenon_H7f). % 0.44/0.71 apply (zenon_or_s _ _ zenon_H83); [ zenon_intro zenon_H29 | zenon_intro zenon_H34 ]. % 0.44/0.71 generalize (mp_non_empty_fm_and_ep zenon_TE_m). zenon_intro zenon_H86. % 0.44/0.71 generalize (zenon_H53 zenon_TT_br). zenon_intro zenon_H87. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H87); [ zenon_intro zenon_H89 | zenon_intro zenon_H88 ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H89); [ zenon_intro zenon_H11 | zenon_intro zenon_H8a ]. % 0.44/0.71 exact (zenon_H11 zenon_H9). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H8a); [ zenon_intro zenon_H10 | zenon_intro zenon_H8b ]. % 0.44/0.71 exact (zenon_H10 zenon_Ha). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H8b); [ zenon_intro zenon_Hb | zenon_intro zenon_H3c ]. % 0.44/0.71 apply (zenon_L1_ zenon_TE_m); trivial. % 0.44/0.71 apply (zenon_L4_ zenon_TE_m zenon_TTo_w zenon_TT_x zenon_TT_br); trivial. % 0.44/0.71 generalize (zenon_H51 zenon_TT_br). zenon_intro zenon_H8c. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H8c); [ zenon_intro zenon_H8e | zenon_intro zenon_H8d ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H8e); [ zenon_intro zenon_H90 | zenon_intro zenon_H8f ]. % 0.44/0.71 generalize (zenon_H86 zenon_TT_br). zenon_intro zenon_H91. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H91); [ zenon_intro zenon_H93 | zenon_intro zenon_H92 ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H93); [ zenon_intro zenon_H11 | zenon_intro zenon_H94 ]. % 0.44/0.71 exact (zenon_H11 zenon_H9). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H94); [ zenon_intro zenon_H96 | zenon_intro zenon_H95 ]. % 0.44/0.71 exact (zenon_H96 zenon_H88). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H95); [ zenon_intro zenon_H98 | zenon_intro zenon_H97 ]. % 0.44/0.71 exact (zenon_H98 zenon_H80). % 0.44/0.71 generalize (t6 zenon_TE_m). zenon_intro zenon_H99. % 0.44/0.71 generalize (zenon_H99 zenon_TT_br). zenon_intro zenon_H9a. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H9a); [ zenon_intro zenon_H9c | zenon_intro zenon_H9b ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H9c); [ zenon_intro zenon_H11 | zenon_intro zenon_H9d ]. % 0.44/0.71 exact (zenon_H11 zenon_H9). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H9d); [ zenon_intro zenon_H96 | zenon_intro zenon_H9e ]. % 0.44/0.71 exact (zenon_H96 zenon_H88). % 0.44/0.71 generalize (mp_greater_or_equal zenon_TT_br). zenon_intro zenon_H81. % 0.44/0.71 generalize (zenon_H81 (appear (efficient_producers) zenon_TE_m)). zenon_intro zenon_H9f. % 0.44/0.71 apply (zenon_equiv_s _ _ zenon_H9f); [ zenon_intro zenon_H9e; zenon_intro zenon_Ha2 | zenon_intro zenon_Ha1; zenon_intro zenon_Ha0 ]. % 0.44/0.71 apply (zenon_notor_s _ _ zenon_Ha2). zenon_intro zenon_H3c. zenon_intro zenon_Ha3. % 0.44/0.71 apply (zenon_L4_ zenon_TE_m zenon_TTo_w zenon_TT_x zenon_TT_br); trivial. % 0.44/0.71 exact (zenon_H9e zenon_Ha1). % 0.44/0.71 exact (zenon_H97 zenon_H9b). % 0.44/0.71 exact (zenon_H90 zenon_H92). % 0.44/0.71 generalize (mp_greater_or_equal zenon_TT_br). zenon_intro zenon_H81. % 0.44/0.71 generalize (zenon_H81 zenon_TTo_w). zenon_intro zenon_Ha4. % 0.44/0.71 apply (zenon_equiv_s _ _ zenon_Ha4); [ zenon_intro zenon_H8f; zenon_intro zenon_Ha7 | zenon_intro zenon_Ha6; zenon_intro zenon_Ha5 ]. % 0.44/0.71 apply (zenon_notor_s _ _ zenon_Ha7). zenon_intro zenon_H2a. zenon_intro zenon_H3f. % 0.44/0.71 apply (zenon_L3_ zenon_TTo_w zenon_TT_x zenon_TT_br); trivial. % 0.44/0.71 exact (zenon_H8f zenon_Ha6). % 0.44/0.71 exact (zenon_H7d zenon_H8d). % 0.44/0.71 generalize (mp_non_empty_fm_and_ep zenon_TE_m). zenon_intro zenon_H86. % 0.44/0.71 generalize (zenon_H51 zenon_TT_br). zenon_intro zenon_H8c. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H8c); [ zenon_intro zenon_H8e | zenon_intro zenon_H8d ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H8e); [ zenon_intro zenon_H90 | zenon_intro zenon_H8f ]. % 0.44/0.71 generalize (zenon_H53 zenon_TT_br). zenon_intro zenon_H87. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H87); [ zenon_intro zenon_H89 | zenon_intro zenon_H88 ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H89); [ zenon_intro zenon_H11 | zenon_intro zenon_H8a ]. % 0.44/0.71 exact (zenon_H11 zenon_H9). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H8a); [ zenon_intro zenon_H10 | zenon_intro zenon_H8b ]. % 0.44/0.71 exact (zenon_H10 zenon_Ha). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H8b); [ zenon_intro zenon_Hb | zenon_intro zenon_H3c ]. % 0.44/0.71 apply (zenon_L1_ zenon_TE_m); trivial. % 0.44/0.71 apply (zenon_L6_ zenon_TE_m zenon_TTo_w zenon_TT_x zenon_TT_br); trivial. % 0.44/0.71 generalize (zenon_H86 zenon_TT_br). zenon_intro zenon_H91. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H91); [ zenon_intro zenon_H93 | zenon_intro zenon_H92 ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H93); [ zenon_intro zenon_H11 | zenon_intro zenon_H94 ]. % 0.44/0.71 exact (zenon_H11 zenon_H9). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H94); [ zenon_intro zenon_H96 | zenon_intro zenon_H95 ]. % 0.44/0.71 exact (zenon_H96 zenon_H88). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H95); [ zenon_intro zenon_H98 | zenon_intro zenon_H97 ]. % 0.44/0.71 exact (zenon_H98 zenon_H80). % 0.44/0.71 generalize (t6 zenon_TE_m). zenon_intro zenon_H99. % 0.44/0.71 generalize (zenon_H99 zenon_TT_br). zenon_intro zenon_H9a. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H9a); [ zenon_intro zenon_H9c | zenon_intro zenon_H9b ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H9c); [ zenon_intro zenon_H11 | zenon_intro zenon_H9d ]. % 0.44/0.71 exact (zenon_H11 zenon_H9). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H9d); [ zenon_intro zenon_H96 | zenon_intro zenon_H9e ]. % 0.44/0.71 exact (zenon_H96 zenon_H88). % 0.44/0.71 generalize (mp_greater_or_equal zenon_TT_br). zenon_intro zenon_H81. % 0.44/0.71 generalize (zenon_H81 (appear (efficient_producers) zenon_TE_m)). zenon_intro zenon_H9f. % 0.44/0.71 apply (zenon_equiv_s _ _ zenon_H9f); [ zenon_intro zenon_H9e; zenon_intro zenon_Ha2 | zenon_intro zenon_Ha1; zenon_intro zenon_Ha0 ]. % 0.44/0.71 apply (zenon_notor_s _ _ zenon_Ha2). zenon_intro zenon_H3c. zenon_intro zenon_Ha3. % 0.44/0.71 apply (zenon_L6_ zenon_TE_m zenon_TTo_w zenon_TT_x zenon_TT_br); trivial. % 0.44/0.71 exact (zenon_H9e zenon_Ha1). % 0.44/0.71 exact (zenon_H97 zenon_H9b). % 0.44/0.71 exact (zenon_H90 zenon_H92). % 0.44/0.71 generalize (mp_greater_or_equal zenon_TT_br). zenon_intro zenon_H81. % 0.44/0.71 generalize (zenon_H81 zenon_TTo_w). zenon_intro zenon_Ha4. % 0.44/0.71 apply (zenon_equiv_s _ _ zenon_Ha4); [ zenon_intro zenon_H8f; zenon_intro zenon_Ha7 | zenon_intro zenon_Ha6; zenon_intro zenon_Ha5 ]. % 0.44/0.71 apply (zenon_notor_s _ _ zenon_Ha7). zenon_intro zenon_H2a. zenon_intro zenon_H3f. % 0.44/0.71 apply (zenon_L5_ zenon_TTo_w zenon_TT_x zenon_TT_br); trivial. % 0.44/0.71 exact (zenon_H8f zenon_Ha6). % 0.44/0.71 exact (zenon_H7d zenon_H8d). % 0.44/0.71 exact (zenon_H73 zenon_H75). % 0.44/0.71 generalize (zenon_H51 zenon_TT_x). zenon_intro zenon_Ha8. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_Ha8); [ zenon_intro zenon_Haa | zenon_intro zenon_Ha9 ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_Haa); [ zenon_intro zenon_Hab | zenon_intro zenon_H6c ]. % 0.44/0.71 generalize (zenon_H53 zenon_TT_x). zenon_intro zenon_H6d. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_H6d); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H6f); [ zenon_intro zenon_H11 | zenon_intro zenon_H70 ]. % 0.44/0.71 exact (zenon_H11 zenon_H9). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H70); [ zenon_intro zenon_H10 | zenon_intro zenon_H71 ]. % 0.44/0.71 exact (zenon_H10 zenon_Ha). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_H71); [ zenon_intro zenon_Hb | zenon_intro zenon_H14 ]. % 0.44/0.71 apply (zenon_L1_ zenon_TE_m); trivial. % 0.44/0.71 apply (zenon_L7_ zenon_TE_m zenon_TTo_w zenon_TT_x); trivial. % 0.44/0.71 generalize (mp_non_empty_fm_and_ep zenon_TE_m). zenon_intro zenon_H86. % 0.44/0.71 generalize (zenon_H86 zenon_TT_x). zenon_intro zenon_Hac. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_Hac); [ zenon_intro zenon_Hae | zenon_intro zenon_Had ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_Hae); [ zenon_intro zenon_H11 | zenon_intro zenon_Haf ]. % 0.44/0.71 exact (zenon_H11 zenon_H9). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_Haf); [ zenon_intro zenon_H7a | zenon_intro zenon_Hb0 ]. % 0.44/0.71 exact (zenon_H7a zenon_H6e). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_Hb0); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hb1 ]. % 0.44/0.71 exact (zenon_Hb2 zenon_H67). % 0.44/0.71 generalize (t6 zenon_TE_m). zenon_intro zenon_H99. % 0.44/0.71 generalize (zenon_H99 zenon_TT_x). zenon_intro zenon_Hb3. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_Hb3); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hb4 ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_Hb5); [ zenon_intro zenon_H11 | zenon_intro zenon_Hb6 ]. % 0.44/0.71 exact (zenon_H11 zenon_H9). % 0.44/0.71 apply (zenon_notand_s _ _ zenon_Hb6); [ zenon_intro zenon_H7a | zenon_intro zenon_Hb7 ]. % 0.44/0.71 exact (zenon_H7a zenon_H6e). % 0.44/0.71 generalize (mp_greater_or_equal zenon_TT_x). zenon_intro zenon_H68. % 0.44/0.71 generalize (zenon_H68 (appear (efficient_producers) zenon_TE_m)). zenon_intro zenon_Hb8. % 0.44/0.71 apply (zenon_equiv_s _ _ zenon_Hb8); [ zenon_intro zenon_Hb7; zenon_intro zenon_Hbb | zenon_intro zenon_Hba; zenon_intro zenon_Hb9 ]. % 0.44/0.71 apply (zenon_notor_s _ _ zenon_Hbb). zenon_intro zenon_H14. zenon_intro zenon_Hbc. % 0.44/0.71 apply (zenon_L7_ zenon_TE_m zenon_TTo_w zenon_TT_x); trivial. % 0.44/0.71 exact (zenon_Hb7 zenon_Hba). % 0.44/0.71 exact (zenon_Hb1 zenon_Hb4). % 0.44/0.71 exact (zenon_Hab zenon_Had). % 0.44/0.71 generalize (mp_greater_or_equal zenon_TT_x). zenon_intro zenon_H68. % 0.44/0.71 generalize (zenon_H68 zenon_TTo_w). zenon_intro zenon_H69. % 0.44/0.71 apply (zenon_equiv_s _ _ zenon_H69); [ zenon_intro zenon_H6c; zenon_intro zenon_H6b | zenon_intro zenon_H66; zenon_intro zenon_H6a ]. % 0.44/0.71 apply (zenon_notor_s _ _ zenon_H6b). zenon_intro zenon_H1a. zenon_intro zenon_H1b. % 0.44/0.71 exact (zenon_H1b zenon_H20). % 0.44/0.71 exact (zenon_H6c zenon_H66). % 0.44/0.71 exact (zenon_H64 zenon_Ha9). % 0.44/0.71 exact (zenon_H5a zenon_H5c). % 0.44/0.71 apply zenon_H48. zenon_intro zenon_Tx_hh. apply NNPP. zenon_intro zenon_Hbe. % 0.44/0.71 apply zenon_Hbe. zenon_intro zenon_Ty_hj. apply NNPP. zenon_intro zenon_Hc0. % 0.44/0.71 apply zenon_Hc0. zenon_intro zenon_Tz_hl. apply NNPP. zenon_intro zenon_Hc2. % 0.44/0.71 apply (zenon_notimply_s _ _ zenon_Hc2). zenon_intro zenon_Hc4. zenon_intro zenon_Hc3. % 0.44/0.71 apply (zenon_notimply_s _ _ zenon_Hc3). zenon_intro zenon_Hc6. zenon_intro zenon_Hc5. % 0.44/0.71 generalize (mp_greater_transitivity zenon_Tx_hh). zenon_intro zenon_Hc7. % 0.44/0.71 generalize (zenon_Hc7 zenon_Ty_hj). zenon_intro zenon_Hc8. % 0.44/0.71 generalize (zenon_Hc8 zenon_Tz_hl). zenon_intro zenon_Hc9. % 0.44/0.71 apply (zenon_imply_s _ _ zenon_Hc9); [ zenon_intro zenon_Hcb | zenon_intro zenon_Hca ]. % 0.44/0.71 apply (zenon_notand_s _ _ zenon_Hcb); [ zenon_intro zenon_Hcd | zenon_intro zenon_Hcc ]. % 0.44/0.71 exact (zenon_Hcd zenon_Hc4). % 0.44/0.71 exact (zenon_Hcc zenon_Hc6). % 0.44/0.71 exact (zenon_Hc5 zenon_Hca). % 0.44/0.71 Qed. % 0.44/0.71 % SZS output end Proof % 0.44/0.71 (* END-PROOF *) % 0.44/0.71 nodes searched: 6901 % 0.44/0.71 max branch formulas: 593 % 0.44/0.71 proof nodes created: 1339 % 0.44/0.71 formulas created: 9117 % 0.44/0.71 %------------------------------------------------------------------------------