%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT085+1 : TPTP v9.3.1. Bugfixed v9.3.1. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:24:27 AM UTC 2026 % Result : Theorem 0.38s 0.65s % Output : Proof 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT085+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 0.00/0.03 % Command : run_zenon %s %d % 0.09/0.35 % Computer : n017.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Mon Sep 7 14:14:24 UTC 2026 % 0.14/0.36 % CPUTime : % 0.38/0.65 (* PROOF-FOUND *) % 0.38/0.65 % SZS status Theorem % 0.38/0.65 (* BEGIN-PROOF *) % 0.38/0.65 % SZS output start Proof % 0.38/0.65 Theorem odrl445 : (~(exists X : zenon_U, (exists Y : zenon_U, (exists Z : zenon_U, (((in_lopen X (v0) (v200))\/((in_lopen Y (v0) (v100))\/(in_lopen Z (v0) (v50))))/\((leq (v400) X)/\((leq (v200) Y)/\(leq (v100) Z)))))))). % 0.38/0.65 Proof. % 0.38/0.65 assert (zenon_L1_ : (~((v400) = (v400))) -> False). % 0.38/0.65 do 0 intro. intros zenon_H2c. % 0.38/0.65 apply zenon_H2c. apply refl_equal. % 0.38/0.65 (* end of lemma zenon_L1_ *) % 0.38/0.65 assert (zenon_L2_ : forall (zenon_TX_bw : zenon_U), (zenon_TX_bw = (v200)) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z)))))) -> (~(less zenon_TX_bw (v400))) -> False). % 0.38/0.65 do 1 intro. intros zenon_H2d zenon_H2e zenon_H2f. % 0.38/0.65 elim (classic ((~(zenon_TX_bw = (v200)))/\(~(less zenon_TX_bw (v200))))); [ zenon_intro zenon_H31 | zenon_intro zenon_H32 ]. % 0.38/0.65 apply (zenon_and_s _ _ zenon_H31). zenon_intro zenon_H34. zenon_intro zenon_H33. % 0.38/0.65 exact (zenon_H34 zenon_H2d). % 0.38/0.65 cut ((less (v200) (v400)) = (less zenon_TX_bw (v400))). % 0.38/0.65 intro zenon_D_pnotp. % 0.38/0.65 apply zenon_H2f. % 0.38/0.65 rewrite <- zenon_D_pnotp. % 0.38/0.65 exact ord_v200_v400. % 0.38/0.65 cut (((v400) = (v400))); [idtac | apply NNPP; zenon_intro zenon_H2c]. % 0.38/0.65 cut (((v200) = zenon_TX_bw)); [idtac | apply NNPP; zenon_intro zenon_H35]. % 0.38/0.65 congruence. % 0.38/0.65 apply (zenon_notand_s _ _ zenon_H32); [ zenon_intro zenon_H37 | zenon_intro zenon_H36 ]. % 0.38/0.65 apply zenon_H37. zenon_intro zenon_H2d. % 0.38/0.65 elim (classic (zenon_TX_bw = zenon_TX_bw)); [ zenon_intro zenon_H38 | zenon_intro zenon_H39 ]. % 0.38/0.65 cut ((zenon_TX_bw = zenon_TX_bw) = ((v200) = zenon_TX_bw)). % 0.38/0.65 intro zenon_D_pnotp. % 0.38/0.65 apply zenon_H35. % 0.38/0.65 rewrite <- zenon_D_pnotp. % 0.38/0.65 exact zenon_H38. % 0.38/0.65 cut ((zenon_TX_bw = zenon_TX_bw)); [idtac | apply NNPP; zenon_intro zenon_H39]. % 0.38/0.65 cut ((zenon_TX_bw = (v200))); [idtac | apply NNPP; zenon_intro zenon_H34]. % 0.38/0.65 congruence. % 0.38/0.65 exact (zenon_H34 zenon_H2d). % 0.38/0.65 apply zenon_H39. apply refl_equal. % 0.38/0.65 apply zenon_H39. apply refl_equal. % 0.38/0.65 apply zenon_H36. zenon_intro zenon_H3a. % 0.38/0.65 generalize (zenon_H2e zenon_TX_bw). zenon_intro zenon_H3b. % 0.38/0.65 generalize (zenon_H3b (v200)). zenon_intro zenon_H3c. % 0.38/0.65 generalize (zenon_H3c (v400)). zenon_intro zenon_H3d. % 0.38/0.65 apply (zenon_imply_s _ _ zenon_H3d); [ zenon_intro zenon_H33 | zenon_intro zenon_H3e ]. % 0.38/0.65 exact (zenon_H33 zenon_H3a). % 0.38/0.65 apply (zenon_imply_s _ _ zenon_H3e); [ zenon_intro zenon_H40 | zenon_intro zenon_H3f ]. % 0.38/0.65 exact (zenon_H40 ord_v200_v400). % 0.38/0.65 exact (zenon_H2f zenon_H3f). % 0.38/0.65 apply zenon_H2c. apply refl_equal. % 0.38/0.65 (* end of lemma zenon_L2_ *) % 0.38/0.65 assert (zenon_L3_ : forall (zenon_TX_bw : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z)))))) -> (in_lopen zenon_TX_bw (v0) (v200)) -> (less (v400) zenon_TX_bw) -> False). % 0.38/0.65 do 1 intro. intros zenon_H2e zenon_H41 zenon_H42. % 0.38/0.65 generalize (in_lopen zenon_TX_bw). zenon_intro zenon_H43. % 0.38/0.65 generalize (zenon_H43 (v0)). zenon_intro zenon_H44. % 0.38/0.65 generalize (zenon_H44 (v200)). zenon_intro zenon_H45. % 0.38/0.65 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H48; zenon_intro zenon_H47 | zenon_intro zenon_H41; zenon_intro zenon_H46 ]. % 0.38/0.65 exact (zenon_H48 zenon_H41). % 0.38/0.65 apply (zenon_and_s _ _ zenon_H46). zenon_intro zenon_H4a. zenon_intro zenon_H49. % 0.38/0.66 generalize (leq_def zenon_TX_bw). zenon_intro zenon_H4b. % 0.38/0.66 generalize (zenon_H4b (v200)). zenon_intro zenon_H4c. % 0.38/0.66 apply (zenon_equiv_s _ _ zenon_H4c); [ zenon_intro zenon_H4f; zenon_intro zenon_H4e | zenon_intro zenon_H49; zenon_intro zenon_H4d ]. % 0.38/0.66 exact (zenon_H4f zenon_H49). % 0.38/0.66 apply (zenon_or_s _ _ zenon_H4d); [ zenon_intro zenon_H3a | zenon_intro zenon_H2d ]. % 0.38/0.66 generalize (irreflexive zenon_TX_bw). zenon_intro zenon_H50. % 0.38/0.66 elim (classic ((~(zenon_TX_bw = (v400)))/\(~(less zenon_TX_bw (v400))))); [ zenon_intro zenon_H51 | zenon_intro zenon_H52 ]. % 0.38/0.66 apply (zenon_and_s _ _ zenon_H51). zenon_intro zenon_H53. zenon_intro zenon_H2f. % 0.38/0.66 elim (classic ((~(zenon_TX_bw = (v200)))/\(~(less zenon_TX_bw (v200))))); [ zenon_intro zenon_H31 | zenon_intro zenon_H32 ]. % 0.38/0.66 apply (zenon_and_s _ _ zenon_H31). zenon_intro zenon_H34. zenon_intro zenon_H33. % 0.38/0.66 exact (zenon_H33 zenon_H3a). % 0.38/0.66 cut ((less (v200) (v400)) = (less zenon_TX_bw (v400))). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_H2f. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact ord_v200_v400. % 0.38/0.66 cut (((v400) = (v400))); [idtac | apply NNPP; zenon_intro zenon_H2c]. % 0.38/0.66 cut (((v200) = zenon_TX_bw)); [idtac | apply NNPP; zenon_intro zenon_H35]. % 0.38/0.66 congruence. % 0.38/0.66 apply (zenon_notand_s _ _ zenon_H32); [ zenon_intro zenon_H37 | zenon_intro zenon_H36 ]. % 0.38/0.66 apply zenon_H37. zenon_intro zenon_H2d. % 0.38/0.66 elim (classic (zenon_TX_bw = zenon_TX_bw)); [ zenon_intro zenon_H38 | zenon_intro zenon_H39 ]. % 0.38/0.66 cut ((zenon_TX_bw = zenon_TX_bw) = ((v200) = zenon_TX_bw)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_H35. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_H38. % 0.38/0.66 cut ((zenon_TX_bw = zenon_TX_bw)); [idtac | apply NNPP; zenon_intro zenon_H39]. % 0.38/0.66 cut ((zenon_TX_bw = (v200))); [idtac | apply NNPP; zenon_intro zenon_H34]. % 0.38/0.66 congruence. % 0.38/0.66 exact (zenon_H34 zenon_H2d). % 0.38/0.66 apply zenon_H39. apply refl_equal. % 0.38/0.66 apply zenon_H39. apply refl_equal. % 0.38/0.66 apply zenon_H36. zenon_intro zenon_H3a. % 0.38/0.66 generalize (zenon_H2e zenon_TX_bw). zenon_intro zenon_H3b. % 0.38/0.66 generalize (zenon_H3b (v200)). zenon_intro zenon_H3c. % 0.38/0.66 generalize (zenon_H3c (v400)). zenon_intro zenon_H3d. % 0.38/0.66 apply (zenon_imply_s _ _ zenon_H3d); [ zenon_intro zenon_H33 | zenon_intro zenon_H3e ]. % 0.38/0.66 exact (zenon_H33 zenon_H3a). % 0.38/0.66 apply (zenon_imply_s _ _ zenon_H3e); [ zenon_intro zenon_H40 | zenon_intro zenon_H3f ]. % 0.38/0.66 exact (zenon_H40 ord_v200_v400). % 0.38/0.66 exact (zenon_H2f zenon_H3f). % 0.38/0.66 apply zenon_H2c. apply refl_equal. % 0.38/0.66 cut ((less (v400) zenon_TX_bw) = (less zenon_TX_bw zenon_TX_bw)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_H50. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_H42. % 0.38/0.66 cut ((zenon_TX_bw = zenon_TX_bw)); [idtac | apply NNPP; zenon_intro zenon_H39]. % 0.38/0.66 cut (((v400) = zenon_TX_bw)); [idtac | apply NNPP; zenon_intro zenon_H54]. % 0.38/0.66 congruence. % 0.38/0.66 apply (zenon_notand_s _ _ zenon_H52); [ zenon_intro zenon_H56 | zenon_intro zenon_H55 ]. % 0.38/0.66 apply zenon_H56. zenon_intro zenon_H57. % 0.38/0.66 elim (classic (zenon_TX_bw = zenon_TX_bw)); [ zenon_intro zenon_H38 | zenon_intro zenon_H39 ]. % 0.38/0.66 cut ((zenon_TX_bw = zenon_TX_bw) = ((v400) = zenon_TX_bw)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_H54. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_H38. % 0.38/0.66 cut ((zenon_TX_bw = zenon_TX_bw)); [idtac | apply NNPP; zenon_intro zenon_H39]. % 0.38/0.66 cut ((zenon_TX_bw = (v400))); [idtac | apply NNPP; zenon_intro zenon_H53]. % 0.38/0.66 congruence. % 0.38/0.66 exact (zenon_H53 zenon_H57). % 0.38/0.66 apply zenon_H39. apply refl_equal. % 0.38/0.66 apply zenon_H39. apply refl_equal. % 0.38/0.66 apply zenon_H55. zenon_intro zenon_H3f. % 0.38/0.66 generalize (zenon_H2e zenon_TX_bw). zenon_intro zenon_H3b. % 0.38/0.66 generalize (zenon_H3b (v400)). zenon_intro zenon_H58. % 0.38/0.66 generalize (zenon_H58 zenon_TX_bw). zenon_intro zenon_H59. % 0.38/0.66 apply (zenon_imply_s _ _ zenon_H59); [ zenon_intro zenon_H2f | zenon_intro zenon_H5a ]. % 0.38/0.66 exact (zenon_H2f zenon_H3f). % 0.38/0.66 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_H5c | zenon_intro zenon_H5b ]. % 0.38/0.66 exact (zenon_H5c zenon_H42). % 0.38/0.66 exact (zenon_H50 zenon_H5b). % 0.38/0.66 apply zenon_H39. apply refl_equal. % 0.38/0.66 generalize (irreflexive zenon_TX_bw). zenon_intro zenon_H50. % 0.38/0.66 elim (classic ((~(zenon_TX_bw = (v400)))/\(~(less zenon_TX_bw (v400))))); [ zenon_intro zenon_H51 | zenon_intro zenon_H52 ]. % 0.38/0.66 apply (zenon_and_s _ _ zenon_H51). zenon_intro zenon_H53. zenon_intro zenon_H2f. % 0.38/0.66 apply (zenon_L2_ zenon_TX_bw); trivial. % 0.38/0.66 cut ((less (v400) zenon_TX_bw) = (less zenon_TX_bw zenon_TX_bw)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_H50. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_H42. % 0.38/0.66 cut ((zenon_TX_bw = zenon_TX_bw)); [idtac | apply NNPP; zenon_intro zenon_H39]. % 0.38/0.66 cut (((v400) = zenon_TX_bw)); [idtac | apply NNPP; zenon_intro zenon_H54]. % 0.38/0.66 congruence. % 0.38/0.66 apply (zenon_notand_s _ _ zenon_H52); [ zenon_intro zenon_H56 | zenon_intro zenon_H55 ]. % 0.38/0.66 apply zenon_H56. zenon_intro zenon_H57. % 0.38/0.66 elim (classic (zenon_TX_bw = zenon_TX_bw)); [ zenon_intro zenon_H38 | zenon_intro zenon_H39 ]. % 0.38/0.66 cut ((zenon_TX_bw = zenon_TX_bw) = ((v400) = zenon_TX_bw)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_H54. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_H38. % 0.38/0.66 cut ((zenon_TX_bw = zenon_TX_bw)); [idtac | apply NNPP; zenon_intro zenon_H39]. % 0.38/0.66 cut ((zenon_TX_bw = (v400))); [idtac | apply NNPP; zenon_intro zenon_H53]. % 0.38/0.66 congruence. % 0.38/0.66 exact (zenon_H53 zenon_H57). % 0.38/0.66 apply zenon_H39. apply refl_equal. % 0.38/0.66 apply zenon_H39. apply refl_equal. % 0.38/0.66 apply zenon_H55. zenon_intro zenon_H3f. % 0.38/0.66 generalize (zenon_H2e zenon_TX_bw). zenon_intro zenon_H3b. % 0.38/0.66 generalize (zenon_H3b (v400)). zenon_intro zenon_H58. % 0.38/0.66 generalize (zenon_H58 zenon_TX_bw). zenon_intro zenon_H59. % 0.38/0.66 apply (zenon_imply_s _ _ zenon_H59); [ zenon_intro zenon_H2f | zenon_intro zenon_H5a ]. % 0.38/0.66 exact (zenon_H2f zenon_H3f). % 0.38/0.66 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_H5c | zenon_intro zenon_H5b ]. % 0.38/0.66 exact (zenon_H5c zenon_H42). % 0.38/0.66 exact (zenon_H50 zenon_H5b). % 0.38/0.66 apply zenon_H39. apply refl_equal. % 0.38/0.66 (* end of lemma zenon_L3_ *) % 0.38/0.66 assert (zenon_L4_ : (~((v200) = (v200))) -> False). % 0.38/0.66 do 0 intro. intros zenon_H5d. % 0.38/0.66 apply zenon_H5d. apply refl_equal. % 0.38/0.66 (* end of lemma zenon_L4_ *) % 0.38/0.66 assert (zenon_L5_ : forall (zenon_TY_ds : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z)))))) -> (in_lopen zenon_TY_ds (v0) (v100)) -> (less (v200) zenon_TY_ds) -> False). % 0.38/0.66 do 1 intro. intros zenon_H2e zenon_H5e zenon_H5f. % 0.38/0.66 generalize (in_lopen zenon_TY_ds). zenon_intro zenon_H61. % 0.38/0.66 generalize (zenon_H61 (v0)). zenon_intro zenon_H62. % 0.38/0.66 generalize (zenon_H62 (v100)). zenon_intro zenon_H63. % 0.38/0.66 apply (zenon_equiv_s _ _ zenon_H63); [ zenon_intro zenon_H66; zenon_intro zenon_H65 | zenon_intro zenon_H5e; zenon_intro zenon_H64 ]. % 0.38/0.66 exact (zenon_H66 zenon_H5e). % 0.38/0.66 apply (zenon_and_s _ _ zenon_H64). zenon_intro zenon_H68. zenon_intro zenon_H67. % 0.38/0.66 generalize (leq_def zenon_TY_ds). zenon_intro zenon_H69. % 0.38/0.66 generalize (zenon_H69 (v100)). zenon_intro zenon_H6a. % 0.38/0.66 apply (zenon_equiv_s _ _ zenon_H6a); [ zenon_intro zenon_H6d; zenon_intro zenon_H6c | zenon_intro zenon_H67; zenon_intro zenon_H6b ]. % 0.38/0.66 exact (zenon_H6d zenon_H67). % 0.38/0.66 apply (zenon_or_s _ _ zenon_H6b); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 0.38/0.66 generalize (irreflexive zenon_TY_ds). zenon_intro zenon_H70. % 0.38/0.66 elim (classic ((~(zenon_TY_ds = (v200)))/\(~(less zenon_TY_ds (v200))))); [ zenon_intro zenon_H71 | zenon_intro zenon_H72 ]. % 0.38/0.66 apply (zenon_and_s _ _ zenon_H71). zenon_intro zenon_H74. zenon_intro zenon_H73. % 0.38/0.66 elim (classic ((~(zenon_TY_ds = (v100)))/\(~(less zenon_TY_ds (v100))))); [ zenon_intro zenon_H75 | zenon_intro zenon_H76 ]. % 0.38/0.66 apply (zenon_and_s _ _ zenon_H75). zenon_intro zenon_H78. zenon_intro zenon_H77. % 0.38/0.66 exact (zenon_H77 zenon_H6f). % 0.38/0.66 cut ((less (v100) (v200)) = (less zenon_TY_ds (v200))). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_H73. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact ord_v100_v200. % 0.38/0.66 cut (((v200) = (v200))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 0.38/0.66 cut (((v100) = zenon_TY_ds)); [idtac | apply NNPP; zenon_intro zenon_H79]. % 0.38/0.66 congruence. % 0.38/0.66 apply (zenon_notand_s _ _ zenon_H76); [ zenon_intro zenon_H7b | zenon_intro zenon_H7a ]. % 0.38/0.66 apply zenon_H7b. zenon_intro zenon_H6e. % 0.38/0.66 elim (classic (zenon_TY_ds = zenon_TY_ds)); [ zenon_intro zenon_H7c | zenon_intro zenon_H7d ]. % 0.38/0.66 cut ((zenon_TY_ds = zenon_TY_ds) = ((v100) = zenon_TY_ds)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_H79. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_H7c. % 0.38/0.66 cut ((zenon_TY_ds = zenon_TY_ds)); [idtac | apply NNPP; zenon_intro zenon_H7d]. % 0.38/0.66 cut ((zenon_TY_ds = (v100))); [idtac | apply NNPP; zenon_intro zenon_H78]. % 0.38/0.66 congruence. % 0.38/0.66 exact (zenon_H78 zenon_H6e). % 0.38/0.66 apply zenon_H7d. apply refl_equal. % 0.38/0.66 apply zenon_H7d. apply refl_equal. % 0.38/0.66 apply zenon_H7a. zenon_intro zenon_H6f. % 0.38/0.66 generalize (zenon_H2e zenon_TY_ds). zenon_intro zenon_H7e. % 0.38/0.66 generalize (zenon_H7e (v100)). zenon_intro zenon_H7f. % 0.38/0.66 generalize (zenon_H7f (v200)). zenon_intro zenon_H80. % 0.38/0.66 apply (zenon_imply_s _ _ zenon_H80); [ zenon_intro zenon_H77 | zenon_intro zenon_H81 ]. % 0.38/0.66 exact (zenon_H77 zenon_H6f). % 0.38/0.66 apply (zenon_imply_s _ _ zenon_H81); [ zenon_intro zenon_H83 | zenon_intro zenon_H82 ]. % 0.38/0.66 exact (zenon_H83 ord_v100_v200). % 0.38/0.66 exact (zenon_H73 zenon_H82). % 0.38/0.66 apply zenon_H5d. apply refl_equal. % 0.38/0.66 cut ((less (v200) zenon_TY_ds) = (less zenon_TY_ds zenon_TY_ds)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_H70. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_H5f. % 0.38/0.66 cut ((zenon_TY_ds = zenon_TY_ds)); [idtac | apply NNPP; zenon_intro zenon_H7d]. % 0.38/0.66 cut (((v200) = zenon_TY_ds)); [idtac | apply NNPP; zenon_intro zenon_H84]. % 0.38/0.66 congruence. % 0.38/0.66 apply (zenon_notand_s _ _ zenon_H72); [ zenon_intro zenon_H86 | zenon_intro zenon_H85 ]. % 0.38/0.66 apply zenon_H86. zenon_intro zenon_H87. % 0.38/0.66 elim (classic (zenon_TY_ds = zenon_TY_ds)); [ zenon_intro zenon_H7c | zenon_intro zenon_H7d ]. % 0.38/0.66 cut ((zenon_TY_ds = zenon_TY_ds) = ((v200) = zenon_TY_ds)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_H84. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_H7c. % 0.38/0.66 cut ((zenon_TY_ds = zenon_TY_ds)); [idtac | apply NNPP; zenon_intro zenon_H7d]. % 0.38/0.66 cut ((zenon_TY_ds = (v200))); [idtac | apply NNPP; zenon_intro zenon_H74]. % 0.38/0.66 congruence. % 0.38/0.66 exact (zenon_H74 zenon_H87). % 0.38/0.66 apply zenon_H7d. apply refl_equal. % 0.38/0.66 apply zenon_H7d. apply refl_equal. % 0.38/0.66 apply zenon_H85. zenon_intro zenon_H82. % 0.38/0.66 generalize (zenon_H2e zenon_TY_ds). zenon_intro zenon_H7e. % 0.38/0.66 generalize (zenon_H7e (v200)). zenon_intro zenon_H88. % 0.38/0.66 generalize (zenon_H88 zenon_TY_ds). zenon_intro zenon_H89. % 0.38/0.66 apply (zenon_imply_s _ _ zenon_H89); [ zenon_intro zenon_H73 | zenon_intro zenon_H8a ]. % 0.38/0.66 exact (zenon_H73 zenon_H82). % 0.38/0.66 apply (zenon_imply_s _ _ zenon_H8a); [ zenon_intro zenon_H8c | zenon_intro zenon_H8b ]. % 0.38/0.66 exact (zenon_H8c zenon_H5f). % 0.38/0.66 exact (zenon_H70 zenon_H8b). % 0.38/0.66 apply zenon_H7d. apply refl_equal. % 0.38/0.66 generalize (irreflexive zenon_TY_ds). zenon_intro zenon_H70. % 0.38/0.66 elim (classic ((~(zenon_TY_ds = (v200)))/\(~(less zenon_TY_ds (v200))))); [ zenon_intro zenon_H71 | zenon_intro zenon_H72 ]. % 0.38/0.66 apply (zenon_and_s _ _ zenon_H71). zenon_intro zenon_H74. zenon_intro zenon_H73. % 0.38/0.66 elim (classic ((~(zenon_TY_ds = (v100)))/\(~(less zenon_TY_ds (v100))))); [ zenon_intro zenon_H75 | zenon_intro zenon_H76 ]. % 0.38/0.66 apply (zenon_and_s _ _ zenon_H75). zenon_intro zenon_H78. zenon_intro zenon_H77. % 0.38/0.66 exact (zenon_H78 zenon_H6e). % 0.38/0.66 cut ((less (v100) (v200)) = (less zenon_TY_ds (v200))). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_H73. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact ord_v100_v200. % 0.38/0.66 cut (((v200) = (v200))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 0.38/0.66 cut (((v100) = zenon_TY_ds)); [idtac | apply NNPP; zenon_intro zenon_H79]. % 0.38/0.66 congruence. % 0.38/0.66 apply (zenon_notand_s _ _ zenon_H76); [ zenon_intro zenon_H7b | zenon_intro zenon_H7a ]. % 0.38/0.66 apply zenon_H7b. zenon_intro zenon_H6e. % 0.38/0.66 elim (classic (zenon_TY_ds = zenon_TY_ds)); [ zenon_intro zenon_H7c | zenon_intro zenon_H7d ]. % 0.38/0.66 cut ((zenon_TY_ds = zenon_TY_ds) = ((v100) = zenon_TY_ds)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_H79. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_H7c. % 0.38/0.66 cut ((zenon_TY_ds = zenon_TY_ds)); [idtac | apply NNPP; zenon_intro zenon_H7d]. % 0.38/0.66 cut ((zenon_TY_ds = (v100))); [idtac | apply NNPP; zenon_intro zenon_H78]. % 0.38/0.66 congruence. % 0.38/0.66 exact (zenon_H78 zenon_H6e). % 0.38/0.66 apply zenon_H7d. apply refl_equal. % 0.38/0.66 apply zenon_H7d. apply refl_equal. % 0.38/0.66 apply zenon_H7a. zenon_intro zenon_H6f. % 0.38/0.66 generalize (zenon_H2e zenon_TY_ds). zenon_intro zenon_H7e. % 0.38/0.66 generalize (zenon_H7e (v100)). zenon_intro zenon_H7f. % 0.38/0.66 generalize (zenon_H7f (v200)). zenon_intro zenon_H80. % 0.38/0.66 apply (zenon_imply_s _ _ zenon_H80); [ zenon_intro zenon_H77 | zenon_intro zenon_H81 ]. % 0.38/0.66 exact (zenon_H77 zenon_H6f). % 0.38/0.66 apply (zenon_imply_s _ _ zenon_H81); [ zenon_intro zenon_H83 | zenon_intro zenon_H82 ]. % 0.38/0.66 exact (zenon_H83 ord_v100_v200). % 0.38/0.66 exact (zenon_H73 zenon_H82). % 0.38/0.66 apply zenon_H5d. apply refl_equal. % 0.38/0.66 cut ((less (v200) zenon_TY_ds) = (less zenon_TY_ds zenon_TY_ds)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_H70. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_H5f. % 0.38/0.66 cut ((zenon_TY_ds = zenon_TY_ds)); [idtac | apply NNPP; zenon_intro zenon_H7d]. % 0.38/0.66 cut (((v200) = zenon_TY_ds)); [idtac | apply NNPP; zenon_intro zenon_H84]. % 0.38/0.66 congruence. % 0.38/0.66 apply (zenon_notand_s _ _ zenon_H72); [ zenon_intro zenon_H86 | zenon_intro zenon_H85 ]. % 0.38/0.66 apply zenon_H86. zenon_intro zenon_H87. % 0.38/0.66 elim (classic (zenon_TY_ds = zenon_TY_ds)); [ zenon_intro zenon_H7c | zenon_intro zenon_H7d ]. % 0.38/0.66 cut ((zenon_TY_ds = zenon_TY_ds) = ((v200) = zenon_TY_ds)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_H84. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_H7c. % 0.38/0.66 cut ((zenon_TY_ds = zenon_TY_ds)); [idtac | apply NNPP; zenon_intro zenon_H7d]. % 0.38/0.66 cut ((zenon_TY_ds = (v200))); [idtac | apply NNPP; zenon_intro zenon_H74]. % 0.38/0.66 congruence. % 0.38/0.66 exact (zenon_H74 zenon_H87). % 0.38/0.66 apply zenon_H7d. apply refl_equal. % 0.38/0.66 apply zenon_H7d. apply refl_equal. % 0.38/0.66 apply zenon_H85. zenon_intro zenon_H82. % 0.38/0.66 generalize (zenon_H2e zenon_TY_ds). zenon_intro zenon_H7e. % 0.38/0.66 generalize (zenon_H7e (v200)). zenon_intro zenon_H88. % 0.38/0.66 generalize (zenon_H88 zenon_TY_ds). zenon_intro zenon_H89. % 0.38/0.66 apply (zenon_imply_s _ _ zenon_H89); [ zenon_intro zenon_H73 | zenon_intro zenon_H8a ]. % 0.38/0.66 exact (zenon_H73 zenon_H82). % 0.38/0.66 apply (zenon_imply_s _ _ zenon_H8a); [ zenon_intro zenon_H8c | zenon_intro zenon_H8b ]. % 0.38/0.66 exact (zenon_H8c zenon_H5f). % 0.38/0.66 exact (zenon_H70 zenon_H8b). % 0.38/0.66 apply zenon_H7d. apply refl_equal. % 0.38/0.66 (* end of lemma zenon_L5_ *) % 0.38/0.66 assert (zenon_L6_ : (~((v100) = (v100))) -> False). % 0.38/0.66 do 0 intro. intros zenon_H8d. % 0.38/0.66 apply zenon_H8d. apply refl_equal. % 0.38/0.66 (* end of lemma zenon_L6_ *) % 0.38/0.66 assert (zenon_L7_ : forall (zenon_TZ_fo : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z)))))) -> (in_lopen zenon_TZ_fo (v0) (v50)) -> (less (v100) zenon_TZ_fo) -> False). % 0.38/0.66 do 1 intro. intros zenon_H2e zenon_H8e zenon_H8f. % 0.38/0.66 generalize (in_lopen zenon_TZ_fo). zenon_intro zenon_H91. % 0.38/0.66 generalize (zenon_H91 (v0)). zenon_intro zenon_H92. % 0.38/0.66 generalize (zenon_H92 (v50)). zenon_intro zenon_H93. % 0.38/0.66 apply (zenon_equiv_s _ _ zenon_H93); [ zenon_intro zenon_H96; zenon_intro zenon_H95 | zenon_intro zenon_H8e; zenon_intro zenon_H94 ]. % 0.38/0.66 exact (zenon_H96 zenon_H8e). % 0.38/0.66 apply (zenon_and_s _ _ zenon_H94). zenon_intro zenon_H98. zenon_intro zenon_H97. % 0.38/0.66 generalize (leq_def zenon_TZ_fo). zenon_intro zenon_H99. % 0.38/0.66 generalize (zenon_H99 (v50)). zenon_intro zenon_H9a. % 0.38/0.66 apply (zenon_equiv_s _ _ zenon_H9a); [ zenon_intro zenon_H9d; zenon_intro zenon_H9c | zenon_intro zenon_H97; zenon_intro zenon_H9b ]. % 0.38/0.66 exact (zenon_H9d zenon_H97). % 0.38/0.66 apply (zenon_or_s _ _ zenon_H9b); [ zenon_intro zenon_H9f | zenon_intro zenon_H9e ]. % 0.38/0.66 generalize (irreflexive zenon_TZ_fo). zenon_intro zenon_Ha0. % 0.38/0.66 elim (classic ((~(zenon_TZ_fo = (v100)))/\(~(less zenon_TZ_fo (v100))))); [ zenon_intro zenon_Ha1 | zenon_intro zenon_Ha2 ]. % 0.38/0.66 apply (zenon_and_s _ _ zenon_Ha1). zenon_intro zenon_Ha4. zenon_intro zenon_Ha3. % 0.38/0.66 elim (classic ((~(zenon_TZ_fo = (v50)))/\(~(less zenon_TZ_fo (v50))))); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Ha6 ]. % 0.38/0.66 apply (zenon_and_s _ _ zenon_Ha5). zenon_intro zenon_Ha8. zenon_intro zenon_Ha7. % 0.38/0.66 exact (zenon_Ha7 zenon_H9f). % 0.38/0.66 cut ((less (v50) (v100)) = (less zenon_TZ_fo (v100))). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Ha3. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact ord_v50_v100. % 0.38/0.66 cut (((v100) = (v100))); [idtac | apply NNPP; zenon_intro zenon_H8d]. % 0.38/0.66 cut (((v50) = zenon_TZ_fo)); [idtac | apply NNPP; zenon_intro zenon_Ha9]. % 0.38/0.66 congruence. % 0.38/0.66 apply (zenon_notand_s _ _ zenon_Ha6); [ zenon_intro zenon_Hab | zenon_intro zenon_Haa ]. % 0.38/0.66 apply zenon_Hab. zenon_intro zenon_H9e. % 0.38/0.66 elim (classic (zenon_TZ_fo = zenon_TZ_fo)); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 0.38/0.66 cut ((zenon_TZ_fo = zenon_TZ_fo) = ((v50) = zenon_TZ_fo)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Ha9. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_Hac. % 0.38/0.66 cut ((zenon_TZ_fo = zenon_TZ_fo)); [idtac | apply NNPP; zenon_intro zenon_Had]. % 0.38/0.66 cut ((zenon_TZ_fo = (v50))); [idtac | apply NNPP; zenon_intro zenon_Ha8]. % 0.38/0.66 congruence. % 0.38/0.66 exact (zenon_Ha8 zenon_H9e). % 0.38/0.66 apply zenon_Had. apply refl_equal. % 0.38/0.66 apply zenon_Had. apply refl_equal. % 0.38/0.66 apply zenon_Haa. zenon_intro zenon_H9f. % 0.38/0.66 generalize (zenon_H2e zenon_TZ_fo). zenon_intro zenon_Hae. % 0.38/0.66 generalize (zenon_Hae (v50)). zenon_intro zenon_Haf. % 0.38/0.66 generalize (zenon_Haf (v100)). zenon_intro zenon_Hb0. % 0.38/0.66 apply (zenon_imply_s _ _ zenon_Hb0); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Hb1 ]. % 0.38/0.66 exact (zenon_Ha7 zenon_H9f). % 0.38/0.66 apply (zenon_imply_s _ _ zenon_Hb1); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hb2 ]. % 0.38/0.66 exact (zenon_Hb3 ord_v50_v100). % 0.38/0.66 exact (zenon_Ha3 zenon_Hb2). % 0.38/0.66 apply zenon_H8d. apply refl_equal. % 0.38/0.66 cut ((less (v100) zenon_TZ_fo) = (less zenon_TZ_fo zenon_TZ_fo)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Ha0. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_H8f. % 0.38/0.66 cut ((zenon_TZ_fo = zenon_TZ_fo)); [idtac | apply NNPP; zenon_intro zenon_Had]. % 0.38/0.66 cut (((v100) = zenon_TZ_fo)); [idtac | apply NNPP; zenon_intro zenon_Hb4]. % 0.38/0.66 congruence. % 0.38/0.66 apply (zenon_notand_s _ _ zenon_Ha2); [ zenon_intro zenon_Hb6 | zenon_intro zenon_Hb5 ]. % 0.38/0.66 apply zenon_Hb6. zenon_intro zenon_Hb7. % 0.38/0.66 elim (classic (zenon_TZ_fo = zenon_TZ_fo)); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 0.38/0.66 cut ((zenon_TZ_fo = zenon_TZ_fo) = ((v100) = zenon_TZ_fo)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Hb4. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_Hac. % 0.38/0.66 cut ((zenon_TZ_fo = zenon_TZ_fo)); [idtac | apply NNPP; zenon_intro zenon_Had]. % 0.38/0.66 cut ((zenon_TZ_fo = (v100))); [idtac | apply NNPP; zenon_intro zenon_Ha4]. % 0.38/0.66 congruence. % 0.38/0.66 exact (zenon_Ha4 zenon_Hb7). % 0.38/0.66 apply zenon_Had. apply refl_equal. % 0.38/0.66 apply zenon_Had. apply refl_equal. % 0.38/0.66 apply zenon_Hb5. zenon_intro zenon_Hb2. % 0.38/0.66 generalize (zenon_H2e zenon_TZ_fo). zenon_intro zenon_Hae. % 0.38/0.66 generalize (zenon_Hae (v100)). zenon_intro zenon_Hb8. % 0.38/0.66 generalize (zenon_Hb8 zenon_TZ_fo). zenon_intro zenon_Hb9. % 0.38/0.66 apply (zenon_imply_s _ _ zenon_Hb9); [ zenon_intro zenon_Ha3 | zenon_intro zenon_Hba ]. % 0.38/0.66 exact (zenon_Ha3 zenon_Hb2). % 0.38/0.66 apply (zenon_imply_s _ _ zenon_Hba); [ zenon_intro zenon_Hbc | zenon_intro zenon_Hbb ]. % 0.38/0.66 exact (zenon_Hbc zenon_H8f). % 0.38/0.66 exact (zenon_Ha0 zenon_Hbb). % 0.38/0.66 apply zenon_Had. apply refl_equal. % 0.38/0.66 generalize (irreflexive zenon_TZ_fo). zenon_intro zenon_Ha0. % 0.38/0.66 elim (classic ((~(zenon_TZ_fo = (v100)))/\(~(less zenon_TZ_fo (v100))))); [ zenon_intro zenon_Ha1 | zenon_intro zenon_Ha2 ]. % 0.38/0.66 apply (zenon_and_s _ _ zenon_Ha1). zenon_intro zenon_Ha4. zenon_intro zenon_Ha3. % 0.38/0.66 elim (classic ((~(zenon_TZ_fo = (v50)))/\(~(less zenon_TZ_fo (v50))))); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Ha6 ]. % 0.38/0.66 apply (zenon_and_s _ _ zenon_Ha5). zenon_intro zenon_Ha8. zenon_intro zenon_Ha7. % 0.38/0.66 exact (zenon_Ha8 zenon_H9e). % 0.38/0.66 cut ((less (v50) (v100)) = (less zenon_TZ_fo (v100))). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Ha3. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact ord_v50_v100. % 0.38/0.66 cut (((v100) = (v100))); [idtac | apply NNPP; zenon_intro zenon_H8d]. % 0.38/0.66 cut (((v50) = zenon_TZ_fo)); [idtac | apply NNPP; zenon_intro zenon_Ha9]. % 0.38/0.66 congruence. % 0.38/0.66 apply (zenon_notand_s _ _ zenon_Ha6); [ zenon_intro zenon_Hab | zenon_intro zenon_Haa ]. % 0.38/0.66 apply zenon_Hab. zenon_intro zenon_H9e. % 0.38/0.66 elim (classic (zenon_TZ_fo = zenon_TZ_fo)); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 0.38/0.66 cut ((zenon_TZ_fo = zenon_TZ_fo) = ((v50) = zenon_TZ_fo)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Ha9. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_Hac. % 0.38/0.66 cut ((zenon_TZ_fo = zenon_TZ_fo)); [idtac | apply NNPP; zenon_intro zenon_Had]. % 0.38/0.66 cut ((zenon_TZ_fo = (v50))); [idtac | apply NNPP; zenon_intro zenon_Ha8]. % 0.38/0.66 congruence. % 0.38/0.66 exact (zenon_Ha8 zenon_H9e). % 0.38/0.66 apply zenon_Had. apply refl_equal. % 0.38/0.66 apply zenon_Had. apply refl_equal. % 0.38/0.66 apply zenon_Haa. zenon_intro zenon_H9f. % 0.38/0.66 generalize (zenon_H2e zenon_TZ_fo). zenon_intro zenon_Hae. % 0.38/0.66 generalize (zenon_Hae (v50)). zenon_intro zenon_Haf. % 0.38/0.66 generalize (zenon_Haf (v100)). zenon_intro zenon_Hb0. % 0.38/0.66 apply (zenon_imply_s _ _ zenon_Hb0); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Hb1 ]. % 0.38/0.66 exact (zenon_Ha7 zenon_H9f). % 0.38/0.66 apply (zenon_imply_s _ _ zenon_Hb1); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hb2 ]. % 0.38/0.66 exact (zenon_Hb3 ord_v50_v100). % 0.38/0.66 exact (zenon_Ha3 zenon_Hb2). % 0.38/0.66 apply zenon_H8d. apply refl_equal. % 0.38/0.66 cut ((less (v100) zenon_TZ_fo) = (less zenon_TZ_fo zenon_TZ_fo)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Ha0. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_H8f. % 0.38/0.66 cut ((zenon_TZ_fo = zenon_TZ_fo)); [idtac | apply NNPP; zenon_intro zenon_Had]. % 0.38/0.66 cut (((v100) = zenon_TZ_fo)); [idtac | apply NNPP; zenon_intro zenon_Hb4]. % 0.38/0.66 congruence. % 0.38/0.66 apply (zenon_notand_s _ _ zenon_Ha2); [ zenon_intro zenon_Hb6 | zenon_intro zenon_Hb5 ]. % 0.38/0.66 apply zenon_Hb6. zenon_intro zenon_Hb7. % 0.38/0.66 elim (classic (zenon_TZ_fo = zenon_TZ_fo)); [ zenon_intro zenon_Hac | zenon_intro zenon_Had ]. % 0.38/0.66 cut ((zenon_TZ_fo = zenon_TZ_fo) = ((v100) = zenon_TZ_fo)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Hb4. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_Hac. % 0.38/0.66 cut ((zenon_TZ_fo = zenon_TZ_fo)); [idtac | apply NNPP; zenon_intro zenon_Had]. % 0.38/0.66 cut ((zenon_TZ_fo = (v100))); [idtac | apply NNPP; zenon_intro zenon_Ha4]. % 0.38/0.66 congruence. % 0.38/0.66 exact (zenon_Ha4 zenon_Hb7). % 0.38/0.66 apply zenon_Had. apply refl_equal. % 0.38/0.66 apply zenon_Had. apply refl_equal. % 0.38/0.66 apply zenon_Hb5. zenon_intro zenon_Hb2. % 0.38/0.66 generalize (zenon_H2e zenon_TZ_fo). zenon_intro zenon_Hae. % 0.38/0.66 generalize (zenon_Hae (v100)). zenon_intro zenon_Hb8. % 0.38/0.66 generalize (zenon_Hb8 zenon_TZ_fo). zenon_intro zenon_Hb9. % 0.38/0.66 apply (zenon_imply_s _ _ zenon_Hb9); [ zenon_intro zenon_Ha3 | zenon_intro zenon_Hba ]. % 0.38/0.66 exact (zenon_Ha3 zenon_Hb2). % 0.38/0.66 apply (zenon_imply_s _ _ zenon_Hba); [ zenon_intro zenon_Hbc | zenon_intro zenon_Hbb ]. % 0.38/0.66 exact (zenon_Hbc zenon_H8f). % 0.38/0.66 exact (zenon_Ha0 zenon_Hbb). % 0.38/0.66 apply zenon_Had. apply refl_equal. % 0.38/0.66 (* end of lemma zenon_L7_ *) % 0.38/0.66 assert (zenon_L8_ : forall (zenon_TX_bw : zenon_U), (~(less (v200) zenon_TX_bw)) -> ((v400) = zenon_TX_bw) -> False). % 0.38/0.66 do 1 intro. intros zenon_Hbd zenon_Hbe. % 0.38/0.66 cut ((less (v200) (v400)) = (less (v200) zenon_TX_bw)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Hbd. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact ord_v200_v400. % 0.38/0.66 cut (((v400) = zenon_TX_bw)); [idtac | apply NNPP; zenon_intro zenon_H54]. % 0.38/0.66 cut (((v200) = (v200))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 0.38/0.66 congruence. % 0.38/0.66 apply zenon_H5d. apply refl_equal. % 0.38/0.66 exact (zenon_H54 zenon_Hbe). % 0.38/0.66 (* end of lemma zenon_L8_ *) % 0.38/0.66 assert (zenon_L9_ : forall (zenon_TX_bw : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z)))))) -> (~(less zenon_TX_bw zenon_TX_bw)) -> (less zenon_TX_bw (v200)) -> ((v400) = zenon_TX_bw) -> False). % 0.38/0.66 do 1 intro. intros zenon_H2e zenon_H50 zenon_H3a zenon_Hbe. % 0.38/0.66 elim (classic (less (v200) zenon_TX_bw)); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hbd ]. % 0.38/0.66 generalize (zenon_H2e zenon_TX_bw). zenon_intro zenon_H3b. % 0.38/0.66 generalize (zenon_H3b (v200)). zenon_intro zenon_H3c. % 0.38/0.66 generalize (zenon_H3c zenon_TX_bw). zenon_intro zenon_Hc0. % 0.38/0.66 apply (zenon_imply_s _ _ zenon_Hc0); [ zenon_intro zenon_H33 | zenon_intro zenon_Hc1 ]. % 0.38/0.66 exact (zenon_H33 zenon_H3a). % 0.38/0.66 apply (zenon_imply_s _ _ zenon_Hc1); [ zenon_intro zenon_Hbd | zenon_intro zenon_H5b ]. % 0.38/0.66 exact (zenon_Hbd zenon_Hbf). % 0.38/0.66 exact (zenon_H50 zenon_H5b). % 0.38/0.66 apply (zenon_L8_ zenon_TX_bw); trivial. % 0.38/0.66 (* end of lemma zenon_L9_ *) % 0.38/0.66 assert (zenon_L10_ : forall (zenon_TX_bw : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z)))))) -> (in_lopen zenon_TX_bw (v0) (v200)) -> (~((v200) = (v400))) -> ((v400) = zenon_TX_bw) -> False). % 0.38/0.66 do 1 intro. intros zenon_H2e zenon_H41 zenon_Hc2 zenon_Hbe. % 0.38/0.66 generalize (in_lopen zenon_TX_bw). zenon_intro zenon_H43. % 0.38/0.66 generalize (zenon_H43 (v0)). zenon_intro zenon_H44. % 0.38/0.66 generalize (zenon_H44 (v200)). zenon_intro zenon_H45. % 0.38/0.66 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H48; zenon_intro zenon_H47 | zenon_intro zenon_H41; zenon_intro zenon_H46 ]. % 0.38/0.66 exact (zenon_H48 zenon_H41). % 0.38/0.66 apply (zenon_and_s _ _ zenon_H46). zenon_intro zenon_H4a. zenon_intro zenon_H49. % 0.38/0.66 generalize (leq_def zenon_TX_bw). zenon_intro zenon_H4b. % 0.38/0.66 generalize (zenon_H4b (v200)). zenon_intro zenon_H4c. % 0.38/0.66 apply (zenon_equiv_s _ _ zenon_H4c); [ zenon_intro zenon_H4f; zenon_intro zenon_H4e | zenon_intro zenon_H49; zenon_intro zenon_H4d ]. % 0.38/0.66 exact (zenon_H4f zenon_H49). % 0.38/0.66 apply (zenon_or_s _ _ zenon_H4d); [ zenon_intro zenon_H3a | zenon_intro zenon_H2d ]. % 0.38/0.66 generalize (irreflexive zenon_TX_bw). zenon_intro zenon_H50. % 0.38/0.66 apply (zenon_L9_ zenon_TX_bw); trivial. % 0.38/0.66 elim (classic ((v400) = (v400))); [ zenon_intro zenon_Hc3 | zenon_intro zenon_H2c ]. % 0.38/0.66 cut (((v400) = (v400)) = ((v200) = (v400))). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Hc2. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_Hc3. % 0.38/0.66 cut (((v400) = (v400))); [idtac | apply NNPP; zenon_intro zenon_H2c]. % 0.38/0.66 cut (((v400) = (v200))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 0.38/0.66 congruence. % 0.38/0.66 cut (((v400) = zenon_TX_bw) = ((v400) = (v200))). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Hc4. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_Hbe. % 0.38/0.66 cut ((zenon_TX_bw = (v200))); [idtac | apply NNPP; zenon_intro zenon_H34]. % 0.38/0.66 cut (((v400) = (v400))); [idtac | apply NNPP; zenon_intro zenon_H2c]. % 0.38/0.66 congruence. % 0.38/0.66 apply zenon_H2c. apply refl_equal. % 0.38/0.66 exact (zenon_H34 zenon_H2d). % 0.38/0.66 apply zenon_H2c. apply refl_equal. % 0.38/0.66 apply zenon_H2c. apply refl_equal. % 0.38/0.66 (* end of lemma zenon_L10_ *) % 0.38/0.66 assert (zenon_L11_ : forall (zenon_TY_ds : zenon_U), (~(less (v100) zenon_TY_ds)) -> ((v200) = zenon_TY_ds) -> False). % 0.38/0.66 do 1 intro. intros zenon_Hc5 zenon_Hc6. % 0.38/0.66 cut ((less (v100) (v200)) = (less (v100) zenon_TY_ds)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Hc5. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact ord_v100_v200. % 0.38/0.66 cut (((v200) = zenon_TY_ds)); [idtac | apply NNPP; zenon_intro zenon_H84]. % 0.38/0.66 cut (((v100) = (v100))); [idtac | apply NNPP; zenon_intro zenon_H8d]. % 0.38/0.66 congruence. % 0.38/0.66 apply zenon_H8d. apply refl_equal. % 0.38/0.66 exact (zenon_H84 zenon_Hc6). % 0.38/0.66 (* end of lemma zenon_L11_ *) % 0.38/0.66 assert (zenon_L12_ : forall (zenon_TY_ds : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z)))))) -> (~(less zenon_TY_ds zenon_TY_ds)) -> (less zenon_TY_ds (v100)) -> ((v200) = zenon_TY_ds) -> False). % 0.38/0.66 do 1 intro. intros zenon_H2e zenon_H70 zenon_H6f zenon_Hc6. % 0.38/0.66 elim (classic (less (v100) zenon_TY_ds)); [ zenon_intro zenon_Hc7 | zenon_intro zenon_Hc5 ]. % 0.38/0.66 generalize (zenon_H2e zenon_TY_ds). zenon_intro zenon_H7e. % 0.38/0.66 generalize (zenon_H7e (v100)). zenon_intro zenon_H7f. % 0.38/0.66 generalize (zenon_H7f zenon_TY_ds). zenon_intro zenon_Hc8. % 0.38/0.66 apply (zenon_imply_s _ _ zenon_Hc8); [ zenon_intro zenon_H77 | zenon_intro zenon_Hc9 ]. % 0.38/0.66 exact (zenon_H77 zenon_H6f). % 0.38/0.66 apply (zenon_imply_s _ _ zenon_Hc9); [ zenon_intro zenon_Hc5 | zenon_intro zenon_H8b ]. % 0.38/0.66 exact (zenon_Hc5 zenon_Hc7). % 0.38/0.66 exact (zenon_H70 zenon_H8b). % 0.38/0.66 apply (zenon_L11_ zenon_TY_ds); trivial. % 0.38/0.66 (* end of lemma zenon_L12_ *) % 0.38/0.66 assert (zenon_L13_ : forall (zenon_TY_ds : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z)))))) -> (in_lopen zenon_TY_ds (v0) (v100)) -> (~((v100) = (v200))) -> ((v200) = zenon_TY_ds) -> False). % 0.38/0.66 do 1 intro. intros zenon_H2e zenon_H5e zenon_Hca zenon_Hc6. % 0.38/0.66 generalize (in_lopen zenon_TY_ds). zenon_intro zenon_H61. % 0.38/0.66 generalize (zenon_H61 (v0)). zenon_intro zenon_H62. % 0.38/0.66 generalize (zenon_H62 (v100)). zenon_intro zenon_H63. % 0.38/0.66 apply (zenon_equiv_s _ _ zenon_H63); [ zenon_intro zenon_H66; zenon_intro zenon_H65 | zenon_intro zenon_H5e; zenon_intro zenon_H64 ]. % 0.38/0.66 exact (zenon_H66 zenon_H5e). % 0.38/0.66 apply (zenon_and_s _ _ zenon_H64). zenon_intro zenon_H68. zenon_intro zenon_H67. % 0.38/0.66 generalize (leq_def zenon_TY_ds). zenon_intro zenon_H69. % 0.38/0.66 generalize (zenon_H69 (v100)). zenon_intro zenon_H6a. % 0.38/0.66 apply (zenon_equiv_s _ _ zenon_H6a); [ zenon_intro zenon_H6d; zenon_intro zenon_H6c | zenon_intro zenon_H67; zenon_intro zenon_H6b ]. % 0.38/0.66 exact (zenon_H6d zenon_H67). % 0.38/0.66 apply (zenon_or_s _ _ zenon_H6b); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 0.38/0.66 generalize (irreflexive zenon_TY_ds). zenon_intro zenon_H70. % 0.38/0.66 apply (zenon_L12_ zenon_TY_ds); trivial. % 0.38/0.66 elim (classic ((v200) = (v200))); [ zenon_intro zenon_Hcb | zenon_intro zenon_H5d ]. % 0.38/0.66 cut (((v200) = (v200)) = ((v100) = (v200))). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Hca. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_Hcb. % 0.38/0.66 cut (((v200) = (v200))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 0.38/0.66 cut (((v200) = (v100))); [idtac | apply NNPP; zenon_intro zenon_Hcc]. % 0.38/0.66 congruence. % 0.38/0.66 cut (((v200) = zenon_TY_ds) = ((v200) = (v100))). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Hcc. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_Hc6. % 0.38/0.66 cut ((zenon_TY_ds = (v100))); [idtac | apply NNPP; zenon_intro zenon_H78]. % 0.38/0.66 cut (((v200) = (v200))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 0.38/0.66 congruence. % 0.38/0.66 apply zenon_H5d. apply refl_equal. % 0.38/0.66 exact (zenon_H78 zenon_H6e). % 0.38/0.66 apply zenon_H5d. apply refl_equal. % 0.38/0.66 apply zenon_H5d. apply refl_equal. % 0.38/0.66 (* end of lemma zenon_L13_ *) % 0.38/0.66 assert (zenon_L14_ : (~((v50) = (v50))) -> False). % 0.38/0.66 do 0 intro. intros zenon_Hcd. % 0.38/0.66 apply zenon_Hcd. apply refl_equal. % 0.38/0.66 (* end of lemma zenon_L14_ *) % 0.38/0.66 assert (zenon_L15_ : forall (zenon_TZ_fo : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z)))))) -> (~(less zenon_TZ_fo zenon_TZ_fo)) -> (less zenon_TZ_fo (v50)) -> ((v100) = zenon_TZ_fo) -> False). % 0.38/0.66 do 1 intro. intros zenon_H2e zenon_Ha0 zenon_H9f zenon_Hce. % 0.38/0.66 elim (classic (less (v50) zenon_TZ_fo)); [ zenon_intro zenon_Hcf | zenon_intro zenon_Hd0 ]. % 0.38/0.66 generalize (zenon_H2e zenon_TZ_fo). zenon_intro zenon_Hae. % 0.38/0.66 generalize (zenon_Hae (v50)). zenon_intro zenon_Haf. % 0.38/0.66 generalize (zenon_Haf zenon_TZ_fo). zenon_intro zenon_Hd1. % 0.38/0.66 apply (zenon_imply_s _ _ zenon_Hd1); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Hd2 ]. % 0.38/0.66 exact (zenon_Ha7 zenon_H9f). % 0.38/0.66 apply (zenon_imply_s _ _ zenon_Hd2); [ zenon_intro zenon_Hd0 | zenon_intro zenon_Hbb ]. % 0.38/0.66 exact (zenon_Hd0 zenon_Hcf). % 0.38/0.66 exact (zenon_Ha0 zenon_Hbb). % 0.38/0.66 cut ((less (v50) (v100)) = (less (v50) zenon_TZ_fo)). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Hd0. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact ord_v50_v100. % 0.38/0.66 cut (((v100) = zenon_TZ_fo)); [idtac | apply NNPP; zenon_intro zenon_Hb4]. % 0.38/0.66 cut (((v50) = (v50))); [idtac | apply NNPP; zenon_intro zenon_Hcd]. % 0.38/0.66 congruence. % 0.38/0.66 apply zenon_Hcd. apply refl_equal. % 0.38/0.66 exact (zenon_Hb4 zenon_Hce). % 0.38/0.66 (* end of lemma zenon_L15_ *) % 0.38/0.66 assert (zenon_L16_ : forall (zenon_TZ_fo : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z)))))) -> (in_lopen zenon_TZ_fo (v0) (v50)) -> (~((v50) = (v100))) -> ((v100) = zenon_TZ_fo) -> False). % 0.38/0.66 do 1 intro. intros zenon_H2e zenon_H8e zenon_Hd3 zenon_Hce. % 0.38/0.66 generalize (in_lopen zenon_TZ_fo). zenon_intro zenon_H91. % 0.38/0.66 generalize (zenon_H91 (v0)). zenon_intro zenon_H92. % 0.38/0.66 generalize (zenon_H92 (v50)). zenon_intro zenon_H93. % 0.38/0.66 apply (zenon_equiv_s _ _ zenon_H93); [ zenon_intro zenon_H96; zenon_intro zenon_H95 | zenon_intro zenon_H8e; zenon_intro zenon_H94 ]. % 0.38/0.66 exact (zenon_H96 zenon_H8e). % 0.38/0.66 apply (zenon_and_s _ _ zenon_H94). zenon_intro zenon_H98. zenon_intro zenon_H97. % 0.38/0.66 generalize (leq_def zenon_TZ_fo). zenon_intro zenon_H99. % 0.38/0.66 generalize (zenon_H99 (v50)). zenon_intro zenon_H9a. % 0.38/0.66 apply (zenon_equiv_s _ _ zenon_H9a); [ zenon_intro zenon_H9d; zenon_intro zenon_H9c | zenon_intro zenon_H97; zenon_intro zenon_H9b ]. % 0.38/0.66 exact (zenon_H9d zenon_H97). % 0.38/0.66 apply (zenon_or_s _ _ zenon_H9b); [ zenon_intro zenon_H9f | zenon_intro zenon_H9e ]. % 0.38/0.66 generalize (irreflexive zenon_TZ_fo). zenon_intro zenon_Ha0. % 0.38/0.66 apply (zenon_L15_ zenon_TZ_fo); trivial. % 0.38/0.66 elim (classic ((v100) = (v100))); [ zenon_intro zenon_Hd4 | zenon_intro zenon_H8d ]. % 0.38/0.66 cut (((v100) = (v100)) = ((v50) = (v100))). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Hd3. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_Hd4. % 0.38/0.66 cut (((v100) = (v100))); [idtac | apply NNPP; zenon_intro zenon_H8d]. % 0.38/0.66 cut (((v100) = (v50))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 0.38/0.66 congruence. % 0.38/0.66 cut (((v100) = zenon_TZ_fo) = ((v100) = (v50))). % 0.38/0.66 intro zenon_D_pnotp. % 0.38/0.66 apply zenon_Hd5. % 0.38/0.66 rewrite <- zenon_D_pnotp. % 0.38/0.66 exact zenon_Hce. % 0.38/0.66 cut ((zenon_TZ_fo = (v50))); [idtac | apply NNPP; zenon_intro zenon_Ha8]. % 0.38/0.66 cut (((v100) = (v100))); [idtac | apply NNPP; zenon_intro zenon_H8d]. % 0.38/0.66 congruence. % 0.38/0.66 apply zenon_H8d. apply refl_equal. % 0.38/0.66 exact (zenon_Ha8 zenon_H9e). % 0.38/0.66 apply zenon_H8d. apply refl_equal. % 0.38/0.66 apply zenon_H8d. apply refl_equal. % 0.38/0.66 (* end of lemma zenon_L16_ *) % 0.38/0.66 apply NNPP. intro zenon_G. % 0.38/0.66 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z))))))); [ zenon_intro zenon_H2e | zenon_intro zenon_Hd6 ]. % 0.38/0.66 apply (zenon_and_s _ _ distinct). zenon_intro zenon_Hd8. zenon_intro zenon_Hd7. % 0.38/0.66 apply (zenon_and_s _ _ zenon_Hd7). zenon_intro zenon_Hda. zenon_intro zenon_Hd9. % 0.38/0.66 apply (zenon_and_s _ _ zenon_Hd9). zenon_intro zenon_Hdc. zenon_intro zenon_Hdb. % 0.38/0.66 apply (zenon_and_s _ _ zenon_Hdb). zenon_intro zenon_Hde. zenon_intro zenon_Hdd. % 0.38/0.66 apply (zenon_and_s _ _ zenon_Hdd). zenon_intro zenon_Hd3. zenon_intro zenon_Hdf. % 0.38/0.66 apply (zenon_and_s _ _ zenon_Hdf). zenon_intro zenon_He1. zenon_intro zenon_He0. % 0.38/0.66 apply (zenon_and_s _ _ zenon_He0). zenon_intro zenon_He3. zenon_intro zenon_He2. % 0.38/0.66 apply (zenon_and_s _ _ zenon_He2). zenon_intro zenon_Hca. zenon_intro zenon_He4. % 0.38/0.66 apply (zenon_and_s _ _ zenon_He4). zenon_intro zenon_He5. zenon_intro zenon_Hc2. % 0.38/0.66 apply zenon_G. zenon_intro zenon_He6. % 0.38/0.66 elim zenon_He6. zenon_intro zenon_TX_bw. zenon_intro zenon_He7. % 0.38/0.66 elim zenon_He7. zenon_intro zenon_TY_ds. zenon_intro zenon_He8. % 0.38/0.66 elim zenon_He8. zenon_intro zenon_TZ_fo. zenon_intro zenon_He9. % 0.38/0.66 apply (zenon_and_s _ _ zenon_He9). zenon_intro zenon_Heb. zenon_intro zenon_Hea. % 0.38/0.66 apply (zenon_and_s _ _ zenon_Hea). zenon_intro zenon_Hed. zenon_intro zenon_Hec. % 0.38/0.66 apply (zenon_and_s _ _ zenon_Hec). zenon_intro zenon_Hef. zenon_intro zenon_Hee. % 0.38/0.66 generalize (leq_def (v400)). zenon_intro zenon_Hf0. % 0.38/0.66 generalize (zenon_Hf0 zenon_TX_bw). zenon_intro zenon_Hf1. % 0.38/0.66 apply (zenon_equiv_s _ _ zenon_Hf1); [ zenon_intro zenon_Hf4; zenon_intro zenon_Hf3 | zenon_intro zenon_Hed; zenon_intro zenon_Hf2 ]. % 0.38/0.66 exact (zenon_Hf4 zenon_Hed). % 0.38/0.66 generalize (leq_def (v200)). zenon_intro zenon_Hf5. % 0.38/0.66 generalize (zenon_Hf5 zenon_TY_ds). zenon_intro zenon_Hf6. % 0.38/0.66 apply (zenon_equiv_s _ _ zenon_Hf6); [ zenon_intro zenon_Hf9; zenon_intro zenon_Hf8 | zenon_intro zenon_Hef; zenon_intro zenon_Hf7 ]. % 0.38/0.66 exact (zenon_Hf9 zenon_Hef). % 0.38/0.66 generalize (leq_def (v100)). zenon_intro zenon_Hfa. % 0.38/0.66 generalize (zenon_Hfa zenon_TZ_fo). zenon_intro zenon_Hfb. % 0.38/0.66 apply (zenon_equiv_s _ _ zenon_Hfb); [ zenon_intro zenon_Hfe; zenon_intro zenon_Hfd | zenon_intro zenon_Hee; zenon_intro zenon_Hfc ]. % 0.38/0.66 exact (zenon_Hfe zenon_Hee). % 0.38/0.66 apply (zenon_or_s _ _ zenon_Hfc); [ zenon_intro zenon_H8f | zenon_intro zenon_Hce ]. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Hf7); [ zenon_intro zenon_H5f | zenon_intro zenon_Hc6 ]. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Hf2); [ zenon_intro zenon_H42 | zenon_intro zenon_Hbe ]. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Heb); [ zenon_intro zenon_H41 | zenon_intro zenon_Hff ]. % 0.38/0.66 apply (zenon_L3_ zenon_TX_bw); trivial. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Hff); [ zenon_intro zenon_H5e | zenon_intro zenon_H8e ]. % 0.38/0.66 apply (zenon_L5_ zenon_TY_ds); trivial. % 0.38/0.66 apply (zenon_L7_ zenon_TZ_fo); trivial. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Heb); [ zenon_intro zenon_H41 | zenon_intro zenon_Hff ]. % 0.38/0.66 apply (zenon_L10_ zenon_TX_bw); trivial. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Hff); [ zenon_intro zenon_H5e | zenon_intro zenon_H8e ]. % 0.38/0.66 apply (zenon_L5_ zenon_TY_ds); trivial. % 0.38/0.66 apply (zenon_L7_ zenon_TZ_fo); trivial. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Hf2); [ zenon_intro zenon_H42 | zenon_intro zenon_Hbe ]. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Heb); [ zenon_intro zenon_H41 | zenon_intro zenon_Hff ]. % 0.38/0.66 apply (zenon_L3_ zenon_TX_bw); trivial. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Hff); [ zenon_intro zenon_H5e | zenon_intro zenon_H8e ]. % 0.38/0.66 apply (zenon_L13_ zenon_TY_ds); trivial. % 0.38/0.66 apply (zenon_L7_ zenon_TZ_fo); trivial. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Heb); [ zenon_intro zenon_H41 | zenon_intro zenon_Hff ]. % 0.38/0.66 apply (zenon_L10_ zenon_TX_bw); trivial. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Hff); [ zenon_intro zenon_H5e | zenon_intro zenon_H8e ]. % 0.38/0.66 apply (zenon_L13_ zenon_TY_ds); trivial. % 0.38/0.66 apply (zenon_L7_ zenon_TZ_fo); trivial. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Hf7); [ zenon_intro zenon_H5f | zenon_intro zenon_Hc6 ]. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Hf2); [ zenon_intro zenon_H42 | zenon_intro zenon_Hbe ]. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Heb); [ zenon_intro zenon_H41 | zenon_intro zenon_Hff ]. % 0.38/0.66 apply (zenon_L3_ zenon_TX_bw); trivial. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Hff); [ zenon_intro zenon_H5e | zenon_intro zenon_H8e ]. % 0.38/0.66 apply (zenon_L5_ zenon_TY_ds); trivial. % 0.38/0.66 apply (zenon_L16_ zenon_TZ_fo); trivial. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Heb); [ zenon_intro zenon_H41 | zenon_intro zenon_Hff ]. % 0.38/0.66 apply (zenon_L10_ zenon_TX_bw); trivial. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Hff); [ zenon_intro zenon_H5e | zenon_intro zenon_H8e ]. % 0.38/0.66 apply (zenon_L5_ zenon_TY_ds); trivial. % 0.38/0.66 apply (zenon_L16_ zenon_TZ_fo); trivial. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Hf2); [ zenon_intro zenon_H42 | zenon_intro zenon_Hbe ]. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Heb); [ zenon_intro zenon_H41 | zenon_intro zenon_Hff ]. % 0.38/0.66 apply (zenon_L3_ zenon_TX_bw); trivial. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Hff); [ zenon_intro zenon_H5e | zenon_intro zenon_H8e ]. % 0.38/0.66 apply (zenon_L13_ zenon_TY_ds); trivial. % 0.38/0.66 apply (zenon_L16_ zenon_TZ_fo); trivial. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Heb); [ zenon_intro zenon_H41 | zenon_intro zenon_Hff ]. % 0.38/0.66 apply (zenon_L10_ zenon_TX_bw); trivial. % 0.38/0.66 apply (zenon_or_s _ _ zenon_Hff); [ zenon_intro zenon_H5e | zenon_intro zenon_H8e ]. % 0.38/0.66 apply (zenon_L13_ zenon_TY_ds); trivial. % 0.38/0.66 apply (zenon_L16_ zenon_TZ_fo); trivial. % 0.38/0.66 apply zenon_Hd6. zenon_intro zenon_Tx_jw. apply NNPP. zenon_intro zenon_H101. % 0.38/0.66 apply zenon_H101. zenon_intro zenon_Ty_jy. apply NNPP. zenon_intro zenon_H103. % 0.38/0.66 apply zenon_H103. zenon_intro zenon_Tz_ka. apply NNPP. zenon_intro zenon_H105. % 0.38/0.66 apply (zenon_notimply_s _ _ zenon_H105). zenon_intro zenon_H107. zenon_intro zenon_H106. % 0.38/0.66 apply (zenon_notimply_s _ _ zenon_H106). zenon_intro zenon_H109. zenon_intro zenon_H108. % 0.38/0.66 generalize (transitive zenon_Tx_jw). zenon_intro zenon_H10a. % 0.38/0.66 generalize (zenon_H10a zenon_Ty_jy). zenon_intro zenon_H10b. % 0.38/0.66 generalize (zenon_H10b zenon_Tz_ka). zenon_intro zenon_H10c. % 0.38/0.66 apply (zenon_imply_s _ _ zenon_H10c); [ zenon_intro zenon_H10e | zenon_intro zenon_H10d ]. % 0.38/0.66 apply (zenon_notand_s _ _ zenon_H10e); [ zenon_intro zenon_H110 | zenon_intro zenon_H10f ]. % 0.38/0.66 exact (zenon_H110 zenon_H107). % 0.38/0.66 exact (zenon_H10f zenon_H109). % 0.38/0.66 exact (zenon_H108 zenon_H10d). % 0.38/0.66 Qed. % 0.38/0.66 % SZS output end Proof % 0.38/0.66 (* END-PROOF *) % 0.38/0.66 nodes searched: 5711 % 0.38/0.66 max branch formulas: 316 % 0.38/0.66 proof nodes created: 369 % 0.38/0.66 formulas created: 7477 % 0.38/0.66 %------------------------------------------------------------------------------