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