%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SYN548+1 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 21 13:54:15 EDT 2022 % Result : Theorem 7.47s 7.69s % Output : Proof 7.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN548+1 : TPTP v8.1.0. Released v2.2.0. % 0.07/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n012.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jul 11 22:56:58 EDT 2022 % 0.13/0.34 % CPUTime : % 7.47/7.69 (* PROOF-FOUND *) % 7.47/7.69 % SZS status Theorem % 7.47/7.69 (* BEGIN-PROOF *) % 7.47/7.69 % SZS output start Proof % 7.47/7.69 Theorem prove_this : (exists X : zenon_U, ((reachable (initial_world) X)/\(forall Y : zenon_U, ((reachable X Y)->((forall Z : zenon_U, ((reachable Y Z)->((p Z)\/(forall V : zenon_U, ((reachable Z V)->(q V))))))<->((forall W : zenon_U, ((reachable Y W)->(p W)))\/(forall W : zenon_U, ((reachable Y W)->(q W))))))))). % 7.47/7.69 Proof. % 7.47/7.69 assert (zenon_L1_ : forall (zenon_TW_h : zenon_U) (zenon_TY_i : zenon_U), (reachable (initial_world) zenon_TY_i) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((reachable x y)->((reachable y z)->(reachable x z)))))) -> (~(reachable (initial_world) zenon_TW_h)) -> (reachable zenon_TY_i zenon_TW_h) -> False). % 7.47/7.69 do 2 intro. intros zenon_H3 zenon_H4 zenon_H5 zenon_H6. % 7.47/7.69 elim (classic ((~((initial_world) = zenon_TY_i))/\(~(reachable (initial_world) zenon_TY_i)))); [ zenon_intro zenon_H9 | zenon_intro zenon_Ha ]. % 7.47/7.69 apply (zenon_and_s _ _ zenon_H9). zenon_intro zenon_Hc. zenon_intro zenon_Hb. % 7.47/7.69 exact (zenon_Hb zenon_H3). % 7.47/7.69 cut ((reachable zenon_TY_i zenon_TW_h) = (reachable (initial_world) zenon_TW_h)). % 7.47/7.69 intro zenon_D_pnotp. % 7.47/7.69 apply zenon_H5. % 7.47/7.69 rewrite <- zenon_D_pnotp. % 7.47/7.69 exact zenon_H6. % 7.47/7.69 cut ((zenon_TW_h = zenon_TW_h)); [idtac | apply NNPP; zenon_intro zenon_Hd]. % 7.47/7.69 cut ((zenon_TY_i = (initial_world))); [idtac | apply NNPP; zenon_intro zenon_He]. % 7.47/7.69 congruence. % 7.47/7.69 apply (zenon_notand_s _ _ zenon_Ha); [ zenon_intro zenon_H10 | zenon_intro zenon_Hf ]. % 7.47/7.69 apply zenon_H10. zenon_intro zenon_H11. % 7.47/7.69 elim (classic ((initial_world) = (initial_world))); [ zenon_intro zenon_H12 | zenon_intro zenon_H13 ]. % 7.47/7.69 cut (((initial_world) = (initial_world)) = (zenon_TY_i = (initial_world))). % 7.47/7.69 intro zenon_D_pnotp. % 7.47/7.69 apply zenon_He. % 7.47/7.69 rewrite <- zenon_D_pnotp. % 7.47/7.69 exact zenon_H12. % 7.47/7.69 cut (((initial_world) = (initial_world))); [idtac | apply NNPP; zenon_intro zenon_H13]. % 7.47/7.69 cut (((initial_world) = zenon_TY_i)); [idtac | apply NNPP; zenon_intro zenon_Hc]. % 7.47/7.69 congruence. % 7.47/7.69 exact (zenon_Hc zenon_H11). % 7.47/7.69 apply zenon_H13. apply refl_equal. % 7.47/7.69 apply zenon_H13. apply refl_equal. % 7.47/7.69 apply zenon_Hf. zenon_intro zenon_H3. % 7.47/7.69 generalize (zenon_H4 (initial_world)). zenon_intro zenon_H14. % 7.47/7.69 generalize (zenon_H14 zenon_TY_i). zenon_intro zenon_H15. % 7.47/7.69 generalize (zenon_H15 zenon_TW_h). zenon_intro zenon_H16. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_H16); [ zenon_intro zenon_Hb | zenon_intro zenon_H17 ]. % 7.47/7.69 exact (zenon_Hb zenon_H3). % 7.47/7.69 apply (zenon_imply_s _ _ zenon_H17); [ zenon_intro zenon_H19 | zenon_intro zenon_H18 ]. % 7.47/7.69 exact (zenon_H19 zenon_H6). % 7.47/7.69 exact (zenon_H5 zenon_H18). % 7.47/7.69 apply zenon_Hd. apply refl_equal. % 7.47/7.69 (* end of lemma zenon_L1_ *) % 7.47/7.69 assert (zenon_L2_ : forall (zenon_TW_be : zenon_U) (zenon_TY_bf : zenon_U) (zenon_TW_bg : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((reachable x y)->((reachable y z)->(reachable x z)))))) -> (forall V : zenon_U, ((reachable zenon_TW_bg V)->(q V))) -> (reachable zenon_TY_bf zenon_TW_be) -> (reachable zenon_TW_bg zenon_TY_bf) -> (~(q zenon_TW_be)) -> False). % 7.47/7.69 do 3 intro. intros zenon_H4 zenon_H1a zenon_H1b zenon_H1c zenon_H1d. % 7.47/7.69 generalize (zenon_H1a zenon_TW_be). zenon_intro zenon_H21. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_H21); [ zenon_intro zenon_H23 | zenon_intro zenon_H22 ]. % 7.47/7.69 elim (classic ((~(zenon_TW_bg = zenon_TY_bf))/\(~(reachable zenon_TW_bg zenon_TY_bf)))); [ zenon_intro zenon_H24 | zenon_intro zenon_H25 ]. % 7.47/7.69 apply (zenon_and_s _ _ zenon_H24). zenon_intro zenon_H27. zenon_intro zenon_H26. % 7.47/7.69 exact (zenon_H26 zenon_H1c). % 7.47/7.69 cut ((reachable zenon_TY_bf zenon_TW_be) = (reachable zenon_TW_bg zenon_TW_be)). % 7.47/7.69 intro zenon_D_pnotp. % 7.47/7.69 apply zenon_H23. % 7.47/7.69 rewrite <- zenon_D_pnotp. % 7.47/7.69 exact zenon_H1b. % 7.47/7.69 cut ((zenon_TW_be = zenon_TW_be)); [idtac | apply NNPP; zenon_intro zenon_H28]. % 7.47/7.69 cut ((zenon_TY_bf = zenon_TW_bg)); [idtac | apply NNPP; zenon_intro zenon_H29]. % 7.47/7.69 congruence. % 7.47/7.69 apply (zenon_notand_s _ _ zenon_H25); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 7.47/7.69 apply zenon_H2b. zenon_intro zenon_H2c. % 7.47/7.69 elim (classic (zenon_TW_bg = zenon_TW_bg)); [ zenon_intro zenon_H2d | zenon_intro zenon_H2e ]. % 7.47/7.69 cut ((zenon_TW_bg = zenon_TW_bg) = (zenon_TY_bf = zenon_TW_bg)). % 7.47/7.69 intro zenon_D_pnotp. % 7.47/7.69 apply zenon_H29. % 7.47/7.69 rewrite <- zenon_D_pnotp. % 7.47/7.69 exact zenon_H2d. % 7.47/7.69 cut ((zenon_TW_bg = zenon_TW_bg)); [idtac | apply NNPP; zenon_intro zenon_H2e]. % 7.47/7.69 cut ((zenon_TW_bg = zenon_TY_bf)); [idtac | apply NNPP; zenon_intro zenon_H27]. % 7.47/7.69 congruence. % 7.47/7.69 exact (zenon_H27 zenon_H2c). % 7.47/7.69 apply zenon_H2e. apply refl_equal. % 7.47/7.69 apply zenon_H2e. apply refl_equal. % 7.47/7.69 apply zenon_H2a. zenon_intro zenon_H1c. % 7.47/7.69 generalize (zenon_H4 zenon_TW_bg). zenon_intro zenon_H2f. % 7.47/7.69 generalize (zenon_H2f zenon_TY_bf). zenon_intro zenon_H30. % 7.47/7.69 generalize (zenon_H30 zenon_TW_be). zenon_intro zenon_H31. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_H31); [ zenon_intro zenon_H26 | zenon_intro zenon_H32 ]. % 7.47/7.69 exact (zenon_H26 zenon_H1c). % 7.47/7.69 apply (zenon_imply_s _ _ zenon_H32); [ zenon_intro zenon_H34 | zenon_intro zenon_H33 ]. % 7.47/7.69 exact (zenon_H34 zenon_H1b). % 7.47/7.69 exact (zenon_H23 zenon_H33). % 7.47/7.69 apply zenon_H28. apply refl_equal. % 7.47/7.69 exact (zenon_H1d zenon_H22). % 7.47/7.69 (* end of lemma zenon_L2_ *) % 7.47/7.69 apply NNPP. intro zenon_G. % 7.47/7.69 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((reachable x y)->((reachable y z)->(reachable x z))))))); [ zenon_intro zenon_H4 | zenon_intro zenon_H35 ]. % 7.47/7.69 apply zenon_G. exists (initial_world). apply NNPP. zenon_intro zenon_H36. % 7.47/7.69 apply (zenon_notand_s _ _ zenon_H36); [ zenon_intro zenon_H38 | zenon_intro zenon_H37 ]. % 7.47/7.69 generalize (reflexivity_of_reachable (initial_world)). zenon_intro zenon_H39. % 7.47/7.69 exact (zenon_H38 zenon_H39). % 7.47/7.69 apply (zenon_notallex_s (fun Y : zenon_U => ((reachable (initial_world) Y)->((forall Z : zenon_U, ((reachable Y Z)->((p Z)\/(forall V : zenon_U, ((reachable Z V)->(q V))))))<->((forall W : zenon_U, ((reachable Y W)->(p W)))\/(forall W : zenon_U, ((reachable Y W)->(q W))))))) zenon_H37); [ zenon_intro zenon_H3a; idtac ]. % 7.47/7.69 elim zenon_H3a. zenon_intro zenon_TY_i. zenon_intro zenon_H3b. % 7.47/7.69 apply (zenon_notimply_s _ _ zenon_H3b). zenon_intro zenon_H3. zenon_intro zenon_H3c. % 7.47/7.69 apply (zenon_notequiv_s _ _ zenon_H3c); [ zenon_intro zenon_H40; zenon_intro zenon_H3f | zenon_intro zenon_H3e; zenon_intro zenon_H3d ]. % 7.47/7.69 apply (zenon_notallex_s (fun Z : zenon_U => ((reachable zenon_TY_i Z)->((p Z)\/(forall V : zenon_U, ((reachable Z V)->(q V)))))) zenon_H40); [ zenon_intro zenon_H41; idtac ]. % 7.47/7.69 elim zenon_H41. zenon_intro zenon_TZ_co. zenon_intro zenon_H43. % 7.47/7.69 apply (zenon_notimply_s _ _ zenon_H43). zenon_intro zenon_H45. zenon_intro zenon_H44. % 7.47/7.69 apply (zenon_notor_s _ _ zenon_H44). zenon_intro zenon_H47. zenon_intro zenon_H46. % 7.47/7.69 apply (zenon_notallex_s (fun V : zenon_U => ((reachable zenon_TZ_co V)->(q V))) zenon_H46); [ zenon_intro zenon_H48; idtac ]. % 7.47/7.69 elim zenon_H48. zenon_intro zenon_TV_cv. zenon_intro zenon_H4a. % 7.47/7.69 apply (zenon_notimply_s _ _ zenon_H4a). zenon_intro zenon_H4c. zenon_intro zenon_H4b. % 7.47/7.69 apply (zenon_or_s _ _ zenon_H3f); [ zenon_intro zenon_H4e | zenon_intro zenon_H4d ]. % 7.47/7.69 generalize (zenon_H4e zenon_TZ_co). zenon_intro zenon_H4f. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_H4f); [ zenon_intro zenon_H51 | zenon_intro zenon_H50 ]. % 7.47/7.69 exact (zenon_H51 zenon_H45). % 7.47/7.69 exact (zenon_H47 zenon_H50). % 7.47/7.69 generalize (zenon_H4d zenon_TV_cv). zenon_intro zenon_H52. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_H52); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 7.47/7.69 elim (classic ((~(zenon_TY_i = zenon_TZ_co))/\(~(reachable zenon_TY_i zenon_TZ_co)))); [ zenon_intro zenon_H55 | zenon_intro zenon_H56 ]. % 7.47/7.69 apply (zenon_and_s _ _ zenon_H55). zenon_intro zenon_H57. zenon_intro zenon_H51. % 7.47/7.69 exact (zenon_H51 zenon_H45). % 7.47/7.69 cut ((reachable zenon_TZ_co zenon_TV_cv) = (reachable zenon_TY_i zenon_TV_cv)). % 7.47/7.69 intro zenon_D_pnotp. % 7.47/7.69 apply zenon_H54. % 7.47/7.69 rewrite <- zenon_D_pnotp. % 7.47/7.69 exact zenon_H4c. % 7.47/7.69 cut ((zenon_TV_cv = zenon_TV_cv)); [idtac | apply NNPP; zenon_intro zenon_H58]. % 7.47/7.69 cut ((zenon_TZ_co = zenon_TY_i)); [idtac | apply NNPP; zenon_intro zenon_H59]. % 7.47/7.69 congruence. % 7.47/7.69 apply (zenon_notand_s _ _ zenon_H56); [ zenon_intro zenon_H5b | zenon_intro zenon_H5a ]. % 7.47/7.69 apply zenon_H5b. zenon_intro zenon_H5c. % 7.47/7.69 elim (classic (zenon_TY_i = zenon_TY_i)); [ zenon_intro zenon_H5d | zenon_intro zenon_H5e ]. % 7.47/7.69 cut ((zenon_TY_i = zenon_TY_i) = (zenon_TZ_co = zenon_TY_i)). % 7.47/7.69 intro zenon_D_pnotp. % 7.47/7.69 apply zenon_H59. % 7.47/7.69 rewrite <- zenon_D_pnotp. % 7.47/7.69 exact zenon_H5d. % 7.47/7.69 cut ((zenon_TY_i = zenon_TY_i)); [idtac | apply NNPP; zenon_intro zenon_H5e]. % 7.47/7.69 cut ((zenon_TY_i = zenon_TZ_co)); [idtac | apply NNPP; zenon_intro zenon_H57]. % 7.47/7.69 congruence. % 7.47/7.69 exact (zenon_H57 zenon_H5c). % 7.47/7.69 apply zenon_H5e. apply refl_equal. % 7.47/7.69 apply zenon_H5e. apply refl_equal. % 7.47/7.69 apply zenon_H5a. zenon_intro zenon_H45. % 7.47/7.69 generalize (zenon_H4 zenon_TY_i). zenon_intro zenon_H5f. % 7.47/7.69 generalize (zenon_H5f zenon_TZ_co). zenon_intro zenon_H60. % 7.47/7.69 generalize (zenon_H60 zenon_TV_cv). zenon_intro zenon_H61. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_H61); [ zenon_intro zenon_H51 | zenon_intro zenon_H62 ]. % 7.47/7.69 exact (zenon_H51 zenon_H45). % 7.47/7.69 apply (zenon_imply_s _ _ zenon_H62); [ zenon_intro zenon_H64 | zenon_intro zenon_H63 ]. % 7.47/7.69 exact (zenon_H64 zenon_H4c). % 7.47/7.69 exact (zenon_H54 zenon_H63). % 7.47/7.69 apply zenon_H58. apply refl_equal. % 7.47/7.69 exact (zenon_H4b zenon_H53). % 7.47/7.69 apply (zenon_notor_s _ _ zenon_H3d). zenon_intro zenon_H66. zenon_intro zenon_H65. % 7.47/7.69 apply (zenon_notallex_s (fun W : zenon_U => ((reachable zenon_TY_i W)->(q W))) zenon_H65); [ zenon_intro zenon_H67; idtac ]. % 7.47/7.69 elim zenon_H67. zenon_intro zenon_TW_h. zenon_intro zenon_H68. % 7.47/7.69 apply (zenon_notimply_s _ _ zenon_H68). zenon_intro zenon_H6. zenon_intro zenon_H69. % 7.47/7.69 apply zenon_G. exists zenon_TW_h. apply NNPP. zenon_intro zenon_H6a. % 7.47/7.69 apply (zenon_notand_s _ _ zenon_H6a); [ zenon_intro zenon_H5 | zenon_intro zenon_H6b ]. % 7.47/7.69 apply (zenon_L1_ zenon_TW_h zenon_TY_i); trivial. % 7.47/7.69 apply (zenon_notallex_s (fun Y : zenon_U => ((reachable zenon_TW_h Y)->((forall Z : zenon_U, ((reachable Y Z)->((p Z)\/(forall V : zenon_U, ((reachable Z V)->(q V))))))<->((forall W : zenon_U, ((reachable Y W)->(p W)))\/(forall W : zenon_U, ((reachable Y W)->(q W))))))) zenon_H6b); [ zenon_intro zenon_H6c; idtac ]. % 7.47/7.69 elim zenon_H6c. zenon_intro zenon_TY_ef. zenon_intro zenon_H6e. % 7.47/7.69 apply (zenon_notimply_s _ _ zenon_H6e). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 7.47/7.69 apply (zenon_notequiv_s _ _ zenon_H6f); [ zenon_intro zenon_H74; zenon_intro zenon_H73 | zenon_intro zenon_H72; zenon_intro zenon_H71 ]. % 7.47/7.69 apply (zenon_notallex_s (fun Z : zenon_U => ((reachable zenon_TY_ef Z)->((p Z)\/(forall V : zenon_U, ((reachable Z V)->(q V)))))) zenon_H74); [ zenon_intro zenon_H75; idtac ]. % 7.47/7.69 elim zenon_H75. zenon_intro zenon_TZ_eo. zenon_intro zenon_H77. % 7.47/7.69 apply (zenon_notimply_s _ _ zenon_H77). zenon_intro zenon_H79. zenon_intro zenon_H78. % 7.47/7.69 apply (zenon_notor_s _ _ zenon_H78). zenon_intro zenon_H7b. zenon_intro zenon_H7a. % 7.47/7.69 apply (zenon_notallex_s (fun V : zenon_U => ((reachable zenon_TZ_eo V)->(q V))) zenon_H7a); [ zenon_intro zenon_H7c; idtac ]. % 7.47/7.69 elim zenon_H7c. zenon_intro zenon_TV_ev. zenon_intro zenon_H7e. % 7.47/7.69 apply (zenon_notimply_s _ _ zenon_H7e). zenon_intro zenon_H80. zenon_intro zenon_H7f. % 7.47/7.69 apply (zenon_or_s _ _ zenon_H73); [ zenon_intro zenon_H82 | zenon_intro zenon_H81 ]. % 7.47/7.69 generalize (zenon_H82 zenon_TZ_eo). zenon_intro zenon_H83. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_H83); [ zenon_intro zenon_H85 | zenon_intro zenon_H84 ]. % 7.47/7.69 exact (zenon_H85 zenon_H79). % 7.47/7.69 exact (zenon_H7b zenon_H84). % 7.47/7.69 generalize (zenon_H81 zenon_TV_ev). zenon_intro zenon_H86. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_H86); [ zenon_intro zenon_H88 | zenon_intro zenon_H87 ]. % 7.47/7.69 elim (classic ((~(zenon_TY_ef = zenon_TZ_eo))/\(~(reachable zenon_TY_ef zenon_TZ_eo)))); [ zenon_intro zenon_H89 | zenon_intro zenon_H8a ]. % 7.47/7.69 apply (zenon_and_s _ _ zenon_H89). zenon_intro zenon_H8b. zenon_intro zenon_H85. % 7.47/7.69 exact (zenon_H85 zenon_H79). % 7.47/7.69 cut ((reachable zenon_TZ_eo zenon_TV_ev) = (reachable zenon_TY_ef zenon_TV_ev)). % 7.47/7.69 intro zenon_D_pnotp. % 7.47/7.69 apply zenon_H88. % 7.47/7.69 rewrite <- zenon_D_pnotp. % 7.47/7.69 exact zenon_H80. % 7.47/7.69 cut ((zenon_TV_ev = zenon_TV_ev)); [idtac | apply NNPP; zenon_intro zenon_H8c]. % 7.47/7.69 cut ((zenon_TZ_eo = zenon_TY_ef)); [idtac | apply NNPP; zenon_intro zenon_H8d]. % 7.47/7.69 congruence. % 7.47/7.69 apply (zenon_notand_s _ _ zenon_H8a); [ zenon_intro zenon_H8f | zenon_intro zenon_H8e ]. % 7.47/7.69 apply zenon_H8f. zenon_intro zenon_H90. % 7.47/7.69 elim (classic (zenon_TY_ef = zenon_TY_ef)); [ zenon_intro zenon_H91 | zenon_intro zenon_H92 ]. % 7.47/7.69 cut ((zenon_TY_ef = zenon_TY_ef) = (zenon_TZ_eo = zenon_TY_ef)). % 7.47/7.69 intro zenon_D_pnotp. % 7.47/7.69 apply zenon_H8d. % 7.47/7.69 rewrite <- zenon_D_pnotp. % 7.47/7.69 exact zenon_H91. % 7.47/7.69 cut ((zenon_TY_ef = zenon_TY_ef)); [idtac | apply NNPP; zenon_intro zenon_H92]. % 7.47/7.69 cut ((zenon_TY_ef = zenon_TZ_eo)); [idtac | apply NNPP; zenon_intro zenon_H8b]. % 7.47/7.69 congruence. % 7.47/7.69 exact (zenon_H8b zenon_H90). % 7.47/7.69 apply zenon_H92. apply refl_equal. % 7.47/7.69 apply zenon_H92. apply refl_equal. % 7.47/7.69 apply zenon_H8e. zenon_intro zenon_H79. % 7.47/7.69 generalize (zenon_H4 zenon_TY_ef). zenon_intro zenon_H93. % 7.47/7.69 generalize (zenon_H93 zenon_TZ_eo). zenon_intro zenon_H94. % 7.47/7.69 generalize (zenon_H94 zenon_TV_ev). zenon_intro zenon_H95. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_H95); [ zenon_intro zenon_H85 | zenon_intro zenon_H96 ]. % 7.47/7.69 exact (zenon_H85 zenon_H79). % 7.47/7.69 apply (zenon_imply_s _ _ zenon_H96); [ zenon_intro zenon_H98 | zenon_intro zenon_H97 ]. % 7.47/7.69 exact (zenon_H98 zenon_H80). % 7.47/7.69 exact (zenon_H88 zenon_H97). % 7.47/7.69 apply zenon_H8c. apply refl_equal. % 7.47/7.69 exact (zenon_H7f zenon_H87). % 7.47/7.69 apply (zenon_notor_s _ _ zenon_H71). zenon_intro zenon_H9a. zenon_intro zenon_H99. % 7.47/7.69 apply (zenon_notallex_s (fun W : zenon_U => ((reachable zenon_TY_ef W)->(p W))) zenon_H9a); [ zenon_intro zenon_H9b; idtac ]. % 7.47/7.69 elim zenon_H9b. zenon_intro zenon_TW_bg. zenon_intro zenon_H9c. % 7.47/7.69 apply (zenon_notimply_s _ _ zenon_H9c). zenon_intro zenon_H9e. zenon_intro zenon_H9d. % 7.47/7.69 apply zenon_G. exists zenon_TW_bg. apply NNPP. zenon_intro zenon_H9f. % 7.47/7.69 apply (zenon_notand_s _ _ zenon_H9f); [ zenon_intro zenon_Ha1 | zenon_intro zenon_Ha0 ]. % 7.47/7.69 elim (classic ((~((initial_world) = zenon_TY_ef))/\(~(reachable (initial_world) zenon_TY_ef)))); [ zenon_intro zenon_Ha2 | zenon_intro zenon_Ha3 ]. % 7.47/7.69 apply (zenon_and_s _ _ zenon_Ha2). zenon_intro zenon_Ha5. zenon_intro zenon_Ha4. % 7.47/7.69 elim (classic ((~((initial_world) = zenon_TW_h))/\(~(reachable (initial_world) zenon_TW_h)))); [ zenon_intro zenon_Ha6 | zenon_intro zenon_Ha7 ]. % 7.47/7.69 apply (zenon_and_s _ _ zenon_Ha6). zenon_intro zenon_Ha8. zenon_intro zenon_H5. % 7.47/7.69 apply (zenon_L1_ zenon_TW_h zenon_TY_i); trivial. % 7.47/7.69 cut ((reachable zenon_TW_h zenon_TY_ef) = (reachable (initial_world) zenon_TY_ef)). % 7.47/7.69 intro zenon_D_pnotp. % 7.47/7.69 apply zenon_Ha4. % 7.47/7.69 rewrite <- zenon_D_pnotp. % 7.47/7.69 exact zenon_H70. % 7.47/7.69 cut ((zenon_TY_ef = zenon_TY_ef)); [idtac | apply NNPP; zenon_intro zenon_H92]. % 7.47/7.69 cut ((zenon_TW_h = (initial_world))); [idtac | apply NNPP; zenon_intro zenon_Ha9]. % 7.47/7.69 congruence. % 7.47/7.69 apply (zenon_notand_s _ _ zenon_Ha7); [ zenon_intro zenon_Hab | zenon_intro zenon_Haa ]. % 7.47/7.69 apply zenon_Hab. zenon_intro zenon_Hac. % 7.47/7.69 elim (classic ((initial_world) = (initial_world))); [ zenon_intro zenon_H12 | zenon_intro zenon_H13 ]. % 7.47/7.69 cut (((initial_world) = (initial_world)) = (zenon_TW_h = (initial_world))). % 7.47/7.69 intro zenon_D_pnotp. % 7.47/7.69 apply zenon_Ha9. % 7.47/7.69 rewrite <- zenon_D_pnotp. % 7.47/7.69 exact zenon_H12. % 7.47/7.69 cut (((initial_world) = (initial_world))); [idtac | apply NNPP; zenon_intro zenon_H13]. % 7.47/7.69 cut (((initial_world) = zenon_TW_h)); [idtac | apply NNPP; zenon_intro zenon_Ha8]. % 7.47/7.69 congruence. % 7.47/7.69 exact (zenon_Ha8 zenon_Hac). % 7.47/7.69 apply zenon_H13. apply refl_equal. % 7.47/7.69 apply zenon_H13. apply refl_equal. % 7.47/7.69 apply zenon_Haa. zenon_intro zenon_H18. % 7.47/7.69 generalize (zenon_H4 (initial_world)). zenon_intro zenon_H14. % 7.47/7.69 generalize (zenon_H14 zenon_TW_h). zenon_intro zenon_Had. % 7.47/7.69 generalize (zenon_Had zenon_TY_ef). zenon_intro zenon_Hae. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_Hae); [ zenon_intro zenon_H5 | zenon_intro zenon_Haf ]. % 7.47/7.69 exact (zenon_H5 zenon_H18). % 7.47/7.69 apply (zenon_imply_s _ _ zenon_Haf); [ zenon_intro zenon_Hb1 | zenon_intro zenon_Hb0 ]. % 7.47/7.69 exact (zenon_Hb1 zenon_H70). % 7.47/7.69 exact (zenon_Ha4 zenon_Hb0). % 7.47/7.69 apply zenon_H92. apply refl_equal. % 7.47/7.69 cut ((reachable zenon_TY_ef zenon_TW_bg) = (reachable (initial_world) zenon_TW_bg)). % 7.47/7.69 intro zenon_D_pnotp. % 7.47/7.69 apply zenon_Ha1. % 7.47/7.69 rewrite <- zenon_D_pnotp. % 7.47/7.69 exact zenon_H9e. % 7.47/7.69 cut ((zenon_TW_bg = zenon_TW_bg)); [idtac | apply NNPP; zenon_intro zenon_H2e]. % 7.47/7.69 cut ((zenon_TY_ef = (initial_world))); [idtac | apply NNPP; zenon_intro zenon_Hb2]. % 7.47/7.69 congruence. % 7.47/7.69 apply (zenon_notand_s _ _ zenon_Ha3); [ zenon_intro zenon_Hb4 | zenon_intro zenon_Hb3 ]. % 7.47/7.69 apply zenon_Hb4. zenon_intro zenon_Hb5. % 7.47/7.69 elim (classic ((initial_world) = (initial_world))); [ zenon_intro zenon_H12 | zenon_intro zenon_H13 ]. % 7.47/7.69 cut (((initial_world) = (initial_world)) = (zenon_TY_ef = (initial_world))). % 7.47/7.69 intro zenon_D_pnotp. % 7.47/7.69 apply zenon_Hb2. % 7.47/7.69 rewrite <- zenon_D_pnotp. % 7.47/7.69 exact zenon_H12. % 7.47/7.69 cut (((initial_world) = (initial_world))); [idtac | apply NNPP; zenon_intro zenon_H13]. % 7.47/7.69 cut (((initial_world) = zenon_TY_ef)); [idtac | apply NNPP; zenon_intro zenon_Ha5]. % 7.47/7.69 congruence. % 7.47/7.69 exact (zenon_Ha5 zenon_Hb5). % 7.47/7.69 apply zenon_H13. apply refl_equal. % 7.47/7.69 apply zenon_H13. apply refl_equal. % 7.47/7.69 apply zenon_Hb3. zenon_intro zenon_Hb0. % 7.47/7.69 generalize (zenon_H4 (initial_world)). zenon_intro zenon_H14. % 7.47/7.69 generalize (zenon_H14 zenon_TY_ef). zenon_intro zenon_Hb6. % 7.47/7.69 generalize (zenon_Hb6 zenon_TW_bg). zenon_intro zenon_Hb7. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_Hb7); [ zenon_intro zenon_Ha4 | zenon_intro zenon_Hb8 ]. % 7.47/7.69 exact (zenon_Ha4 zenon_Hb0). % 7.47/7.69 apply (zenon_imply_s _ _ zenon_Hb8); [ zenon_intro zenon_Hba | zenon_intro zenon_Hb9 ]. % 7.47/7.69 exact (zenon_Hba zenon_H9e). % 7.47/7.69 exact (zenon_Ha1 zenon_Hb9). % 7.47/7.69 apply zenon_H2e. apply refl_equal. % 7.47/7.69 apply (zenon_notallex_s (fun Y : zenon_U => ((reachable zenon_TW_bg Y)->((forall Z : zenon_U, ((reachable Y Z)->((p Z)\/(forall V : zenon_U, ((reachable Z V)->(q V))))))<->((forall W : zenon_U, ((reachable Y W)->(p W)))\/(forall W : zenon_U, ((reachable Y W)->(q W))))))) zenon_Ha0); [ zenon_intro zenon_Hbb; idtac ]. % 7.47/7.69 elim zenon_Hbb. zenon_intro zenon_TY_bf. zenon_intro zenon_Hbc. % 7.47/7.69 apply (zenon_notimply_s _ _ zenon_Hbc). zenon_intro zenon_H1c. zenon_intro zenon_Hbd. % 7.47/7.69 apply (zenon_notequiv_s _ _ zenon_Hbd); [ zenon_intro zenon_Hc1; zenon_intro zenon_Hc0 | zenon_intro zenon_Hbf; zenon_intro zenon_Hbe ]. % 7.47/7.69 apply (zenon_notallex_s (fun Z : zenon_U => ((reachable zenon_TY_bf Z)->((p Z)\/(forall V : zenon_U, ((reachable Z V)->(q V)))))) zenon_Hc1); [ zenon_intro zenon_Hc2; idtac ]. % 7.47/7.69 elim zenon_Hc2. zenon_intro zenon_TZ_hn. zenon_intro zenon_Hc4. % 7.47/7.69 apply (zenon_notimply_s _ _ zenon_Hc4). zenon_intro zenon_Hc6. zenon_intro zenon_Hc5. % 7.47/7.69 apply (zenon_notor_s _ _ zenon_Hc5). zenon_intro zenon_Hc8. zenon_intro zenon_Hc7. % 7.47/7.69 apply (zenon_notallex_s (fun V : zenon_U => ((reachable zenon_TZ_hn V)->(q V))) zenon_Hc7); [ zenon_intro zenon_Hc9; idtac ]. % 7.47/7.69 elim zenon_Hc9. zenon_intro zenon_TV_hu. zenon_intro zenon_Hcb. % 7.47/7.69 apply (zenon_notimply_s _ _ zenon_Hcb). zenon_intro zenon_Hcd. zenon_intro zenon_Hcc. % 7.47/7.69 apply (zenon_or_s _ _ zenon_Hc0); [ zenon_intro zenon_Hcf | zenon_intro zenon_Hce ]. % 7.47/7.69 generalize (zenon_Hcf zenon_TZ_hn). zenon_intro zenon_Hd0. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_Hd0); [ zenon_intro zenon_Hd2 | zenon_intro zenon_Hd1 ]. % 7.47/7.69 exact (zenon_Hd2 zenon_Hc6). % 7.47/7.69 exact (zenon_Hc8 zenon_Hd1). % 7.47/7.69 generalize (zenon_Hce zenon_TV_hu). zenon_intro zenon_Hd3. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_Hd3); [ zenon_intro zenon_Hd5 | zenon_intro zenon_Hd4 ]. % 7.47/7.69 elim (classic ((~(zenon_TY_bf = zenon_TZ_hn))/\(~(reachable zenon_TY_bf zenon_TZ_hn)))); [ zenon_intro zenon_Hd6 | zenon_intro zenon_Hd7 ]. % 7.47/7.69 apply (zenon_and_s _ _ zenon_Hd6). zenon_intro zenon_Hd8. zenon_intro zenon_Hd2. % 7.47/7.69 exact (zenon_Hd2 zenon_Hc6). % 7.47/7.69 cut ((reachable zenon_TZ_hn zenon_TV_hu) = (reachable zenon_TY_bf zenon_TV_hu)). % 7.47/7.69 intro zenon_D_pnotp. % 7.47/7.69 apply zenon_Hd5. % 7.47/7.69 rewrite <- zenon_D_pnotp. % 7.47/7.69 exact zenon_Hcd. % 7.47/7.69 cut ((zenon_TV_hu = zenon_TV_hu)); [idtac | apply NNPP; zenon_intro zenon_Hd9]. % 7.47/7.69 cut ((zenon_TZ_hn = zenon_TY_bf)); [idtac | apply NNPP; zenon_intro zenon_Hda]. % 7.47/7.69 congruence. % 7.47/7.69 apply (zenon_notand_s _ _ zenon_Hd7); [ zenon_intro zenon_Hdc | zenon_intro zenon_Hdb ]. % 7.47/7.69 apply zenon_Hdc. zenon_intro zenon_Hdd. % 7.47/7.69 elim (classic (zenon_TY_bf = zenon_TY_bf)); [ zenon_intro zenon_Hde | zenon_intro zenon_Hdf ]. % 7.47/7.69 cut ((zenon_TY_bf = zenon_TY_bf) = (zenon_TZ_hn = zenon_TY_bf)). % 7.47/7.69 intro zenon_D_pnotp. % 7.47/7.69 apply zenon_Hda. % 7.47/7.69 rewrite <- zenon_D_pnotp. % 7.47/7.69 exact zenon_Hde. % 7.47/7.69 cut ((zenon_TY_bf = zenon_TY_bf)); [idtac | apply NNPP; zenon_intro zenon_Hdf]. % 7.47/7.69 cut ((zenon_TY_bf = zenon_TZ_hn)); [idtac | apply NNPP; zenon_intro zenon_Hd8]. % 7.47/7.69 congruence. % 7.47/7.69 exact (zenon_Hd8 zenon_Hdd). % 7.47/7.69 apply zenon_Hdf. apply refl_equal. % 7.47/7.69 apply zenon_Hdf. apply refl_equal. % 7.47/7.69 apply zenon_Hdb. zenon_intro zenon_Hc6. % 7.47/7.69 generalize (zenon_H4 zenon_TY_bf). zenon_intro zenon_He0. % 7.47/7.69 generalize (zenon_He0 zenon_TZ_hn). zenon_intro zenon_He1. % 7.47/7.69 generalize (zenon_He1 zenon_TV_hu). zenon_intro zenon_He2. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_He2); [ zenon_intro zenon_Hd2 | zenon_intro zenon_He3 ]. % 7.47/7.69 exact (zenon_Hd2 zenon_Hc6). % 7.47/7.69 apply (zenon_imply_s _ _ zenon_He3); [ zenon_intro zenon_He5 | zenon_intro zenon_He4 ]. % 7.47/7.69 exact (zenon_He5 zenon_Hcd). % 7.47/7.69 exact (zenon_Hd5 zenon_He4). % 7.47/7.69 apply zenon_Hd9. apply refl_equal. % 7.47/7.69 exact (zenon_Hcc zenon_Hd4). % 7.47/7.69 apply (zenon_notor_s _ _ zenon_Hbe). zenon_intro zenon_He7. zenon_intro zenon_He6. % 7.47/7.69 apply (zenon_notallex_s (fun W : zenon_U => ((reachable zenon_TY_bf W)->(q W))) zenon_He6); [ zenon_intro zenon_He8; idtac ]. % 7.47/7.69 elim zenon_He8. zenon_intro zenon_TW_be. zenon_intro zenon_He9. % 7.47/7.69 apply (zenon_notimply_s _ _ zenon_He9). zenon_intro zenon_H1b. zenon_intro zenon_H1d. % 7.47/7.69 generalize (zenon_H72 zenon_TW_bg). zenon_intro zenon_Hea. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_Hea); [ zenon_intro zenon_Hba | zenon_intro zenon_Heb ]. % 7.47/7.69 exact (zenon_Hba zenon_H9e). % 7.47/7.69 apply (zenon_or_s _ _ zenon_Heb); [ zenon_intro zenon_Hec | zenon_intro zenon_H1a ]. % 7.47/7.69 exact (zenon_H9d zenon_Hec). % 7.47/7.69 apply (zenon_L2_ zenon_TW_be zenon_TY_bf zenon_TW_bg); trivial. % 7.47/7.69 apply zenon_H35. zenon_intro zenon_Tx_jd. apply NNPP. zenon_intro zenon_Hee. % 7.47/7.69 apply zenon_Hee. zenon_intro zenon_Ty_jf. apply NNPP. zenon_intro zenon_Hf0. % 7.47/7.69 apply zenon_Hf0. zenon_intro zenon_Tz_jh. apply NNPP. zenon_intro zenon_Hf2. % 7.47/7.69 apply (zenon_notimply_s _ _ zenon_Hf2). zenon_intro zenon_Hf4. zenon_intro zenon_Hf3. % 7.47/7.69 apply (zenon_notimply_s _ _ zenon_Hf3). zenon_intro zenon_Hf6. zenon_intro zenon_Hf5. % 7.47/7.69 generalize (transitivity_of_reachable zenon_Tx_jd). zenon_intro zenon_Hf7. % 7.47/7.69 generalize (zenon_Hf7 zenon_Ty_jf). zenon_intro zenon_Hf8. % 7.47/7.69 generalize (zenon_Hf8 zenon_Tz_jh). zenon_intro zenon_Hf9. % 7.47/7.69 apply (zenon_imply_s _ _ zenon_Hf9); [ zenon_intro zenon_Hfb | zenon_intro zenon_Hfa ]. % 7.47/7.69 apply (zenon_notand_s _ _ zenon_Hfb); [ zenon_intro zenon_Hfd | zenon_intro zenon_Hfc ]. % 7.47/7.69 exact (zenon_Hfd zenon_Hf4). % 7.47/7.69 exact (zenon_Hfc zenon_Hf6). % 7.47/7.69 exact (zenon_Hf5 zenon_Hfa). % 7.47/7.69 Qed. % 7.47/7.69 % SZS output end Proof % 7.47/7.69 (* END-PROOF *) % 7.47/7.69 nodes searched: 80030 % 7.47/7.69 max branch formulas: 12854 % 7.47/7.69 proof nodes created: 8137 % 7.47/7.69 formulas created: 269800 % 7.47/7.69 %------------------------------------------------------------------------------