%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT062+1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n006.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:25 AM UTC 2026 % Result : Theorem 40.93s 41.27s % Output : Proof 40.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT062+1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_zenon %s %d % 0.10/0.38 % Computer : n006.cluster.edu % 0.10/0.38 % Model : x86_64 x86_64 % 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.38 % Memory : 8046.5625MB % 0.10/0.38 % OS : Linux 6.8.0-71-generic % 0.10/0.38 % CPULimit : 300 % 0.10/0.38 % WCLimit : 300 % 0.10/0.38 % DateTime : Mon Sep 7 13:37:01 UTC 2026 % 0.10/0.39 % CPUTime : % 40.93/41.27 (* PROOF-FOUND *) % 40.93/41.27 % SZS status Theorem % 40.93/41.27 (* BEGIN-PROOF *) % 40.93/41.27 % SZS output start Proof % 40.93/41.27 Theorem theorem_8 : (forall X : zenon_U, (forall T0 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization X)/\((robust_position X)/\((~(has_endowment X))/\(((age X T0) = (zero))/\((greater (sigma) (zero))/\((greater (tau) (zero))/\(((sigma) = (tau))/\((smaller_or_equal (age X T1) (sigma))/\(greater (age X T2) (sigma))))))))))->((smaller (hazard_of_mortality X T2) (hazard_of_mortality X T1))/\((hazard_of_mortality X T1) = (hazard_of_mortality X T0)))))))). % 40.93/41.27 Proof. % 40.93/41.27 assert (zenon_L1_ : forall (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> ((sigma) = (tau)) -> (greater (sigma) (age zenon_TX_t zenon_TT1_s)) -> (~(smaller_or_equal (age zenon_TX_t zenon_TT1_s) (tau))) -> False). % 40.93/41.27 do 2 intro. intros zenon_He zenon_Hf zenon_H10 zenon_H11. % 40.93/41.27 generalize (definition_smaller_or_equal (age zenon_TX_t zenon_TT1_s)). zenon_intro zenon_H14. % 40.93/41.27 generalize (zenon_H14 (tau)). zenon_intro zenon_H15. % 40.93/41.27 apply (zenon_equiv_s _ _ zenon_H15); [ zenon_intro zenon_H11; zenon_intro zenon_H18 | zenon_intro zenon_H17; zenon_intro zenon_H16 ]. % 40.93/41.27 apply (zenon_notor_s _ _ zenon_H18). zenon_intro zenon_H1a. zenon_intro zenon_H19. % 40.93/41.27 generalize (definition_smaller (age zenon_TX_t zenon_TT1_s)). zenon_intro zenon_H1b. % 40.93/41.27 generalize (zenon_H1b (tau)). zenon_intro zenon_H1c. % 40.93/41.27 apply (zenon_equiv_s _ _ zenon_H1c); [ zenon_intro zenon_H1a; zenon_intro zenon_H1f | zenon_intro zenon_H1e; zenon_intro zenon_H1d ]. % 40.93/41.27 elim (classic ((~((tau) = (sigma)))/\(~(greater (tau) (sigma))))); [ zenon_intro zenon_H20 | zenon_intro zenon_H21 ]. % 40.93/41.27 apply (zenon_and_s _ _ zenon_H20). zenon_intro zenon_H23. zenon_intro zenon_H22. % 40.93/41.27 apply zenon_H23. apply sym_equal. exact zenon_Hf. % 40.93/41.27 cut ((greater (sigma) (age zenon_TX_t zenon_TT1_s)) = (greater (tau) (age zenon_TX_t zenon_TT1_s))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_H1f. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_H10. % 40.93/41.27 cut (((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_H24]. % 40.93/41.27 cut (((sigma) = (tau))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 40.93/41.27 congruence. % 40.93/41.27 apply (zenon_notand_s _ _ zenon_H21); [ zenon_intro zenon_H27 | zenon_intro zenon_H26 ]. % 40.93/41.27 apply zenon_H27. zenon_intro zenon_H28. % 40.93/41.27 elim (classic ((tau) = (tau))); [ zenon_intro zenon_H29 | zenon_intro zenon_H2a ]. % 40.93/41.27 cut (((tau) = (tau)) = ((sigma) = (tau))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_H25. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_H29. % 40.93/41.27 cut (((tau) = (tau))); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 40.93/41.27 cut (((tau) = (sigma))); [idtac | apply NNPP; zenon_intro zenon_H23]. % 40.93/41.27 congruence. % 40.93/41.27 exact (zenon_H23 zenon_H28). % 40.93/41.27 apply zenon_H2a. apply refl_equal. % 40.93/41.27 apply zenon_H2a. apply refl_equal. % 40.93/41.27 apply zenon_H26. zenon_intro zenon_H2b. % 40.93/41.27 generalize (zenon_He (tau)). zenon_intro zenon_H2c. % 40.93/41.27 generalize (zenon_H2c (sigma)). zenon_intro zenon_H2d. % 40.93/41.27 generalize (zenon_H2d (age zenon_TX_t zenon_TT1_s)). zenon_intro zenon_H2e. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H2e); [ zenon_intro zenon_H22 | zenon_intro zenon_H2f ]. % 40.93/41.27 exact (zenon_H22 zenon_H2b). % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H2f); [ zenon_intro zenon_H30 | zenon_intro zenon_H1d ]. % 40.93/41.27 exact (zenon_H30 zenon_H10). % 40.93/41.27 exact (zenon_H1f zenon_H1d). % 40.93/41.27 apply zenon_H24. apply refl_equal. % 40.93/41.27 exact (zenon_H1a zenon_H1e). % 40.93/41.27 exact (zenon_H11 zenon_H17). % 40.93/41.27 (* end of lemma zenon_L1_ *) % 40.93/41.27 assert (zenon_L2_ : (~((tau) = (tau))) -> False). % 40.93/41.27 do 0 intro. intros zenon_H2a. % 40.93/41.27 apply zenon_H2a. apply refl_equal. % 40.93/41.27 (* end of lemma zenon_L2_ *) % 40.93/41.27 assert (zenon_L3_ : forall (zenon_TT2_bz : zenon_U) (zenon_TX_t : zenon_U), (~(greater (age zenon_TX_t zenon_TT2_bz) (tau))) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> ((sigma) = (tau)) -> False). % 40.93/41.27 do 2 intro. intros zenon_H31 zenon_H32 zenon_Hf. % 40.93/41.27 cut ((greater (age zenon_TX_t zenon_TT2_bz) (sigma)) = (greater (age zenon_TX_t zenon_TT2_bz) (tau))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_H31. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_H32. % 40.93/41.27 cut (((sigma) = (tau))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 40.93/41.27 cut (((age zenon_TX_t zenon_TT2_bz) = (age zenon_TX_t zenon_TT2_bz))); [idtac | apply NNPP; zenon_intro zenon_H34]. % 40.93/41.27 congruence. % 40.93/41.27 apply zenon_H34. apply refl_equal. % 40.93/41.27 exact (zenon_H25 zenon_Hf). % 40.93/41.27 (* end of lemma zenon_L3_ *) % 40.93/41.27 assert (zenon_L4_ : forall (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), (~(~(has_immunity zenon_TX_t zenon_TT1_s))) -> (organization zenon_TX_t) -> (~(has_endowment zenon_TX_t)) -> False). % 40.93/41.27 do 2 intro. intros zenon_H35 zenon_H36 zenon_H37. % 40.93/41.27 apply zenon_H35. zenon_intro zenon_H38. % 40.93/41.27 generalize (assumption_1 zenon_TX_t). zenon_intro zenon_H39. % 40.93/41.27 generalize (zenon_H39 zenon_TT1_s). zenon_intro zenon_H3a. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H3a); [ zenon_intro zenon_H3c | zenon_intro zenon_H3b ]. % 40.93/41.27 apply (zenon_notand_s _ _ zenon_H3c); [ zenon_intro zenon_H3e | zenon_intro zenon_H3d ]. % 40.93/41.27 exact (zenon_H3e zenon_H36). % 40.93/41.27 exact (zenon_H3d zenon_H37). % 40.93/41.27 exact (zenon_H3b zenon_H38). % 40.93/41.27 (* end of lemma zenon_L4_ *) % 40.93/41.27 assert (zenon_L5_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> (~(is_aligned zenon_TX_t zenon_TT1_s)) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> False). % 40.93/41.27 do 3 intro. intros zenon_H3f zenon_H40 zenon_H41 zenon_H42 zenon_H43 zenon_H36. % 40.93/41.27 generalize (zenon_H3f zenon_TT0_cq). zenon_intro zenon_H45. % 40.93/41.27 generalize (zenon_H45 zenon_TT1_s). zenon_intro zenon_H46. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H46); [ zenon_intro zenon_H48 | zenon_intro zenon_H47 ]. % 40.93/41.27 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H3e | zenon_intro zenon_H49 ]. % 40.93/41.27 exact (zenon_H3e zenon_H36). % 40.93/41.27 exact (zenon_H49 zenon_H43). % 40.93/41.27 apply (zenon_equiv_s _ _ zenon_H47); [ zenon_intro zenon_H42; zenon_intro zenon_H4c | zenon_intro zenon_H4b; zenon_intro zenon_H4a ]. % 40.93/41.27 generalize (definition_2 zenon_TX_t). zenon_intro zenon_H4d. % 40.93/41.27 generalize (zenon_H4d zenon_TT0_cq). zenon_intro zenon_H4e. % 40.93/41.27 generalize (zenon_H4e zenon_TT1_s). zenon_intro zenon_H4f. % 40.93/41.27 apply (zenon_equiv_s _ _ zenon_H4f); [ zenon_intro zenon_H4c; zenon_intro zenon_H51 | zenon_intro zenon_H4a; zenon_intro zenon_H50 ]. % 40.93/41.27 apply (zenon_notand_s _ _ zenon_H51); [ zenon_intro zenon_H3e | zenon_intro zenon_H52 ]. % 40.93/41.27 exact (zenon_H3e zenon_H36). % 40.93/41.27 apply zenon_H52. zenon_intro zenon_H53. % 40.93/41.27 apply (zenon_equiv_s _ _ zenon_H53); [ zenon_intro zenon_H55; zenon_intro zenon_H41 | zenon_intro zenon_H40; zenon_intro zenon_H54 ]. % 40.93/41.27 exact (zenon_H55 zenon_H40). % 40.93/41.27 exact (zenon_H41 zenon_H54). % 40.93/41.27 exact (zenon_H4c zenon_H4a). % 40.93/41.27 exact (zenon_H42 zenon_H4b). % 40.93/41.27 (* end of lemma zenon_L5_ *) % 40.93/41.27 assert (zenon_L6_ : forall (zenon_TT1_s : zenon_U) (zenon_TX_t : 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, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (positional_advantage zenon_TX_t zenon_TT1_s) -> (greater (sigma) (age zenon_TX_t zenon_TT1_s)) -> ((sigma) = (tau)) -> False). % 40.93/41.27 do 2 intro. intros zenon_He zenon_H56 zenon_H57 zenon_H10 zenon_Hf. % 40.93/41.27 generalize (zenon_H56 zenon_TT1_s). zenon_intro zenon_H58. % 40.93/41.27 apply (zenon_and_s _ _ zenon_H58). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_H11 | zenon_intro zenon_H5b ]. % 40.93/41.27 apply (zenon_L1_ zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.27 exact (zenon_H5b zenon_H57). % 40.93/41.27 (* end of lemma zenon_L6_ *) % 40.93/41.27 assert (zenon_L7_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : 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_t)->(((has_immunity zenon_TX_t T)->((hazard_of_mortality zenon_TX_t T) = (very_low)))/\((~(has_immunity zenon_TX_t T))->((((is_aligned zenon_TX_t T)/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (low)))/\((((~(is_aligned zenon_TX_t T))/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (mod1)))/\((((is_aligned zenon_TX_t T)/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (mod2)))/\(((~(is_aligned zenon_TX_t T))/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (high)))))))))) -> (organization zenon_TX_t) -> (~(has_endowment zenon_TX_t)) -> (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (greater (sigma) (age zenon_TX_t zenon_TT1_s)) -> ((sigma) = (tau)) -> (~((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))) -> False). % 40.93/41.27 do 3 intro. intros zenon_He zenon_H5c zenon_H36 zenon_H37 zenon_H3f zenon_H40 zenon_H42 zenon_H43 zenon_H56 zenon_H10 zenon_Hf zenon_H5d. % 40.93/41.27 generalize (zenon_H5c zenon_TT1_s). zenon_intro zenon_H5e. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H5e); [ zenon_intro zenon_H3e | zenon_intro zenon_H5f ]. % 40.93/41.27 exact (zenon_H3e zenon_H36). % 40.93/41.27 apply (zenon_and_s _ _ zenon_H5f). zenon_intro zenon_H61. zenon_intro zenon_H60. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H60); [ zenon_intro zenon_H35 | zenon_intro zenon_H62 ]. % 40.93/41.27 apply (zenon_L4_ zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.27 apply (zenon_and_s _ _ zenon_H62). zenon_intro zenon_H64. zenon_intro zenon_H63. % 40.93/41.27 apply (zenon_and_s _ _ zenon_H63). zenon_intro zenon_H66. zenon_intro zenon_H65. % 40.93/41.27 apply (zenon_and_s _ _ zenon_H65). zenon_intro zenon_H68. zenon_intro zenon_H67. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H68); [ zenon_intro zenon_H6a | zenon_intro zenon_H69 ]. % 40.93/41.27 apply (zenon_notand_s _ _ zenon_H6a); [ zenon_intro zenon_H41 | zenon_intro zenon_H6b ]. % 40.93/41.27 apply (zenon_L5_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 apply zenon_H6b. zenon_intro zenon_H57. % 40.93/41.27 apply (zenon_L6_ zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.27 apply zenon_H5d. apply sym_equal. exact zenon_H69. % 40.93/41.27 (* end of lemma zenon_L7_ *) % 40.93/41.27 assert (zenon_L8_ : forall (zenon_TT2_bz : zenon_U) (zenon_TX_t : zenon_U), (~(~(has_immunity zenon_TX_t zenon_TT2_bz))) -> (organization zenon_TX_t) -> (~(has_endowment zenon_TX_t)) -> False). % 40.93/41.27 do 2 intro. intros zenon_H6c zenon_H36 zenon_H37. % 40.93/41.27 apply zenon_H6c. zenon_intro zenon_H6d. % 40.93/41.27 generalize (assumption_1 zenon_TX_t). zenon_intro zenon_H39. % 40.93/41.27 generalize (zenon_H39 zenon_TT2_bz). zenon_intro zenon_H6e. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H6e); [ zenon_intro zenon_H3c | zenon_intro zenon_H6f ]. % 40.93/41.27 apply (zenon_notand_s _ _ zenon_H3c); [ zenon_intro zenon_H3e | zenon_intro zenon_H3d ]. % 40.93/41.27 exact (zenon_H3e zenon_H36). % 40.93/41.27 exact (zenon_H3d zenon_H37). % 40.93/41.27 exact (zenon_H6f zenon_H6d). % 40.93/41.27 (* end of lemma zenon_L8_ *) % 40.93/41.27 assert (zenon_L9_ : forall (zenon_TT2_bz : zenon_U) (zenon_TX_t : zenon_U), (((~(is_aligned zenon_TX_t zenon_TT2_bz))/\(positional_advantage zenon_TX_t zenon_TT2_bz))->((hazard_of_mortality zenon_TX_t zenon_TT2_bz) = (mod1))) -> (positional_advantage zenon_TX_t zenon_TT2_bz) -> (~(is_aligned zenon_TX_t zenon_TT2_bz)) -> (~((mod1) = (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> False). % 40.93/41.27 do 2 intro. intros zenon_H70 zenon_H71 zenon_H72 zenon_H73. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H70); [ zenon_intro zenon_H75 | zenon_intro zenon_H74 ]. % 40.93/41.27 apply (zenon_notand_s _ _ zenon_H75); [ zenon_intro zenon_H77 | zenon_intro zenon_H76 ]. % 40.93/41.27 exact (zenon_H77 zenon_H72). % 40.93/41.27 exact (zenon_H76 zenon_H71). % 40.93/41.27 apply zenon_H73. apply sym_equal. exact zenon_H74. % 40.93/41.27 (* end of lemma zenon_L9_ *) % 40.93/41.27 assert (zenon_L10_ : forall (zenon_TT2_bz : zenon_U) (zenon_TX_t : zenon_U), (~((mod1) = (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> (positional_advantage zenon_TX_t zenon_TT2_bz) -> (~(is_aligned zenon_TX_t zenon_TT2_bz)) -> (~(has_endowment zenon_TX_t)) -> (organization zenon_TX_t) -> False). % 40.93/41.27 do 2 intro. intros zenon_H73 zenon_H71 zenon_H72 zenon_H37 zenon_H36. % 40.93/41.27 generalize (assumption_17 zenon_TX_t). zenon_intro zenon_H5c. % 40.93/41.27 generalize (zenon_H5c zenon_TT2_bz). zenon_intro zenon_H78. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H78); [ zenon_intro zenon_H3e | zenon_intro zenon_H79 ]. % 40.93/41.27 exact (zenon_H3e zenon_H36). % 40.93/41.27 apply (zenon_and_s _ _ zenon_H79). zenon_intro zenon_H7b. zenon_intro zenon_H7a. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H7a); [ zenon_intro zenon_H6c | zenon_intro zenon_H7c ]. % 40.93/41.27 apply (zenon_L8_ zenon_TT2_bz zenon_TX_t); trivial. % 40.93/41.27 apply (zenon_and_s _ _ zenon_H7c). zenon_intro zenon_H7e. zenon_intro zenon_H7d. % 40.93/41.27 apply (zenon_and_s _ _ zenon_H7d). zenon_intro zenon_H70. zenon_intro zenon_H7f. % 40.93/41.27 apply (zenon_L9_ zenon_TT2_bz zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L10_ *) % 40.93/41.27 assert (zenon_L11_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT2_bz : zenon_U) (zenon_TX_t : zenon_U), (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> (~(has_endowment zenon_TX_t)) -> (positional_advantage zenon_TX_t zenon_TT2_bz) -> (~((mod1) = (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> False). % 40.93/41.27 do 3 intro. intros zenon_H3f zenon_H32 zenon_H37 zenon_H71 zenon_H73 zenon_H40 zenon_H43 zenon_H36. % 40.93/41.27 generalize (zenon_H3f zenon_TT0_cq). zenon_intro zenon_H45. % 40.93/41.27 generalize (zenon_H45 zenon_TT2_bz). zenon_intro zenon_H80. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H80); [ zenon_intro zenon_H48 | zenon_intro zenon_H81 ]. % 40.93/41.27 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H3e | zenon_intro zenon_H49 ]. % 40.93/41.27 exact (zenon_H3e zenon_H36). % 40.93/41.27 exact (zenon_H49 zenon_H43). % 40.93/41.27 apply (zenon_equiv_s _ _ zenon_H81); [ zenon_intro zenon_H84; zenon_intro zenon_H83 | zenon_intro zenon_H32; zenon_intro zenon_H82 ]. % 40.93/41.27 exact (zenon_H84 zenon_H32). % 40.93/41.27 generalize (definition_2 zenon_TX_t). zenon_intro zenon_H4d. % 40.93/41.27 generalize (zenon_H4d zenon_TT0_cq). zenon_intro zenon_H4e. % 40.93/41.27 generalize (zenon_H4e zenon_TT2_bz). zenon_intro zenon_H85. % 40.93/41.27 apply (zenon_equiv_s _ _ zenon_H85); [ zenon_intro zenon_H83; zenon_intro zenon_H87 | zenon_intro zenon_H82; zenon_intro zenon_H86 ]. % 40.93/41.27 exact (zenon_H83 zenon_H82). % 40.93/41.27 apply (zenon_and_s _ _ zenon_H86). zenon_intro zenon_H36. zenon_intro zenon_H88. % 40.93/41.27 apply (zenon_notequiv_s _ _ zenon_H88); [ zenon_intro zenon_H55; zenon_intro zenon_H89 | zenon_intro zenon_H40; zenon_intro zenon_H72 ]. % 40.93/41.27 exact (zenon_H55 zenon_H40). % 40.93/41.27 apply (zenon_L10_ zenon_TT2_bz zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L11_ *) % 40.93/41.27 assert (zenon_L12_ : forall (zenon_TT2_bz : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : 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_t)/\((age zenon_TX_t T) = (zero)))->(is_aligned zenon_TX_t T))) -> (organization zenon_TX_t) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (~(greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> (positional_advantage zenon_TX_t zenon_TT2_bz) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> ((sigma) = (tau)) -> (greater (sigma) (age zenon_TX_t zenon_TT1_s)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> (~(has_endowment zenon_TX_t)) -> False). % 40.93/41.27 do 4 intro. intros zenon_He zenon_H8a zenon_H36 zenon_H43 zenon_H8b zenon_H71 zenon_H32 zenon_Hf zenon_H10 zenon_H56 zenon_H42 zenon_H37. % 40.93/41.27 generalize (assumption_15 zenon_TX_t). zenon_intro zenon_H3f. % 40.93/41.27 generalize (assumption_17 zenon_TX_t). zenon_intro zenon_H5c. % 40.93/41.27 generalize (zenon_H8a zenon_TT0_cq). zenon_intro zenon_H8c. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H8c); [ zenon_intro zenon_H48 | zenon_intro zenon_H40 ]. % 40.93/41.27 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H3e | zenon_intro zenon_H49 ]. % 40.93/41.27 exact (zenon_H3e zenon_H36). % 40.93/41.27 exact (zenon_H49 zenon_H43). % 40.93/41.27 cut ((greater (mod2) (mod1)) = (greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_H8b. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact assumption_19. % 40.93/41.27 cut (((mod1) = (hazard_of_mortality zenon_TX_t zenon_TT2_bz))); [idtac | apply NNPP; zenon_intro zenon_H73]. % 40.93/41.27 cut (((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 40.93/41.27 congruence. % 40.93/41.27 apply (zenon_L7_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 apply (zenon_L11_ zenon_TT0_cq zenon_TT2_bz zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L12_ *) % 40.93/41.27 assert (zenon_L13_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TT2_bz : zenon_U) (zenon_TX_t : 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_t zenon_TT2_bz) (sigma)) -> ((sigma) = (tau)) -> (organization zenon_TX_t) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (~(greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> (greater (sigma) (age zenon_TX_t zenon_TT1_s)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> (~(has_endowment zenon_TX_t)) -> False). % 40.93/41.27 do 4 intro. intros zenon_He zenon_H32 zenon_Hf zenon_H36 zenon_H43 zenon_H8b zenon_H10 zenon_H56 zenon_H42 zenon_H37. % 40.93/41.27 generalize (assumption_13 zenon_TX_t). zenon_intro zenon_H8a. % 40.93/41.27 generalize (zenon_H56 zenon_TT2_bz). zenon_intro zenon_H8d. % 40.93/41.27 apply (zenon_and_s _ _ zenon_H8d). zenon_intro zenon_H8f. zenon_intro zenon_H8e. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H8e); [ zenon_intro zenon_H31 | zenon_intro zenon_H71 ]. % 40.93/41.27 apply (zenon_L3_ zenon_TT2_bz zenon_TX_t); trivial. % 40.93/41.27 apply (zenon_L12_ zenon_TT2_bz zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L13_ *) % 40.93/41.27 assert (zenon_L14_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT2_bz : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TX_t : 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_t zenon_TT1_s) (tau))) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> ((sigma) = (tau)) -> (organization zenon_TX_t) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (~(greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> (greater (sigma) (age zenon_TX_t zenon_TT1_s)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (~(has_endowment zenon_TX_t)) -> False). % 40.93/41.27 do 4 intro. intros zenon_He zenon_H90 zenon_H32 zenon_Hf zenon_H36 zenon_H43 zenon_H8b zenon_H10 zenon_H56 zenon_H37. % 40.93/41.27 elim (classic (greater (age zenon_TX_t zenon_TT1_s) (sigma))); [ zenon_intro zenon_H4b | zenon_intro zenon_H42 ]. % 40.93/41.27 cut ((greater (age zenon_TX_t zenon_TT1_s) (sigma)) = (greater (age zenon_TX_t zenon_TT1_s) (tau))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_H90. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_H4b. % 40.93/41.27 cut (((sigma) = (tau))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 40.93/41.27 cut (((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_H24]. % 40.93/41.27 congruence. % 40.93/41.27 apply zenon_H24. apply refl_equal. % 40.93/41.27 exact (zenon_H25 zenon_Hf). % 40.93/41.27 apply (zenon_L13_ zenon_TT1_s zenon_TT0_cq zenon_TT2_bz zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L14_ *) % 40.93/41.27 assert (zenon_L15_ : forall (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (~(~(has_immunity zenon_TX_t zenon_TT0_cq))) -> (organization zenon_TX_t) -> (~(has_endowment zenon_TX_t)) -> False). % 40.93/41.27 do 2 intro. intros zenon_H91 zenon_H36 zenon_H37. % 40.93/41.27 apply zenon_H91. zenon_intro zenon_H92. % 40.93/41.27 generalize (assumption_1 zenon_TX_t). zenon_intro zenon_H39. % 40.93/41.27 generalize (zenon_H39 zenon_TT0_cq). zenon_intro zenon_H93. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H93); [ zenon_intro zenon_H3c | zenon_intro zenon_H94 ]. % 40.93/41.27 apply (zenon_notand_s _ _ zenon_H3c); [ zenon_intro zenon_H3e | zenon_intro zenon_H3d ]. % 40.93/41.27 exact (zenon_H3e zenon_H36). % 40.93/41.27 exact (zenon_H3d zenon_H37). % 40.93/41.27 exact (zenon_H94 zenon_H92). % 40.93/41.27 (* end of lemma zenon_L15_ *) % 40.93/41.27 assert (zenon_L16_ : forall (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (greater (tau) (zero)) -> (~(smaller_or_equal (age zenon_TX_t zenon_TT0_cq) (tau))) -> False). % 40.93/41.27 do 2 intro. intros zenon_H43 zenon_H95 zenon_H96. % 40.93/41.27 generalize (definition_smaller_or_equal (age zenon_TX_t zenon_TT0_cq)). zenon_intro zenon_H97. % 40.93/41.27 generalize (zenon_H97 (tau)). zenon_intro zenon_H98. % 40.93/41.27 apply (zenon_equiv_s _ _ zenon_H98); [ zenon_intro zenon_H96; zenon_intro zenon_H9b | zenon_intro zenon_H9a; zenon_intro zenon_H99 ]. % 40.93/41.27 apply (zenon_notor_s _ _ zenon_H9b). zenon_intro zenon_H9d. zenon_intro zenon_H9c. % 40.93/41.27 generalize (definition_smaller (age zenon_TX_t zenon_TT0_cq)). zenon_intro zenon_H9e. % 40.93/41.27 generalize (zenon_H9e (tau)). zenon_intro zenon_H9f. % 40.93/41.27 apply (zenon_equiv_s _ _ zenon_H9f); [ zenon_intro zenon_H9d; zenon_intro zenon_Ha2 | zenon_intro zenon_Ha1; zenon_intro zenon_Ha0 ]. % 40.93/41.27 elim (classic ((zero) = (age zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Ha3 | zenon_intro zenon_Ha4 ]. % 40.93/41.27 cut ((greater (tau) (zero)) = (greater (tau) (age zenon_TX_t zenon_TT0_cq))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_Ha2. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_H95. % 40.93/41.27 cut (((zero) = (age zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Ha4]. % 40.93/41.27 cut (((tau) = (tau))); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 40.93/41.27 congruence. % 40.93/41.27 apply zenon_H2a. apply refl_equal. % 40.93/41.27 exact (zenon_Ha4 zenon_Ha3). % 40.93/41.27 apply zenon_Ha4. apply sym_equal. exact zenon_H43. % 40.93/41.27 exact (zenon_H9d zenon_Ha1). % 40.93/41.27 exact (zenon_H96 zenon_H9a). % 40.93/41.27 (* end of lemma zenon_L16_ *) % 40.93/41.27 assert (zenon_L17_ : forall (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (positional_advantage zenon_TX_t zenon_TT0_cq) -> (greater (tau) (zero)) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> False). % 40.93/41.27 do 2 intro. intros zenon_H56 zenon_Ha5 zenon_H95 zenon_H43. % 40.93/41.27 generalize (zenon_H56 zenon_TT0_cq). zenon_intro zenon_Ha6. % 40.93/41.27 apply (zenon_and_s _ _ zenon_Ha6). zenon_intro zenon_Ha8. zenon_intro zenon_Ha7. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_Ha8); [ zenon_intro zenon_H96 | zenon_intro zenon_Ha9 ]. % 40.93/41.27 apply (zenon_L16_ zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 exact (zenon_Ha9 zenon_Ha5). % 40.93/41.27 (* end of lemma zenon_L17_ *) % 40.93/41.27 assert (zenon_L18_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> (forall T : zenon_U, ((organization zenon_TX_t)->(((has_immunity zenon_TX_t T)->((hazard_of_mortality zenon_TX_t T) = (very_low)))/\((~(has_immunity zenon_TX_t T))->((((is_aligned zenon_TX_t T)/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (low)))/\((((~(is_aligned zenon_TX_t T))/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (mod1)))/\((((is_aligned zenon_TX_t T)/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (mod2)))/\(((~(is_aligned zenon_TX_t T))/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (high)))))))))) -> (organization zenon_TX_t) -> (~(has_endowment zenon_TX_t)) -> (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (greater (sigma) (age zenon_TX_t zenon_TT1_s)) -> ((sigma) = (tau)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> False). % 40.93/41.27 do 3 intro. intros zenon_He zenon_Haa zenon_H5c zenon_H36 zenon_H37 zenon_H3f zenon_H40 zenon_H42 zenon_H43 zenon_H56 zenon_H10 zenon_Hf zenon_Hab. % 40.93/41.27 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = ((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_Hab. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_Hac. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 40.93/41.27 congruence. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) = ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_Hae. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_Haa. % 40.93/41.27 cut (((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.27 congruence. % 40.93/41.27 apply zenon_Had. apply refl_equal. % 40.93/41.27 apply (zenon_L7_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 apply zenon_Had. apply refl_equal. % 40.93/41.27 apply zenon_Had. apply refl_equal. % 40.93/41.27 (* end of lemma zenon_L18_ *) % 40.93/41.27 assert (zenon_L19_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (((is_aligned zenon_TX_t zenon_TT0_cq)/\(~(positional_advantage zenon_TX_t zenon_TT0_cq)))->((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))) -> (greater (tau) (zero)) -> (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_t)->(((has_immunity zenon_TX_t T)->((hazard_of_mortality zenon_TX_t T) = (very_low)))/\((~(has_immunity zenon_TX_t T))->((((is_aligned zenon_TX_t T)/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (low)))/\((((~(is_aligned zenon_TX_t T))/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (mod1)))/\((((is_aligned zenon_TX_t T)/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (mod2)))/\(((~(is_aligned zenon_TX_t T))/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (high)))))))))) -> (organization zenon_TX_t) -> (~(has_endowment zenon_TX_t)) -> (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (greater (sigma) (age zenon_TX_t zenon_TT1_s)) -> ((sigma) = (tau)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> False). % 40.93/41.27 do 3 intro. intros zenon_Haf zenon_H95 zenon_He zenon_H5c zenon_H36 zenon_H37 zenon_H3f zenon_H40 zenon_H42 zenon_H43 zenon_H56 zenon_H10 zenon_Hf zenon_Hab. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_Haf); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Haa ]. % 40.93/41.27 apply (zenon_notand_s _ _ zenon_Hb0); [ zenon_intro zenon_H55 | zenon_intro zenon_Hb1 ]. % 40.93/41.27 exact (zenon_H55 zenon_H40). % 40.93/41.27 apply zenon_Hb1. zenon_intro zenon_Ha5. % 40.93/41.27 apply (zenon_L17_ zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 apply (zenon_L18_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L19_ *) % 40.93/41.27 assert (zenon_L20_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (organization zenon_TX_t) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> (greater (sigma) (age zenon_TX_t zenon_TT1_s)) -> ((sigma) = (tau)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> (greater (tau) (zero)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (~(has_endowment zenon_TX_t)) -> False). % 40.93/41.27 do 3 intro. intros zenon_He zenon_H36 zenon_H43 zenon_H42 zenon_H10 zenon_Hf zenon_Hab zenon_H95 zenon_H56 zenon_H37. % 40.93/41.27 generalize (assumption_13 zenon_TX_t). zenon_intro zenon_H8a. % 40.93/41.27 generalize (assumption_15 zenon_TX_t). zenon_intro zenon_H3f. % 40.93/41.27 generalize (zenon_H8a zenon_TT0_cq). zenon_intro zenon_H8c. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H8c); [ zenon_intro zenon_H48 | zenon_intro zenon_H40 ]. % 40.93/41.27 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H3e | zenon_intro zenon_H49 ]. % 40.93/41.27 exact (zenon_H3e zenon_H36). % 40.93/41.27 exact (zenon_H49 zenon_H43). % 40.93/41.27 generalize (assumption_17 zenon_TX_t). zenon_intro zenon_H5c. % 40.93/41.27 generalize (zenon_H5c zenon_TT0_cq). zenon_intro zenon_Hb2. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_Hb2); [ zenon_intro zenon_H3e | zenon_intro zenon_Hb3 ]. % 40.93/41.27 exact (zenon_H3e zenon_H36). % 40.93/41.27 apply (zenon_and_s _ _ zenon_Hb3). zenon_intro zenon_Hb5. zenon_intro zenon_Hb4. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_Hb4); [ zenon_intro zenon_H91 | zenon_intro zenon_Hb6 ]. % 40.93/41.27 apply (zenon_L15_ zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 apply (zenon_and_s _ _ zenon_Hb6). zenon_intro zenon_Hb8. zenon_intro zenon_Hb7. % 40.93/41.27 apply (zenon_and_s _ _ zenon_Hb7). zenon_intro zenon_Hba. zenon_intro zenon_Hb9. % 40.93/41.27 apply (zenon_and_s _ _ zenon_Hb9). zenon_intro zenon_Haf. zenon_intro zenon_Hbb. % 40.93/41.27 apply (zenon_L19_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L20_ *) % 40.93/41.27 assert (zenon_L21_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TX_t : 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_t zenon_TT1_s) (tau))) -> (organization zenon_TX_t) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (greater (sigma) (age zenon_TX_t zenon_TT1_s)) -> ((sigma) = (tau)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> (greater (tau) (zero)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (~(has_endowment zenon_TX_t)) -> False). % 40.93/41.27 do 3 intro. intros zenon_He zenon_H90 zenon_H36 zenon_H43 zenon_H10 zenon_Hf zenon_Hab zenon_H95 zenon_H56 zenon_H37. % 40.93/41.27 elim (classic (greater (age zenon_TX_t zenon_TT1_s) (sigma))); [ zenon_intro zenon_H4b | zenon_intro zenon_H42 ]. % 40.93/41.27 cut ((greater (age zenon_TX_t zenon_TT1_s) (sigma)) = (greater (age zenon_TX_t zenon_TT1_s) (tau))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_H90. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_H4b. % 40.93/41.27 cut (((sigma) = (tau))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 40.93/41.27 cut (((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_H24]. % 40.93/41.27 congruence. % 40.93/41.27 apply zenon_H24. apply refl_equal. % 40.93/41.27 exact (zenon_H25 zenon_Hf). % 40.93/41.27 apply (zenon_L20_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L21_ *) % 40.93/41.27 assert (zenon_L22_ : forall (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), (~((age zenon_TX_t zenon_TT1_s) = (tau))) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> ((sigma) = (tau)) -> False). % 40.93/41.27 do 2 intro. intros zenon_H19 zenon_Hbc zenon_Hf. % 40.93/41.27 cut (((age zenon_TX_t zenon_TT1_s) = (sigma)) = ((age zenon_TX_t zenon_TT1_s) = (tau))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_H19. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_Hbc. % 40.93/41.27 cut (((sigma) = (tau))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 40.93/41.27 cut (((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_H24]. % 40.93/41.27 congruence. % 40.93/41.27 apply zenon_H24. apply refl_equal. % 40.93/41.27 exact (zenon_H25 zenon_Hf). % 40.93/41.27 (* end of lemma zenon_L22_ *) % 40.93/41.27 assert (zenon_L23_ : forall (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> ((sigma) = (tau)) -> (~(smaller_or_equal (age zenon_TX_t zenon_TT1_s) (tau))) -> False). % 40.93/41.27 do 2 intro. intros zenon_Hbc zenon_Hf zenon_H11. % 40.93/41.27 generalize (definition_smaller_or_equal (age zenon_TX_t zenon_TT1_s)). zenon_intro zenon_H14. % 40.93/41.27 generalize (zenon_H14 (tau)). zenon_intro zenon_H15. % 40.93/41.27 apply (zenon_equiv_s _ _ zenon_H15); [ zenon_intro zenon_H11; zenon_intro zenon_H18 | zenon_intro zenon_H17; zenon_intro zenon_H16 ]. % 40.93/41.27 apply (zenon_notor_s _ _ zenon_H18). zenon_intro zenon_H1a. zenon_intro zenon_H19. % 40.93/41.27 apply (zenon_L22_ zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.27 exact (zenon_H11 zenon_H17). % 40.93/41.27 (* end of lemma zenon_L23_ *) % 40.93/41.27 assert (zenon_L24_ : (~((sigma) = (sigma))) -> False). % 40.93/41.27 do 0 intro. intros zenon_Hbd. % 40.93/41.27 apply zenon_Hbd. apply refl_equal. % 40.93/41.27 (* end of lemma zenon_L24_ *) % 40.93/41.27 assert (zenon_L25_ : (~((mod2) = (mod2))) -> False). % 40.93/41.27 do 0 intro. intros zenon_Hbe. % 40.93/41.27 apply zenon_Hbe. apply refl_equal. % 40.93/41.27 (* end of lemma zenon_L25_ *) % 40.93/41.27 assert (zenon_L26_ : forall (zenon_TT2_bz : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (((organization zenon_TX_t)/\((age zenon_TX_t zenon_TT0_cq) = (zero)))->(is_aligned zenon_TX_t zenon_TT0_cq)) -> (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> (~(has_endowment zenon_TX_t)) -> (positional_advantage zenon_TX_t zenon_TT2_bz) -> (~((mod1) = (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> False). % 40.93/41.27 do 3 intro. intros zenon_H8c zenon_H3f zenon_H32 zenon_H37 zenon_H71 zenon_H73 zenon_H43 zenon_H36. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H8c); [ zenon_intro zenon_H48 | zenon_intro zenon_H40 ]. % 40.93/41.27 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H3e | zenon_intro zenon_H49 ]. % 40.93/41.27 exact (zenon_H3e zenon_H36). % 40.93/41.27 exact (zenon_H49 zenon_H43). % 40.93/41.27 apply (zenon_L11_ zenon_TT0_cq zenon_TT2_bz zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L26_ *) % 40.93/41.27 assert (zenon_L27_ : forall (zenon_TT2_bz : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T) = (zero)))->(is_aligned zenon_TX_t T))) -> (organization zenon_TX_t) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> (~(has_endowment zenon_TX_t)) -> (positional_advantage zenon_TX_t zenon_TT2_bz) -> (~((mod1) = (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> False). % 40.93/41.27 do 3 intro. intros zenon_H8a zenon_H36 zenon_H43 zenon_H3f zenon_H32 zenon_H37 zenon_H71 zenon_H73. % 40.93/41.27 generalize (zenon_H8a zenon_TT0_cq). zenon_intro zenon_H8c. % 40.93/41.27 apply (zenon_L26_ zenon_TT2_bz zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L27_ *) % 40.93/41.27 assert (zenon_L28_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT2_bz : zenon_U) (zenon_TX_t : zenon_U), (~((mod1) = (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> (positional_advantage zenon_TX_t zenon_TT2_bz) -> (~(has_endowment zenon_TX_t)) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T) = (zero)))->(is_aligned zenon_TX_t T))) -> False). % 40.93/41.27 do 3 intro. intros zenon_H73 zenon_H71 zenon_H37 zenon_H32 zenon_H43 zenon_H36 zenon_H8a. % 40.93/41.27 generalize (assumption_15 zenon_TX_t). zenon_intro zenon_H3f. % 40.93/41.27 apply (zenon_L27_ zenon_TT2_bz zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L28_ *) % 40.93/41.27 assert (zenon_L29_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT2_bz : zenon_U) (zenon_TX_t : zenon_U), ((greater (age zenon_TX_t zenon_TT2_bz) (tau))->(positional_advantage zenon_TX_t zenon_TT2_bz)) -> (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T) = (zero)))->(is_aligned zenon_TX_t T))) -> (organization zenon_TX_t) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (~(has_endowment zenon_TX_t)) -> (~((mod1) = (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> ((sigma) = (tau)) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> False). % 40.93/41.27 do 3 intro. intros zenon_H8e zenon_H8a zenon_H36 zenon_H43 zenon_H37 zenon_H73 zenon_Hf zenon_H32. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H8e); [ zenon_intro zenon_H31 | zenon_intro zenon_H71 ]. % 40.93/41.27 apply (zenon_L3_ zenon_TT2_bz zenon_TX_t); trivial. % 40.93/41.27 apply (zenon_L28_ zenon_TT0_cq zenon_TT2_bz zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L29_ *) % 40.93/41.27 assert (zenon_L30_ : forall (zenon_TT2_bz : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T) = (zero)))->(is_aligned zenon_TX_t T))) -> (organization zenon_TX_t) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (~(has_endowment zenon_TX_t)) -> (~((mod1) = (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> ((sigma) = (tau)) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> False). % 40.93/41.27 do 3 intro. intros zenon_H56 zenon_H8a zenon_H36 zenon_H43 zenon_H37 zenon_H73 zenon_Hf zenon_H32. % 40.93/41.27 generalize (zenon_H56 zenon_TT2_bz). zenon_intro zenon_H8d. % 40.93/41.27 apply (zenon_and_s _ _ zenon_H8d). zenon_intro zenon_H8f. zenon_intro zenon_H8e. % 40.93/41.27 apply (zenon_L29_ zenon_TT0_cq zenon_TT2_bz zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L30_ *) % 40.93/41.27 assert (zenon_L31_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT2_bz : zenon_U) (zenon_TX_t : zenon_U), (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> ((sigma) = (tau)) -> (~((mod1) = (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> (~(has_endowment zenon_TX_t)) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> False). % 40.93/41.27 do 3 intro. intros zenon_H32 zenon_Hf zenon_H73 zenon_H37 zenon_H43 zenon_H36 zenon_H56. % 40.93/41.27 generalize (assumption_13 zenon_TX_t). zenon_intro zenon_H8a. % 40.93/41.27 apply (zenon_L30_ zenon_TT2_bz zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L31_ *) % 40.93/41.27 assert (zenon_L32_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT2_bz : zenon_U) (zenon_TX_t : zenon_U), (~(greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> ((sigma) = (tau)) -> (~(has_endowment zenon_TX_t)) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> False). % 40.93/41.27 do 3 intro. intros zenon_Hbf zenon_H32 zenon_Hf zenon_H37 zenon_H43 zenon_H36 zenon_H56. % 40.93/41.27 elim (classic ((mod1) = (hazard_of_mortality zenon_TX_t zenon_TT2_bz))); [ zenon_intro zenon_Hc0 | zenon_intro zenon_H73 ]. % 40.93/41.27 cut ((greater (mod2) (mod1)) = (greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_Hbf. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact assumption_19. % 40.93/41.27 cut (((mod1) = (hazard_of_mortality zenon_TX_t zenon_TT2_bz))); [idtac | apply NNPP; zenon_intro zenon_H73]. % 40.93/41.27 cut (((mod2) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hbe]. % 40.93/41.27 congruence. % 40.93/41.27 apply zenon_Hbe. apply refl_equal. % 40.93/41.27 exact (zenon_H73 zenon_Hc0). % 40.93/41.27 apply (zenon_L31_ zenon_TT0_cq zenon_TT2_bz zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L32_ *) % 40.93/41.27 assert (zenon_L33_ : forall (zenon_TT2_bz : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> (~(greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (organization zenon_TX_t) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (~(has_endowment zenon_TX_t)) -> ((sigma) = (tau)) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> False). % 40.93/41.27 do 3 intro. intros zenon_Haa zenon_Hc1 zenon_H56 zenon_H36 zenon_H43 zenon_H37 zenon_Hf zenon_H32. % 40.93/41.27 elim (classic (greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))); [ zenon_intro zenon_Hc2 | zenon_intro zenon_Hbf ]. % 40.93/41.27 cut ((greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT2_bz)) = (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_Hc1. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_Hc2. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT2_bz) = (hazard_of_mortality zenon_TX_t zenon_TT2_bz))); [idtac | apply NNPP; zenon_intro zenon_Hc3]. % 40.93/41.27 cut (((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 40.93/41.27 congruence. % 40.93/41.27 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_Hc4. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_Hac. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.27 congruence. % 40.93/41.27 exact (zenon_Hc5 zenon_Haa). % 40.93/41.27 apply zenon_Had. apply refl_equal. % 40.93/41.27 apply zenon_Had. apply refl_equal. % 40.93/41.27 apply zenon_Hc3. apply refl_equal. % 40.93/41.27 apply (zenon_L32_ zenon_TT0_cq zenon_TT2_bz zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L33_ *) % 40.93/41.27 assert (zenon_L34_ : forall (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (positional_advantage zenon_TX_t zenon_TT1_s) -> ((sigma) = (tau)) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> False). % 40.93/41.27 do 2 intro. intros zenon_H56 zenon_H57 zenon_Hf zenon_Hbc. % 40.93/41.27 generalize (zenon_H56 zenon_TT1_s). zenon_intro zenon_H58. % 40.93/41.27 apply (zenon_and_s _ _ zenon_H58). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_H11 | zenon_intro zenon_H5b ]. % 40.93/41.27 apply (zenon_L23_ zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.27 exact (zenon_H5b zenon_H57). % 40.93/41.27 (* end of lemma zenon_L34_ *) % 40.93/41.27 assert (zenon_L35_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (~(greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT1_s))) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> (~(greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> False). % 40.93/41.27 do 3 intro. intros zenon_Hc6 zenon_Hab zenon_Hc7. % 40.93/41.27 generalize (meaning_postulate_greater_comparable (hazard_of_mortality zenon_TX_t zenon_TT0_cq)). zenon_intro zenon_Hc8. % 40.93/41.27 generalize (zenon_Hc8 (hazard_of_mortality zenon_TX_t zenon_TT1_s)). zenon_intro zenon_Hc9. % 40.93/41.27 apply (zenon_or_s _ _ zenon_Hc9); [ zenon_intro zenon_Hcb | zenon_intro zenon_Hca ]. % 40.93/41.27 generalize (definition_smaller (hazard_of_mortality zenon_TX_t zenon_TT0_cq)). zenon_intro zenon_Hcc. % 40.93/41.27 generalize (zenon_Hcc (hazard_of_mortality zenon_TX_t zenon_TT1_s)). zenon_intro zenon_Hcd. % 40.93/41.27 apply (zenon_equiv_s _ _ zenon_Hcd); [ zenon_intro zenon_Hcf; zenon_intro zenon_Hc7 | zenon_intro zenon_Hcb; zenon_intro zenon_Hce ]. % 40.93/41.27 exact (zenon_Hcf zenon_Hcb). % 40.93/41.27 exact (zenon_Hc7 zenon_Hce). % 40.93/41.27 apply (zenon_or_s _ _ zenon_Hca); [ zenon_intro zenon_Hd1 | zenon_intro zenon_Hd0 ]. % 40.93/41.27 apply zenon_Hab. apply sym_equal. exact zenon_Hd1. % 40.93/41.27 exact (zenon_Hc6 zenon_Hd0). % 40.93/41.27 (* end of lemma zenon_L35_ *) % 40.93/41.27 assert (zenon_L36_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), ((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (mod2)) -> ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> (~(greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT1_s))) -> (~(greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT1_s))) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> False). % 40.93/41.27 do 3 intro. intros zenon_H69 zenon_Haa zenon_Hd2 zenon_Hc6 zenon_Hab. % 40.93/41.27 elim (classic (greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hce | zenon_intro zenon_Hc7 ]. % 40.93/41.27 elim (classic (greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (mod2))); [ zenon_intro zenon_Hd3 | zenon_intro zenon_Hd4 ]. % 40.93/41.27 cut ((greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (mod2)) = (greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT1_s))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_Hd2. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_Hd3. % 40.93/41.27 cut (((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 40.93/41.27 congruence. % 40.93/41.27 apply zenon_Hd5. apply refl_equal. % 40.93/41.27 apply zenon_H5d. apply sym_equal. exact zenon_H69. % 40.93/41.27 cut ((greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = (greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (mod2))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_Hd4. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_Hce. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 40.93/41.27 congruence. % 40.93/41.27 apply zenon_Hd5. apply refl_equal. % 40.93/41.27 exact (zenon_Hc5 zenon_Haa). % 40.93/41.27 apply (zenon_L35_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L36_ *) % 40.93/41.27 assert (zenon_L37_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (mod2)) -> (~(greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT1_s))) -> (~(greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT1_s))) -> ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> False). % 40.93/41.27 do 3 intro. intros zenon_Hab zenon_H69 zenon_Hd2 zenon_Hd6 zenon_Haa. % 40.93/41.27 elim (classic ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hd7 | zenon_intro zenon_Hc4 ]. % 40.93/41.27 elim (classic (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [ zenon_intro zenon_Hd0 | zenon_intro zenon_Hc6 ]. % 40.93/41.27 cut ((greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT1_s)) = (greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT1_s))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_Hd6. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_Hd0. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.27 congruence. % 40.93/41.27 elim (classic ((mod2) = (mod2))); [ zenon_intro zenon_Hd8 | zenon_intro zenon_Hbe ]. % 40.93/41.27 cut (((mod2) = (mod2)) = ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_Hc5. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_Hd8. % 40.93/41.27 cut (((mod2) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hbe]. % 40.93/41.27 cut (((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 40.93/41.27 congruence. % 40.93/41.27 exact (zenon_Hc4 zenon_Hd7). % 40.93/41.27 apply zenon_Hbe. apply refl_equal. % 40.93/41.27 apply zenon_Hbe. apply refl_equal. % 40.93/41.27 apply zenon_Hd5. apply refl_equal. % 40.93/41.27 apply (zenon_L36_ zenon_TT0_cq zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.27 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_Hc4. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_Hac. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.27 congruence. % 40.93/41.27 exact (zenon_Hc5 zenon_Haa). % 40.93/41.27 apply zenon_Had. apply refl_equal. % 40.93/41.27 apply zenon_Had. apply refl_equal. % 40.93/41.27 (* end of lemma zenon_L37_ *) % 40.93/41.27 assert (zenon_L38_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> (~(greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT1_s))) -> ((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (mod2)) -> False). % 40.93/41.27 do 3 intro. intros zenon_Haa zenon_Hab zenon_Hd6 zenon_H69. % 40.93/41.27 elim (classic ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [ zenon_intro zenon_Hd9 | zenon_intro zenon_H5d ]. % 40.93/41.27 elim (classic (greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hd2 ]. % 40.93/41.27 cut ((greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT1_s)) = (greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT1_s))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_Hd6. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_Hda. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 40.93/41.27 congruence. % 40.93/41.27 elim (classic ((mod2) = (mod2))); [ zenon_intro zenon_Hd8 | zenon_intro zenon_Hbe ]. % 40.93/41.27 cut (((mod2) = (mod2)) = ((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (mod2))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_Hdb. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_Hd8. % 40.93/41.27 cut (((mod2) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hbe]. % 40.93/41.27 cut (((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 40.93/41.27 congruence. % 40.93/41.27 exact (zenon_H5d zenon_Hd9). % 40.93/41.27 apply zenon_Hbe. apply refl_equal. % 40.93/41.27 apply zenon_Hbe. apply refl_equal. % 40.93/41.27 apply zenon_Hd5. apply refl_equal. % 40.93/41.27 apply (zenon_L37_ zenon_TT0_cq zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.27 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [ zenon_intro zenon_Hdc | zenon_intro zenon_Hd5 ]. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s)) = ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_H5d. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_Hdc. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 40.93/41.27 congruence. % 40.93/41.27 exact (zenon_Hdb zenon_H69). % 40.93/41.27 apply zenon_Hd5. apply refl_equal. % 40.93/41.27 apply zenon_Hd5. apply refl_equal. % 40.93/41.27 (* end of lemma zenon_L38_ *) % 40.93/41.27 assert (zenon_L39_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (~(greater (mod2) (mod2))) -> ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> ((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (mod2)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> False). % 40.93/41.27 do 3 intro. intros zenon_Hdd zenon_Haa zenon_H69 zenon_Hab. % 40.93/41.27 elim (classic (greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [ zenon_intro zenon_Hde | zenon_intro zenon_Hd6 ]. % 40.93/41.27 cut ((greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT1_s)) = (greater (mod2) (mod2))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_Hdd. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_Hde. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 40.93/41.27 cut (((mod2) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hbe]. % 40.93/41.27 congruence. % 40.93/41.27 apply zenon_Hbe. apply refl_equal. % 40.93/41.27 exact (zenon_Hdb zenon_H69). % 40.93/41.27 apply (zenon_L38_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L39_ *) % 40.93/41.27 assert (zenon_L40_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), ((((is_aligned zenon_TX_t zenon_TT1_s)/\(positional_advantage zenon_TX_t zenon_TT1_s))->((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (low)))/\((((~(is_aligned zenon_TX_t zenon_TT1_s))/\(positional_advantage zenon_TX_t zenon_TT1_s))->((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (mod1)))/\((((is_aligned zenon_TX_t zenon_TT1_s)/\(~(positional_advantage zenon_TX_t zenon_TT1_s)))->((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (mod2)))/\(((~(is_aligned zenon_TX_t zenon_TT1_s))/\(~(positional_advantage zenon_TX_t zenon_TT1_s)))->((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (high)))))) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> ((sigma) = (tau)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (is_aligned zenon_TX_t zenon_TT1_s) -> (~(greater (mod2) (mod2))) -> ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> False). % 40.93/41.27 do 3 intro. intros zenon_H62 zenon_Hbc zenon_Hf zenon_H56 zenon_H54 zenon_Hdd zenon_Haa zenon_Hab. % 40.93/41.27 apply (zenon_and_s _ _ zenon_H62). zenon_intro zenon_H64. zenon_intro zenon_H63. % 40.93/41.27 apply (zenon_and_s _ _ zenon_H63). zenon_intro zenon_H66. zenon_intro zenon_H65. % 40.93/41.27 apply (zenon_and_s _ _ zenon_H65). zenon_intro zenon_H68. zenon_intro zenon_H67. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H68); [ zenon_intro zenon_H6a | zenon_intro zenon_H69 ]. % 40.93/41.27 apply (zenon_notand_s _ _ zenon_H6a); [ zenon_intro zenon_H41 | zenon_intro zenon_H6b ]. % 40.93/41.27 exact (zenon_H41 zenon_H54). % 40.93/41.27 apply zenon_H6b. zenon_intro zenon_H57. % 40.93/41.27 apply (zenon_L34_ zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.27 apply (zenon_L39_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L40_ *) % 40.93/41.27 assert (zenon_L41_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), (forall T : zenon_U, ((organization zenon_TX_t)->(((has_immunity zenon_TX_t T)->((hazard_of_mortality zenon_TX_t T) = (very_low)))/\((~(has_immunity zenon_TX_t T))->((((is_aligned zenon_TX_t T)/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (low)))/\((((~(is_aligned zenon_TX_t T))/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (mod1)))/\((((is_aligned zenon_TX_t T)/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (mod2)))/\(((~(is_aligned zenon_TX_t T))/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (high)))))))))) -> (organization zenon_TX_t) -> (~(has_endowment zenon_TX_t)) -> (is_aligned zenon_TX_t zenon_TT1_s) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> ((sigma) = (tau)) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> (~(greater (mod2) (mod2))) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> False). % 40.93/41.27 do 3 intro. intros zenon_H5c zenon_H36 zenon_H37 zenon_H54 zenon_H56 zenon_Hf zenon_Hbc zenon_Hdd zenon_Hab zenon_Haa. % 40.93/41.27 generalize (zenon_H5c zenon_TT1_s). zenon_intro zenon_H5e. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H5e); [ zenon_intro zenon_H3e | zenon_intro zenon_H5f ]. % 40.93/41.27 exact (zenon_H3e zenon_H36). % 40.93/41.27 apply (zenon_and_s _ _ zenon_H5f). zenon_intro zenon_H61. zenon_intro zenon_H60. % 40.93/41.27 apply (zenon_imply_s _ _ zenon_H60); [ zenon_intro zenon_H35 | zenon_intro zenon_H62 ]. % 40.93/41.27 apply (zenon_L4_ zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.27 apply (zenon_L40_ zenon_TT0_cq zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.27 (* end of lemma zenon_L41_ *) % 40.93/41.27 assert (zenon_L42_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> ((sigma) = (tau)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (is_aligned zenon_TX_t zenon_TT1_s) -> (~(has_endowment zenon_TX_t)) -> (organization zenon_TX_t) -> (forall T : zenon_U, ((organization zenon_TX_t)->(((has_immunity zenon_TX_t T)->((hazard_of_mortality zenon_TX_t T) = (very_low)))/\((~(has_immunity zenon_TX_t T))->((((is_aligned zenon_TX_t T)/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (low)))/\((((~(is_aligned zenon_TX_t T))/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (mod1)))/\((((is_aligned zenon_TX_t T)/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (mod2)))/\(((~(is_aligned zenon_TX_t T))/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (high)))))))))) -> (~(greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> False). % 40.93/41.27 do 3 intro. intros zenon_Hab zenon_Hbc zenon_Hf zenon_H56 zenon_H54 zenon_H37 zenon_H36 zenon_H5c zenon_Hdf zenon_Haa. % 40.93/41.27 elim (classic ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hd7 | zenon_intro zenon_Hc4 ]. % 40.93/41.27 elim (classic (greater (mod2) (mod2))); [ zenon_intro zenon_He0 | zenon_intro zenon_Hdd ]. % 40.93/41.27 cut ((greater (mod2) (mod2)) = (greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.27 apply zenon_Hdf. % 40.93/41.27 rewrite <- zenon_D_pnotp. % 40.93/41.27 exact zenon_He0. % 40.93/41.27 cut (((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 40.93/41.27 cut (((mod2) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hbe]. % 40.93/41.27 congruence. % 40.93/41.27 apply zenon_Hbe. apply refl_equal. % 40.93/41.27 exact (zenon_Hc4 zenon_Hd7). % 40.93/41.27 apply (zenon_L41_ zenon_TT0_cq zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.27 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 40.93/41.27 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.27 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hc4. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hac. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.28 congruence. % 40.93/41.28 exact (zenon_Hc5 zenon_Haa). % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 (* end of lemma zenon_L42_ *) % 40.93/41.28 assert (zenon_L43_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> (~(greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> ((sigma) = (tau)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (~(has_endowment zenon_TX_t)) -> (forall T : zenon_U, ((organization zenon_TX_t)->(((has_immunity zenon_TX_t T)->((hazard_of_mortality zenon_TX_t T) = (very_low)))/\((~(has_immunity zenon_TX_t T))->((((is_aligned zenon_TX_t T)/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (low)))/\((((~(is_aligned zenon_TX_t T))/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (mod1)))/\((((is_aligned zenon_TX_t T)/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (mod2)))/\(((~(is_aligned zenon_TX_t T))/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (high)))))))))) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> False). % 40.93/41.28 do 3 intro. intros zenon_H3f zenon_H40 zenon_Hdf zenon_Haa zenon_Hab zenon_Hbc zenon_Hf zenon_H56 zenon_H37 zenon_H5c zenon_H42 zenon_H43 zenon_H36. % 40.93/41.28 generalize (zenon_H3f zenon_TT0_cq). zenon_intro zenon_H45. % 40.93/41.28 generalize (zenon_H45 zenon_TT1_s). zenon_intro zenon_H46. % 40.93/41.28 apply (zenon_imply_s _ _ zenon_H46); [ zenon_intro zenon_H48 | zenon_intro zenon_H47 ]. % 40.93/41.28 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H3e | zenon_intro zenon_H49 ]. % 40.93/41.28 exact (zenon_H3e zenon_H36). % 40.93/41.28 exact (zenon_H49 zenon_H43). % 40.93/41.28 apply (zenon_equiv_s _ _ zenon_H47); [ zenon_intro zenon_H42; zenon_intro zenon_H4c | zenon_intro zenon_H4b; zenon_intro zenon_H4a ]. % 40.93/41.28 generalize (definition_2 zenon_TX_t). zenon_intro zenon_H4d. % 40.93/41.28 generalize (zenon_H4d zenon_TT0_cq). zenon_intro zenon_H4e. % 40.93/41.28 generalize (zenon_H4e zenon_TT1_s). zenon_intro zenon_H4f. % 40.93/41.28 apply (zenon_equiv_s _ _ zenon_H4f); [ zenon_intro zenon_H4c; zenon_intro zenon_H51 | zenon_intro zenon_H4a; zenon_intro zenon_H50 ]. % 40.93/41.28 apply (zenon_notand_s _ _ zenon_H51); [ zenon_intro zenon_H3e | zenon_intro zenon_H52 ]. % 40.93/41.28 exact (zenon_H3e zenon_H36). % 40.93/41.28 apply zenon_H52. zenon_intro zenon_H53. % 40.93/41.28 apply (zenon_equiv_s _ _ zenon_H53); [ zenon_intro zenon_H55; zenon_intro zenon_H41 | zenon_intro zenon_H40; zenon_intro zenon_H54 ]. % 40.93/41.28 exact (zenon_H55 zenon_H40). % 40.93/41.28 apply (zenon_L42_ zenon_TT0_cq zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.28 exact (zenon_H4c zenon_H4a). % 40.93/41.28 exact (zenon_H42 zenon_H4b). % 40.93/41.28 (* end of lemma zenon_L43_ *) % 40.93/41.28 assert (zenon_L44_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (~(greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> ((sigma) = (tau)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (~(has_endowment zenon_TX_t)) -> (forall T : zenon_U, ((organization zenon_TX_t)->(((has_immunity zenon_TX_t T)->((hazard_of_mortality zenon_TX_t T) = (very_low)))/\((~(has_immunity zenon_TX_t T))->((((is_aligned zenon_TX_t T)/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (low)))/\((((~(is_aligned zenon_TX_t T))/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (mod1)))/\((((is_aligned zenon_TX_t T)/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (mod2)))/\(((~(is_aligned zenon_TX_t T))/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (high)))))))))) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> False). % 40.93/41.28 do 3 intro. intros zenon_He1 zenon_H3f zenon_H40 zenon_Haa zenon_Hab zenon_Hbc zenon_Hf zenon_H56 zenon_H37 zenon_H5c zenon_H42 zenon_H43 zenon_H36. % 40.93/41.28 elim (classic (greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_He2 | zenon_intro zenon_Hdf ]. % 40.93/41.28 cut ((greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_He1. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_He2. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.28 cut (((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 40.93/41.28 congruence. % 40.93/41.28 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hc4. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hac. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.28 congruence. % 40.93/41.28 exact (zenon_Hc5 zenon_Haa). % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply (zenon_L43_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.28 (* end of lemma zenon_L44_ *) % 40.93/41.28 assert (zenon_L45_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (~(greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (mod2))) -> (organization zenon_TX_t) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> (forall T : zenon_U, ((organization zenon_TX_t)->(((has_immunity zenon_TX_t T)->((hazard_of_mortality zenon_TX_t T) = (very_low)))/\((~(has_immunity zenon_TX_t T))->((((is_aligned zenon_TX_t T)/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (low)))/\((((~(is_aligned zenon_TX_t T))/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (mod1)))/\((((is_aligned zenon_TX_t T)/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (mod2)))/\(((~(is_aligned zenon_TX_t T))/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (high)))))))))) -> (~(has_endowment zenon_TX_t)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> ((sigma) = (tau)) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> False). % 40.93/41.28 do 3 intro. intros zenon_He3 zenon_H36 zenon_H43 zenon_H42 zenon_H5c zenon_H37 zenon_H56 zenon_Hf zenon_Hbc zenon_Hab zenon_Haa zenon_H40 zenon_H3f. % 40.93/41.28 elim (classic (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_He4 | zenon_intro zenon_He1 ]. % 40.93/41.28 cut ((greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (mod2))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_He3. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_He4. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.28 congruence. % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 exact (zenon_Hc5 zenon_Haa). % 40.93/41.28 apply (zenon_L44_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.28 (* end of lemma zenon_L45_ *) % 40.93/41.28 assert (zenon_L46_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (organization zenon_TX_t) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> (forall T : zenon_U, ((organization zenon_TX_t)->(((has_immunity zenon_TX_t T)->((hazard_of_mortality zenon_TX_t T) = (very_low)))/\((~(has_immunity zenon_TX_t T))->((((is_aligned zenon_TX_t T)/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (low)))/\((((~(is_aligned zenon_TX_t T))/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (mod1)))/\((((is_aligned zenon_TX_t T)/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (mod2)))/\(((~(is_aligned zenon_TX_t T))/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (high)))))))))) -> (~(has_endowment zenon_TX_t)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> ((sigma) = (tau)) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> (~(greater (mod2) (mod2))) -> ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> False). % 40.93/41.28 do 3 intro. intros zenon_H36 zenon_H43 zenon_H42 zenon_H5c zenon_H37 zenon_H56 zenon_Hf zenon_Hbc zenon_Hab zenon_H40 zenon_H3f zenon_Hdd zenon_Haa. % 40.93/41.28 elim (classic ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hd7 | zenon_intro zenon_Hc4 ]. % 40.93/41.28 elim (classic (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (mod2))); [ zenon_intro zenon_He5 | zenon_intro zenon_He3 ]. % 40.93/41.28 cut ((greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (mod2)) = (greater (mod2) (mod2))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hdd. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_He5. % 40.93/41.28 cut (((mod2) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hbe]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.28 congruence. % 40.93/41.28 elim (classic ((mod2) = (mod2))); [ zenon_intro zenon_Hd8 | zenon_intro zenon_Hbe ]. % 40.93/41.28 cut (((mod2) = (mod2)) = ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hc5. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hd8. % 40.93/41.28 cut (((mod2) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hbe]. % 40.93/41.28 cut (((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 40.93/41.28 congruence. % 40.93/41.28 exact (zenon_Hc4 zenon_Hd7). % 40.93/41.28 apply zenon_Hbe. apply refl_equal. % 40.93/41.28 apply zenon_Hbe. apply refl_equal. % 40.93/41.28 apply zenon_Hbe. apply refl_equal. % 40.93/41.28 apply (zenon_L45_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.28 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hc4. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hac. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.28 congruence. % 40.93/41.28 exact (zenon_Hc5 zenon_Haa). % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 (* end of lemma zenon_L46_ *) % 40.93/41.28 assert (zenon_L47_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (forall Y : zenon_U, (~((greater (mod2) Y)/\(greater Y (mod2))))) -> (organization zenon_TX_t) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> (forall T : zenon_U, ((organization zenon_TX_t)->(((has_immunity zenon_TX_t T)->((hazard_of_mortality zenon_TX_t T) = (very_low)))/\((~(has_immunity zenon_TX_t T))->((((is_aligned zenon_TX_t T)/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (low)))/\((((~(is_aligned zenon_TX_t T))/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (mod1)))/\((((is_aligned zenon_TX_t T)/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (mod2)))/\(((~(is_aligned zenon_TX_t T))/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (high)))))))))) -> (~(has_endowment zenon_TX_t)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> ((sigma) = (tau)) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> False). % 40.93/41.28 do 3 intro. intros zenon_He6 zenon_H36 zenon_H43 zenon_H42 zenon_H5c zenon_H37 zenon_H56 zenon_Hf zenon_Hbc zenon_Hab zenon_Haa zenon_H40 zenon_H3f. % 40.93/41.28 generalize (zenon_He6 (mod2)). zenon_intro zenon_He7. % 40.93/41.28 apply (zenon_notand_s _ _ zenon_He7); [ zenon_intro zenon_Hdd | zenon_intro zenon_Hdd ]. % 40.93/41.28 apply (zenon_L46_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.28 apply (zenon_L46_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.28 (* end of lemma zenon_L47_ *) % 40.93/41.28 assert (zenon_L48_ : forall (zenon_TT2_bz : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> ((sigma) = (tau)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (~(has_endowment zenon_TX_t)) -> (forall T : zenon_U, ((organization zenon_TX_t)->(((has_immunity zenon_TX_t T)->((hazard_of_mortality zenon_TX_t T) = (very_low)))/\((~(has_immunity zenon_TX_t T))->((((is_aligned zenon_TX_t T)/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (low)))/\((((~(is_aligned zenon_TX_t T))/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (mod1)))/\((((is_aligned zenon_TX_t T)/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (mod2)))/\(((~(is_aligned zenon_TX_t T))/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (high)))))))))) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> (~(greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> (~(greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> False). % 40.93/41.28 do 4 intro. intros zenon_H3f zenon_H40 zenon_Hbc zenon_Hf zenon_H56 zenon_H37 zenon_H5c zenon_H42 zenon_H43 zenon_H36 zenon_H32 zenon_H8b zenon_He1 zenon_Haa. % 40.93/41.28 elim (classic ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hd7 | zenon_intro zenon_Hc4 ]. % 40.93/41.28 elim (classic (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (mod2))); [ zenon_intro zenon_He5 | zenon_intro zenon_He3 ]. % 40.93/41.28 cut ((greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (mod2)) = (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_He1. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_He5. % 40.93/41.28 cut (((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.28 congruence. % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 exact (zenon_Hc4 zenon_Hd7). % 40.93/41.28 elim (classic (greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))); [ zenon_intro zenon_Hc2 | zenon_intro zenon_Hbf ]. % 40.93/41.28 elim (classic (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))); [ zenon_intro zenon_He8 | zenon_intro zenon_Hc1 ]. % 40.93/41.28 cut ((greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT2_bz)) = (greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_H8b. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_He8. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT2_bz) = (hazard_of_mortality zenon_TX_t zenon_TT2_bz))); [idtac | apply NNPP; zenon_intro zenon_Hc3]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 40.93/41.28 congruence. % 40.93/41.28 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [ zenon_intro zenon_Hdc | zenon_intro zenon_Hd5 ]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s)) = ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hae. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hdc. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 40.93/41.28 congruence. % 40.93/41.28 apply (zenon_L45_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.28 apply zenon_Hd5. apply refl_equal. % 40.93/41.28 apply zenon_Hd5. apply refl_equal. % 40.93/41.28 apply zenon_Hc3. apply refl_equal. % 40.93/41.28 cut ((greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT2_bz)) = (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hc1. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hc2. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT2_bz) = (hazard_of_mortality zenon_TX_t zenon_TT2_bz))); [idtac | apply NNPP; zenon_intro zenon_Hc3]. % 40.93/41.28 cut (((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 40.93/41.28 congruence. % 40.93/41.28 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hc4. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hac. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.28 congruence. % 40.93/41.28 exact (zenon_Hc5 zenon_Haa). % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply zenon_Hc3. apply refl_equal. % 40.93/41.28 apply (zenon_L32_ zenon_TT0_cq zenon_TT2_bz zenon_TX_t); trivial. % 40.93/41.28 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hc4. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hac. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.28 congruence. % 40.93/41.28 exact (zenon_Hc5 zenon_Haa). % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 (* end of lemma zenon_L48_ *) % 40.93/41.28 assert (zenon_L49_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT2_bz : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), (~(greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> (organization zenon_TX_t) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> (forall T : zenon_U, ((organization zenon_TX_t)->(((has_immunity zenon_TX_t T)->((hazard_of_mortality zenon_TX_t T) = (very_low)))/\((~(has_immunity zenon_TX_t T))->((((is_aligned zenon_TX_t T)/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (low)))/\((((~(is_aligned zenon_TX_t T))/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (mod1)))/\((((is_aligned zenon_TX_t T)/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (mod2)))/\(((~(is_aligned zenon_TX_t T))/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (high)))))))))) -> (~(has_endowment zenon_TX_t)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> ((sigma) = (tau)) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> (~(greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> False). % 40.93/41.28 do 4 intro. intros zenon_H8b zenon_H32 zenon_H36 zenon_H43 zenon_H42 zenon_H5c zenon_H37 zenon_H56 zenon_Hf zenon_Hbc zenon_H40 zenon_H3f zenon_Hdf zenon_Haa. % 40.93/41.28 elim (classic ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hd7 | zenon_intro zenon_Hc4 ]. % 40.93/41.28 elim (classic (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_He4 | zenon_intro zenon_He1 ]. % 40.93/41.28 cut ((greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = (greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hdf. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_He4. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.28 congruence. % 40.93/41.28 elim (classic ((mod2) = (mod2))); [ zenon_intro zenon_Hd8 | zenon_intro zenon_Hbe ]. % 40.93/41.28 cut (((mod2) = (mod2)) = ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hc5. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hd8. % 40.93/41.28 cut (((mod2) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hbe]. % 40.93/41.28 cut (((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 40.93/41.28 congruence. % 40.93/41.28 exact (zenon_Hc4 zenon_Hd7). % 40.93/41.28 apply zenon_Hbe. apply refl_equal. % 40.93/41.28 apply zenon_Hbe. apply refl_equal. % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply (zenon_L48_ zenon_TT2_bz zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.28 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hc4. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hac. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.28 congruence. % 40.93/41.28 exact (zenon_Hc5 zenon_Haa). % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 (* end of lemma zenon_L49_ *) % 40.93/41.28 assert (zenon_L50_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT2_bz : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> ((sigma) = (tau)) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> (~(greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> (~(greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (mod2))) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> (~(has_endowment zenon_TX_t)) -> (organization zenon_TX_t) -> (greater (tau) (zero)) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> False). % 40.93/41.28 do 4 intro. intros zenon_H42 zenon_H56 zenon_Hf zenon_Hbc zenon_H3f zenon_H32 zenon_H8b zenon_Hd4 zenon_H40 zenon_H37 zenon_H36 zenon_H95 zenon_H43. % 40.93/41.28 generalize (zenon_H56 zenon_TT0_cq). zenon_intro zenon_Ha6. % 40.93/41.28 apply (zenon_and_s _ _ zenon_Ha6). zenon_intro zenon_Ha8. zenon_intro zenon_Ha7. % 40.93/41.28 apply (zenon_imply_s _ _ zenon_Ha8); [ zenon_intro zenon_H96 | zenon_intro zenon_Ha9 ]. % 40.93/41.28 apply (zenon_L16_ zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.28 generalize (assumption_17 zenon_TX_t). zenon_intro zenon_H5c. % 40.93/41.28 generalize (meaning_postulate_greater_strict (mod2)). zenon_intro zenon_He6. % 40.93/41.28 generalize (zenon_H5c zenon_TT0_cq). zenon_intro zenon_Hb2. % 40.93/41.28 apply (zenon_imply_s _ _ zenon_Hb2); [ zenon_intro zenon_H3e | zenon_intro zenon_Hb3 ]. % 40.93/41.28 exact (zenon_H3e zenon_H36). % 40.93/41.28 apply (zenon_and_s _ _ zenon_Hb3). zenon_intro zenon_Hb5. zenon_intro zenon_Hb4. % 40.93/41.28 apply (zenon_imply_s _ _ zenon_Hb4); [ zenon_intro zenon_H91 | zenon_intro zenon_Hb6 ]. % 40.93/41.28 apply (zenon_L15_ zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.28 apply (zenon_and_s _ _ zenon_Hb6). zenon_intro zenon_Hb8. zenon_intro zenon_Hb7. % 40.93/41.28 apply (zenon_and_s _ _ zenon_Hb7). zenon_intro zenon_Hba. zenon_intro zenon_Hb9. % 40.93/41.28 apply (zenon_and_s _ _ zenon_Hb9). zenon_intro zenon_Haf. zenon_intro zenon_Hbb. % 40.93/41.28 apply (zenon_imply_s _ _ zenon_Haf); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Haa ]. % 40.93/41.28 apply (zenon_notand_s _ _ zenon_Hb0); [ zenon_intro zenon_H55 | zenon_intro zenon_Hb1 ]. % 40.93/41.28 exact (zenon_H55 zenon_H40). % 40.93/41.28 exact (zenon_Hb1 zenon_Ha9). % 40.93/41.28 elim (classic (greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hce | zenon_intro zenon_Hc7 ]. % 40.93/41.28 cut ((greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = (greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (mod2))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hd4. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hce. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 40.93/41.28 congruence. % 40.93/41.28 apply zenon_Hd5. apply refl_equal. % 40.93/41.28 exact (zenon_Hc5 zenon_Haa). % 40.93/41.28 elim (classic (greater (mod2) (mod2))); [ zenon_intro zenon_He0 | zenon_intro zenon_Hdd ]. % 40.93/41.28 elim (classic (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (mod2))); [ zenon_intro zenon_He5 | zenon_intro zenon_He3 ]. % 40.93/41.28 cut ((greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (mod2)) = (greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (mod2))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hd4. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_He5. % 40.93/41.28 cut (((mod2) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hbe]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 40.93/41.28 congruence. % 40.93/41.28 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [ zenon_intro zenon_Hdc | zenon_intro zenon_Hd5 ]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s)) = ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hae. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hdc. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 40.93/41.28 congruence. % 40.93/41.28 apply (zenon_L47_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.28 apply zenon_Hd5. apply refl_equal. % 40.93/41.28 apply zenon_Hd5. apply refl_equal. % 40.93/41.28 apply zenon_Hbe. apply refl_equal. % 40.93/41.28 cut ((greater (mod2) (mod2)) = (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (mod2))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_He3. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_He0. % 40.93/41.28 cut (((mod2) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hbe]. % 40.93/41.28 cut (((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 40.93/41.28 congruence. % 40.93/41.28 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hc4. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hac. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.28 congruence. % 40.93/41.28 exact (zenon_Hc5 zenon_Haa). % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply zenon_Hbe. apply refl_equal. % 40.93/41.28 elim (classic (greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_He2 | zenon_intro zenon_Hdf ]. % 40.93/41.28 elim (classic (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_He4 | zenon_intro zenon_He1 ]. % 40.93/41.28 cut ((greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = (greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hc7. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_He4. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 40.93/41.28 congruence. % 40.93/41.28 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [ zenon_intro zenon_Hdc | zenon_intro zenon_Hd5 ]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s)) = ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hae. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hdc. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 40.93/41.28 congruence. % 40.93/41.28 apply (zenon_L46_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.28 apply zenon_Hd5. apply refl_equal. % 40.93/41.28 apply zenon_Hd5. apply refl_equal. % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 cut ((greater (mod2) (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_He1. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_He2. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.28 cut (((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 40.93/41.28 congruence. % 40.93/41.28 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hc4. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hac. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.28 congruence. % 40.93/41.28 exact (zenon_Hc5 zenon_Haa). % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply (zenon_L49_ zenon_TT0_cq zenon_TT2_bz zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.28 (* end of lemma zenon_L50_ *) % 40.93/41.28 assert (zenon_L51_ : forall (zenon_TT2_bz : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (greater (tau) (zero)) -> (organization zenon_TX_t) -> (~(has_endowment zenon_TX_t)) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> (~(greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (mod2))) -> (~(greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> ((sigma) = (tau)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> False). % 40.93/41.28 do 4 intro. intros zenon_H43 zenon_H95 zenon_H36 zenon_H37 zenon_H40 zenon_Hd4 zenon_H8b zenon_H32 zenon_Hbc zenon_Hf zenon_H56 zenon_H42. % 40.93/41.28 generalize (assumption_15 zenon_TX_t). zenon_intro zenon_H3f. % 40.93/41.28 apply (zenon_L50_ zenon_TT0_cq zenon_TT2_bz zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.28 (* end of lemma zenon_L51_ *) % 40.93/41.28 assert (zenon_L52_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT2_bz : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), (~(greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> ((sigma) = (tau)) -> (greater (tau) (zero)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (~(has_endowment zenon_TX_t)) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater (sigma) (sigma))) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> False). % 40.93/41.28 do 4 intro. intros zenon_H8b zenon_H32 zenon_Hf zenon_H95 zenon_H56 zenon_H37 zenon_H43 zenon_H36 zenon_He zenon_He9 zenon_Hbc. % 40.93/41.28 elim (classic ((sigma) = (age zenon_TX_t zenon_TT1_s))); [ zenon_intro zenon_Hea | zenon_intro zenon_Heb ]. % 40.93/41.28 elim (classic (greater (age zenon_TX_t zenon_TT1_s) (sigma))); [ zenon_intro zenon_H4b | zenon_intro zenon_H42 ]. % 40.93/41.28 cut ((greater (age zenon_TX_t zenon_TT1_s) (sigma)) = (greater (sigma) (sigma))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_He9. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_H4b. % 40.93/41.28 cut (((sigma) = (sigma))); [idtac | apply NNPP; zenon_intro zenon_Hbd]. % 40.93/41.28 cut (((age zenon_TX_t zenon_TT1_s) = (sigma))); [idtac | apply NNPP; zenon_intro zenon_Hec]. % 40.93/41.28 congruence. % 40.93/41.28 elim (classic ((sigma) = (sigma))); [ zenon_intro zenon_Hed | zenon_intro zenon_Hbd ]. % 40.93/41.28 cut (((sigma) = (sigma)) = ((age zenon_TX_t zenon_TT1_s) = (sigma))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hec. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hed. % 40.93/41.28 cut (((sigma) = (sigma))); [idtac | apply NNPP; zenon_intro zenon_Hbd]. % 40.93/41.28 cut (((sigma) = (age zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Heb]. % 40.93/41.28 congruence. % 40.93/41.28 exact (zenon_Heb zenon_Hea). % 40.93/41.28 apply zenon_Hbd. apply refl_equal. % 40.93/41.28 apply zenon_Hbd. apply refl_equal. % 40.93/41.28 apply zenon_Hbd. apply refl_equal. % 40.93/41.28 generalize (assumption_13 zenon_TX_t). zenon_intro zenon_H8a. % 40.93/41.28 generalize (assumption_17 zenon_TX_t). zenon_intro zenon_H5c. % 40.93/41.28 generalize (zenon_H8a zenon_TT0_cq). zenon_intro zenon_H8c. % 40.93/41.28 apply (zenon_imply_s _ _ zenon_H8c); [ zenon_intro zenon_H48 | zenon_intro zenon_H40 ]. % 40.93/41.28 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H3e | zenon_intro zenon_H49 ]. % 40.93/41.28 exact (zenon_H3e zenon_H36). % 40.93/41.28 exact (zenon_H49 zenon_H43). % 40.93/41.28 generalize (zenon_H5c zenon_TT0_cq). zenon_intro zenon_Hb2. % 40.93/41.28 apply (zenon_imply_s _ _ zenon_Hb2); [ zenon_intro zenon_H3e | zenon_intro zenon_Hb3 ]. % 40.93/41.28 exact (zenon_H3e zenon_H36). % 40.93/41.28 apply (zenon_and_s _ _ zenon_Hb3). zenon_intro zenon_Hb5. zenon_intro zenon_Hb4. % 40.93/41.28 apply (zenon_imply_s _ _ zenon_Hb4); [ zenon_intro zenon_H91 | zenon_intro zenon_Hb6 ]. % 40.93/41.28 apply (zenon_L15_ zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.28 apply (zenon_and_s _ _ zenon_Hb6). zenon_intro zenon_Hb8. zenon_intro zenon_Hb7. % 40.93/41.28 apply (zenon_and_s _ _ zenon_Hb7). zenon_intro zenon_Hba. zenon_intro zenon_Hb9. % 40.93/41.28 apply (zenon_and_s _ _ zenon_Hb9). zenon_intro zenon_Haf. zenon_intro zenon_Hbb. % 40.93/41.28 apply (zenon_imply_s _ _ zenon_Haf); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Haa ]. % 40.93/41.28 apply (zenon_notand_s _ _ zenon_Hb0); [ zenon_intro zenon_H55 | zenon_intro zenon_Hb1 ]. % 40.93/41.28 exact (zenon_H55 zenon_H40). % 40.93/41.28 apply zenon_Hb1. zenon_intro zenon_Ha5. % 40.93/41.28 apply (zenon_L17_ zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.28 elim (classic ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hd7 | zenon_intro zenon_Hc4 ]. % 40.93/41.28 elim (classic (greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (mod2))); [ zenon_intro zenon_Hd3 | zenon_intro zenon_Hd4 ]. % 40.93/41.28 elim (classic (greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hce | zenon_intro zenon_Hc7 ]. % 40.93/41.28 elim (classic (greater (hazard_of_mortality zenon_TX_t zenon_TT0_cq) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))); [ zenon_intro zenon_He8 | zenon_intro zenon_Hc1 ]. % 40.93/41.28 generalize (zenon_He (hazard_of_mortality zenon_TX_t zenon_TT1_s)). zenon_intro zenon_Hee. % 40.93/41.28 generalize (zenon_Hee (hazard_of_mortality zenon_TX_t zenon_TT0_cq)). zenon_intro zenon_Hef. % 40.93/41.28 generalize (zenon_Hef (hazard_of_mortality zenon_TX_t zenon_TT2_bz)). zenon_intro zenon_Hf0. % 40.93/41.28 apply (zenon_imply_s _ _ zenon_Hf0); [ zenon_intro zenon_Hc7 | zenon_intro zenon_Hf1 ]. % 40.93/41.28 exact (zenon_Hc7 zenon_Hce). % 40.93/41.28 apply (zenon_imply_s _ _ zenon_Hf1); [ zenon_intro zenon_Hc1 | zenon_intro zenon_Hf2 ]. % 40.93/41.28 exact (zenon_Hc1 zenon_He8). % 40.93/41.28 exact (zenon_H8b zenon_Hf2). % 40.93/41.28 apply (zenon_L33_ zenon_TT2_bz zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.28 cut ((greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (mod2)) = (greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hc7. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hd3. % 40.93/41.28 cut (((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 40.93/41.28 congruence. % 40.93/41.28 apply zenon_Hd5. apply refl_equal. % 40.93/41.28 exact (zenon_Hc4 zenon_Hd7). % 40.93/41.28 apply (zenon_L51_ zenon_TT2_bz zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.28 elim (classic ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq)) = ((mod2) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Hc4. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.28 exact zenon_Hac. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 40.93/41.28 cut (((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 40.93/41.28 congruence. % 40.93/41.28 exact (zenon_Hc5 zenon_Haa). % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 apply zenon_Had. apply refl_equal. % 40.93/41.28 elim (classic ((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s))); [ zenon_intro zenon_Hf3 | zenon_intro zenon_H24 ]. % 40.93/41.28 cut (((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s)) = ((sigma) = (age zenon_TX_t zenon_TT1_s))). % 40.93/41.28 intro zenon_D_pnotp. % 40.93/41.28 apply zenon_Heb. % 40.93/41.28 rewrite <- zenon_D_pnotp. % 40.93/41.29 exact zenon_Hf3. % 40.93/41.29 cut (((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_H24]. % 40.93/41.29 cut (((age zenon_TX_t zenon_TT1_s) = (sigma))); [idtac | apply NNPP; zenon_intro zenon_Hec]. % 40.93/41.29 congruence. % 40.93/41.29 exact (zenon_Hec zenon_Hbc). % 40.93/41.29 apply zenon_H24. apply refl_equal. % 40.93/41.29 apply zenon_H24. apply refl_equal. % 40.93/41.29 (* end of lemma zenon_L52_ *) % 40.93/41.29 assert (zenon_L53_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT2_bz : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater (sigma) (tau))) -> (~(greater (hazard_of_mortality zenon_TX_t zenon_TT1_s) (hazard_of_mortality zenon_TX_t zenon_TT2_bz))) -> (greater (age zenon_TX_t zenon_TT2_bz) (sigma)) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> ((sigma) = (tau)) -> (greater (tau) (zero)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (~(has_endowment zenon_TX_t)) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> False). % 40.93/41.29 do 4 intro. intros zenon_He zenon_Hf4 zenon_H8b zenon_H32 zenon_Hbc zenon_Hf zenon_H95 zenon_H56 zenon_H37 zenon_H43 zenon_H36. % 40.93/41.29 elim (classic (greater (sigma) (sigma))); [ zenon_intro zenon_Hf5 | zenon_intro zenon_He9 ]. % 40.93/41.29 cut ((greater (sigma) (sigma)) = (greater (sigma) (tau))). % 40.93/41.29 intro zenon_D_pnotp. % 40.93/41.29 apply zenon_Hf4. % 40.93/41.29 rewrite <- zenon_D_pnotp. % 40.93/41.29 exact zenon_Hf5. % 40.93/41.29 cut (((sigma) = (tau))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 40.93/41.29 cut (((sigma) = (sigma))); [idtac | apply NNPP; zenon_intro zenon_Hbd]. % 40.93/41.29 congruence. % 40.93/41.29 apply zenon_Hbd. apply refl_equal. % 40.93/41.29 exact (zenon_H25 zenon_Hf). % 40.93/41.29 apply (zenon_L52_ zenon_TT0_cq zenon_TT2_bz zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.29 (* end of lemma zenon_L53_ *) % 40.93/41.29 assert (zenon_L54_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> ((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> ((sigma) = (tau)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (~(has_endowment zenon_TX_t)) -> (forall T : zenon_U, ((organization zenon_TX_t)->(((has_immunity zenon_TX_t T)->((hazard_of_mortality zenon_TX_t T) = (very_low)))/\((~(has_immunity zenon_TX_t T))->((((is_aligned zenon_TX_t T)/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (low)))/\((((~(is_aligned zenon_TX_t T))/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (mod1)))/\((((is_aligned zenon_TX_t T)/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (mod2)))/\(((~(is_aligned zenon_TX_t T))/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (high)))))))))) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> False). % 40.93/41.29 do 3 intro. intros zenon_H3f zenon_H40 zenon_Haa zenon_Hab zenon_Hbc zenon_Hf zenon_H56 zenon_H37 zenon_H5c zenon_H42 zenon_H43 zenon_H36. % 40.93/41.29 generalize (meaning_postulate_greater_strict (mod2)). zenon_intro zenon_He6. % 40.93/41.29 apply (zenon_L47_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.29 (* end of lemma zenon_L54_ *) % 40.93/41.29 assert (zenon_L55_ : forall (zenon_TT1_s : zenon_U) (zenon_TT0_cq : zenon_U) (zenon_TX_t : zenon_U), ((((is_aligned zenon_TX_t zenon_TT0_cq)/\(positional_advantage zenon_TX_t zenon_TT0_cq))->((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (low)))/\((((~(is_aligned zenon_TX_t zenon_TT0_cq))/\(positional_advantage zenon_TX_t zenon_TT0_cq))->((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod1)))/\((((is_aligned zenon_TX_t zenon_TT0_cq)/\(~(positional_advantage zenon_TX_t zenon_TT0_cq)))->((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (mod2)))/\(((~(is_aligned zenon_TX_t zenon_TT0_cq))/\(~(positional_advantage zenon_TX_t zenon_TT0_cq)))->((hazard_of_mortality zenon_TX_t zenon_TT0_cq) = (high)))))) -> (greater (tau) (zero)) -> (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_t)/\((age zenon_TX_t T0) = (zero)))->((greater (age zenon_TX_t T) (sigma))<->(dissimilar zenon_TX_t T0 T))))) -> (is_aligned zenon_TX_t zenon_TT0_cq) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> ((sigma) = (tau)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (~(has_endowment zenon_TX_t)) -> (forall T : zenon_U, ((organization zenon_TX_t)->(((has_immunity zenon_TX_t T)->((hazard_of_mortality zenon_TX_t T) = (very_low)))/\((~(has_immunity zenon_TX_t T))->((((is_aligned zenon_TX_t T)/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (low)))/\((((~(is_aligned zenon_TX_t T))/\(positional_advantage zenon_TX_t T))->((hazard_of_mortality zenon_TX_t T) = (mod1)))/\((((is_aligned zenon_TX_t T)/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (mod2)))/\(((~(is_aligned zenon_TX_t T))/\(~(positional_advantage zenon_TX_t T)))->((hazard_of_mortality zenon_TX_t T) = (high)))))))))) -> (~(greater (age zenon_TX_t zenon_TT1_s) (sigma))) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> False). % 40.93/41.29 do 3 intro. intros zenon_Hb6 zenon_H95 zenon_H3f zenon_H40 zenon_Hab zenon_Hbc zenon_Hf zenon_H56 zenon_H37 zenon_H5c zenon_H42 zenon_H43 zenon_H36. % 40.93/41.29 apply (zenon_and_s _ _ zenon_Hb6). zenon_intro zenon_Hb8. zenon_intro zenon_Hb7. % 40.93/41.29 apply (zenon_and_s _ _ zenon_Hb7). zenon_intro zenon_Hba. zenon_intro zenon_Hb9. % 40.93/41.29 apply (zenon_and_s _ _ zenon_Hb9). zenon_intro zenon_Haf. zenon_intro zenon_Hbb. % 40.93/41.29 apply (zenon_imply_s _ _ zenon_Haf); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Haa ]. % 40.93/41.29 apply (zenon_notand_s _ _ zenon_Hb0); [ zenon_intro zenon_H55 | zenon_intro zenon_Hb1 ]. % 40.93/41.29 exact (zenon_H55 zenon_H40). % 40.93/41.29 apply zenon_Hb1. zenon_intro zenon_Ha5. % 40.93/41.29 apply (zenon_L17_ zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.29 apply (zenon_L54_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.29 (* end of lemma zenon_L55_ *) % 40.93/41.29 assert (zenon_L56_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), (~(has_endowment zenon_TX_t)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (greater (tau) (zero)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((sigma) = (tau)) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> (~(greater (sigma) (sigma))) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> False). % 40.93/41.29 do 3 intro. intros zenon_H37 zenon_H56 zenon_H95 zenon_Hab zenon_Hf zenon_H43 zenon_H36 zenon_He9 zenon_Hbc. % 40.93/41.29 elim (classic ((sigma) = (age zenon_TX_t zenon_TT1_s))); [ zenon_intro zenon_Hea | zenon_intro zenon_Heb ]. % 40.93/41.29 elim (classic (greater (age zenon_TX_t zenon_TT1_s) (sigma))); [ zenon_intro zenon_H4b | zenon_intro zenon_H42 ]. % 40.93/41.29 cut ((greater (age zenon_TX_t zenon_TT1_s) (sigma)) = (greater (sigma) (sigma))). % 40.93/41.29 intro zenon_D_pnotp. % 40.93/41.29 apply zenon_He9. % 40.93/41.29 rewrite <- zenon_D_pnotp. % 40.93/41.29 exact zenon_H4b. % 40.93/41.29 cut (((sigma) = (sigma))); [idtac | apply NNPP; zenon_intro zenon_Hbd]. % 40.93/41.29 cut (((age zenon_TX_t zenon_TT1_s) = (sigma))); [idtac | apply NNPP; zenon_intro zenon_Hec]. % 40.93/41.29 congruence. % 40.93/41.29 elim (classic ((sigma) = (sigma))); [ zenon_intro zenon_Hed | zenon_intro zenon_Hbd ]. % 40.93/41.29 cut (((sigma) = (sigma)) = ((age zenon_TX_t zenon_TT1_s) = (sigma))). % 40.93/41.29 intro zenon_D_pnotp. % 40.93/41.29 apply zenon_Hec. % 40.93/41.29 rewrite <- zenon_D_pnotp. % 40.93/41.29 exact zenon_Hed. % 40.93/41.29 cut (((sigma) = (sigma))); [idtac | apply NNPP; zenon_intro zenon_Hbd]. % 40.93/41.29 cut (((sigma) = (age zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Heb]. % 40.93/41.29 congruence. % 40.93/41.29 exact (zenon_Heb zenon_Hea). % 40.93/41.29 apply zenon_Hbd. apply refl_equal. % 40.93/41.29 apply zenon_Hbd. apply refl_equal. % 40.93/41.29 apply zenon_Hbd. apply refl_equal. % 40.93/41.29 generalize (assumption_13 zenon_TX_t). zenon_intro zenon_H8a. % 40.93/41.29 generalize (assumption_15 zenon_TX_t). zenon_intro zenon_H3f. % 40.93/41.29 generalize (zenon_H8a zenon_TT0_cq). zenon_intro zenon_H8c. % 40.93/41.29 apply (zenon_imply_s _ _ zenon_H8c); [ zenon_intro zenon_H48 | zenon_intro zenon_H40 ]. % 40.93/41.29 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H3e | zenon_intro zenon_H49 ]. % 40.93/41.29 exact (zenon_H3e zenon_H36). % 40.93/41.29 exact (zenon_H49 zenon_H43). % 40.93/41.29 generalize (assumption_17 zenon_TX_t). zenon_intro zenon_H5c. % 40.93/41.29 generalize (zenon_H5c zenon_TT0_cq). zenon_intro zenon_Hb2. % 40.93/41.29 apply (zenon_imply_s _ _ zenon_Hb2); [ zenon_intro zenon_H3e | zenon_intro zenon_Hb3 ]. % 40.93/41.29 exact (zenon_H3e zenon_H36). % 40.93/41.29 apply (zenon_and_s _ _ zenon_Hb3). zenon_intro zenon_Hb5. zenon_intro zenon_Hb4. % 40.93/41.29 apply (zenon_imply_s _ _ zenon_Hb4); [ zenon_intro zenon_H91 | zenon_intro zenon_Hb6 ]. % 40.93/41.29 apply (zenon_L15_ zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.29 apply (zenon_L55_ zenon_TT1_s zenon_TT0_cq zenon_TX_t); trivial. % 40.93/41.29 elim (classic ((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s))); [ zenon_intro zenon_Hf3 | zenon_intro zenon_H24 ]. % 40.93/41.29 cut (((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s)) = ((sigma) = (age zenon_TX_t zenon_TT1_s))). % 40.93/41.29 intro zenon_D_pnotp. % 40.93/41.29 apply zenon_Heb. % 40.93/41.29 rewrite <- zenon_D_pnotp. % 40.93/41.29 exact zenon_Hf3. % 40.93/41.29 cut (((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_H24]. % 40.93/41.29 cut (((age zenon_TX_t zenon_TT1_s) = (sigma))); [idtac | apply NNPP; zenon_intro zenon_Hec]. % 40.93/41.29 congruence. % 40.93/41.29 exact (zenon_Hec zenon_Hbc). % 40.93/41.29 apply zenon_H24. apply refl_equal. % 40.93/41.29 apply zenon_H24. apply refl_equal. % 40.93/41.29 (* end of lemma zenon_L56_ *) % 40.93/41.29 assert (zenon_L57_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), (~(greater (sigma) (tau))) -> (~(has_endowment zenon_TX_t)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (greater (tau) (zero)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> ((sigma) = (tau)) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> False). % 40.93/41.29 do 3 intro. intros zenon_Hf4 zenon_H37 zenon_H56 zenon_H95 zenon_Hab zenon_Hbc zenon_Hf zenon_H43 zenon_H36. % 40.93/41.29 elim (classic (greater (sigma) (sigma))); [ zenon_intro zenon_Hf5 | zenon_intro zenon_He9 ]. % 40.93/41.29 cut ((greater (sigma) (sigma)) = (greater (sigma) (tau))). % 40.93/41.29 intro zenon_D_pnotp. % 40.93/41.29 apply zenon_Hf4. % 40.93/41.29 rewrite <- zenon_D_pnotp. % 40.93/41.29 exact zenon_Hf5. % 40.93/41.29 cut (((sigma) = (tau))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 40.93/41.29 cut (((sigma) = (sigma))); [idtac | apply NNPP; zenon_intro zenon_Hbd]. % 40.93/41.29 congruence. % 40.93/41.29 apply zenon_Hbd. apply refl_equal. % 40.93/41.29 exact (zenon_H25 zenon_Hf). % 40.93/41.29 apply (zenon_L56_ zenon_TT0_cq zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.29 (* end of lemma zenon_L57_ *) % 40.93/41.29 assert (zenon_L58_ : forall (zenon_TT0_cq : zenon_U) (zenon_TT1_s : zenon_U) (zenon_TX_t : zenon_U), (~(has_endowment zenon_TX_t)) -> (forall T : zenon_U, (((smaller_or_equal (age zenon_TX_t T) (tau))->(~(positional_advantage zenon_TX_t T)))/\((greater (age zenon_TX_t T) (tau))->(positional_advantage zenon_TX_t T)))) -> (greater (tau) (zero)) -> (~((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))) -> ((age zenon_TX_t zenon_TT0_cq) = (zero)) -> (organization zenon_TX_t) -> ((sigma) = (tau)) -> ((age zenon_TX_t zenon_TT1_s) = (sigma)) -> False). % 40.93/41.29 do 3 intro. intros zenon_H37 zenon_H56 zenon_H95 zenon_Hab zenon_H43 zenon_H36 zenon_Hf zenon_Hbc. % 40.93/41.29 generalize (zenon_H56 zenon_TT1_s). zenon_intro zenon_H58. % 40.93/41.29 apply (zenon_and_s _ _ zenon_H58). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 40.93/41.29 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_H11 | zenon_intro zenon_H5b ]. % 40.93/41.29 apply (zenon_L23_ zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.29 apply (zenon_imply_s _ _ zenon_H59); [ zenon_intro zenon_H90 | zenon_intro zenon_H57 ]. % 40.93/41.29 elim (classic (greater (sigma) (tau))); [ zenon_intro zenon_Hf6 | zenon_intro zenon_Hf4 ]. % 40.93/41.29 cut ((greater (sigma) (tau)) = (greater (age zenon_TX_t zenon_TT1_s) (tau))). % 40.93/41.29 intro zenon_D_pnotp. % 40.93/41.29 apply zenon_H90. % 40.93/41.29 rewrite <- zenon_D_pnotp. % 40.93/41.29 exact zenon_Hf6. % 40.93/41.29 cut (((tau) = (tau))); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 40.93/41.29 cut (((sigma) = (age zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Heb]. % 40.93/41.29 congruence. % 40.93/41.29 elim (classic ((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s))); [ zenon_intro zenon_Hf3 | zenon_intro zenon_H24 ]. % 40.93/41.29 cut (((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s)) = ((sigma) = (age zenon_TX_t zenon_TT1_s))). % 40.93/41.29 intro zenon_D_pnotp. % 40.93/41.29 apply zenon_Heb. % 40.93/41.29 rewrite <- zenon_D_pnotp. % 40.93/41.29 exact zenon_Hf3. % 40.93/41.29 cut (((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_H24]. % 40.93/41.29 cut (((age zenon_TX_t zenon_TT1_s) = (sigma))); [idtac | apply NNPP; zenon_intro zenon_Hec]. % 40.93/41.29 congruence. % 40.93/41.29 exact (zenon_Hec zenon_Hbc). % 40.93/41.29 apply zenon_H24. apply refl_equal. % 40.93/41.29 apply zenon_H24. apply refl_equal. % 40.93/41.29 apply zenon_H2a. apply refl_equal. % 40.93/41.29 apply (zenon_L57_ zenon_TT0_cq zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.29 exact (zenon_H5b zenon_H57). % 40.93/41.29 (* end of lemma zenon_L58_ *) % 40.93/41.29 apply NNPP. intro zenon_G. % 40.93/41.29 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_He | zenon_intro zenon_Hf7 ]. % 40.93/41.29 apply (zenon_notallex_s (fun X : zenon_U => (forall T0 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization X)/\((robust_position X)/\((~(has_endowment X))/\(((age X T0) = (zero))/\((greater (sigma) (zero))/\((greater (tau) (zero))/\(((sigma) = (tau))/\((smaller_or_equal (age X T1) (sigma))/\(greater (age X T2) (sigma))))))))))->((smaller (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_Hf8; idtac ]. % 40.93/41.29 elim zenon_Hf8. zenon_intro zenon_TX_t. zenon_intro zenon_Hf9. % 40.93/41.29 apply (zenon_notallex_s (fun T0 : zenon_U => (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_t)/\((robust_position zenon_TX_t)/\((~(has_endowment zenon_TX_t))/\(((age zenon_TX_t T0) = (zero))/\((greater (sigma) (zero))/\((greater (tau) (zero))/\(((sigma) = (tau))/\((smaller_or_equal (age zenon_TX_t T1) (sigma))/\(greater (age zenon_TX_t T2) (sigma))))))))))->((smaller (hazard_of_mortality zenon_TX_t T2) (hazard_of_mortality zenon_TX_t T1))/\((hazard_of_mortality zenon_TX_t T1) = (hazard_of_mortality zenon_TX_t T0))))))) zenon_Hf9); [ zenon_intro zenon_Hfa; idtac ]. % 40.93/41.29 elim zenon_Hfa. zenon_intro zenon_TT0_cq. zenon_intro zenon_Hfb. % 40.93/41.29 apply (zenon_notallex_s (fun T1 : zenon_U => (forall T2 : zenon_U, (((organization zenon_TX_t)/\((robust_position zenon_TX_t)/\((~(has_endowment zenon_TX_t))/\(((age zenon_TX_t zenon_TT0_cq) = (zero))/\((greater (sigma) (zero))/\((greater (tau) (zero))/\(((sigma) = (tau))/\((smaller_or_equal (age zenon_TX_t T1) (sigma))/\(greater (age zenon_TX_t T2) (sigma))))))))))->((smaller (hazard_of_mortality zenon_TX_t T2) (hazard_of_mortality zenon_TX_t T1))/\((hazard_of_mortality zenon_TX_t T1) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq)))))) zenon_Hfb); [ zenon_intro zenon_Hfc; idtac ]. % 40.93/41.29 elim zenon_Hfc. zenon_intro zenon_TT1_s. zenon_intro zenon_Hfd. % 40.93/41.29 apply (zenon_notallex_s (fun T2 : zenon_U => (((organization zenon_TX_t)/\((robust_position zenon_TX_t)/\((~(has_endowment zenon_TX_t))/\(((age zenon_TX_t zenon_TT0_cq) = (zero))/\((greater (sigma) (zero))/\((greater (tau) (zero))/\(((sigma) = (tau))/\((smaller_or_equal (age zenon_TX_t zenon_TT1_s) (sigma))/\(greater (age zenon_TX_t T2) (sigma))))))))))->((smaller (hazard_of_mortality zenon_TX_t T2) (hazard_of_mortality zenon_TX_t zenon_TT1_s))/\((hazard_of_mortality zenon_TX_t zenon_TT1_s) = (hazard_of_mortality zenon_TX_t zenon_TT0_cq))))) zenon_Hfd); [ zenon_intro zenon_Hfe; idtac ]. % 40.93/41.29 elim zenon_Hfe. zenon_intro zenon_TT2_bz. zenon_intro zenon_Hff. % 40.93/41.29 apply (zenon_notimply_s _ _ zenon_Hff). zenon_intro zenon_H101. zenon_intro zenon_H100. % 40.93/41.29 apply (zenon_and_s _ _ zenon_H101). zenon_intro zenon_H36. zenon_intro zenon_H102. % 40.93/41.29 apply (zenon_and_s _ _ zenon_H102). zenon_intro zenon_H104. zenon_intro zenon_H103. % 40.93/41.29 apply (zenon_and_s _ _ zenon_H103). zenon_intro zenon_H37. zenon_intro zenon_H105. % 40.93/41.29 apply (zenon_and_s _ _ zenon_H105). zenon_intro zenon_H43. zenon_intro zenon_H106. % 40.93/41.29 apply (zenon_and_s _ _ zenon_H106). zenon_intro zenon_H108. zenon_intro zenon_H107. % 40.93/41.29 apply (zenon_and_s _ _ zenon_H107). zenon_intro zenon_H95. zenon_intro zenon_H109. % 40.93/41.29 apply (zenon_and_s _ _ zenon_H109). zenon_intro zenon_Hf. zenon_intro zenon_H10a. % 40.93/41.29 apply (zenon_and_s _ _ zenon_H10a). zenon_intro zenon_H10b. zenon_intro zenon_H32. % 40.93/41.29 generalize (definition_4 zenon_TX_t). zenon_intro zenon_H10c. % 40.93/41.29 apply (zenon_equiv_s _ _ zenon_H10c); [ zenon_intro zenon_H10e; zenon_intro zenon_H10d | zenon_intro zenon_H104; zenon_intro zenon_H56 ]. % 40.93/41.29 exact (zenon_H10e zenon_H104). % 40.93/41.29 generalize (definition_smaller_or_equal (age zenon_TX_t zenon_TT1_s)). zenon_intro zenon_H14. % 40.93/41.29 generalize (zenon_H14 (sigma)). zenon_intro zenon_H10f. % 40.93/41.29 apply (zenon_equiv_s _ _ zenon_H10f); [ zenon_intro zenon_H112; zenon_intro zenon_H111 | zenon_intro zenon_H10b; zenon_intro zenon_H110 ]. % 40.93/41.29 exact (zenon_H112 zenon_H10b). % 40.93/41.29 apply (zenon_or_s _ _ zenon_H110); [ zenon_intro zenon_H113 | zenon_intro zenon_Hbc ]. % 40.93/41.29 generalize (definition_smaller (age zenon_TX_t zenon_TT1_s)). zenon_intro zenon_H1b. % 40.93/41.29 generalize (zenon_H1b (sigma)). zenon_intro zenon_H114. % 40.93/41.29 apply (zenon_equiv_s _ _ zenon_H114); [ zenon_intro zenon_H115; zenon_intro zenon_H30 | zenon_intro zenon_H113; zenon_intro zenon_H10 ]. % 40.93/41.29 exact (zenon_H115 zenon_H113). % 40.93/41.29 apply (zenon_notand_s _ _ zenon_H100); [ zenon_intro zenon_H116 | zenon_intro zenon_Hab ]. % 40.93/41.29 generalize (definition_smaller (hazard_of_mortality zenon_TX_t zenon_TT2_bz)). zenon_intro zenon_H117. % 40.93/41.29 generalize (zenon_H117 (hazard_of_mortality zenon_TX_t zenon_TT1_s)). zenon_intro zenon_H118. % 40.93/41.29 apply (zenon_equiv_s _ _ zenon_H118); [ zenon_intro zenon_H116; zenon_intro zenon_H8b | zenon_intro zenon_H119; zenon_intro zenon_Hf2 ]. % 40.93/41.29 generalize (zenon_H56 zenon_TT1_s). zenon_intro zenon_H58. % 40.93/41.29 apply (zenon_and_s _ _ zenon_H58). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 40.93/41.29 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_H11 | zenon_intro zenon_H5b ]. % 40.93/41.29 apply (zenon_L1_ zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.29 apply (zenon_imply_s _ _ zenon_H59); [ zenon_intro zenon_H90 | zenon_intro zenon_H57 ]. % 40.93/41.29 apply (zenon_L14_ zenon_TT0_cq zenon_TT2_bz zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.29 exact (zenon_H5b zenon_H57). % 40.93/41.29 exact (zenon_H116 zenon_H119). % 40.93/41.29 generalize (zenon_H56 zenon_TT1_s). zenon_intro zenon_H58. % 40.93/41.29 apply (zenon_and_s _ _ zenon_H58). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 40.93/41.29 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_H11 | zenon_intro zenon_H5b ]. % 40.93/41.29 apply (zenon_L1_ zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.29 apply (zenon_imply_s _ _ zenon_H59); [ zenon_intro zenon_H90 | zenon_intro zenon_H57 ]. % 40.93/41.29 apply (zenon_L21_ zenon_TT0_cq zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.29 exact (zenon_H5b zenon_H57). % 40.93/41.29 apply (zenon_notand_s _ _ zenon_H100); [ zenon_intro zenon_H116 | zenon_intro zenon_Hab ]. % 40.93/41.29 generalize (definition_smaller (hazard_of_mortality zenon_TX_t zenon_TT2_bz)). zenon_intro zenon_H117. % 40.93/41.29 generalize (zenon_H117 (hazard_of_mortality zenon_TX_t zenon_TT1_s)). zenon_intro zenon_H118. % 40.93/41.29 apply (zenon_equiv_s _ _ zenon_H118); [ zenon_intro zenon_H116; zenon_intro zenon_H8b | zenon_intro zenon_H119; zenon_intro zenon_Hf2 ]. % 40.93/41.29 generalize (zenon_H56 zenon_TT1_s). zenon_intro zenon_H58. % 40.93/41.29 apply (zenon_and_s _ _ zenon_H58). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 40.93/41.29 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_H11 | zenon_intro zenon_H5b ]. % 40.93/41.29 apply (zenon_L23_ zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.29 apply (zenon_imply_s _ _ zenon_H59); [ zenon_intro zenon_H90 | zenon_intro zenon_H57 ]. % 40.93/41.29 elim (classic (greater (sigma) (tau))); [ zenon_intro zenon_Hf6 | zenon_intro zenon_Hf4 ]. % 40.93/41.29 cut ((greater (sigma) (tau)) = (greater (age zenon_TX_t zenon_TT1_s) (tau))). % 40.93/41.29 intro zenon_D_pnotp. % 40.93/41.29 apply zenon_H90. % 40.93/41.29 rewrite <- zenon_D_pnotp. % 40.93/41.29 exact zenon_Hf6. % 40.93/41.29 cut (((tau) = (tau))); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 40.93/41.29 cut (((sigma) = (age zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_Heb]. % 40.93/41.29 congruence. % 40.93/41.29 elim (classic ((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s))); [ zenon_intro zenon_Hf3 | zenon_intro zenon_H24 ]. % 40.93/41.29 cut (((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s)) = ((sigma) = (age zenon_TX_t zenon_TT1_s))). % 40.93/41.29 intro zenon_D_pnotp. % 40.93/41.29 apply zenon_Heb. % 40.93/41.29 rewrite <- zenon_D_pnotp. % 40.93/41.29 exact zenon_Hf3. % 40.93/41.29 cut (((age zenon_TX_t zenon_TT1_s) = (age zenon_TX_t zenon_TT1_s))); [idtac | apply NNPP; zenon_intro zenon_H24]. % 40.93/41.29 cut (((age zenon_TX_t zenon_TT1_s) = (sigma))); [idtac | apply NNPP; zenon_intro zenon_Hec]. % 40.93/41.29 congruence. % 40.93/41.29 exact (zenon_Hec zenon_Hbc). % 40.93/41.29 apply zenon_H24. apply refl_equal. % 40.93/41.29 apply zenon_H24. apply refl_equal. % 40.93/41.29 apply zenon_H2a. apply refl_equal. % 40.93/41.29 apply (zenon_L53_ zenon_TT0_cq zenon_TT2_bz zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.29 exact (zenon_H5b zenon_H57). % 40.93/41.29 exact (zenon_H116 zenon_H119). % 40.93/41.29 apply (zenon_L58_ zenon_TT0_cq zenon_TT1_s zenon_TX_t); trivial. % 40.93/41.29 apply zenon_Hf7. zenon_intro zenon_Tx_kw. apply NNPP. zenon_intro zenon_H11b. % 40.93/41.29 apply zenon_H11b. zenon_intro zenon_Ty_ky. apply NNPP. zenon_intro zenon_H11d. % 40.93/41.29 apply zenon_H11d. zenon_intro zenon_Tz_la. apply NNPP. zenon_intro zenon_H11f. % 40.93/41.29 apply (zenon_notimply_s _ _ zenon_H11f). zenon_intro zenon_H121. zenon_intro zenon_H120. % 40.93/41.29 apply (zenon_notimply_s _ _ zenon_H120). zenon_intro zenon_H123. zenon_intro zenon_H122. % 40.93/41.29 generalize (meaning_postulate_greater_transitive zenon_Tx_kw). zenon_intro zenon_H124. % 40.93/41.29 generalize (zenon_H124 zenon_Ty_ky). zenon_intro zenon_H125. % 40.93/41.29 generalize (zenon_H125 zenon_Tz_la). zenon_intro zenon_H126. % 40.93/41.29 apply (zenon_imply_s _ _ zenon_H126); [ zenon_intro zenon_H128 | zenon_intro zenon_H127 ]. % 40.93/41.29 apply (zenon_notand_s _ _ zenon_H128); [ zenon_intro zenon_H12a | zenon_intro zenon_H129 ]. % 40.93/41.29 exact (zenon_H12a zenon_H121). % 40.93/41.29 exact (zenon_H129 zenon_H123). % 40.93/41.29 exact (zenon_H122 zenon_H127). % 40.93/41.29 Qed. % 40.93/41.29 % SZS output end Proof % 40.93/41.29 (* END-PROOF *) % 40.93/41.29 nodes searched: 1032449 % 40.93/41.29 max branch formulas: 1892 % 40.93/41.29 proof nodes created: 18584 % 40.93/41.29 formulas created: 360847 % 40.93/41.29 %------------------------------------------------------------------------------