%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT051+1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n005.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:23 AM UTC 2026 % Result : Theorem 39.94s 40.22s % Output : Proof 39.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT051+1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : run_zenon %s %d % 0.10/0.33 % Computer : n005.cluster.edu % 0.10/0.33 % Model : x86_64 x86_64 % 0.10/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.33 % Memory : 8046.5625MB % 0.10/0.33 % OS : Linux 6.8.0-71-generic % 0.10/0.33 % CPULimit : 300 % 0.10/0.33 % WCLimit : 300 % 0.10/0.33 % DateTime : Mon Sep 7 13:19:20 UTC 2026 % 0.10/0.34 % CPUTime : % 39.94/40.22 (* PROOF-FOUND *) % 39.94/40.22 % SZS status Theorem % 39.94/40.22 (* BEGIN-PROOF *) % 39.94/40.22 % SZS output start Proof % 39.94/40.22 Theorem theorem_4 : (forall X : zenon_U, (forall T0 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (forall T3 : zenon_U, (((organization X)/\((has_endowment X)/\((smaller_or_equal (age X T0) (age X T1))/\((smaller_or_equal (age X T1) (eta))/\((greater (age X T2) (eta))/\(greater (age X T3) (age X T2)))))))->((greater (hazard_of_mortality X T3) (hazard_of_mortality X T2))/\((greater (hazard_of_mortality X T2) (hazard_of_mortality X T1))/\((hazard_of_mortality X T1) = (hazard_of_mortality X T0)))))))))). % 39.94/40.22 Proof. % 39.94/40.22 assert (zenon_L1_ : forall (zenon_TT3_t : zenon_U) (zenon_TX_u : zenon_U), (~(greater_or_equal (capability zenon_TX_u zenon_TT3_t) (capability zenon_TX_u zenon_TT3_t))) -> False). % 39.94/40.22 do 2 intro. intros zenon_H12. % 39.94/40.22 generalize (definition_greater_or_equal (capability zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H15. % 39.94/40.22 generalize (zenon_H15 (capability zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H16. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H16); [ zenon_intro zenon_H12; zenon_intro zenon_H19 | zenon_intro zenon_H18; zenon_intro zenon_H17 ]. % 39.94/40.22 apply (zenon_notor_s _ _ zenon_H19). zenon_intro zenon_H1b. zenon_intro zenon_H1a. % 39.94/40.22 apply zenon_H1a. apply refl_equal. % 39.94/40.22 exact (zenon_H12 zenon_H18). % 39.94/40.22 (* end of lemma zenon_L1_ *) % 39.94/40.22 assert (zenon_L2_ : forall (zenon_TT3_t : zenon_U) (zenon_TT2_bg : zenon_U) (zenon_TX_u : zenon_U), (forall Y : zenon_U, ((smaller (stock_of_knowledge zenon_TX_u zenon_TT2_bg) Y)\/(((stock_of_knowledge zenon_TX_u zenon_TT2_bg) = Y)\/(greater (stock_of_knowledge zenon_TX_u zenon_TT2_bg) Y)))) -> (~(greater (stock_of_knowledge zenon_TX_u zenon_TT3_t) (stock_of_knowledge zenon_TX_u zenon_TT2_bg))) -> (~((stock_of_knowledge zenon_TX_u zenon_TT3_t) = (stock_of_knowledge zenon_TX_u zenon_TT2_bg))) -> (~(greater (stock_of_knowledge zenon_TX_u zenon_TT2_bg) (stock_of_knowledge zenon_TX_u zenon_TT3_t))) -> False). % 39.94/40.22 do 3 intro. intros zenon_H1c zenon_H1d zenon_H1e zenon_H1f. % 39.94/40.22 generalize (zenon_H1c (stock_of_knowledge zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H21. % 39.94/40.22 apply (zenon_or_s _ _ zenon_H21); [ zenon_intro zenon_H23 | zenon_intro zenon_H22 ]. % 39.94/40.22 generalize (definition_smaller (stock_of_knowledge zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H24. % 39.94/40.22 generalize (zenon_H24 (stock_of_knowledge zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H25. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H25); [ zenon_intro zenon_H27; zenon_intro zenon_H1d | zenon_intro zenon_H23; zenon_intro zenon_H26 ]. % 39.94/40.22 exact (zenon_H27 zenon_H23). % 39.94/40.22 exact (zenon_H1d zenon_H26). % 39.94/40.22 apply (zenon_or_s _ _ zenon_H22); [ zenon_intro zenon_H29 | zenon_intro zenon_H28 ]. % 39.94/40.22 apply zenon_H1e. apply sym_equal. exact zenon_H29. % 39.94/40.22 exact (zenon_H1f zenon_H28). % 39.94/40.22 (* end of lemma zenon_L2_ *) % 39.94/40.22 assert (zenon_L3_ : forall (zenon_TT3_t : zenon_U) (zenon_TT2_bg : zenon_U) (zenon_TX_u : zenon_U), ((stock_of_knowledge zenon_TX_u zenon_TT2_bg) = (stock_of_knowledge zenon_TX_u zenon_E)) -> (forall Y : zenon_U, ((smaller (stock_of_knowledge zenon_TX_u zenon_TT2_bg) Y)\/(((stock_of_knowledge zenon_TX_u zenon_TT2_bg) = Y)\/(greater (stock_of_knowledge zenon_TX_u zenon_TT2_bg) Y)))) -> (~(greater (stock_of_knowledge zenon_TX_u zenon_TT2_bg) (stock_of_knowledge zenon_TX_u zenon_TT2_bg))) -> (organization zenon_TX_u) -> (forall T : zenon_U, ((organization zenon_TX_u)->((stock_of_knowledge zenon_TX_u T) = (stock_of_knowledge zenon_TX_u zenon_E)))) -> (~(smaller_or_equal (stock_of_knowledge zenon_TX_u zenon_TT3_t) (stock_of_knowledge zenon_TX_u zenon_TT2_bg))) -> False). % 39.94/40.22 do 3 intro. intros zenon_H2a zenon_H1c zenon_H2b zenon_H2c zenon_H2d zenon_H2e. % 39.94/40.22 generalize (definition_smaller_or_equal (stock_of_knowledge zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H2f. % 39.94/40.22 generalize (zenon_H2f (stock_of_knowledge zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H30. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H30); [ zenon_intro zenon_H2e; zenon_intro zenon_H33 | zenon_intro zenon_H32; zenon_intro zenon_H31 ]. % 39.94/40.22 apply (zenon_notor_s _ _ zenon_H33). zenon_intro zenon_H34. zenon_intro zenon_H1e. % 39.94/40.22 generalize (definition_smaller (stock_of_knowledge zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H35. % 39.94/40.22 generalize (zenon_H35 (stock_of_knowledge zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H36. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H36); [ zenon_intro zenon_H34; zenon_intro zenon_H1f | zenon_intro zenon_H37; zenon_intro zenon_H28 ]. % 39.94/40.22 generalize (zenon_H2d zenon_TT3_t). zenon_intro zenon_H38. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H38); [ zenon_intro zenon_H3a | zenon_intro zenon_H39 ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 elim (classic ((stock_of_knowledge zenon_TX_u zenon_E) = (stock_of_knowledge zenon_TX_u zenon_TT3_t))); [ zenon_intro zenon_H3b | zenon_intro zenon_H3c ]. % 39.94/40.22 elim (classic (greater (stock_of_knowledge zenon_TX_u zenon_TT3_t) (stock_of_knowledge zenon_TX_u zenon_TT2_bg))); [ zenon_intro zenon_H26 | zenon_intro zenon_H1d ]. % 39.94/40.22 elim (classic (greater (stock_of_knowledge zenon_TX_u zenon_E) (stock_of_knowledge zenon_TX_u zenon_TT2_bg))); [ zenon_intro zenon_H3d | zenon_intro zenon_H3e ]. % 39.94/40.22 cut ((greater (stock_of_knowledge zenon_TX_u zenon_E) (stock_of_knowledge zenon_TX_u zenon_TT2_bg)) = (greater (stock_of_knowledge zenon_TX_u zenon_TT2_bg) (stock_of_knowledge zenon_TX_u zenon_TT2_bg))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H2b. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H3d. % 39.94/40.22 cut (((stock_of_knowledge zenon_TX_u zenon_TT2_bg) = (stock_of_knowledge zenon_TX_u zenon_TT2_bg))); [idtac | apply NNPP; zenon_intro zenon_H3f]. % 39.94/40.22 cut (((stock_of_knowledge zenon_TX_u zenon_E) = (stock_of_knowledge zenon_TX_u zenon_TT2_bg))); [idtac | apply NNPP; zenon_intro zenon_H40]. % 39.94/40.22 congruence. % 39.94/40.22 elim (classic ((stock_of_knowledge zenon_TX_u zenon_TT2_bg) = (stock_of_knowledge zenon_TX_u zenon_TT2_bg))); [ zenon_intro zenon_H41 | zenon_intro zenon_H3f ]. % 39.94/40.22 cut (((stock_of_knowledge zenon_TX_u zenon_TT2_bg) = (stock_of_knowledge zenon_TX_u zenon_TT2_bg)) = ((stock_of_knowledge zenon_TX_u zenon_E) = (stock_of_knowledge zenon_TX_u zenon_TT2_bg))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H40. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H41. % 39.94/40.22 cut (((stock_of_knowledge zenon_TX_u zenon_TT2_bg) = (stock_of_knowledge zenon_TX_u zenon_TT2_bg))); [idtac | apply NNPP; zenon_intro zenon_H3f]. % 39.94/40.22 cut (((stock_of_knowledge zenon_TX_u zenon_TT2_bg) = (stock_of_knowledge zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H42]. % 39.94/40.22 congruence. % 39.94/40.22 exact (zenon_H42 zenon_H2a). % 39.94/40.22 apply zenon_H3f. apply refl_equal. % 39.94/40.22 apply zenon_H3f. apply refl_equal. % 39.94/40.22 apply zenon_H3f. apply refl_equal. % 39.94/40.22 cut ((greater (stock_of_knowledge zenon_TX_u zenon_TT3_t) (stock_of_knowledge zenon_TX_u zenon_TT2_bg)) = (greater (stock_of_knowledge zenon_TX_u zenon_E) (stock_of_knowledge zenon_TX_u zenon_TT2_bg))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H3e. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H26. % 39.94/40.22 cut (((stock_of_knowledge zenon_TX_u zenon_TT2_bg) = (stock_of_knowledge zenon_TX_u zenon_TT2_bg))); [idtac | apply NNPP; zenon_intro zenon_H3f]. % 39.94/40.22 cut (((stock_of_knowledge zenon_TX_u zenon_TT3_t) = (stock_of_knowledge zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H43]. % 39.94/40.22 congruence. % 39.94/40.22 elim (classic ((stock_of_knowledge zenon_TX_u zenon_E) = (stock_of_knowledge zenon_TX_u zenon_E))); [ zenon_intro zenon_H44 | zenon_intro zenon_H45 ]. % 39.94/40.22 cut (((stock_of_knowledge zenon_TX_u zenon_E) = (stock_of_knowledge zenon_TX_u zenon_E)) = ((stock_of_knowledge zenon_TX_u zenon_TT3_t) = (stock_of_knowledge zenon_TX_u zenon_E))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H43. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H44. % 39.94/40.22 cut (((stock_of_knowledge zenon_TX_u zenon_E) = (stock_of_knowledge zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H45]. % 39.94/40.22 cut (((stock_of_knowledge zenon_TX_u zenon_E) = (stock_of_knowledge zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_H3c]. % 39.94/40.22 congruence. % 39.94/40.22 exact (zenon_H3c zenon_H3b). % 39.94/40.22 apply zenon_H45. apply refl_equal. % 39.94/40.22 apply zenon_H45. apply refl_equal. % 39.94/40.22 apply zenon_H3f. apply refl_equal. % 39.94/40.22 apply (zenon_L2_ zenon_TT3_t zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 elim (classic ((stock_of_knowledge zenon_TX_u zenon_TT3_t) = (stock_of_knowledge zenon_TX_u zenon_TT3_t))); [ zenon_intro zenon_H46 | zenon_intro zenon_H47 ]. % 39.94/40.22 cut (((stock_of_knowledge zenon_TX_u zenon_TT3_t) = (stock_of_knowledge zenon_TX_u zenon_TT3_t)) = ((stock_of_knowledge zenon_TX_u zenon_E) = (stock_of_knowledge zenon_TX_u zenon_TT3_t))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H3c. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H46. % 39.94/40.22 cut (((stock_of_knowledge zenon_TX_u zenon_TT3_t) = (stock_of_knowledge zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_H47]. % 39.94/40.22 cut (((stock_of_knowledge zenon_TX_u zenon_TT3_t) = (stock_of_knowledge zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H43]. % 39.94/40.22 congruence. % 39.94/40.22 exact (zenon_H43 zenon_H39). % 39.94/40.22 apply zenon_H47. apply refl_equal. % 39.94/40.22 apply zenon_H47. apply refl_equal. % 39.94/40.22 exact (zenon_H34 zenon_H37). % 39.94/40.22 exact (zenon_H2e zenon_H32). % 39.94/40.22 (* end of lemma zenon_L3_ *) % 39.94/40.22 assert (zenon_L4_ : forall (zenon_TT3_t : zenon_U) (zenon_TT2_bg : zenon_U) (zenon_TX_u : zenon_U), (forall T : zenon_U, (((organization zenon_TX_u)/\(greater (age zenon_TX_u T) (age zenon_TX_u zenon_TT2_bg)))->(greater (internal_friction zenon_TX_u T) (internal_friction zenon_TX_u zenon_TT2_bg)))) -> (organization zenon_TX_u) -> (greater (age zenon_TX_u zenon_TT3_t) (age zenon_TX_u zenon_TT2_bg)) -> (~(greater (internal_friction zenon_TX_u zenon_TT3_t) (internal_friction zenon_TX_u zenon_TT2_bg))) -> False). % 39.94/40.22 do 3 intro. intros zenon_H48 zenon_H2c zenon_H49 zenon_H4a. % 39.94/40.22 generalize (zenon_H48 zenon_TT3_t). zenon_intro zenon_H4b. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H4b); [ zenon_intro zenon_H4d | zenon_intro zenon_H4c ]. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H4d); [ zenon_intro zenon_H3a | zenon_intro zenon_H4e ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 exact (zenon_H4e zenon_H49). % 39.94/40.22 exact (zenon_H4a zenon_H4c). % 39.94/40.22 (* end of lemma zenon_L4_ *) % 39.94/40.22 assert (zenon_L5_ : forall (zenon_TT3_t : zenon_U) (zenon_TX_u : zenon_U), (forall T : zenon_U, ((organization zenon_TX_u)->((external_ties zenon_TX_u T) = (external_ties zenon_TX_u zenon_E)))) -> (organization zenon_TX_u) -> (~((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_TT3_t))) -> False). % 39.94/40.22 do 2 intro. intros zenon_H4f zenon_H2c zenon_H50. % 39.94/40.22 generalize (zenon_H4f zenon_TT3_t). zenon_intro zenon_H51. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H51); [ zenon_intro zenon_H3a | zenon_intro zenon_H52 ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 apply zenon_H50. apply sym_equal. exact zenon_H52. % 39.94/40.22 (* end of lemma zenon_L5_ *) % 39.94/40.22 assert (zenon_L6_ : forall (zenon_TT3_t : zenon_U) (zenon_TT2_bg : zenon_U) (zenon_TX_u : zenon_U), (forall Y : zenon_U, ((smaller (external_ties zenon_TX_u zenon_TT2_bg) Y)\/(((external_ties zenon_TX_u zenon_TT2_bg) = Y)\/(greater (external_ties zenon_TX_u zenon_TT2_bg) Y)))) -> (~(greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_TT2_bg))) -> (~((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT2_bg))) -> (~(greater (external_ties zenon_TX_u zenon_TT2_bg) (external_ties zenon_TX_u zenon_TT3_t))) -> False). % 39.94/40.22 do 3 intro. intros zenon_H53 zenon_H54 zenon_H55 zenon_H56. % 39.94/40.22 generalize (zenon_H53 (external_ties zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H57. % 39.94/40.22 apply (zenon_or_s _ _ zenon_H57); [ zenon_intro zenon_H59 | zenon_intro zenon_H58 ]. % 39.94/40.22 generalize (definition_smaller (external_ties zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H5a. % 39.94/40.22 generalize (zenon_H5a (external_ties zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H5b. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H5b); [ zenon_intro zenon_H5d; zenon_intro zenon_H54 | zenon_intro zenon_H59; zenon_intro zenon_H5c ]. % 39.94/40.22 exact (zenon_H5d zenon_H59). % 39.94/40.22 exact (zenon_H54 zenon_H5c). % 39.94/40.22 apply (zenon_or_s _ _ zenon_H58); [ zenon_intro zenon_H5f | zenon_intro zenon_H5e ]. % 39.94/40.22 apply zenon_H55. apply sym_equal. exact zenon_H5f. % 39.94/40.22 exact (zenon_H56 zenon_H5e). % 39.94/40.22 (* end of lemma zenon_L6_ *) % 39.94/40.22 assert (zenon_L7_ : forall (zenon_TT3_t : zenon_U) (zenon_TT2_bg : zenon_U) (zenon_TX_u : zenon_U), (forall T : zenon_U, ((organization zenon_TX_u)->((external_ties zenon_TX_u T) = (external_ties zenon_TX_u zenon_E)))) -> (organization zenon_TX_u) -> ((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E)) -> (~(greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_TT3_t))) -> (forall Y : zenon_U, ((smaller (external_ties zenon_TX_u zenon_TT2_bg) Y)\/(((external_ties zenon_TX_u zenon_TT2_bg) = Y)\/(greater (external_ties zenon_TX_u zenon_TT2_bg) Y)))) -> (~((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT2_bg))) -> (~(greater (external_ties zenon_TX_u zenon_TT2_bg) (external_ties zenon_TX_u zenon_TT3_t))) -> False). % 39.94/40.22 do 3 intro. intros zenon_H4f zenon_H2c zenon_H60 zenon_H61 zenon_H53 zenon_H55 zenon_H56. % 39.94/40.22 elim (classic (greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_TT2_bg))); [ zenon_intro zenon_H5c | zenon_intro zenon_H54 ]. % 39.94/40.22 elim (classic (greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_E))); [ zenon_intro zenon_H62 | zenon_intro zenon_H63 ]. % 39.94/40.22 cut ((greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_E)) = (greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_TT3_t))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H61. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H62. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 39.94/40.22 congruence. % 39.94/40.22 apply zenon_H64. apply refl_equal. % 39.94/40.22 apply (zenon_L5_ zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 cut ((greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_TT2_bg)) = (greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_E))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H63. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H5c. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 39.94/40.22 congruence. % 39.94/40.22 apply zenon_H64. apply refl_equal. % 39.94/40.22 exact (zenon_H65 zenon_H60). % 39.94/40.22 apply (zenon_L6_ zenon_TT3_t zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 (* end of lemma zenon_L7_ *) % 39.94/40.22 assert (zenon_L8_ : forall (zenon_TT3_t : zenon_U) (zenon_TT2_bg : zenon_U) (zenon_TX_u : zenon_U), (forall Y : zenon_U, ((smaller (external_ties zenon_TX_u zenon_TT2_bg) Y)\/(((external_ties zenon_TX_u zenon_TT2_bg) = Y)\/(greater (external_ties zenon_TX_u zenon_TT2_bg) Y)))) -> (~((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT2_bg))) -> (forall T : zenon_U, ((organization zenon_TX_u)->((external_ties zenon_TX_u T) = (external_ties zenon_TX_u zenon_E)))) -> (organization zenon_TX_u) -> (~(greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_TT3_t))) -> (~(greater (external_ties zenon_TX_u zenon_E) (external_ties zenon_TX_u zenon_TT3_t))) -> ((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E)) -> False). % 39.94/40.22 do 3 intro. intros zenon_H53 zenon_H55 zenon_H4f zenon_H2c zenon_H61 zenon_H66 zenon_H60. % 39.94/40.22 elim (classic ((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_TT2_bg))); [ zenon_intro zenon_H67 | zenon_intro zenon_H68 ]. % 39.94/40.22 elim (classic (greater (external_ties zenon_TX_u zenon_TT2_bg) (external_ties zenon_TX_u zenon_TT3_t))); [ zenon_intro zenon_H5e | zenon_intro zenon_H56 ]. % 39.94/40.22 cut ((greater (external_ties zenon_TX_u zenon_TT2_bg) (external_ties zenon_TX_u zenon_TT3_t)) = (greater (external_ties zenon_TX_u zenon_E) (external_ties zenon_TX_u zenon_TT3_t))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H66. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H5e. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 39.94/40.22 congruence. % 39.94/40.22 elim (classic ((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_E))); [ zenon_intro zenon_H69 | zenon_intro zenon_H6a ]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_E)) = ((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H65. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H69. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H6a]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_TT2_bg))); [idtac | apply NNPP; zenon_intro zenon_H68]. % 39.94/40.22 congruence. % 39.94/40.22 exact (zenon_H68 zenon_H67). % 39.94/40.22 apply zenon_H6a. apply refl_equal. % 39.94/40.22 apply zenon_H6a. apply refl_equal. % 39.94/40.22 apply zenon_H64. apply refl_equal. % 39.94/40.22 apply (zenon_L7_ zenon_TT3_t zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 elim (classic ((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_TT2_bg))); [ zenon_intro zenon_H6b | zenon_intro zenon_H6c ]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_TT2_bg)) = ((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_TT2_bg))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H68. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H6b. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_TT2_bg))); [idtac | apply NNPP; zenon_intro zenon_H6c]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 39.94/40.22 congruence. % 39.94/40.22 exact (zenon_H65 zenon_H60). % 39.94/40.22 apply zenon_H6c. apply refl_equal. % 39.94/40.22 apply zenon_H6c. apply refl_equal. % 39.94/40.22 (* end of lemma zenon_L8_ *) % 39.94/40.22 assert (zenon_L9_ : forall (zenon_TT2_bg : zenon_U) (zenon_TT3_t : zenon_U) (zenon_TX_u : zenon_U), (~((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT2_bg))) -> (~(greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_TT2_bg))) -> (forall Y : zenon_U, ((smaller (external_ties zenon_TX_u zenon_TT2_bg) Y)\/(((external_ties zenon_TX_u zenon_TT2_bg) = Y)\/(greater (external_ties zenon_TX_u zenon_TT2_bg) Y)))) -> (forall T : zenon_U, ((organization zenon_TX_u)->((external_ties zenon_TX_u T) = (external_ties zenon_TX_u zenon_E)))) -> (organization zenon_TX_u) -> (~(greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_TT3_t))) -> ((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E)) -> False). % 39.94/40.22 do 3 intro. intros zenon_H55 zenon_H54 zenon_H53 zenon_H4f zenon_H2c zenon_H61 zenon_H60. % 39.94/40.22 elim (classic ((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_TT2_bg))); [ zenon_intro zenon_H67 | zenon_intro zenon_H68 ]. % 39.94/40.22 elim (classic (greater (external_ties zenon_TX_u zenon_TT2_bg) (external_ties zenon_TX_u zenon_TT3_t))); [ zenon_intro zenon_H5e | zenon_intro zenon_H56 ]. % 39.94/40.22 elim (classic (greater (external_ties zenon_TX_u zenon_E) (external_ties zenon_TX_u zenon_TT3_t))); [ zenon_intro zenon_H6d | zenon_intro zenon_H66 ]. % 39.94/40.22 cut ((greater (external_ties zenon_TX_u zenon_E) (external_ties zenon_TX_u zenon_TT3_t)) = (greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_TT3_t))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H61. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H6d. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 39.94/40.22 congruence. % 39.94/40.22 elim (classic ((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT3_t))); [ zenon_intro zenon_H6e | zenon_intro zenon_H64 ]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT3_t)) = ((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_TT3_t))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H50. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H6e. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H6f]. % 39.94/40.22 congruence. % 39.94/40.22 generalize (zenon_H4f zenon_TT3_t). zenon_intro zenon_H51. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H51); [ zenon_intro zenon_H3a | zenon_intro zenon_H52 ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 exact (zenon_H6f zenon_H52). % 39.94/40.22 apply zenon_H64. apply refl_equal. % 39.94/40.22 apply zenon_H64. apply refl_equal. % 39.94/40.22 apply zenon_H64. apply refl_equal. % 39.94/40.22 cut ((greater (external_ties zenon_TX_u zenon_TT2_bg) (external_ties zenon_TX_u zenon_TT3_t)) = (greater (external_ties zenon_TX_u zenon_E) (external_ties zenon_TX_u zenon_TT3_t))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H66. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H5e. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 39.94/40.22 congruence. % 39.94/40.22 elim (classic ((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_E))); [ zenon_intro zenon_H69 | zenon_intro zenon_H6a ]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_E)) = ((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H65. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H69. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H6a]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_TT2_bg))); [idtac | apply NNPP; zenon_intro zenon_H68]. % 39.94/40.22 congruence. % 39.94/40.22 exact (zenon_H68 zenon_H67). % 39.94/40.22 apply zenon_H6a. apply refl_equal. % 39.94/40.22 apply zenon_H6a. apply refl_equal. % 39.94/40.22 apply zenon_H64. apply refl_equal. % 39.94/40.22 apply (zenon_L6_ zenon_TT3_t zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 elim (classic ((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_TT2_bg))); [ zenon_intro zenon_H6b | zenon_intro zenon_H6c ]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_TT2_bg)) = ((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_TT2_bg))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H68. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H6b. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_TT2_bg))); [idtac | apply NNPP; zenon_intro zenon_H6c]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 39.94/40.22 congruence. % 39.94/40.22 exact (zenon_H65 zenon_H60). % 39.94/40.22 apply zenon_H6c. apply refl_equal. % 39.94/40.22 apply zenon_H6c. apply refl_equal. % 39.94/40.22 (* end of lemma zenon_L9_ *) % 39.94/40.22 assert (zenon_L10_ : forall (zenon_TT2_bg : zenon_U) (zenon_TT3_t : zenon_U) (zenon_TX_u : zenon_U), (forall T0 : zenon_U, (forall T : zenon_U, ((organization zenon_TX_u)->(((greater (external_ties zenon_TX_u T) (external_ties zenon_TX_u T0))->(greater (position zenon_TX_u T) (position zenon_TX_u T0)))/\(((external_ties zenon_TX_u T) = (external_ties zenon_TX_u T0))->((position zenon_TX_u T) = (position zenon_TX_u T0))))))) -> (~(greater (position zenon_TX_u zenon_TT3_t) (position zenon_TX_u zenon_TT3_t))) -> (forall T : zenon_U, ((organization zenon_TX_u)->((external_ties zenon_TX_u T) = (external_ties zenon_TX_u zenon_E)))) -> (forall Y : zenon_U, ((smaller (external_ties zenon_TX_u zenon_TT2_bg) Y)\/(((external_ties zenon_TX_u zenon_TT2_bg) = Y)\/(greater (external_ties zenon_TX_u zenon_TT2_bg) Y)))) -> (~(greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_TT2_bg))) -> (~((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT2_bg))) -> ((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E)) -> (organization zenon_TX_u) -> False). % 39.94/40.22 do 3 intro. intros zenon_H70 zenon_H71 zenon_H4f zenon_H53 zenon_H54 zenon_H55 zenon_H60 zenon_H2c. % 39.94/40.22 generalize (zenon_H70 zenon_TT3_t). zenon_intro zenon_H72. % 39.94/40.22 generalize (zenon_H72 zenon_TT3_t). zenon_intro zenon_H73. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H73); [ zenon_intro zenon_H3a | zenon_intro zenon_H74 ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 apply (zenon_and_s _ _ zenon_H74). zenon_intro zenon_H76. zenon_intro zenon_H75. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H76); [ zenon_intro zenon_H61 | zenon_intro zenon_H77 ]. % 39.94/40.22 apply (zenon_L9_ zenon_TT2_bg zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 exact (zenon_H71 zenon_H77). % 39.94/40.22 (* end of lemma zenon_L10_ *) % 39.94/40.22 assert (zenon_L11_ : forall (zenon_TT2_bg : zenon_U) (zenon_TT3_t : zenon_U) (zenon_TX_u : zenon_U), ((position zenon_TX_u zenon_TT3_t) = (position zenon_TX_u zenon_TT2_bg)) -> (~(greater_or_equal (position zenon_TX_u zenon_TT2_bg) (position zenon_TX_u zenon_TT3_t))) -> False). % 39.94/40.22 do 3 intro. intros zenon_H78 zenon_H79. % 39.94/40.22 generalize (definition_greater_or_equal (position zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H7a. % 39.94/40.22 generalize (zenon_H7a (position zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H7b. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H7b); [ zenon_intro zenon_H79; zenon_intro zenon_H7e | zenon_intro zenon_H7d; zenon_intro zenon_H7c ]. % 39.94/40.22 apply (zenon_notor_s _ _ zenon_H7e). zenon_intro zenon_H80. zenon_intro zenon_H7f. % 39.94/40.22 apply zenon_H7f. apply sym_equal. exact zenon_H78. % 39.94/40.22 exact (zenon_H79 zenon_H7d). % 39.94/40.22 (* end of lemma zenon_L11_ *) % 39.94/40.22 assert (zenon_L12_ : forall (zenon_TT3_t : zenon_U) (zenon_TT2_bg : zenon_U) (zenon_TX_u : zenon_U), (smaller (hazard_of_mortality zenon_TX_u zenon_TT2_bg) (hazard_of_mortality zenon_TX_u zenon_TT3_t)) -> (~(greater (hazard_of_mortality zenon_TX_u zenon_TT3_t) (hazard_of_mortality zenon_TX_u zenon_TT2_bg))) -> False). % 39.94/40.22 do 3 intro. intros zenon_H81 zenon_H82. % 39.94/40.22 generalize (definition_smaller (hazard_of_mortality zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H83. % 39.94/40.22 generalize (zenon_H83 (hazard_of_mortality zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H84. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H84); [ zenon_intro zenon_H86; zenon_intro zenon_H82 | zenon_intro zenon_H81; zenon_intro zenon_H85 ]. % 39.94/40.22 exact (zenon_H86 zenon_H81). % 39.94/40.22 exact (zenon_H82 zenon_H85). % 39.94/40.22 (* end of lemma zenon_L12_ *) % 39.94/40.22 assert (zenon_L13_ : forall (zenon_TT2_bg : zenon_U) (zenon_TT3_t : zenon_U) (zenon_TX_u : zenon_U), (forall T : zenon_U, (((organization zenon_TX_u)/\((~(has_immunity zenon_TX_u zenon_TT3_t))/\(~(has_immunity zenon_TX_u T))))->((((greater (capability zenon_TX_u T) (capability zenon_TX_u zenon_TT3_t))/\(greater_or_equal (position zenon_TX_u T) (position zenon_TX_u zenon_TT3_t)))->(smaller (hazard_of_mortality zenon_TX_u T) (hazard_of_mortality zenon_TX_u zenon_TT3_t)))/\((((greater_or_equal (capability zenon_TX_u T) (capability zenon_TX_u zenon_TT3_t))/\(greater (position zenon_TX_u T) (position zenon_TX_u zenon_TT3_t)))->(smaller (hazard_of_mortality zenon_TX_u T) (hazard_of_mortality zenon_TX_u zenon_TT3_t)))/\((((capability zenon_TX_u T) = (capability zenon_TX_u zenon_TT3_t))/\((position zenon_TX_u T) = (position zenon_TX_u zenon_TT3_t)))->((hazard_of_mortality zenon_TX_u T) = (hazard_of_mortality zenon_TX_u zenon_TT3_t))))))) -> (organization zenon_TX_u) -> (~(has_immunity zenon_TX_u zenon_TT3_t)) -> (~(has_immunity zenon_TX_u zenon_TT2_bg)) -> (greater (capability zenon_TX_u zenon_TT2_bg) (capability zenon_TX_u zenon_TT3_t)) -> ((position zenon_TX_u zenon_TT3_t) = (position zenon_TX_u zenon_TT2_bg)) -> (~(greater (hazard_of_mortality zenon_TX_u zenon_TT3_t) (hazard_of_mortality zenon_TX_u zenon_TT2_bg))) -> False). % 39.94/40.22 do 3 intro. intros zenon_H87 zenon_H2c zenon_H88 zenon_H89 zenon_H8a zenon_H78 zenon_H82. % 39.94/40.22 generalize (zenon_H87 zenon_TT2_bg). zenon_intro zenon_H8b. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H8b); [ zenon_intro zenon_H8d | zenon_intro zenon_H8c ]. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H8d); [ zenon_intro zenon_H3a | zenon_intro zenon_H8e ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H8e); [ zenon_intro zenon_H90 | zenon_intro zenon_H8f ]. % 39.94/40.22 exact (zenon_H90 zenon_H88). % 39.94/40.22 exact (zenon_H8f zenon_H89). % 39.94/40.22 apply (zenon_and_s _ _ zenon_H8c). zenon_intro zenon_H92. zenon_intro zenon_H91. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H92); [ zenon_intro zenon_H93 | zenon_intro zenon_H81 ]. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H93); [ zenon_intro zenon_H94 | zenon_intro zenon_H79 ]. % 39.94/40.22 exact (zenon_H94 zenon_H8a). % 39.94/40.22 apply (zenon_L11_ zenon_TT2_bg zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_L12_ zenon_TT3_t zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 (* end of lemma zenon_L13_ *) % 39.94/40.22 assert (zenon_L14_ : forall (zenon_TT2_bg : zenon_U) (zenon_TT3_t : zenon_U) (zenon_TX_u : zenon_U), (((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT2_bg))->((position zenon_TX_u zenon_TT3_t) = (position zenon_TX_u zenon_TT2_bg))) -> (~(greater (hazard_of_mortality zenon_TX_u zenon_TT3_t) (hazard_of_mortality zenon_TX_u zenon_TT2_bg))) -> (greater (capability zenon_TX_u zenon_TT2_bg) (capability zenon_TX_u zenon_TT3_t)) -> (~(has_immunity zenon_TX_u zenon_TT2_bg)) -> (~(has_immunity zenon_TX_u zenon_TT3_t)) -> (forall T : zenon_U, (((organization zenon_TX_u)/\((~(has_immunity zenon_TX_u zenon_TT3_t))/\(~(has_immunity zenon_TX_u T))))->((((greater (capability zenon_TX_u T) (capability zenon_TX_u zenon_TT3_t))/\(greater_or_equal (position zenon_TX_u T) (position zenon_TX_u zenon_TT3_t)))->(smaller (hazard_of_mortality zenon_TX_u T) (hazard_of_mortality zenon_TX_u zenon_TT3_t)))/\((((greater_or_equal (capability zenon_TX_u T) (capability zenon_TX_u zenon_TT3_t))/\(greater (position zenon_TX_u T) (position zenon_TX_u zenon_TT3_t)))->(smaller (hazard_of_mortality zenon_TX_u T) (hazard_of_mortality zenon_TX_u zenon_TT3_t)))/\((((capability zenon_TX_u T) = (capability zenon_TX_u zenon_TT3_t))/\((position zenon_TX_u T) = (position zenon_TX_u zenon_TT3_t)))->((hazard_of_mortality zenon_TX_u T) = (hazard_of_mortality zenon_TX_u zenon_TT3_t))))))) -> (organization zenon_TX_u) -> ((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E)) -> (~(greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_TT2_bg))) -> (forall Y : zenon_U, ((smaller (external_ties zenon_TX_u zenon_TT2_bg) Y)\/(((external_ties zenon_TX_u zenon_TT2_bg) = Y)\/(greater (external_ties zenon_TX_u zenon_TT2_bg) Y)))) -> (forall T : zenon_U, ((organization zenon_TX_u)->((external_ties zenon_TX_u T) = (external_ties zenon_TX_u zenon_E)))) -> (~(greater (position zenon_TX_u zenon_TT3_t) (position zenon_TX_u zenon_TT3_t))) -> (forall T0 : zenon_U, (forall T : zenon_U, ((organization zenon_TX_u)->(((greater (external_ties zenon_TX_u T) (external_ties zenon_TX_u T0))->(greater (position zenon_TX_u T) (position zenon_TX_u T0)))/\(((external_ties zenon_TX_u T) = (external_ties zenon_TX_u T0))->((position zenon_TX_u T) = (position zenon_TX_u T0))))))) -> False). % 39.94/40.22 do 3 intro. intros zenon_H95 zenon_H82 zenon_H8a zenon_H89 zenon_H88 zenon_H87 zenon_H2c zenon_H60 zenon_H54 zenon_H53 zenon_H4f zenon_H71 zenon_H70. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H95); [ zenon_intro zenon_H55 | zenon_intro zenon_H78 ]. % 39.94/40.22 apply (zenon_L10_ zenon_TT2_bg zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_L13_ zenon_TT2_bg zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 (* end of lemma zenon_L14_ *) % 39.94/40.22 assert (zenon_L15_ : forall (zenon_TT2_bg : zenon_U) (zenon_TT3_t : zenon_U) (zenon_TX_u : zenon_U), (~((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT2_bg))) -> (~(greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_TT2_bg))) -> (forall Y : zenon_U, ((smaller (external_ties zenon_TX_u zenon_TT2_bg) Y)\/(((external_ties zenon_TX_u zenon_TT2_bg) = Y)\/(greater (external_ties zenon_TX_u zenon_TT2_bg) Y)))) -> (~(greater (external_ties zenon_TX_u zenon_E) (external_ties zenon_TX_u zenon_TT3_t))) -> ((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E)) -> False). % 39.94/40.22 do 3 intro. intros zenon_H55 zenon_H54 zenon_H53 zenon_H66 zenon_H60. % 39.94/40.22 elim (classic ((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_TT2_bg))); [ zenon_intro zenon_H67 | zenon_intro zenon_H68 ]. % 39.94/40.22 elim (classic (greater (external_ties zenon_TX_u zenon_TT2_bg) (external_ties zenon_TX_u zenon_TT3_t))); [ zenon_intro zenon_H5e | zenon_intro zenon_H56 ]. % 39.94/40.22 cut ((greater (external_ties zenon_TX_u zenon_TT2_bg) (external_ties zenon_TX_u zenon_TT3_t)) = (greater (external_ties zenon_TX_u zenon_E) (external_ties zenon_TX_u zenon_TT3_t))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H66. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H5e. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 39.94/40.22 congruence. % 39.94/40.22 elim (classic ((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_E))); [ zenon_intro zenon_H69 | zenon_intro zenon_H6a ]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_E)) = ((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H65. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H69. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H6a]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_TT2_bg))); [idtac | apply NNPP; zenon_intro zenon_H68]. % 39.94/40.22 congruence. % 39.94/40.22 exact (zenon_H68 zenon_H67). % 39.94/40.22 apply zenon_H6a. apply refl_equal. % 39.94/40.22 apply zenon_H6a. apply refl_equal. % 39.94/40.22 apply zenon_H64. apply refl_equal. % 39.94/40.22 apply (zenon_L6_ zenon_TT3_t zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 elim (classic ((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_TT2_bg))); [ zenon_intro zenon_H6b | zenon_intro zenon_H6c ]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_TT2_bg)) = ((external_ties zenon_TX_u zenon_E) = (external_ties zenon_TX_u zenon_TT2_bg))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H68. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H6b. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_TT2_bg))); [idtac | apply NNPP; zenon_intro zenon_H6c]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 39.94/40.22 congruence. % 39.94/40.22 exact (zenon_H65 zenon_H60). % 39.94/40.22 apply zenon_H6c. apply refl_equal. % 39.94/40.22 apply zenon_H6c. apply refl_equal. % 39.94/40.22 (* end of lemma zenon_L15_ *) % 39.94/40.22 assert (zenon_L16_ : forall (zenon_TT2_bg : zenon_U) (zenon_TT3_t : zenon_U) (zenon_TX_u : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (forall T : zenon_U, ((organization zenon_TX_u)->(((greater (external_ties zenon_TX_u T) (external_ties zenon_TX_u zenon_TT3_t))->(greater (position zenon_TX_u T) (position zenon_TX_u zenon_TT3_t)))/\(((external_ties zenon_TX_u T) = (external_ties zenon_TX_u zenon_TT3_t))->((position zenon_TX_u T) = (position zenon_TX_u zenon_TT3_t)))))) -> (organization zenon_TX_u) -> (~((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT2_bg))) -> (forall T0 : zenon_U, (forall T : zenon_U, ((organization zenon_TX_u)->(((greater (external_ties zenon_TX_u T) (external_ties zenon_TX_u T0))->(greater (position zenon_TX_u T) (position zenon_TX_u T0)))/\(((external_ties zenon_TX_u T) = (external_ties zenon_TX_u T0))->((position zenon_TX_u T) = (position zenon_TX_u T0))))))) -> (~(greater (position zenon_TX_u zenon_TT3_t) (position zenon_TX_u zenon_TT3_t))) -> (forall T : zenon_U, ((organization zenon_TX_u)->((external_ties zenon_TX_u T) = (external_ties zenon_TX_u zenon_E)))) -> (forall Y : zenon_U, ((smaller (external_ties zenon_TX_u zenon_TT2_bg) Y)\/(((external_ties zenon_TX_u zenon_TT2_bg) = Y)\/(greater (external_ties zenon_TX_u zenon_TT2_bg) Y)))) -> ((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E)) -> (forall T : zenon_U, (((organization zenon_TX_u)/\((~(has_immunity zenon_TX_u zenon_TT3_t))/\(~(has_immunity zenon_TX_u T))))->((((greater (capability zenon_TX_u T) (capability zenon_TX_u zenon_TT3_t))/\(greater_or_equal (position zenon_TX_u T) (position zenon_TX_u zenon_TT3_t)))->(smaller (hazard_of_mortality zenon_TX_u T) (hazard_of_mortality zenon_TX_u zenon_TT3_t)))/\((((greater_or_equal (capability zenon_TX_u T) (capability zenon_TX_u zenon_TT3_t))/\(greater (position zenon_TX_u T) (position zenon_TX_u zenon_TT3_t)))->(smaller (hazard_of_mortality zenon_TX_u T) (hazard_of_mortality zenon_TX_u zenon_TT3_t)))/\((((capability zenon_TX_u T) = (capability zenon_TX_u zenon_TT3_t))/\((position zenon_TX_u T) = (position zenon_TX_u zenon_TT3_t)))->((hazard_of_mortality zenon_TX_u T) = (hazard_of_mortality zenon_TX_u zenon_TT3_t))))))) -> (~(has_immunity zenon_TX_u zenon_TT3_t)) -> (~(has_immunity zenon_TX_u zenon_TT2_bg)) -> (greater (capability zenon_TX_u zenon_TT2_bg) (capability zenon_TX_u zenon_TT3_t)) -> (~(greater (hazard_of_mortality zenon_TX_u zenon_TT3_t) (hazard_of_mortality zenon_TX_u zenon_TT2_bg))) -> (((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT2_bg))->((position zenon_TX_u zenon_TT3_t) = (position zenon_TX_u zenon_TT2_bg))) -> False). % 39.94/40.22 do 3 intro. intros zenon_H96 zenon_H72 zenon_H2c zenon_H55 zenon_H70 zenon_H71 zenon_H4f zenon_H53 zenon_H60 zenon_H87 zenon_H88 zenon_H89 zenon_H8a zenon_H82 zenon_H95. % 39.94/40.22 generalize (zenon_H72 zenon_TT3_t). zenon_intro zenon_H73. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H73); [ zenon_intro zenon_H3a | zenon_intro zenon_H74 ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 apply (zenon_and_s _ _ zenon_H74). zenon_intro zenon_H76. zenon_intro zenon_H75. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H76); [ zenon_intro zenon_H61 | zenon_intro zenon_H77 ]. % 39.94/40.22 elim (classic (greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_TT2_bg))); [ zenon_intro zenon_H5c | zenon_intro zenon_H54 ]. % 39.94/40.22 elim (classic (greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_E))); [ zenon_intro zenon_H62 | zenon_intro zenon_H63 ]. % 39.94/40.22 elim (classic (greater (external_ties zenon_TX_u zenon_E) (external_ties zenon_TX_u zenon_TT3_t))); [ zenon_intro zenon_H6d | zenon_intro zenon_H66 ]. % 39.94/40.22 generalize (zenon_H96 (external_ties zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H97. % 39.94/40.22 generalize (zenon_H97 (external_ties zenon_TX_u zenon_E)). zenon_intro zenon_H98. % 39.94/40.22 generalize (zenon_H98 (external_ties zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H99. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H99); [ zenon_intro zenon_H63 | zenon_intro zenon_H9a ]. % 39.94/40.22 exact (zenon_H63 zenon_H62). % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H9a); [ zenon_intro zenon_H66 | zenon_intro zenon_H9b ]. % 39.94/40.22 exact (zenon_H66 zenon_H6d). % 39.94/40.22 exact (zenon_H61 zenon_H9b). % 39.94/40.22 apply (zenon_L8_ zenon_TT3_t zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 cut ((greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_TT2_bg)) = (greater (external_ties zenon_TX_u zenon_TT3_t) (external_ties zenon_TX_u zenon_E))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H63. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H5c. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT2_bg) = (external_ties zenon_TX_u zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 39.94/40.22 cut (((external_ties zenon_TX_u zenon_TT3_t) = (external_ties zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 39.94/40.22 congruence. % 39.94/40.22 apply zenon_H64. apply refl_equal. % 39.94/40.22 exact (zenon_H65 zenon_H60). % 39.94/40.22 apply (zenon_L14_ zenon_TT2_bg zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 exact (zenon_H71 zenon_H77). % 39.94/40.22 (* end of lemma zenon_L16_ *) % 39.94/40.22 assert (zenon_L17_ : forall (zenon_TT3_t : zenon_U) (zenon_TX_u : zenon_U), (smaller (hazard_of_mortality zenon_TX_u zenon_TT3_t) (hazard_of_mortality zenon_TX_u zenon_TT3_t)) -> False). % 39.94/40.22 do 2 intro. intros zenon_H9c. % 39.94/40.22 generalize (definition_smaller (hazard_of_mortality zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H9d. % 39.94/40.22 generalize (zenon_H9d (hazard_of_mortality zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H9e. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H9e); [ zenon_intro zenon_Ha1; zenon_intro zenon_Ha0 | zenon_intro zenon_H9c; zenon_intro zenon_H9f ]. % 39.94/40.22 exact (zenon_Ha1 zenon_H9c). % 39.94/40.22 generalize (meaning_postulate_greater_strict (hazard_of_mortality zenon_TX_u zenon_TT3_t)). zenon_intro zenon_Ha2. % 39.94/40.22 generalize (zenon_Ha2 (hazard_of_mortality zenon_TX_u zenon_TT3_t)). zenon_intro zenon_Ha3. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_Ha3); [ zenon_intro zenon_Ha0 | zenon_intro zenon_Ha0 ]. % 39.94/40.22 exact (zenon_Ha0 zenon_H9f). % 39.94/40.22 exact (zenon_Ha0 zenon_H9f). % 39.94/40.22 (* end of lemma zenon_L17_ *) % 39.94/40.22 assert (zenon_L18_ : forall (zenon_TT2_bg : zenon_U) (zenon_TX_u : zenon_U), (~(smaller_or_equal (internal_friction zenon_TX_u zenon_TT2_bg) (internal_friction zenon_TX_u zenon_TT2_bg))) -> False). % 39.94/40.22 do 2 intro. intros zenon_Ha4. % 39.94/40.22 generalize (definition_smaller_or_equal (internal_friction zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_Ha5. % 39.94/40.22 generalize (zenon_Ha5 (internal_friction zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_Ha6. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_Ha6); [ zenon_intro zenon_Ha4; zenon_intro zenon_Ha9 | zenon_intro zenon_Ha8; zenon_intro zenon_Ha7 ]. % 39.94/40.22 apply (zenon_notor_s _ _ zenon_Ha9). zenon_intro zenon_Hab. zenon_intro zenon_Haa. % 39.94/40.22 apply zenon_Haa. apply refl_equal. % 39.94/40.22 exact (zenon_Ha4 zenon_Ha8). % 39.94/40.22 (* end of lemma zenon_L18_ *) % 39.94/40.22 assert (zenon_L19_ : forall (zenon_TT2_bg : zenon_U) (zenon_TX_u : zenon_U), (smaller (hazard_of_mortality zenon_TX_u zenon_TT2_bg) (hazard_of_mortality zenon_TX_u zenon_TT2_bg)) -> False). % 39.94/40.22 do 2 intro. intros zenon_Hac. % 39.94/40.22 generalize (definition_smaller (hazard_of_mortality zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H83. % 39.94/40.22 generalize (zenon_H83 (hazard_of_mortality zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_Had. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_Had); [ zenon_intro zenon_Hb0; zenon_intro zenon_Haf | zenon_intro zenon_Hac; zenon_intro zenon_Hae ]. % 39.94/40.22 exact (zenon_Hb0 zenon_Hac). % 39.94/40.22 generalize (meaning_postulate_greater_strict (hazard_of_mortality zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_Hb1. % 39.94/40.22 generalize (zenon_Hb1 (hazard_of_mortality zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_Hb2. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_Hb2); [ zenon_intro zenon_Haf | zenon_intro zenon_Haf ]. % 39.94/40.22 exact (zenon_Haf zenon_Hae). % 39.94/40.22 exact (zenon_Haf zenon_Hae). % 39.94/40.22 (* end of lemma zenon_L19_ *) % 39.94/40.22 assert (zenon_L20_ : forall (zenon_TT2_bg : zenon_U) (zenon_TT3_t : zenon_U) (zenon_TX_u : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater (eta) (age zenon_TX_u zenon_TT3_t))) -> (~((eta) = (age zenon_TX_u zenon_TT3_t))) -> (forall T : zenon_U, ((organization zenon_TX_u)/\(((smaller_or_equal (age zenon_TX_u T) (eta))->(has_immunity zenon_TX_u T))/\((greater (age zenon_TX_u T) (eta))->(~(has_immunity zenon_TX_u T)))))) -> (greater (age zenon_TX_u zenon_TT3_t) (age zenon_TX_u zenon_TT2_bg)) -> (~(greater (hazard_of_mortality zenon_TX_u zenon_TT3_t) (hazard_of_mortality zenon_TX_u zenon_TT2_bg))) -> (~(has_immunity zenon_TX_u zenon_TT2_bg)) -> (organization zenon_TX_u) -> False). % 39.94/40.22 do 3 intro. intros zenon_H96 zenon_Hb3 zenon_Hb4 zenon_Hb5 zenon_H49 zenon_H82 zenon_H89 zenon_H2c. % 39.94/40.22 generalize (assumption_4 zenon_TX_u). zenon_intro zenon_Hb6. % 39.94/40.22 generalize (meaning_postulate_greater_comparable (eta)). zenon_intro zenon_Hb7. % 39.94/40.22 generalize (zenon_Hb6 zenon_TT2_bg). zenon_intro zenon_Hb8. % 39.94/40.22 generalize (zenon_Hb8 zenon_TT2_bg). zenon_intro zenon_Hb9. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_Hb9); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hba ]. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_Hbb); [ zenon_intro zenon_H3a | zenon_intro zenon_Hbc ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 apply (zenon_notand_s _ _ zenon_Hbc); [ zenon_intro zenon_H8f | zenon_intro zenon_H8f ]. % 39.94/40.22 exact (zenon_H8f zenon_H89). % 39.94/40.22 exact (zenon_H8f zenon_H89). % 39.94/40.22 apply (zenon_and_s _ _ zenon_Hba). zenon_intro zenon_Hbe. zenon_intro zenon_Hbd. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_Hbe); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hac ]. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_Hbf); [ zenon_intro zenon_Hc1 | zenon_intro zenon_Hc0 ]. % 39.94/40.22 generalize (assumption_6 zenon_TX_u). zenon_intro zenon_H70. % 39.94/40.22 generalize (assumption_5 zenon_TX_u). zenon_intro zenon_Hc2. % 39.94/40.22 generalize (zenon_H70 zenon_TT2_bg). zenon_intro zenon_Hc3. % 39.94/40.22 generalize (zenon_Hc2 zenon_TT2_bg). zenon_intro zenon_Hc4. % 39.94/40.22 generalize (zenon_Hc4 zenon_TT2_bg). zenon_intro zenon_Hc5. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_Hc5); [ zenon_intro zenon_H3a | zenon_intro zenon_Hc6 ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 apply (zenon_and_s _ _ zenon_Hc6). zenon_intro zenon_Hc8. zenon_intro zenon_Hc7. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_Hc8); [ zenon_intro zenon_Hca | zenon_intro zenon_Hc9 ]. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_Hca); [ zenon_intro zenon_H2b | zenon_intro zenon_Ha4 ]. % 39.94/40.22 generalize (assumption_12 zenon_TX_u). zenon_intro zenon_Hcb. % 39.94/40.22 generalize (assumption_11 zenon_TX_u). zenon_intro zenon_H1. % 39.94/40.22 generalize (zenon_H1 zenon_E). zenon_intro zenon_H4f. % 39.94/40.22 generalize (zenon_Hcb zenon_TT2_bg). zenon_intro zenon_H48. % 39.94/40.22 generalize (assumption_10 zenon_TX_u). zenon_intro zenon_H0. % 39.94/40.22 generalize (zenon_H0 zenon_E). zenon_intro zenon_H2d. % 39.94/40.22 generalize (zenon_Hb7 (age zenon_TX_u zenon_TT3_t)). zenon_intro zenon_Hcc. % 39.94/40.22 apply (zenon_or_s _ _ zenon_Hcc); [ zenon_intro zenon_Hce | zenon_intro zenon_Hcd ]. % 39.94/40.22 generalize (definition_smaller (eta)). zenon_intro zenon_Hcf. % 39.94/40.22 generalize (zenon_Hcf (age zenon_TX_u zenon_TT3_t)). zenon_intro zenon_Hd0. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_Hd0); [ zenon_intro zenon_Hd3; zenon_intro zenon_Hd2 | zenon_intro zenon_Hce; zenon_intro zenon_Hd1 ]. % 39.94/40.22 exact (zenon_Hd3 zenon_Hce). % 39.94/40.22 generalize (zenon_H4f zenon_TT2_bg). zenon_intro zenon_Hd4. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_Hd4); [ zenon_intro zenon_H3a | zenon_intro zenon_H60 ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 generalize (zenon_Hb5 zenon_TT3_t). zenon_intro zenon_Hd5. % 39.94/40.22 apply (zenon_and_s _ _ zenon_Hd5). zenon_intro zenon_H2c. zenon_intro zenon_Hd6. % 39.94/40.22 apply (zenon_and_s _ _ zenon_Hd6). zenon_intro zenon_Hd8. zenon_intro zenon_Hd7. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_Hd7); [ zenon_intro zenon_Hd2 | zenon_intro zenon_H88 ]. % 39.94/40.22 exact (zenon_Hd2 zenon_Hd1). % 39.94/40.22 generalize (meaning_postulate_greater_comparable (external_ties zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H53. % 39.94/40.22 generalize (zenon_H2d zenon_TT2_bg). zenon_intro zenon_Hd9. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_Hd9); [ zenon_intro zenon_H3a | zenon_intro zenon_H2a ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 generalize (meaning_postulate_greater_comparable (stock_of_knowledge zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H1c. % 39.94/40.22 generalize (zenon_Hb6 zenon_TT3_t). zenon_intro zenon_H87. % 39.94/40.22 generalize (zenon_H87 zenon_TT3_t). zenon_intro zenon_Hda. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_Hda); [ zenon_intro zenon_Hdc | zenon_intro zenon_Hdb ]. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_Hdc); [ zenon_intro zenon_H3a | zenon_intro zenon_Hdd ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 apply (zenon_notand_s _ _ zenon_Hdd); [ zenon_intro zenon_H90 | zenon_intro zenon_H90 ]. % 39.94/40.22 exact (zenon_H90 zenon_H88). % 39.94/40.22 exact (zenon_H90 zenon_H88). % 39.94/40.22 apply (zenon_and_s _ _ zenon_Hdb). zenon_intro zenon_Hdf. zenon_intro zenon_Hde. % 39.94/40.22 apply (zenon_and_s _ _ zenon_Hde). zenon_intro zenon_He1. zenon_intro zenon_He0. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_He1); [ zenon_intro zenon_He2 | zenon_intro zenon_H9c ]. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_He2); [ zenon_intro zenon_H12 | zenon_intro zenon_H71 ]. % 39.94/40.22 apply (zenon_L1_ zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 generalize (zenon_Hc4 zenon_TT3_t). zenon_intro zenon_He3. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_He3); [ zenon_intro zenon_H3a | zenon_intro zenon_He4 ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 apply (zenon_and_s _ _ zenon_He4). zenon_intro zenon_He6. zenon_intro zenon_He5. % 39.94/40.22 apply (zenon_and_s _ _ zenon_He5). zenon_intro zenon_He8. zenon_intro zenon_He7. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_He8); [ zenon_intro zenon_Hea | zenon_intro zenon_He9 ]. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_Hea); [ zenon_intro zenon_H2e | zenon_intro zenon_H4a ]. % 39.94/40.22 apply (zenon_L3_ zenon_TT3_t zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_L4_ zenon_TT3_t zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 generalize (definition_smaller (capability zenon_TX_u zenon_TT3_t)). zenon_intro zenon_Heb. % 39.94/40.22 generalize (zenon_Heb (capability zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_Hec. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_Hec); [ zenon_intro zenon_Hed; zenon_intro zenon_H94 | zenon_intro zenon_He9; zenon_intro zenon_H8a ]. % 39.94/40.22 exact (zenon_Hed zenon_He9). % 39.94/40.22 generalize (zenon_Hc3 zenon_TT3_t). zenon_intro zenon_Hee. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_Hee); [ zenon_intro zenon_H3a | zenon_intro zenon_Hef ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 apply (zenon_and_s _ _ zenon_Hef). zenon_intro zenon_Hf0. zenon_intro zenon_H95. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H95); [ zenon_intro zenon_H55 | zenon_intro zenon_H78 ]. % 39.94/40.22 generalize (zenon_H70 zenon_TT3_t). zenon_intro zenon_H72. % 39.94/40.22 apply (zenon_L16_ zenon_TT2_bg zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_L13_ zenon_TT2_bg zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_L17_ zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_or_s _ _ zenon_Hcd); [ zenon_intro zenon_Hf2 | zenon_intro zenon_Hf1 ]. % 39.94/40.22 exact (zenon_Hb4 zenon_Hf2). % 39.94/40.22 exact (zenon_Hb3 zenon_Hf1). % 39.94/40.22 apply (zenon_L18_ zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 exact (zenon_Hc1 zenon_Hc9). % 39.94/40.22 generalize (definition_greater_or_equal (position zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H7a. % 39.94/40.22 generalize (zenon_H7a (position zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_Hf3. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_Hf3); [ zenon_intro zenon_Hc0; zenon_intro zenon_Hf6 | zenon_intro zenon_Hf5; zenon_intro zenon_Hf4 ]. % 39.94/40.22 apply (zenon_notor_s _ _ zenon_Hf6). zenon_intro zenon_Hf8. zenon_intro zenon_Hf7. % 39.94/40.22 apply zenon_Hf7. apply refl_equal. % 39.94/40.22 exact (zenon_Hc0 zenon_Hf5). % 39.94/40.22 apply (zenon_L19_ zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 (* end of lemma zenon_L20_ *) % 39.94/40.22 assert (zenon_L21_ : forall (zenon_TT2_bg : zenon_U) (zenon_TX_u : zenon_U), ((greater (age zenon_TX_u zenon_TT2_bg) (eta))->(~(has_immunity zenon_TX_u zenon_TT2_bg))) -> (has_immunity zenon_TX_u zenon_TT2_bg) -> (greater (age zenon_TX_u zenon_TT2_bg) (eta)) -> False). % 39.94/40.22 do 2 intro. intros zenon_Hf9 zenon_Hfa zenon_Hfb. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_Hf9); [ zenon_intro zenon_Hfc | zenon_intro zenon_H89 ]. % 39.94/40.22 exact (zenon_Hfc zenon_Hfb). % 39.94/40.22 exact (zenon_H89 zenon_Hfa). % 39.94/40.22 (* end of lemma zenon_L21_ *) % 39.94/40.22 assert (zenon_L22_ : forall (zenon_TT2_bg : zenon_U) (zenon_TT3_t : zenon_U) (zenon_TX_u : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (forall T : zenon_U, ((organization zenon_TX_u)/\(((smaller_or_equal (age zenon_TX_u T) (eta))->(has_immunity zenon_TX_u T))/\((greater (age zenon_TX_u T) (eta))->(~(has_immunity zenon_TX_u T)))))) -> (greater (age zenon_TX_u zenon_TT3_t) (age zenon_TX_u zenon_TT2_bg)) -> (~(greater (hazard_of_mortality zenon_TX_u zenon_TT3_t) (hazard_of_mortality zenon_TX_u zenon_TT2_bg))) -> (greater (age zenon_TX_u zenon_TT2_bg) (eta)) -> False). % 39.94/40.22 do 3 intro. intros zenon_H96 zenon_Hb5 zenon_H49 zenon_H82 zenon_Hfb. % 39.94/40.22 generalize (zenon_Hb5 zenon_TT2_bg). zenon_intro zenon_Hfd. % 39.94/40.22 apply (zenon_and_s _ _ zenon_Hfd). zenon_intro zenon_H2c. zenon_intro zenon_Hfe. % 39.94/40.22 apply (zenon_and_s _ _ zenon_Hfe). zenon_intro zenon_Hff. zenon_intro zenon_Hf9. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_Hff); [ zenon_intro zenon_H100 | zenon_intro zenon_Hfa ]. % 39.94/40.22 generalize (definition_smaller_or_equal (age zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H101. % 39.94/40.22 generalize (zenon_H101 (eta)). zenon_intro zenon_H102. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H102); [ zenon_intro zenon_H100; zenon_intro zenon_H105 | zenon_intro zenon_H104; zenon_intro zenon_H103 ]. % 39.94/40.22 apply (zenon_notor_s _ _ zenon_H105). zenon_intro zenon_H107. zenon_intro zenon_H106. % 39.94/40.22 generalize (definition_smaller (age zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H108. % 39.94/40.22 generalize (zenon_H108 (eta)). zenon_intro zenon_H109. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H109); [ zenon_intro zenon_H107; zenon_intro zenon_H10c | zenon_intro zenon_H10b; zenon_intro zenon_H10a ]. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_Hf9); [ zenon_intro zenon_Hfc | zenon_intro zenon_H89 ]. % 39.94/40.22 exact (zenon_Hfc zenon_Hfb). % 39.94/40.22 elim (classic ((~((eta) = (age zenon_TX_u zenon_TT3_t)))/\(~(greater (eta) (age zenon_TX_u zenon_TT3_t))))); [ zenon_intro zenon_H10d | zenon_intro zenon_H10e ]. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H10d). zenon_intro zenon_Hb4. zenon_intro zenon_Hb3. % 39.94/40.22 apply (zenon_L20_ zenon_TT2_bg zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 cut ((greater (age zenon_TX_u zenon_TT3_t) (age zenon_TX_u zenon_TT2_bg)) = (greater (eta) (age zenon_TX_u zenon_TT2_bg))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H10c. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H49. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT2_bg) = (age zenon_TX_u zenon_TT2_bg))); [idtac | apply NNPP; zenon_intro zenon_H10f]. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT3_t) = (eta))); [idtac | apply NNPP; zenon_intro zenon_H110]. % 39.94/40.22 congruence. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H10e); [ zenon_intro zenon_H112 | zenon_intro zenon_H111 ]. % 39.94/40.22 apply zenon_H112. zenon_intro zenon_Hf2. % 39.94/40.22 elim (classic ((eta) = (eta))); [ zenon_intro zenon_H113 | zenon_intro zenon_H114 ]. % 39.94/40.22 cut (((eta) = (eta)) = ((age zenon_TX_u zenon_TT3_t) = (eta))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H110. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H113. % 39.94/40.22 cut (((eta) = (eta))); [idtac | apply NNPP; zenon_intro zenon_H114]. % 39.94/40.22 cut (((eta) = (age zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_Hb4]. % 39.94/40.22 congruence. % 39.94/40.22 exact (zenon_Hb4 zenon_Hf2). % 39.94/40.22 apply zenon_H114. apply refl_equal. % 39.94/40.22 apply zenon_H114. apply refl_equal. % 39.94/40.22 apply zenon_H111. zenon_intro zenon_Hf1. % 39.94/40.22 generalize (zenon_H96 (eta)). zenon_intro zenon_H115. % 39.94/40.22 generalize (zenon_H115 (age zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H116. % 39.94/40.22 generalize (zenon_H116 (age zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H117. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H117); [ zenon_intro zenon_Hb3 | zenon_intro zenon_H118 ]. % 39.94/40.22 exact (zenon_Hb3 zenon_Hf1). % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H118); [ zenon_intro zenon_H4e | zenon_intro zenon_H10a ]. % 39.94/40.22 exact (zenon_H4e zenon_H49). % 39.94/40.22 exact (zenon_H10c zenon_H10a). % 39.94/40.22 apply zenon_H10f. apply refl_equal. % 39.94/40.22 exact (zenon_H107 zenon_H10b). % 39.94/40.22 exact (zenon_H100 zenon_H104). % 39.94/40.22 apply (zenon_L21_ zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 (* end of lemma zenon_L22_ *) % 39.94/40.22 assert (zenon_L23_ : forall (zenon_TT1_kx : zenon_U) (zenon_TX_u : zenon_U), (greater (eta) (age zenon_TX_u zenon_TT1_kx)) -> (~(smaller_or_equal (age zenon_TX_u zenon_TT1_kx) (eta))) -> False). % 39.94/40.22 do 2 intro. intros zenon_H119 zenon_H11a. % 39.94/40.22 generalize (definition_smaller_or_equal (age zenon_TX_u zenon_TT1_kx)). zenon_intro zenon_H11c. % 39.94/40.22 generalize (zenon_H11c (eta)). zenon_intro zenon_H11d. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H11d); [ zenon_intro zenon_H11a; zenon_intro zenon_H120 | zenon_intro zenon_H11f; zenon_intro zenon_H11e ]. % 39.94/40.22 apply (zenon_notor_s _ _ zenon_H120). zenon_intro zenon_H122. zenon_intro zenon_H121. % 39.94/40.22 generalize (definition_smaller (age zenon_TX_u zenon_TT1_kx)). zenon_intro zenon_H123. % 39.94/40.22 generalize (zenon_H123 (eta)). zenon_intro zenon_H124. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H124); [ zenon_intro zenon_H122; zenon_intro zenon_H126 | zenon_intro zenon_H125; zenon_intro zenon_H119 ]. % 39.94/40.22 exact (zenon_H126 zenon_H119). % 39.94/40.22 exact (zenon_H122 zenon_H125). % 39.94/40.22 exact (zenon_H11a zenon_H11f). % 39.94/40.22 (* end of lemma zenon_L23_ *) % 39.94/40.22 assert (zenon_L24_ : forall (zenon_TT1_kx : zenon_U) (zenon_TT2_bg : zenon_U) (zenon_TX_u : zenon_U), (forall T : zenon_U, ((organization zenon_TX_u)/\(((smaller_or_equal (age zenon_TX_u T) (eta))->(has_immunity zenon_TX_u T))/\((greater (age zenon_TX_u T) (eta))->(~(has_immunity zenon_TX_u T)))))) -> (~(greater (hazard_of_mortality zenon_TX_u zenon_TT2_bg) (hazard_of_mortality zenon_TX_u zenon_TT1_kx))) -> (has_immunity zenon_TX_u zenon_TT1_kx) -> (greater (age zenon_TX_u zenon_TT2_bg) (eta)) -> False). % 39.94/40.22 do 3 intro. intros zenon_Hb5 zenon_H127 zenon_H128 zenon_Hfb. % 39.94/40.22 generalize (zenon_Hb5 zenon_TT2_bg). zenon_intro zenon_Hfd. % 39.94/40.22 apply (zenon_and_s _ _ zenon_Hfd). zenon_intro zenon_H2c. zenon_intro zenon_Hfe. % 39.94/40.22 apply (zenon_and_s _ _ zenon_Hfe). zenon_intro zenon_Hff. zenon_intro zenon_Hf9. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_Hf9); [ zenon_intro zenon_Hfc | zenon_intro zenon_H89 ]. % 39.94/40.22 exact (zenon_Hfc zenon_Hfb). % 39.94/40.22 generalize (assumption_3 zenon_TX_u). zenon_intro zenon_H129. % 39.94/40.22 generalize (zenon_H129 zenon_TT1_kx). zenon_intro zenon_H12a. % 39.94/40.22 generalize (zenon_H12a zenon_TT2_bg). zenon_intro zenon_H12b. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H12b); [ zenon_intro zenon_H12d | zenon_intro zenon_H12c ]. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H12d); [ zenon_intro zenon_H3a | zenon_intro zenon_H12e ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H12e); [ zenon_intro zenon_H12f | zenon_intro zenon_H8f ]. % 39.94/40.22 exact (zenon_H12f zenon_H128). % 39.94/40.22 exact (zenon_H8f zenon_H89). % 39.94/40.22 exact (zenon_H127 zenon_H12c). % 39.94/40.22 (* end of lemma zenon_L24_ *) % 39.94/40.22 assert (zenon_L25_ : forall (zenon_TT1_kx : zenon_U) (zenon_TT2_bg : zenon_U) (zenon_TX_u : zenon_U), (greater (age zenon_TX_u zenon_TT2_bg) (eta)) -> (~(greater (hazard_of_mortality zenon_TX_u zenon_TT2_bg) (hazard_of_mortality zenon_TX_u zenon_TT1_kx))) -> (forall T : zenon_U, ((organization zenon_TX_u)/\(((smaller_or_equal (age zenon_TX_u T) (eta))->(has_immunity zenon_TX_u T))/\((greater (age zenon_TX_u T) (eta))->(~(has_immunity zenon_TX_u T)))))) -> (greater (eta) (age zenon_TX_u zenon_TT1_kx)) -> False). % 39.94/40.22 do 3 intro. intros zenon_Hfb zenon_H127 zenon_Hb5 zenon_H119. % 39.94/40.22 generalize (zenon_Hb5 zenon_TT1_kx). zenon_intro zenon_H130. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H130). zenon_intro zenon_H2c. zenon_intro zenon_H131. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H131). zenon_intro zenon_H133. zenon_intro zenon_H132. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H133); [ zenon_intro zenon_H11a | zenon_intro zenon_H128 ]. % 39.94/40.22 apply (zenon_L23_ zenon_TT1_kx zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_L24_ zenon_TT1_kx zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 (* end of lemma zenon_L25_ *) % 39.94/40.22 assert (zenon_L26_ : (~((eta) = (eta))) -> False). % 39.94/40.22 do 0 intro. intros zenon_H114. % 39.94/40.22 apply zenon_H114. apply refl_equal. % 39.94/40.22 (* end of lemma zenon_L26_ *) % 39.94/40.22 assert (zenon_L27_ : forall (zenon_TT1_kx : zenon_U) (zenon_TT0_ly : zenon_U) (zenon_TX_u : zenon_U), (organization zenon_TX_u) -> (has_immunity zenon_TX_u zenon_TT0_ly) -> (has_immunity zenon_TX_u zenon_TT1_kx) -> (~((hazard_of_mortality zenon_TX_u zenon_TT1_kx) = (hazard_of_mortality zenon_TX_u zenon_TT0_ly))) -> False). % 39.94/40.22 do 3 intro. intros zenon_H2c zenon_H134 zenon_H128 zenon_H135. % 39.94/40.22 generalize (assumption_2 zenon_TX_u). zenon_intro zenon_H137. % 39.94/40.22 generalize (zenon_H137 zenon_TT0_ly). zenon_intro zenon_H138. % 39.94/40.22 generalize (zenon_H138 zenon_TT1_kx). zenon_intro zenon_H139. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H139); [ zenon_intro zenon_H13b | zenon_intro zenon_H13a ]. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H13b); [ zenon_intro zenon_H3a | zenon_intro zenon_H13c ]. % 39.94/40.22 exact (zenon_H3a zenon_H2c). % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H13c); [ zenon_intro zenon_H13d | zenon_intro zenon_H12f ]. % 39.94/40.22 exact (zenon_H13d zenon_H134). % 39.94/40.22 exact (zenon_H12f zenon_H128). % 39.94/40.22 apply zenon_H135. apply sym_equal. exact zenon_H13a. % 39.94/40.22 (* end of lemma zenon_L27_ *) % 39.94/40.22 assert (zenon_L28_ : forall (zenon_TT1_kx : zenon_U) (zenon_TX_u : zenon_U), ((age zenon_TX_u zenon_TT1_kx) = (eta)) -> (~(smaller_or_equal (age zenon_TX_u zenon_TT1_kx) (eta))) -> False). % 39.94/40.22 do 2 intro. intros zenon_H13e zenon_H11a. % 39.94/40.22 generalize (definition_smaller_or_equal (age zenon_TX_u zenon_TT1_kx)). zenon_intro zenon_H11c. % 39.94/40.22 generalize (zenon_H11c (eta)). zenon_intro zenon_H11d. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H11d); [ zenon_intro zenon_H11a; zenon_intro zenon_H120 | zenon_intro zenon_H11f; zenon_intro zenon_H11e ]. % 39.94/40.22 apply (zenon_notor_s _ _ zenon_H120). zenon_intro zenon_H122. zenon_intro zenon_H121. % 39.94/40.22 exact (zenon_H121 zenon_H13e). % 39.94/40.22 exact (zenon_H11a zenon_H11f). % 39.94/40.22 (* end of lemma zenon_L28_ *) % 39.94/40.22 assert (zenon_L29_ : forall (zenon_TT2_bg : zenon_U) (zenon_TT3_t : zenon_U) (zenon_TX_u : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater (hazard_of_mortality zenon_TX_u zenon_TT3_t) (hazard_of_mortality zenon_TX_u zenon_TT2_bg))) -> (greater (age zenon_TX_u zenon_TT3_t) (age zenon_TX_u zenon_TT2_bg)) -> (forall T : zenon_U, ((organization zenon_TX_u)/\(((smaller_or_equal (age zenon_TX_u T) (eta))->(has_immunity zenon_TX_u T))/\((greater (age zenon_TX_u T) (eta))->(~(has_immunity zenon_TX_u T)))))) -> (~((eta) = (age zenon_TX_u zenon_TT3_t))) -> (~(greater (eta) (age zenon_TX_u zenon_TT3_t))) -> (greater (age zenon_TX_u zenon_TT2_bg) (eta)) -> False). % 39.94/40.22 do 3 intro. intros zenon_H96 zenon_H82 zenon_H49 zenon_Hb5 zenon_Hb4 zenon_Hb3 zenon_Hfb. % 39.94/40.22 generalize (zenon_Hb5 zenon_TT2_bg). zenon_intro zenon_Hfd. % 39.94/40.22 apply (zenon_and_s _ _ zenon_Hfd). zenon_intro zenon_H2c. zenon_intro zenon_Hfe. % 39.94/40.22 apply (zenon_and_s _ _ zenon_Hfe). zenon_intro zenon_Hff. zenon_intro zenon_Hf9. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_Hf9); [ zenon_intro zenon_Hfc | zenon_intro zenon_H89 ]. % 39.94/40.22 exact (zenon_Hfc zenon_Hfb). % 39.94/40.22 apply (zenon_L20_ zenon_TT2_bg zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 (* end of lemma zenon_L29_ *) % 39.94/40.22 assert (zenon_L30_ : forall (zenon_TT3_t : zenon_U) (zenon_TT2_bg : zenon_U) (zenon_TX_u : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (greater (age zenon_TX_u zenon_TT2_bg) (eta)) -> (~(greater (eta) (age zenon_TX_u zenon_TT3_t))) -> (forall T : zenon_U, ((organization zenon_TX_u)/\(((smaller_or_equal (age zenon_TX_u T) (eta))->(has_immunity zenon_TX_u T))/\((greater (age zenon_TX_u T) (eta))->(~(has_immunity zenon_TX_u T)))))) -> (greater (age zenon_TX_u zenon_TT3_t) (age zenon_TX_u zenon_TT2_bg)) -> (~(greater (hazard_of_mortality zenon_TX_u zenon_TT3_t) (hazard_of_mortality zenon_TX_u zenon_TT2_bg))) -> False). % 39.94/40.22 do 3 intro. intros zenon_H96 zenon_Hfb zenon_Hb3 zenon_Hb5 zenon_H49 zenon_H82. % 39.94/40.22 elim (classic ((~((eta) = (age zenon_TX_u zenon_TT3_t)))/\(~(greater (eta) (age zenon_TX_u zenon_TT3_t))))); [ zenon_intro zenon_H10d | zenon_intro zenon_H10e ]. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H10d). zenon_intro zenon_Hb4. zenon_intro zenon_Hb3. % 39.94/40.22 apply (zenon_L29_ zenon_TT2_bg zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 elim (classic (greater (age zenon_TX_u zenon_TT2_bg) (age zenon_TX_u zenon_TT3_t))); [ zenon_intro zenon_H13f | zenon_intro zenon_H140 ]. % 39.94/40.22 generalize (zenon_H96 (age zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H141. % 39.94/40.22 generalize (zenon_H141 (age zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H142. % 39.94/40.22 generalize (zenon_H142 (age zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H143. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H143); [ zenon_intro zenon_H4e | zenon_intro zenon_H144 ]. % 39.94/40.22 exact (zenon_H4e zenon_H49). % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H144); [ zenon_intro zenon_H140 | zenon_intro zenon_H145 ]. % 39.94/40.22 exact (zenon_H140 zenon_H13f). % 39.94/40.22 cut ((greater (age zenon_TX_u zenon_TT3_t) (age zenon_TX_u zenon_TT3_t)) = (greater (eta) (age zenon_TX_u zenon_TT3_t))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_Hb3. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H145. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT3_t) = (age zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_H146]. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT3_t) = (eta))); [idtac | apply NNPP; zenon_intro zenon_H110]. % 39.94/40.22 congruence. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H10e); [ zenon_intro zenon_H112 | zenon_intro zenon_H111 ]. % 39.94/40.22 apply zenon_H112. zenon_intro zenon_Hf2. % 39.94/40.22 apply zenon_H110. apply sym_equal. exact zenon_Hf2. % 39.94/40.22 exact (zenon_H111 zenon_Hb3). % 39.94/40.22 apply zenon_H146. apply refl_equal. % 39.94/40.22 elim (classic ((eta) = (age zenon_TX_u zenon_TT3_t))); [ zenon_intro zenon_Hf2 | zenon_intro zenon_Hb4 ]. % 39.94/40.22 cut ((greater (age zenon_TX_u zenon_TT2_bg) (eta)) = (greater (age zenon_TX_u zenon_TT2_bg) (age zenon_TX_u zenon_TT3_t))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H140. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_Hfb. % 39.94/40.22 cut (((eta) = (age zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_Hb4]. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT2_bg) = (age zenon_TX_u zenon_TT2_bg))); [idtac | apply NNPP; zenon_intro zenon_H10f]. % 39.94/40.22 congruence. % 39.94/40.22 apply zenon_H10f. apply refl_equal. % 39.94/40.22 exact (zenon_Hb4 zenon_Hf2). % 39.94/40.22 elim (classic (greater (eta) (age zenon_TX_u zenon_TT3_t))); [ zenon_intro zenon_Hf1 | zenon_intro zenon_Hb3 ]. % 39.94/40.22 generalize (zenon_H96 (age zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H147. % 39.94/40.22 generalize (zenon_H147 (eta)). zenon_intro zenon_H148. % 39.94/40.22 generalize (zenon_H148 (age zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H149. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H149); [ zenon_intro zenon_Hfc | zenon_intro zenon_H14a ]. % 39.94/40.22 exact (zenon_Hfc zenon_Hfb). % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H14a); [ zenon_intro zenon_Hb3 | zenon_intro zenon_H13f ]. % 39.94/40.22 exact (zenon_Hb3 zenon_Hf1). % 39.94/40.22 exact (zenon_H140 zenon_H13f). % 39.94/40.22 apply (zenon_L29_ zenon_TT2_bg zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 (* end of lemma zenon_L30_ *) % 39.94/40.22 assert (zenon_L31_ : forall (zenon_TT2_bg : zenon_U) (zenon_TT3_t : zenon_U) (zenon_TT1_kx : zenon_U) (zenon_TX_u : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> ((age zenon_TX_u zenon_TT1_kx) = (eta)) -> (~(greater (age zenon_TX_u zenon_TT1_kx) (age zenon_TX_u zenon_TT3_t))) -> (greater (age zenon_TX_u zenon_TT2_bg) (eta)) -> (forall T : zenon_U, ((organization zenon_TX_u)/\(((smaller_or_equal (age zenon_TX_u T) (eta))->(has_immunity zenon_TX_u T))/\((greater (age zenon_TX_u T) (eta))->(~(has_immunity zenon_TX_u T)))))) -> (greater (age zenon_TX_u zenon_TT3_t) (age zenon_TX_u zenon_TT2_bg)) -> (~(greater (hazard_of_mortality zenon_TX_u zenon_TT3_t) (hazard_of_mortality zenon_TX_u zenon_TT2_bg))) -> False). % 39.94/40.22 do 4 intro. intros zenon_H96 zenon_H13e zenon_H14b zenon_Hfb zenon_Hb5 zenon_H49 zenon_H82. % 39.94/40.22 elim (classic (greater (eta) (age zenon_TX_u zenon_TT3_t))); [ zenon_intro zenon_Hf1 | zenon_intro zenon_Hb3 ]. % 39.94/40.22 cut ((greater (eta) (age zenon_TX_u zenon_TT3_t)) = (greater (age zenon_TX_u zenon_TT1_kx) (age zenon_TX_u zenon_TT3_t))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H14b. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_Hf1. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT3_t) = (age zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_H146]. % 39.94/40.22 cut (((eta) = (age zenon_TX_u zenon_TT1_kx))); [idtac | apply NNPP; zenon_intro zenon_H14c]. % 39.94/40.22 congruence. % 39.94/40.22 elim (classic ((age zenon_TX_u zenon_TT1_kx) = (age zenon_TX_u zenon_TT1_kx))); [ zenon_intro zenon_H14d | zenon_intro zenon_H14e ]. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT1_kx) = (age zenon_TX_u zenon_TT1_kx)) = ((eta) = (age zenon_TX_u zenon_TT1_kx))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H14c. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H14d. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT1_kx) = (age zenon_TX_u zenon_TT1_kx))); [idtac | apply NNPP; zenon_intro zenon_H14e]. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT1_kx) = (eta))); [idtac | apply NNPP; zenon_intro zenon_H121]. % 39.94/40.22 congruence. % 39.94/40.22 exact (zenon_H121 zenon_H13e). % 39.94/40.22 apply zenon_H14e. apply refl_equal. % 39.94/40.22 apply zenon_H14e. apply refl_equal. % 39.94/40.22 apply zenon_H146. apply refl_equal. % 39.94/40.22 apply (zenon_L30_ zenon_TT3_t zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 (* end of lemma zenon_L31_ *) % 39.94/40.22 assert (zenon_L32_ : forall (zenon_TT1_kx : zenon_U) (zenon_TT3_t : zenon_U) (zenon_TT2_bg : zenon_U) (zenon_TX_u : zenon_U), (greater (age zenon_TX_u zenon_TT2_bg) (eta)) -> (forall T : zenon_U, ((organization zenon_TX_u)/\(((smaller_or_equal (age zenon_TX_u T) (eta))->(has_immunity zenon_TX_u T))/\((greater (age zenon_TX_u T) (eta))->(~(has_immunity zenon_TX_u T)))))) -> (~(greater (hazard_of_mortality zenon_TX_u zenon_TT3_t) (hazard_of_mortality zenon_TX_u zenon_TT2_bg))) -> ((age zenon_TX_u zenon_TT1_kx) = (eta)) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater (age zenon_TX_u zenon_TT1_kx) (age zenon_TX_u zenon_TT2_bg))) -> (greater (age zenon_TX_u zenon_TT3_t) (age zenon_TX_u zenon_TT2_bg)) -> False). % 39.94/40.22 do 4 intro. intros zenon_Hfb zenon_Hb5 zenon_H82 zenon_H13e zenon_H96 zenon_H14f zenon_H49. % 39.94/40.22 elim (classic ((~((age zenon_TX_u zenon_TT1_kx) = (age zenon_TX_u zenon_TT3_t)))/\(~(greater (age zenon_TX_u zenon_TT1_kx) (age zenon_TX_u zenon_TT3_t))))); [ zenon_intro zenon_H150 | zenon_intro zenon_H151 ]. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H150). zenon_intro zenon_H152. zenon_intro zenon_H14b. % 39.94/40.22 apply (zenon_L31_ zenon_TT2_bg zenon_TT3_t zenon_TT1_kx zenon_TX_u); trivial. % 39.94/40.22 cut ((greater (age zenon_TX_u zenon_TT3_t) (age zenon_TX_u zenon_TT2_bg)) = (greater (age zenon_TX_u zenon_TT1_kx) (age zenon_TX_u zenon_TT2_bg))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H14f. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H49. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT2_bg) = (age zenon_TX_u zenon_TT2_bg))); [idtac | apply NNPP; zenon_intro zenon_H10f]. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT3_t) = (age zenon_TX_u zenon_TT1_kx))); [idtac | apply NNPP; zenon_intro zenon_H153]. % 39.94/40.22 congruence. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H151); [ zenon_intro zenon_H155 | zenon_intro zenon_H154 ]. % 39.94/40.22 apply zenon_H155. zenon_intro zenon_H156. % 39.94/40.22 elim (classic ((age zenon_TX_u zenon_TT1_kx) = (age zenon_TX_u zenon_TT1_kx))); [ zenon_intro zenon_H14d | zenon_intro zenon_H14e ]. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT1_kx) = (age zenon_TX_u zenon_TT1_kx)) = ((age zenon_TX_u zenon_TT3_t) = (age zenon_TX_u zenon_TT1_kx))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H153. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H14d. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT1_kx) = (age zenon_TX_u zenon_TT1_kx))); [idtac | apply NNPP; zenon_intro zenon_H14e]. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT1_kx) = (age zenon_TX_u zenon_TT3_t))); [idtac | apply NNPP; zenon_intro zenon_H152]. % 39.94/40.22 congruence. % 39.94/40.22 exact (zenon_H152 zenon_H156). % 39.94/40.22 apply zenon_H14e. apply refl_equal. % 39.94/40.22 apply zenon_H14e. apply refl_equal. % 39.94/40.22 apply zenon_H154. zenon_intro zenon_H157. % 39.94/40.22 generalize (zenon_H96 (age zenon_TX_u zenon_TT1_kx)). zenon_intro zenon_H158. % 39.94/40.22 generalize (zenon_H158 (age zenon_TX_u zenon_TT3_t)). zenon_intro zenon_H159. % 39.94/40.22 generalize (zenon_H159 (age zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H15a. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H15a); [ zenon_intro zenon_H14b | zenon_intro zenon_H15b ]. % 39.94/40.22 exact (zenon_H14b zenon_H157). % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H15b); [ zenon_intro zenon_H4e | zenon_intro zenon_H15c ]. % 39.94/40.22 exact (zenon_H4e zenon_H49). % 39.94/40.22 exact (zenon_H14f zenon_H15c). % 39.94/40.22 apply zenon_H10f. apply refl_equal. % 39.94/40.22 (* end of lemma zenon_L32_ *) % 39.94/40.22 assert (zenon_L33_ : forall (zenon_TT1_kx : zenon_U) (zenon_TT2_bg : zenon_U) (zenon_TT3_t : zenon_U) (zenon_TX_u : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater (hazard_of_mortality zenon_TX_u zenon_TT3_t) (hazard_of_mortality zenon_TX_u zenon_TT2_bg))) -> (greater (age zenon_TX_u zenon_TT3_t) (age zenon_TX_u zenon_TT2_bg)) -> (forall T : zenon_U, ((organization zenon_TX_u)/\(((smaller_or_equal (age zenon_TX_u T) (eta))->(has_immunity zenon_TX_u T))/\((greater (age zenon_TX_u T) (eta))->(~(has_immunity zenon_TX_u T)))))) -> (greater (age zenon_TX_u zenon_TT2_bg) (eta)) -> ((age zenon_TX_u zenon_TT1_kx) = (eta)) -> False). % 39.94/40.22 do 4 intro. intros zenon_H96 zenon_H82 zenon_H49 zenon_Hb5 zenon_Hfb zenon_H13e. % 39.94/40.22 generalize (zenon_Hb5 zenon_TT1_kx). zenon_intro zenon_H130. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H130). zenon_intro zenon_H2c. zenon_intro zenon_H131. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H131). zenon_intro zenon_H133. zenon_intro zenon_H132. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H133); [ zenon_intro zenon_H11a | zenon_intro zenon_H128 ]. % 39.94/40.22 apply (zenon_L28_ zenon_TT1_kx zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H132); [ zenon_intro zenon_H15d | zenon_intro zenon_H12f ]. % 39.94/40.22 elim (classic ((~((age zenon_TX_u zenon_TT1_kx) = (age zenon_TX_u zenon_TT2_bg)))/\(~(greater (age zenon_TX_u zenon_TT1_kx) (age zenon_TX_u zenon_TT2_bg))))); [ zenon_intro zenon_H15e | zenon_intro zenon_H15f ]. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H15e). zenon_intro zenon_H160. zenon_intro zenon_H14f. % 39.94/40.22 apply (zenon_L32_ zenon_TT1_kx zenon_TT3_t zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 cut ((greater (age zenon_TX_u zenon_TT2_bg) (eta)) = (greater (age zenon_TX_u zenon_TT1_kx) (eta))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H15d. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_Hfb. % 39.94/40.22 cut (((eta) = (eta))); [idtac | apply NNPP; zenon_intro zenon_H114]. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT2_bg) = (age zenon_TX_u zenon_TT1_kx))); [idtac | apply NNPP; zenon_intro zenon_H161]. % 39.94/40.22 congruence. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H15f); [ zenon_intro zenon_H163 | zenon_intro zenon_H162 ]. % 39.94/40.22 apply zenon_H163. zenon_intro zenon_H164. % 39.94/40.22 elim (classic ((age zenon_TX_u zenon_TT1_kx) = (age zenon_TX_u zenon_TT1_kx))); [ zenon_intro zenon_H14d | zenon_intro zenon_H14e ]. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT1_kx) = (age zenon_TX_u zenon_TT1_kx)) = ((age zenon_TX_u zenon_TT2_bg) = (age zenon_TX_u zenon_TT1_kx))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H161. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H14d. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT1_kx) = (age zenon_TX_u zenon_TT1_kx))); [idtac | apply NNPP; zenon_intro zenon_H14e]. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT1_kx) = (age zenon_TX_u zenon_TT2_bg))); [idtac | apply NNPP; zenon_intro zenon_H160]. % 39.94/40.22 congruence. % 39.94/40.22 exact (zenon_H160 zenon_H164). % 39.94/40.22 apply zenon_H14e. apply refl_equal. % 39.94/40.22 apply zenon_H14e. apply refl_equal. % 39.94/40.22 apply zenon_H162. zenon_intro zenon_H15c. % 39.94/40.22 generalize (zenon_H96 (age zenon_TX_u zenon_TT1_kx)). zenon_intro zenon_H158. % 39.94/40.22 generalize (zenon_H158 (age zenon_TX_u zenon_TT2_bg)). zenon_intro zenon_H165. % 39.94/40.22 generalize (zenon_H165 (eta)). zenon_intro zenon_H166. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H166); [ zenon_intro zenon_H14f | zenon_intro zenon_H167 ]. % 39.94/40.22 exact (zenon_H14f zenon_H15c). % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H167); [ zenon_intro zenon_Hfc | zenon_intro zenon_H168 ]. % 39.94/40.22 exact (zenon_Hfc zenon_Hfb). % 39.94/40.22 exact (zenon_H15d zenon_H168). % 39.94/40.22 apply zenon_H114. apply refl_equal. % 39.94/40.22 exact (zenon_H12f zenon_H128). % 39.94/40.22 (* end of lemma zenon_L33_ *) % 39.94/40.22 assert (zenon_L34_ : forall (zenon_TT1_kx : zenon_U) (zenon_TT2_bg : zenon_U) (zenon_TX_u : zenon_U), (greater (age zenon_TX_u zenon_TT2_bg) (eta)) -> (~(greater (hazard_of_mortality zenon_TX_u zenon_TT2_bg) (hazard_of_mortality zenon_TX_u zenon_TT1_kx))) -> (forall T : zenon_U, ((organization zenon_TX_u)/\(((smaller_or_equal (age zenon_TX_u T) (eta))->(has_immunity zenon_TX_u T))/\((greater (age zenon_TX_u T) (eta))->(~(has_immunity zenon_TX_u T)))))) -> ((age zenon_TX_u zenon_TT1_kx) = (eta)) -> False). % 39.94/40.22 do 3 intro. intros zenon_Hfb zenon_H127 zenon_Hb5 zenon_H13e. % 39.94/40.22 generalize (zenon_Hb5 zenon_TT1_kx). zenon_intro zenon_H130. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H130). zenon_intro zenon_H2c. zenon_intro zenon_H131. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H131). zenon_intro zenon_H133. zenon_intro zenon_H132. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H133); [ zenon_intro zenon_H11a | zenon_intro zenon_H128 ]. % 39.94/40.22 apply (zenon_L28_ zenon_TT1_kx zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_L24_ zenon_TT1_kx zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 (* end of lemma zenon_L34_ *) % 39.94/40.22 assert (zenon_L35_ : forall (zenon_TT1_kx : zenon_U) (zenon_TT0_ly : zenon_U) (zenon_TX_u : zenon_U), (~((age zenon_TX_u zenon_TT0_ly) = (eta))) -> ((age zenon_TX_u zenon_TT0_ly) = (age zenon_TX_u zenon_TT1_kx)) -> ((age zenon_TX_u zenon_TT1_kx) = (eta)) -> False). % 39.94/40.22 do 3 intro. intros zenon_H169 zenon_H16a zenon_H13e. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT0_ly) = (age zenon_TX_u zenon_TT1_kx)) = ((age zenon_TX_u zenon_TT0_ly) = (eta))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H169. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H16a. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT1_kx) = (eta))); [idtac | apply NNPP; zenon_intro zenon_H121]. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT0_ly) = (age zenon_TX_u zenon_TT0_ly))); [idtac | apply NNPP; zenon_intro zenon_H16b]. % 39.94/40.22 congruence. % 39.94/40.22 apply zenon_H16b. apply refl_equal. % 39.94/40.22 exact (zenon_H121 zenon_H13e). % 39.94/40.22 (* end of lemma zenon_L35_ *) % 39.94/40.22 apply NNPP. intro zenon_G. % 39.94/40.22 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_H96 | zenon_intro zenon_H16c ]. % 39.94/40.22 apply (zenon_notallex_s (fun X : zenon_U => (forall T0 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (forall T3 : zenon_U, (((organization X)/\((has_endowment X)/\((smaller_or_equal (age X T0) (age X T1))/\((smaller_or_equal (age X T1) (eta))/\((greater (age X T2) (eta))/\(greater (age X T3) (age X T2)))))))->((greater (hazard_of_mortality X T3) (hazard_of_mortality X T2))/\((greater (hazard_of_mortality X T2) (hazard_of_mortality X T1))/\((hazard_of_mortality X T1) = (hazard_of_mortality X T0)))))))))) zenon_G); [ zenon_intro zenon_H16d; idtac ]. % 39.94/40.22 elim zenon_H16d. zenon_intro zenon_TX_u. zenon_intro zenon_H16e. % 39.94/40.22 apply (zenon_notallex_s (fun T0 : zenon_U => (forall T1 : zenon_U, (forall T2 : zenon_U, (forall T3 : zenon_U, (((organization zenon_TX_u)/\((has_endowment zenon_TX_u)/\((smaller_or_equal (age zenon_TX_u T0) (age zenon_TX_u T1))/\((smaller_or_equal (age zenon_TX_u T1) (eta))/\((greater (age zenon_TX_u T2) (eta))/\(greater (age zenon_TX_u T3) (age zenon_TX_u T2)))))))->((greater (hazard_of_mortality zenon_TX_u T3) (hazard_of_mortality zenon_TX_u T2))/\((greater (hazard_of_mortality zenon_TX_u T2) (hazard_of_mortality zenon_TX_u T1))/\((hazard_of_mortality zenon_TX_u T1) = (hazard_of_mortality zenon_TX_u T0))))))))) zenon_H16e); [ zenon_intro zenon_H16f; idtac ]. % 39.94/40.22 elim zenon_H16f. zenon_intro zenon_TT0_ly. zenon_intro zenon_H170. % 39.94/40.22 apply (zenon_notallex_s (fun T1 : zenon_U => (forall T2 : zenon_U, (forall T3 : zenon_U, (((organization zenon_TX_u)/\((has_endowment zenon_TX_u)/\((smaller_or_equal (age zenon_TX_u zenon_TT0_ly) (age zenon_TX_u T1))/\((smaller_or_equal (age zenon_TX_u T1) (eta))/\((greater (age zenon_TX_u T2) (eta))/\(greater (age zenon_TX_u T3) (age zenon_TX_u T2)))))))->((greater (hazard_of_mortality zenon_TX_u T3) (hazard_of_mortality zenon_TX_u T2))/\((greater (hazard_of_mortality zenon_TX_u T2) (hazard_of_mortality zenon_TX_u T1))/\((hazard_of_mortality zenon_TX_u T1) = (hazard_of_mortality zenon_TX_u zenon_TT0_ly)))))))) zenon_H170); [ zenon_intro zenon_H171; idtac ]. % 39.94/40.22 elim zenon_H171. zenon_intro zenon_TT1_kx. zenon_intro zenon_H172. % 39.94/40.22 apply (zenon_notallex_s (fun T2 : zenon_U => (forall T3 : zenon_U, (((organization zenon_TX_u)/\((has_endowment zenon_TX_u)/\((smaller_or_equal (age zenon_TX_u zenon_TT0_ly) (age zenon_TX_u zenon_TT1_kx))/\((smaller_or_equal (age zenon_TX_u zenon_TT1_kx) (eta))/\((greater (age zenon_TX_u T2) (eta))/\(greater (age zenon_TX_u T3) (age zenon_TX_u T2)))))))->((greater (hazard_of_mortality zenon_TX_u T3) (hazard_of_mortality zenon_TX_u T2))/\((greater (hazard_of_mortality zenon_TX_u T2) (hazard_of_mortality zenon_TX_u zenon_TT1_kx))/\((hazard_of_mortality zenon_TX_u zenon_TT1_kx) = (hazard_of_mortality zenon_TX_u zenon_TT0_ly))))))) zenon_H172); [ zenon_intro zenon_H173; idtac ]. % 39.94/40.22 elim zenon_H173. zenon_intro zenon_TT2_bg. zenon_intro zenon_H174. % 39.94/40.22 apply (zenon_notallex_s (fun T3 : zenon_U => (((organization zenon_TX_u)/\((has_endowment zenon_TX_u)/\((smaller_or_equal (age zenon_TX_u zenon_TT0_ly) (age zenon_TX_u zenon_TT1_kx))/\((smaller_or_equal (age zenon_TX_u zenon_TT1_kx) (eta))/\((greater (age zenon_TX_u zenon_TT2_bg) (eta))/\(greater (age zenon_TX_u T3) (age zenon_TX_u zenon_TT2_bg)))))))->((greater (hazard_of_mortality zenon_TX_u T3) (hazard_of_mortality zenon_TX_u zenon_TT2_bg))/\((greater (hazard_of_mortality zenon_TX_u zenon_TT2_bg) (hazard_of_mortality zenon_TX_u zenon_TT1_kx))/\((hazard_of_mortality zenon_TX_u zenon_TT1_kx) = (hazard_of_mortality zenon_TX_u zenon_TT0_ly)))))) zenon_H174); [ zenon_intro zenon_H175; idtac ]. % 39.94/40.22 elim zenon_H175. zenon_intro zenon_TT3_t. zenon_intro zenon_H176. % 39.94/40.22 apply (zenon_notimply_s _ _ zenon_H176). zenon_intro zenon_H178. zenon_intro zenon_H177. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H178). zenon_intro zenon_H2c. zenon_intro zenon_H179. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H179). zenon_intro zenon_H17b. zenon_intro zenon_H17a. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H17a). zenon_intro zenon_H17d. zenon_intro zenon_H17c. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H17c). zenon_intro zenon_H11f. zenon_intro zenon_H17e. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H17e). zenon_intro zenon_Hfb. zenon_intro zenon_H49. % 39.94/40.22 generalize (definition_1 zenon_TX_u). zenon_intro zenon_H17f. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H17f); [ zenon_intro zenon_H181; zenon_intro zenon_H180 | zenon_intro zenon_H17b; zenon_intro zenon_Hb5 ]. % 39.94/40.22 exact (zenon_H181 zenon_H17b). % 39.94/40.22 generalize (definition_smaller_or_equal (age zenon_TX_u zenon_TT0_ly)). zenon_intro zenon_H182. % 39.94/40.22 generalize (zenon_H182 (age zenon_TX_u zenon_TT1_kx)). zenon_intro zenon_H183. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H183); [ zenon_intro zenon_H186; zenon_intro zenon_H185 | zenon_intro zenon_H17d; zenon_intro zenon_H184 ]. % 39.94/40.22 exact (zenon_H186 zenon_H17d). % 39.94/40.22 generalize (definition_smaller_or_equal (age zenon_TX_u zenon_TT1_kx)). zenon_intro zenon_H11c. % 39.94/40.22 generalize (zenon_H11c (eta)). zenon_intro zenon_H11d. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H11d); [ zenon_intro zenon_H11a; zenon_intro zenon_H120 | zenon_intro zenon_H11f; zenon_intro zenon_H11e ]. % 39.94/40.22 exact (zenon_H11a zenon_H11f). % 39.94/40.22 apply (zenon_or_s _ _ zenon_H11e); [ zenon_intro zenon_H125 | zenon_intro zenon_H13e ]. % 39.94/40.22 generalize (definition_smaller (age zenon_TX_u zenon_TT1_kx)). zenon_intro zenon_H123. % 39.94/40.22 generalize (zenon_H123 (eta)). zenon_intro zenon_H124. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H124); [ zenon_intro zenon_H122; zenon_intro zenon_H126 | zenon_intro zenon_H125; zenon_intro zenon_H119 ]. % 39.94/40.22 exact (zenon_H122 zenon_H125). % 39.94/40.22 apply (zenon_or_s _ _ zenon_H184); [ zenon_intro zenon_H187 | zenon_intro zenon_H16a ]. % 39.94/40.22 generalize (definition_smaller (age zenon_TX_u zenon_TT0_ly)). zenon_intro zenon_H188. % 39.94/40.22 generalize (zenon_H188 (age zenon_TX_u zenon_TT1_kx)). zenon_intro zenon_H189. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H189); [ zenon_intro zenon_H18c; zenon_intro zenon_H18b | zenon_intro zenon_H187; zenon_intro zenon_H18a ]. % 39.94/40.22 exact (zenon_H18c zenon_H187). % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H177); [ zenon_intro zenon_H82 | zenon_intro zenon_H18d ]. % 39.94/40.22 apply (zenon_L22_ zenon_TT2_bg zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H18d); [ zenon_intro zenon_H127 | zenon_intro zenon_H135 ]. % 39.94/40.22 apply (zenon_L25_ zenon_TT1_kx zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 generalize (zenon_Hb5 zenon_TT1_kx). zenon_intro zenon_H130. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H130). zenon_intro zenon_H2c. zenon_intro zenon_H131. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H131). zenon_intro zenon_H133. zenon_intro zenon_H132. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H133); [ zenon_intro zenon_H11a | zenon_intro zenon_H128 ]. % 39.94/40.22 apply (zenon_L23_ zenon_TT1_kx zenon_TX_u); trivial. % 39.94/40.22 generalize (zenon_Hb5 zenon_TT0_ly). zenon_intro zenon_H18e. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H18e). zenon_intro zenon_H2c. zenon_intro zenon_H18f. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H18f). zenon_intro zenon_H191. zenon_intro zenon_H190. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H191); [ zenon_intro zenon_H192 | zenon_intro zenon_H134 ]. % 39.94/40.22 generalize (definition_smaller_or_equal (age zenon_TX_u zenon_TT0_ly)). zenon_intro zenon_H182. % 39.94/40.22 generalize (zenon_H182 (eta)). zenon_intro zenon_H193. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H193); [ zenon_intro zenon_H192; zenon_intro zenon_H196 | zenon_intro zenon_H195; zenon_intro zenon_H194 ]. % 39.94/40.22 apply (zenon_notor_s _ _ zenon_H196). zenon_intro zenon_H197. zenon_intro zenon_H169. % 39.94/40.22 generalize (definition_smaller (age zenon_TX_u zenon_TT0_ly)). zenon_intro zenon_H188. % 39.94/40.22 generalize (zenon_H188 (eta)). zenon_intro zenon_H198. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H198); [ zenon_intro zenon_H197; zenon_intro zenon_H19b | zenon_intro zenon_H19a; zenon_intro zenon_H199 ]. % 39.94/40.22 generalize (zenon_H96 (eta)). zenon_intro zenon_H115. % 39.94/40.22 generalize (zenon_H115 (age zenon_TX_u zenon_TT1_kx)). zenon_intro zenon_H19c. % 39.94/40.22 generalize (zenon_H19c (age zenon_TX_u zenon_TT0_ly)). zenon_intro zenon_H19d. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H19d); [ zenon_intro zenon_H126 | zenon_intro zenon_H19e ]. % 39.94/40.22 exact (zenon_H126 zenon_H119). % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H19e); [ zenon_intro zenon_H18b | zenon_intro zenon_H199 ]. % 39.94/40.22 exact (zenon_H18b zenon_H18a). % 39.94/40.22 exact (zenon_H19b zenon_H199). % 39.94/40.22 exact (zenon_H197 zenon_H19a). % 39.94/40.22 exact (zenon_H192 zenon_H195). % 39.94/40.22 apply (zenon_L27_ zenon_TT1_kx zenon_TT0_ly zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H177); [ zenon_intro zenon_H82 | zenon_intro zenon_H18d ]. % 39.94/40.22 apply (zenon_L22_ zenon_TT2_bg zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H18d); [ zenon_intro zenon_H127 | zenon_intro zenon_H135 ]. % 39.94/40.22 apply (zenon_L25_ zenon_TT1_kx zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 generalize (zenon_Hb5 zenon_TT1_kx). zenon_intro zenon_H130. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H130). zenon_intro zenon_H2c. zenon_intro zenon_H131. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H131). zenon_intro zenon_H133. zenon_intro zenon_H132. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H133); [ zenon_intro zenon_H11a | zenon_intro zenon_H128 ]. % 39.94/40.22 apply (zenon_L23_ zenon_TT1_kx zenon_TX_u); trivial. % 39.94/40.22 generalize (zenon_Hb5 zenon_TT0_ly). zenon_intro zenon_H18e. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H18e). zenon_intro zenon_H2c. zenon_intro zenon_H18f. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H18f). zenon_intro zenon_H191. zenon_intro zenon_H190. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H191); [ zenon_intro zenon_H192 | zenon_intro zenon_H134 ]. % 39.94/40.22 generalize (definition_smaller_or_equal (age zenon_TX_u zenon_TT0_ly)). zenon_intro zenon_H182. % 39.94/40.22 generalize (zenon_H182 (eta)). zenon_intro zenon_H193. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H193); [ zenon_intro zenon_H192; zenon_intro zenon_H196 | zenon_intro zenon_H195; zenon_intro zenon_H194 ]. % 39.94/40.22 apply (zenon_notor_s _ _ zenon_H196). zenon_intro zenon_H197. zenon_intro zenon_H169. % 39.94/40.22 generalize (definition_smaller (age zenon_TX_u zenon_TT0_ly)). zenon_intro zenon_H188. % 39.94/40.22 generalize (zenon_H188 (eta)). zenon_intro zenon_H198. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H198); [ zenon_intro zenon_H197; zenon_intro zenon_H19b | zenon_intro zenon_H19a; zenon_intro zenon_H199 ]. % 39.94/40.22 cut ((greater (eta) (age zenon_TX_u zenon_TT1_kx)) = (greater (eta) (age zenon_TX_u zenon_TT0_ly))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H19b. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H119. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT1_kx) = (age zenon_TX_u zenon_TT0_ly))); [idtac | apply NNPP; zenon_intro zenon_H19f]. % 39.94/40.22 cut (((eta) = (eta))); [idtac | apply NNPP; zenon_intro zenon_H114]. % 39.94/40.22 congruence. % 39.94/40.22 apply zenon_H114. apply refl_equal. % 39.94/40.22 apply zenon_H19f. apply sym_equal. exact zenon_H16a. % 39.94/40.22 exact (zenon_H197 zenon_H19a). % 39.94/40.22 exact (zenon_H192 zenon_H195). % 39.94/40.22 apply (zenon_L27_ zenon_TT1_kx zenon_TT0_ly zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_or_s _ _ zenon_H184); [ zenon_intro zenon_H187 | zenon_intro zenon_H16a ]. % 39.94/40.22 generalize (definition_smaller (age zenon_TX_u zenon_TT0_ly)). zenon_intro zenon_H188. % 39.94/40.22 generalize (zenon_H188 (age zenon_TX_u zenon_TT1_kx)). zenon_intro zenon_H189. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H189); [ zenon_intro zenon_H18c; zenon_intro zenon_H18b | zenon_intro zenon_H187; zenon_intro zenon_H18a ]. % 39.94/40.22 exact (zenon_H18c zenon_H187). % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H177); [ zenon_intro zenon_H82 | zenon_intro zenon_H18d ]. % 39.94/40.22 apply (zenon_L33_ zenon_TT1_kx zenon_TT2_bg zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H18d); [ zenon_intro zenon_H127 | zenon_intro zenon_H135 ]. % 39.94/40.22 apply (zenon_L34_ zenon_TT1_kx zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 generalize (zenon_Hb5 zenon_TT0_ly). zenon_intro zenon_H18e. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H18e). zenon_intro zenon_H2c. zenon_intro zenon_H18f. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H18f). zenon_intro zenon_H191. zenon_intro zenon_H190. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H191); [ zenon_intro zenon_H192 | zenon_intro zenon_H134 ]. % 39.94/40.22 generalize (definition_smaller_or_equal (age zenon_TX_u zenon_TT0_ly)). zenon_intro zenon_H182. % 39.94/40.22 generalize (zenon_H182 (eta)). zenon_intro zenon_H193. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H193); [ zenon_intro zenon_H192; zenon_intro zenon_H196 | zenon_intro zenon_H195; zenon_intro zenon_H194 ]. % 39.94/40.22 apply (zenon_notor_s _ _ zenon_H196). zenon_intro zenon_H197. zenon_intro zenon_H169. % 39.94/40.22 generalize (definition_smaller (age zenon_TX_u zenon_TT0_ly)). zenon_intro zenon_H188. % 39.94/40.22 generalize (zenon_H188 (eta)). zenon_intro zenon_H198. % 39.94/40.22 apply (zenon_equiv_s _ _ zenon_H198); [ zenon_intro zenon_H197; zenon_intro zenon_H19b | zenon_intro zenon_H19a; zenon_intro zenon_H199 ]. % 39.94/40.22 elim (classic ((~((eta) = (age zenon_TX_u zenon_TT1_kx)))/\(~(greater (eta) (age zenon_TX_u zenon_TT1_kx))))); [ zenon_intro zenon_H1a0 | zenon_intro zenon_H1a1 ]. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H1a0). zenon_intro zenon_H14c. zenon_intro zenon_H126. % 39.94/40.22 apply zenon_H14c. apply sym_equal. exact zenon_H13e. % 39.94/40.22 cut ((greater (age zenon_TX_u zenon_TT1_kx) (age zenon_TX_u zenon_TT0_ly)) = (greater (eta) (age zenon_TX_u zenon_TT0_ly))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H19b. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H18a. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT0_ly) = (age zenon_TX_u zenon_TT0_ly))); [idtac | apply NNPP; zenon_intro zenon_H16b]. % 39.94/40.22 cut (((age zenon_TX_u zenon_TT1_kx) = (eta))); [idtac | apply NNPP; zenon_intro zenon_H121]. % 39.94/40.22 congruence. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H1a1); [ zenon_intro zenon_H1a3 | zenon_intro zenon_H1a2 ]. % 39.94/40.22 apply zenon_H1a3. zenon_intro zenon_H1a4. % 39.94/40.22 elim (classic ((eta) = (eta))); [ zenon_intro zenon_H113 | zenon_intro zenon_H114 ]. % 39.94/40.22 cut (((eta) = (eta)) = ((age zenon_TX_u zenon_TT1_kx) = (eta))). % 39.94/40.22 intro zenon_D_pnotp. % 39.94/40.22 apply zenon_H121. % 39.94/40.22 rewrite <- zenon_D_pnotp. % 39.94/40.22 exact zenon_H113. % 39.94/40.22 cut (((eta) = (eta))); [idtac | apply NNPP; zenon_intro zenon_H114]. % 39.94/40.22 cut (((eta) = (age zenon_TX_u zenon_TT1_kx))); [idtac | apply NNPP; zenon_intro zenon_H14c]. % 39.94/40.22 congruence. % 39.94/40.22 exact (zenon_H14c zenon_H1a4). % 39.94/40.22 apply zenon_H114. apply refl_equal. % 39.94/40.22 apply zenon_H114. apply refl_equal. % 39.94/40.22 apply zenon_H1a2. zenon_intro zenon_H119. % 39.94/40.22 generalize (zenon_H96 (eta)). zenon_intro zenon_H115. % 39.94/40.22 generalize (zenon_H115 (age zenon_TX_u zenon_TT1_kx)). zenon_intro zenon_H19c. % 39.94/40.22 generalize (zenon_H19c (age zenon_TX_u zenon_TT0_ly)). zenon_intro zenon_H19d. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H19d); [ zenon_intro zenon_H126 | zenon_intro zenon_H19e ]. % 39.94/40.22 exact (zenon_H126 zenon_H119). % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H19e); [ zenon_intro zenon_H18b | zenon_intro zenon_H199 ]. % 39.94/40.22 exact (zenon_H18b zenon_H18a). % 39.94/40.22 exact (zenon_H19b zenon_H199). % 39.94/40.22 apply zenon_H16b. apply refl_equal. % 39.94/40.22 exact (zenon_H197 zenon_H19a). % 39.94/40.22 exact (zenon_H192 zenon_H195). % 39.94/40.22 generalize (zenon_Hb5 zenon_TT1_kx). zenon_intro zenon_H130. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H130). zenon_intro zenon_H2c. zenon_intro zenon_H131. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H131). zenon_intro zenon_H133. zenon_intro zenon_H132. % 39.94/40.22 apply (zenon_imply_s _ _ zenon_H133); [ zenon_intro zenon_H11a | zenon_intro zenon_H128 ]. % 39.94/40.22 apply (zenon_L28_ zenon_TT1_kx zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_L27_ zenon_TT1_kx zenon_TT0_ly zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H177); [ zenon_intro zenon_H82 | zenon_intro zenon_H18d ]. % 39.94/40.22 apply (zenon_L33_ zenon_TT1_kx zenon_TT2_bg zenon_TT3_t zenon_TX_u); trivial. % 39.94/40.22 apply (zenon_notand_s _ _ zenon_H18d); [ zenon_intro zenon_H127 | zenon_intro zenon_H135 ]. % 39.94/40.22 apply (zenon_L34_ zenon_TT1_kx zenon_TT2_bg zenon_TX_u); trivial. % 39.94/40.22 generalize (zenon_Hb5 zenon_TT1_kx). zenon_intro zenon_H130. % 39.94/40.22 apply (zenon_and_s _ _ zenon_H130). zenon_intro zenon_H2c. zenon_intro zenon_H131. % 39.94/40.24 apply (zenon_and_s _ _ zenon_H131). zenon_intro zenon_H133. zenon_intro zenon_H132. % 39.94/40.24 apply (zenon_imply_s _ _ zenon_H133); [ zenon_intro zenon_H11a | zenon_intro zenon_H128 ]. % 39.94/40.24 apply (zenon_L28_ zenon_TT1_kx zenon_TX_u); trivial. % 39.94/40.24 generalize (zenon_Hb5 zenon_TT0_ly). zenon_intro zenon_H18e. % 39.94/40.24 apply (zenon_and_s _ _ zenon_H18e). zenon_intro zenon_H2c. zenon_intro zenon_H18f. % 39.94/40.24 apply (zenon_and_s _ _ zenon_H18f). zenon_intro zenon_H191. zenon_intro zenon_H190. % 39.94/40.24 apply (zenon_imply_s _ _ zenon_H191); [ zenon_intro zenon_H192 | zenon_intro zenon_H134 ]. % 39.94/40.24 generalize (definition_smaller_or_equal (age zenon_TX_u zenon_TT0_ly)). zenon_intro zenon_H182. % 39.94/40.24 generalize (zenon_H182 (eta)). zenon_intro zenon_H193. % 39.94/40.24 apply (zenon_equiv_s _ _ zenon_H193); [ zenon_intro zenon_H192; zenon_intro zenon_H196 | zenon_intro zenon_H195; zenon_intro zenon_H194 ]. % 39.94/40.24 apply (zenon_notor_s _ _ zenon_H196). zenon_intro zenon_H197. zenon_intro zenon_H169. % 39.94/40.24 apply (zenon_L35_ zenon_TT1_kx zenon_TT0_ly zenon_TX_u); trivial. % 39.94/40.24 exact (zenon_H192 zenon_H195). % 39.94/40.24 apply (zenon_L27_ zenon_TT1_kx zenon_TT0_ly zenon_TX_u); trivial. % 39.94/40.24 apply zenon_H16c. zenon_intro zenon_Tx_qf. apply NNPP. zenon_intro zenon_H1a6. % 39.94/40.24 apply zenon_H1a6. zenon_intro zenon_Ty_qh. apply NNPP. zenon_intro zenon_H1a8. % 39.94/40.24 apply zenon_H1a8. zenon_intro zenon_Tz_qj. apply NNPP. zenon_intro zenon_H1aa. % 39.94/40.24 apply (zenon_notimply_s _ _ zenon_H1aa). zenon_intro zenon_H1ac. zenon_intro zenon_H1ab. % 39.94/40.24 apply (zenon_notimply_s _ _ zenon_H1ab). zenon_intro zenon_H1ae. zenon_intro zenon_H1ad. % 39.94/40.24 generalize (meaning_postulate_greater_transitive zenon_Tx_qf). zenon_intro zenon_H1af. % 39.94/40.24 generalize (zenon_H1af zenon_Ty_qh). zenon_intro zenon_H1b0. % 39.94/40.24 generalize (zenon_H1b0 zenon_Tz_qj). zenon_intro zenon_H1b1. % 39.94/40.24 apply (zenon_imply_s _ _ zenon_H1b1); [ zenon_intro zenon_H1b3 | zenon_intro zenon_H1b2 ]. % 39.94/40.24 apply (zenon_notand_s _ _ zenon_H1b3); [ zenon_intro zenon_H1b5 | zenon_intro zenon_H1b4 ]. % 39.94/40.24 exact (zenon_H1b5 zenon_H1ac). % 39.94/40.24 exact (zenon_H1b4 zenon_H1ae). % 39.94/40.24 exact (zenon_H1ad zenon_H1b2). % 39.94/40.24 Qed. % 39.94/40.24 % SZS output end Proof % 39.94/40.24 (* END-PROOF *) % 39.94/40.24 nodes searched: 2981578 % 39.94/40.24 max branch formulas: 8989 % 39.94/40.24 proof nodes created: 12120 % 39.94/40.24 formulas created: 538692 % 39.94/40.24 %------------------------------------------------------------------------------