%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWV208+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n009.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 : Wed Jul 20 23:03:19 EDT 2022 % Result : Theorem 6.67s 6.88s % Output : Proof 6.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV208+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.07/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n009.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Wed Jun 15 16:35:53 EDT 2022 % 0.12/0.33 % CPUTime : % 6.67/6.88 (* PROOF-FOUND *) % 6.67/6.88 % SZS status Theorem % 6.67/6.88 (* BEGIN-PROOF *) % 6.67/6.88 % SZS output start Proof % 6.67/6.88 Theorem quaternion_ds1_inuse_0019 : ((((a_select2 (rho_defuse) (n0)) = (use))/\(((a_select2 (rho_defuse) (n1)) = (use))/\(((a_select2 (rho_defuse) (n2)) = (use))/\(((a_select2 (sigma_defuse) (n0)) = (use))/\(((a_select2 (sigma_defuse) (n1)) = (use))/\(((a_select2 (sigma_defuse) (n2)) = (use))/\(((a_select2 (sigma_defuse) (n3)) = (use))/\(((a_select2 (sigma_defuse) (n4)) = (use))/\(((a_select2 (sigma_defuse) (n5)) = (use))/\(((a_select3 (u_defuse) (n0) (n0)) = (use))/\(((a_select3 (u_defuse) (n1) (n0)) = (use))/\(((a_select3 (u_defuse) (n2) (n0)) = (use))/\(((a_select2 (xinit_defuse) (n3)) = (use))/\(((a_select2 (xinit_defuse) (n4)) = (use))/\(((a_select2 (xinit_defuse) (n5)) = (use))/\(((a_select2 (xinit_mean_defuse) (n0)) = (use))/\(((a_select2 (xinit_mean_defuse) (n1)) = (use))/\(((a_select2 (xinit_mean_defuse) (n2)) = (use))/\(((a_select2 (xinit_mean_defuse) (n3)) = (use))/\(((a_select2 (xinit_mean_defuse) (n4)) = (use))/\(((a_select2 (xinit_mean_defuse) (n5)) = (use))/\(((a_select2 (xinit_noise_defuse) (n0)) = (use))/\(((a_select2 (xinit_noise_defuse) (n1)) = (use))/\(((a_select2 (xinit_noise_defuse) (n2)) = (use))/\(((a_select2 (xinit_noise_defuse) (n3)) = (use))/\(((a_select2 (xinit_noise_defuse) (n4)) = (use))/\(((a_select2 (xinit_noise_defuse) (n5)) = (use))/\((forall A : zenon_U, (forall B : zenon_U, (((leq (n0) A)/\((leq (n0) B)/\((leq A (n2))/\(leq B (n998)))))->((a_select3 (u_defuse) A B) = (use)))))/\(forall C : zenon_U, (forall D : zenon_U, (((leq (n0) C)/\((leq (n0) D)/\((leq C (n2))/\(leq D (n998)))))->((a_select3 (z_defuse) C D) = (use)))))))))))))))))))))))))))))))))->(forall E : zenon_U, (((leq (n0) E)/\(leq E (n5)))->((a_select2 (xinit_mean_defuse) E) = (use))))). % 6.67/6.88 Proof. % 6.67/6.88 assert (zenon_L1_ : forall (zenon_TE_dq : zenon_U), (gt (succ zenon_TE_dq) (n0)) -> (~(leq (n0) zenon_TE_dq)) -> False). % 6.67/6.88 do 1 intro. intros zenon_H5c zenon_H5d. % 6.67/6.88 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H5f. % 6.67/6.88 generalize (zenon_H5f zenon_TE_dq). zenon_intro zenon_H60. % 6.67/6.88 apply (zenon_equiv_s _ _ zenon_H60); [ zenon_intro zenon_H5d; zenon_intro zenon_H62 | zenon_intro zenon_H61; zenon_intro zenon_H5c ]. % 6.67/6.88 exact (zenon_H62 zenon_H5c). % 6.67/6.88 exact (zenon_H5d zenon_H61). % 6.67/6.88 (* end of lemma zenon_L1_ *) % 6.67/6.88 assert (zenon_L2_ : (~((n4) = (n4))) -> False). % 6.67/6.88 do 0 intro. intros zenon_H63. % 6.67/6.88 apply zenon_H63. apply refl_equal. % 6.67/6.88 (* end of lemma zenon_L2_ *) % 6.67/6.88 assert (zenon_L3_ : (~((n3) = (n3))) -> False). % 6.67/6.88 do 0 intro. intros zenon_H64. % 6.67/6.88 apply zenon_H64. apply refl_equal. % 6.67/6.88 (* end of lemma zenon_L3_ *) % 6.67/6.88 assert (zenon_L4_ : (~((n2) = (n2))) -> False). % 6.67/6.88 do 0 intro. intros zenon_H65. % 6.67/6.88 apply zenon_H65. apply refl_equal. % 6.67/6.88 (* end of lemma zenon_L4_ *) % 6.67/6.88 assert (zenon_L5_ : (~((xinit_mean_defuse) = (xinit_mean_defuse))) -> False). % 6.67/6.88 do 0 intro. intros zenon_H66. % 6.67/6.88 apply zenon_H66. apply refl_equal. % 6.67/6.88 (* end of lemma zenon_L5_ *) % 6.67/6.88 assert (zenon_L6_ : forall (zenon_TE_dq : zenon_U), (gt (succ (n5)) zenon_TE_dq) -> (~(leq zenon_TE_dq (n5))) -> False). % 6.67/6.88 do 1 intro. intros zenon_H67 zenon_H68. % 6.67/6.88 generalize (leq_succ_gt_equiv zenon_TE_dq). zenon_intro zenon_H69. % 6.67/6.88 generalize (zenon_H69 (n5)). zenon_intro zenon_H6a. % 6.67/6.88 apply (zenon_equiv_s _ _ zenon_H6a); [ zenon_intro zenon_H68; zenon_intro zenon_H6c | zenon_intro zenon_H6b; zenon_intro zenon_H67 ]. % 6.67/6.88 exact (zenon_H6c zenon_H67). % 6.67/6.88 exact (zenon_H68 zenon_H6b). % 6.67/6.88 (* end of lemma zenon_L6_ *) % 6.67/6.88 assert (zenon_L7_ : forall (zenon_TE_dq : zenon_U), (gt (succ zenon_TE_dq) (n0)) -> (gt (succ (n5)) zenon_TE_dq) -> (~((n0) = zenon_TE_dq)) -> (~((n1) = zenon_TE_dq)) -> (~((n2) = zenon_TE_dq)) -> (~((n3) = zenon_TE_dq)) -> (~(zenon_TE_dq = (n4))) -> (~(zenon_TE_dq = (n5))) -> False). % 6.67/6.88 do 1 intro. intros zenon_H5c zenon_H67 zenon_H6d zenon_H6e zenon_H6f zenon_H70 zenon_H71 zenon_H72. % 6.67/6.88 generalize (finite_domain_5 zenon_TE_dq). zenon_intro zenon_H73. % 6.67/6.88 apply (zenon_imply_s _ _ zenon_H73); [ zenon_intro zenon_H75 | zenon_intro zenon_H74 ]. % 6.67/6.88 apply (zenon_notand_s _ _ zenon_H75); [ zenon_intro zenon_H5d | zenon_intro zenon_H68 ]. % 6.67/6.88 apply (zenon_L1_ zenon_TE_dq); trivial. % 6.67/6.88 apply (zenon_L6_ zenon_TE_dq); trivial. % 6.67/6.88 apply (zenon_or_s _ _ zenon_H74); [ zenon_intro zenon_H77 | zenon_intro zenon_H76 ]. % 6.67/6.88 apply zenon_H6d. apply sym_equal. exact zenon_H77. % 6.67/6.88 apply (zenon_or_s _ _ zenon_H76); [ zenon_intro zenon_H79 | zenon_intro zenon_H78 ]. % 6.67/6.88 apply zenon_H6e. apply sym_equal. exact zenon_H79. % 6.67/6.88 apply (zenon_or_s _ _ zenon_H78); [ zenon_intro zenon_H7b | zenon_intro zenon_H7a ]. % 6.67/6.88 apply zenon_H6f. apply sym_equal. exact zenon_H7b. % 6.67/6.88 apply (zenon_or_s _ _ zenon_H7a); [ zenon_intro zenon_H7d | zenon_intro zenon_H7c ]. % 6.67/6.88 apply zenon_H70. apply sym_equal. exact zenon_H7d. % 6.67/6.88 apply (zenon_or_s _ _ zenon_H7c); [ zenon_intro zenon_H7f | zenon_intro zenon_H7e ]. % 6.67/6.88 exact (zenon_H71 zenon_H7f). % 6.67/6.88 exact (zenon_H72 zenon_H7e). % 6.67/6.88 (* end of lemma zenon_L7_ *) % 6.67/6.88 assert (zenon_L8_ : forall (zenon_TE_dq : zenon_U), (~((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) (n4)))) -> (~(zenon_TE_dq = (n5))) -> (~((n3) = zenon_TE_dq)) -> (~((n2) = zenon_TE_dq)) -> (~((n1) = zenon_TE_dq)) -> (~((n0) = zenon_TE_dq)) -> (gt (succ (n5)) zenon_TE_dq) -> (gt (succ zenon_TE_dq) (n0)) -> False). % 6.67/6.88 do 1 intro. intros zenon_H80 zenon_H72 zenon_H70 zenon_H6f zenon_H6e zenon_H6d zenon_H67 zenon_H5c. % 6.67/6.88 cut ((zenon_TE_dq = (n4))); [idtac | apply NNPP; zenon_intro zenon_H71]. % 6.67/6.88 cut (((xinit_mean_defuse) = (xinit_mean_defuse))); [idtac | apply NNPP; zenon_intro zenon_H66]. % 6.67/6.88 congruence. % 6.67/6.88 apply zenon_H66. apply refl_equal. % 6.67/6.88 apply (zenon_L7_ zenon_TE_dq); trivial. % 6.67/6.88 (* end of lemma zenon_L8_ *) % 6.67/6.88 assert (zenon_L9_ : (~((use) = (use))) -> False). % 6.67/6.88 do 0 intro. intros zenon_H81. % 6.67/6.88 apply zenon_H81. apply refl_equal. % 6.67/6.88 (* end of lemma zenon_L9_ *) % 6.67/6.88 assert (zenon_L10_ : forall (zenon_TE_dq : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((gt x y)->((gt y z)->(gt x z)))))) -> (~(gt (n4) zenon_TE_dq)) -> ((a_select2 (xinit_mean_defuse) (n4)) = (use)) -> (gt (succ zenon_TE_dq) (n0)) -> (gt (succ (n5)) zenon_TE_dq) -> (~((n0) = zenon_TE_dq)) -> ((a_select2 (xinit_mean_defuse) (n5)) = (use)) -> (~((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))) -> False). % 6.67/6.88 do 1 intro. intros zenon_H82 zenon_H83 zenon_H84 zenon_H5c zenon_H67 zenon_H6d zenon_H85 zenon_H86. % 6.67/6.88 elim (classic ((n3) = zenon_TE_dq)); [ zenon_intro zenon_H87 | zenon_intro zenon_H70 ]. % 6.67/6.88 cut ((gt (n4) (n3)) = (gt (n4) zenon_TE_dq)). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_H83. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact gt_4_3. % 6.67/6.88 cut (((n3) = zenon_TE_dq)); [idtac | apply NNPP; zenon_intro zenon_H70]. % 6.67/6.88 cut (((n4) = (n4))); [idtac | apply NNPP; zenon_intro zenon_H63]. % 6.67/6.88 congruence. % 6.67/6.88 apply zenon_H63. apply refl_equal. % 6.67/6.88 exact (zenon_H70 zenon_H87). % 6.67/6.88 elim (classic (gt (n3) zenon_TE_dq)); [ zenon_intro zenon_H88 | zenon_intro zenon_H89 ]. % 6.67/6.88 generalize (zenon_H82 (n4)). zenon_intro zenon_H8a. % 6.67/6.88 generalize (zenon_H8a (n3)). zenon_intro zenon_H8b. % 6.67/6.88 generalize (zenon_H8b zenon_TE_dq). zenon_intro zenon_H8c. % 6.67/6.88 apply (zenon_imply_s _ _ zenon_H8c); [ zenon_intro zenon_H8e | zenon_intro zenon_H8d ]. % 6.67/6.88 exact (zenon_H8e gt_4_3). % 6.67/6.88 apply (zenon_imply_s _ _ zenon_H8d); [ zenon_intro zenon_H89 | zenon_intro zenon_H8f ]. % 6.67/6.88 exact (zenon_H89 zenon_H88). % 6.67/6.88 exact (zenon_H83 zenon_H8f). % 6.67/6.88 elim (classic ((n2) = zenon_TE_dq)); [ zenon_intro zenon_H90 | zenon_intro zenon_H6f ]. % 6.67/6.88 cut ((gt (n3) (n2)) = (gt (n3) zenon_TE_dq)). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_H89. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact gt_3_2. % 6.67/6.88 cut (((n2) = zenon_TE_dq)); [idtac | apply NNPP; zenon_intro zenon_H6f]. % 6.67/6.88 cut (((n3) = (n3))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 6.67/6.88 congruence. % 6.67/6.88 apply zenon_H64. apply refl_equal. % 6.67/6.88 exact (zenon_H6f zenon_H90). % 6.67/6.88 elim (classic (gt (n2) zenon_TE_dq)); [ zenon_intro zenon_H91 | zenon_intro zenon_H92 ]. % 6.67/6.88 generalize (zenon_H82 (n3)). zenon_intro zenon_H93. % 6.67/6.88 generalize (zenon_H93 (n2)). zenon_intro zenon_H94. % 6.67/6.88 generalize (zenon_H94 zenon_TE_dq). zenon_intro zenon_H95. % 6.67/6.88 apply (zenon_imply_s _ _ zenon_H95); [ zenon_intro zenon_H97 | zenon_intro zenon_H96 ]. % 6.67/6.88 exact (zenon_H97 gt_3_2). % 6.67/6.88 apply (zenon_imply_s _ _ zenon_H96); [ zenon_intro zenon_H92 | zenon_intro zenon_H88 ]. % 6.67/6.88 exact (zenon_H92 zenon_H91). % 6.67/6.88 exact (zenon_H89 zenon_H88). % 6.67/6.88 elim (classic ((n1) = zenon_TE_dq)); [ zenon_intro zenon_H98 | zenon_intro zenon_H6e ]. % 6.67/6.88 cut ((gt (n2) (n1)) = (gt (n2) zenon_TE_dq)). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_H92. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact gt_2_1. % 6.67/6.88 cut (((n1) = zenon_TE_dq)); [idtac | apply NNPP; zenon_intro zenon_H6e]. % 6.67/6.88 cut (((n2) = (n2))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 6.67/6.88 congruence. % 6.67/6.88 apply zenon_H65. apply refl_equal. % 6.67/6.88 exact (zenon_H6e zenon_H98). % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) (n4)) = (use)) = ((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_H86. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_H84. % 6.67/6.88 cut (((use) = (use))); [idtac | apply NNPP; zenon_intro zenon_H81]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) (n4)) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_H99]. % 6.67/6.88 congruence. % 6.67/6.88 elim (classic ((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [ zenon_intro zenon_H9a | zenon_intro zenon_H9b ]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq)) = ((a_select2 (xinit_mean_defuse) (n4)) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_H99. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_H9a. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_H9b]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) (n4)))); [idtac | apply NNPP; zenon_intro zenon_H80]. % 6.67/6.88 congruence. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) (n5)) = (use)) = ((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_H86. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_H85. % 6.67/6.88 cut (((use) = (use))); [idtac | apply NNPP; zenon_intro zenon_H81]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) (n5)) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_H9c]. % 6.67/6.88 congruence. % 6.67/6.88 elim (classic ((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [ zenon_intro zenon_H9a | zenon_intro zenon_H9b ]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq)) = ((a_select2 (xinit_mean_defuse) (n5)) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_H9c. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_H9a. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_H9b]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) (n5)))); [idtac | apply NNPP; zenon_intro zenon_H9d]. % 6.67/6.88 congruence. % 6.67/6.88 cut ((zenon_TE_dq = (n5))); [idtac | apply NNPP; zenon_intro zenon_H72]. % 6.67/6.88 cut (((xinit_mean_defuse) = (xinit_mean_defuse))); [idtac | apply NNPP; zenon_intro zenon_H66]. % 6.67/6.88 congruence. % 6.67/6.88 apply zenon_H66. apply refl_equal. % 6.67/6.88 apply (zenon_L8_ zenon_TE_dq); trivial. % 6.67/6.88 apply zenon_H9b. apply refl_equal. % 6.67/6.88 apply zenon_H9b. apply refl_equal. % 6.67/6.88 apply zenon_H81. apply refl_equal. % 6.67/6.88 apply zenon_H9b. apply refl_equal. % 6.67/6.88 apply zenon_H9b. apply refl_equal. % 6.67/6.88 apply zenon_H81. apply refl_equal. % 6.67/6.88 (* end of lemma zenon_L10_ *) % 6.67/6.88 assert (zenon_L11_ : (~((succ (n3)) = (succ (succ (succ (succ (n0))))))) -> False). % 6.67/6.88 do 0 intro. intros zenon_H9e. % 6.67/6.88 cut (((n3) = (succ (succ (succ (n0)))))); [idtac | apply NNPP; zenon_intro zenon_H9f]. % 6.67/6.88 congruence. % 6.67/6.88 apply zenon_H9f. apply sym_equal. exact successor_3. % 6.67/6.88 (* end of lemma zenon_L11_ *) % 6.67/6.88 assert (zenon_L12_ : forall (zenon_TE_dq : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((gt x y)->((gt y z)->(gt x z)))))) -> (~(gt (succ (n3)) zenon_TE_dq)) -> (~((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))) -> ((a_select2 (xinit_mean_defuse) (n5)) = (use)) -> (~((n0) = zenon_TE_dq)) -> (gt (succ (n5)) zenon_TE_dq) -> (gt (succ zenon_TE_dq) (n0)) -> ((a_select2 (xinit_mean_defuse) (n4)) = (use)) -> False). % 6.67/6.88 do 1 intro. intros zenon_H82 zenon_Ha0 zenon_H86 zenon_H85 zenon_H6d zenon_H67 zenon_H5c zenon_H84. % 6.67/6.88 elim (classic (gt (n4) zenon_TE_dq)); [ zenon_intro zenon_H8f | zenon_intro zenon_H83 ]. % 6.67/6.88 elim (classic (gt (succ (succ (succ (succ (n0))))) zenon_TE_dq)); [ zenon_intro zenon_Ha1 | zenon_intro zenon_Ha2 ]. % 6.67/6.88 cut ((gt (succ (succ (succ (succ (n0))))) zenon_TE_dq) = (gt (succ (n3)) zenon_TE_dq)). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Ha0. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Ha1. % 6.67/6.88 cut ((zenon_TE_dq = zenon_TE_dq)); [idtac | apply NNPP; zenon_intro zenon_Ha3]. % 6.67/6.88 cut (((succ (succ (succ (succ (n0))))) = (succ (n3)))); [idtac | apply NNPP; zenon_intro zenon_Ha4]. % 6.67/6.88 congruence. % 6.67/6.88 elim (classic ((succ (n3)) = (succ (n3)))); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Ha6 ]. % 6.67/6.88 cut (((succ (n3)) = (succ (n3))) = ((succ (succ (succ (succ (n0))))) = (succ (n3)))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Ha4. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Ha5. % 6.67/6.88 cut (((succ (n3)) = (succ (n3)))); [idtac | apply NNPP; zenon_intro zenon_Ha6]. % 6.67/6.88 cut (((succ (n3)) = (succ (succ (succ (succ (n0))))))); [idtac | apply NNPP; zenon_intro zenon_H9e]. % 6.67/6.88 congruence. % 6.67/6.88 apply (zenon_L11_); trivial. % 6.67/6.88 apply zenon_Ha6. apply refl_equal. % 6.67/6.88 apply zenon_Ha6. apply refl_equal. % 6.67/6.88 apply zenon_Ha3. apply refl_equal. % 6.67/6.88 cut ((gt (n4) zenon_TE_dq) = (gt (succ (succ (succ (succ (n0))))) zenon_TE_dq)). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Ha2. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_H8f. % 6.67/6.88 cut ((zenon_TE_dq = zenon_TE_dq)); [idtac | apply NNPP; zenon_intro zenon_Ha3]. % 6.67/6.88 cut (((n4) = (succ (succ (succ (succ (n0))))))); [idtac | apply NNPP; zenon_intro zenon_Ha7]. % 6.67/6.88 congruence. % 6.67/6.88 elim (classic ((succ (succ (succ (succ (n0))))) = (succ (succ (succ (succ (n0))))))); [ zenon_intro zenon_Ha8 | zenon_intro zenon_Ha9 ]. % 6.67/6.88 cut (((succ (succ (succ (succ (n0))))) = (succ (succ (succ (succ (n0)))))) = ((n4) = (succ (succ (succ (succ (n0))))))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Ha7. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Ha8. % 6.67/6.88 cut (((succ (succ (succ (succ (n0))))) = (succ (succ (succ (succ (n0))))))); [idtac | apply NNPP; zenon_intro zenon_Ha9]. % 6.67/6.88 cut (((succ (succ (succ (succ (n0))))) = (n4))); [idtac | apply NNPP; zenon_intro zenon_Haa]. % 6.67/6.88 congruence. % 6.67/6.88 exact (zenon_Haa successor_4). % 6.67/6.88 apply zenon_Ha9. apply refl_equal. % 6.67/6.88 apply zenon_Ha9. apply refl_equal. % 6.67/6.88 apply zenon_Ha3. apply refl_equal. % 6.67/6.88 apply (zenon_L10_ zenon_TE_dq); trivial. % 6.67/6.88 (* end of lemma zenon_L12_ *) % 6.67/6.88 assert (zenon_L13_ : forall (zenon_TE_dq : zenon_U), (~((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))) -> ((a_select2 (xinit_mean_defuse) (n1)) = (use)) -> (zenon_TE_dq = (n1)) -> False). % 6.67/6.88 do 1 intro. intros zenon_H86 zenon_Hab zenon_H79. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) (n1)) = (use)) = ((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_H86. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Hab. % 6.67/6.88 cut (((use) = (use))); [idtac | apply NNPP; zenon_intro zenon_H81]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) (n1)) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_Hac]. % 6.67/6.88 congruence. % 6.67/6.88 elim (classic ((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [ zenon_intro zenon_H9a | zenon_intro zenon_H9b ]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq)) = ((a_select2 (xinit_mean_defuse) (n1)) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Hac. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_H9a. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_H9b]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) (n1)))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 6.67/6.88 congruence. % 6.67/6.88 cut ((zenon_TE_dq = (n1))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 6.67/6.88 cut (((xinit_mean_defuse) = (xinit_mean_defuse))); [idtac | apply NNPP; zenon_intro zenon_H66]. % 6.67/6.88 congruence. % 6.67/6.88 apply zenon_H66. apply refl_equal. % 6.67/6.88 exact (zenon_Hae zenon_H79). % 6.67/6.88 apply zenon_H9b. apply refl_equal. % 6.67/6.88 apply zenon_H9b. apply refl_equal. % 6.67/6.88 apply zenon_H81. apply refl_equal. % 6.67/6.88 (* end of lemma zenon_L13_ *) % 6.67/6.88 assert (zenon_L14_ : forall (zenon_TE_dq : zenon_U), (~((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))) -> ((a_select2 (xinit_mean_defuse) (n2)) = (use)) -> (zenon_TE_dq = (n2)) -> False). % 6.67/6.88 do 1 intro. intros zenon_H86 zenon_Haf zenon_H7b. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) (n2)) = (use)) = ((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_H86. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Haf. % 6.67/6.88 cut (((use) = (use))); [idtac | apply NNPP; zenon_intro zenon_H81]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) (n2)) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_Hb0]. % 6.67/6.88 congruence. % 6.67/6.88 elim (classic ((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [ zenon_intro zenon_H9a | zenon_intro zenon_H9b ]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq)) = ((a_select2 (xinit_mean_defuse) (n2)) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Hb0. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_H9a. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_H9b]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) (n2)))); [idtac | apply NNPP; zenon_intro zenon_Hb1]. % 6.67/6.88 congruence. % 6.67/6.88 cut ((zenon_TE_dq = (n2))); [idtac | apply NNPP; zenon_intro zenon_Hb2]. % 6.67/6.88 cut (((xinit_mean_defuse) = (xinit_mean_defuse))); [idtac | apply NNPP; zenon_intro zenon_H66]. % 6.67/6.88 congruence. % 6.67/6.88 apply zenon_H66. apply refl_equal. % 6.67/6.88 exact (zenon_Hb2 zenon_H7b). % 6.67/6.88 apply zenon_H9b. apply refl_equal. % 6.67/6.88 apply zenon_H9b. apply refl_equal. % 6.67/6.88 apply zenon_H81. apply refl_equal. % 6.67/6.88 (* end of lemma zenon_L14_ *) % 6.67/6.88 assert (zenon_L15_ : forall (zenon_TE_dq : zenon_U), (~((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))) -> ((a_select2 (xinit_mean_defuse) (n3)) = (use)) -> (zenon_TE_dq = (n3)) -> False). % 6.67/6.88 do 1 intro. intros zenon_H86 zenon_Hb3 zenon_H7d. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) (n3)) = (use)) = ((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_H86. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Hb3. % 6.67/6.88 cut (((use) = (use))); [idtac | apply NNPP; zenon_intro zenon_H81]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) (n3)) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_Hb4]. % 6.67/6.88 congruence. % 6.67/6.88 elim (classic ((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [ zenon_intro zenon_H9a | zenon_intro zenon_H9b ]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq)) = ((a_select2 (xinit_mean_defuse) (n3)) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Hb4. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_H9a. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_H9b]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) (n3)))); [idtac | apply NNPP; zenon_intro zenon_Hb5]. % 6.67/6.88 congruence. % 6.67/6.88 cut ((zenon_TE_dq = (n3))); [idtac | apply NNPP; zenon_intro zenon_Hb6]. % 6.67/6.88 cut (((xinit_mean_defuse) = (xinit_mean_defuse))); [idtac | apply NNPP; zenon_intro zenon_H66]. % 6.67/6.88 congruence. % 6.67/6.88 apply zenon_H66. apply refl_equal. % 6.67/6.88 exact (zenon_Hb6 zenon_H7d). % 6.67/6.88 apply zenon_H9b. apply refl_equal. % 6.67/6.88 apply zenon_H9b. apply refl_equal. % 6.67/6.88 apply zenon_H81. apply refl_equal. % 6.67/6.88 (* end of lemma zenon_L15_ *) % 6.67/6.88 assert (zenon_L16_ : forall (zenon_TE_dq : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((gt x y)->((gt y z)->(gt x z)))))) -> (gt (succ zenon_TE_dq) (n0)) -> (~((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))) -> ((a_select2 (xinit_mean_defuse) (n5)) = (use)) -> (~((n0) = zenon_TE_dq)) -> (gt (succ (n5)) zenon_TE_dq) -> ((a_select2 (xinit_mean_defuse) (n4)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n1)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n2)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n3)) = (use)) -> False). % 6.67/6.88 do 1 intro. intros zenon_H82 zenon_H5c zenon_H86 zenon_H85 zenon_H6d zenon_H67 zenon_H84 zenon_Hab zenon_Haf zenon_Hb3. % 6.67/6.88 generalize (finite_domain_3 zenon_TE_dq). zenon_intro zenon_Hb7. % 6.67/6.88 apply (zenon_imply_s _ _ zenon_Hb7); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hb8 ]. % 6.67/6.88 apply (zenon_notand_s _ _ zenon_Hb9); [ zenon_intro zenon_H5d | zenon_intro zenon_Hba ]. % 6.67/6.88 apply (zenon_L1_ zenon_TE_dq); trivial. % 6.67/6.88 generalize (leq_succ_gt_equiv zenon_TE_dq). zenon_intro zenon_H69. % 6.67/6.88 generalize (zenon_H69 (n3)). zenon_intro zenon_Hbb. % 6.67/6.88 apply (zenon_equiv_s _ _ zenon_Hbb); [ zenon_intro zenon_Hba; zenon_intro zenon_Ha0 | zenon_intro zenon_Hbd; zenon_intro zenon_Hbc ]. % 6.67/6.88 apply (zenon_L12_ zenon_TE_dq); trivial. % 6.67/6.88 exact (zenon_Hba zenon_Hbd). % 6.67/6.88 apply (zenon_or_s _ _ zenon_Hb8); [ zenon_intro zenon_H77 | zenon_intro zenon_Hbe ]. % 6.67/6.88 apply zenon_H6d. apply sym_equal. exact zenon_H77. % 6.67/6.88 apply (zenon_or_s _ _ zenon_Hbe); [ zenon_intro zenon_H79 | zenon_intro zenon_Hbf ]. % 6.67/6.88 apply (zenon_L13_ zenon_TE_dq); trivial. % 6.67/6.88 apply (zenon_or_s _ _ zenon_Hbf); [ zenon_intro zenon_H7b | zenon_intro zenon_H7d ]. % 6.67/6.88 apply (zenon_L14_ zenon_TE_dq); trivial. % 6.67/6.88 apply (zenon_L15_ zenon_TE_dq); trivial. % 6.67/6.88 (* end of lemma zenon_L16_ *) % 6.67/6.88 assert (zenon_L17_ : forall (zenon_TE_dq : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((gt x y)->((gt y z)->(gt x z)))))) -> (~((succ (n0)) = (succ zenon_TE_dq))) -> ((a_select2 (xinit_mean_defuse) (n3)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n2)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n1)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n4)) = (use)) -> (gt (succ (n5)) zenon_TE_dq) -> ((a_select2 (xinit_mean_defuse) (n5)) = (use)) -> (~((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))) -> (gt (succ zenon_TE_dq) (n0)) -> False). % 6.67/6.88 do 1 intro. intros zenon_H82 zenon_Hc0 zenon_Hb3 zenon_Haf zenon_Hab zenon_H84 zenon_H67 zenon_H85 zenon_H86 zenon_H5c. % 6.67/6.88 cut (((n0) = zenon_TE_dq)); [idtac | apply NNPP; zenon_intro zenon_H6d]. % 6.67/6.88 congruence. % 6.67/6.88 apply (zenon_L16_ zenon_TE_dq); trivial. % 6.67/6.88 (* end of lemma zenon_L17_ *) % 6.67/6.88 assert (zenon_L18_ : (~((n1) = (n1))) -> False). % 6.67/6.88 do 0 intro. intros zenon_Hc1. % 6.67/6.88 apply zenon_Hc1. apply refl_equal. % 6.67/6.88 (* end of lemma zenon_L18_ *) % 6.67/6.88 assert (zenon_L19_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((gt x y)->((gt y z)->(gt x z)))))) -> (~(gt (succ (succ (n0))) (n1))) -> False). % 6.67/6.88 do 0 intro. intros zenon_H82 zenon_Hc2. % 6.67/6.88 elim (classic ((~((succ (succ (n0))) = (n2)))/\(~(gt (succ (succ (n0))) (n2))))); [ zenon_intro zenon_Hc3 | zenon_intro zenon_Hc4 ]. % 6.67/6.88 apply (zenon_and_s _ _ zenon_Hc3). zenon_intro zenon_Hc6. zenon_intro zenon_Hc5. % 6.67/6.88 exact (zenon_Hc6 successor_2). % 6.67/6.88 cut ((gt (n2) (n1)) = (gt (succ (succ (n0))) (n1))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Hc2. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact gt_2_1. % 6.67/6.88 cut (((n1) = (n1))); [idtac | apply NNPP; zenon_intro zenon_Hc1]. % 6.67/6.88 cut (((n2) = (succ (succ (n0))))); [idtac | apply NNPP; zenon_intro zenon_Hc7]. % 6.67/6.88 congruence. % 6.67/6.88 apply (zenon_notand_s _ _ zenon_Hc4); [ zenon_intro zenon_Hc9 | zenon_intro zenon_Hc8 ]. % 6.67/6.88 apply zenon_Hc9. zenon_intro successor_2. % 6.67/6.88 elim (classic ((succ (succ (n0))) = (succ (succ (n0))))); [ zenon_intro zenon_Hca | zenon_intro zenon_Hcb ]. % 6.67/6.88 cut (((succ (succ (n0))) = (succ (succ (n0)))) = ((n2) = (succ (succ (n0))))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Hc7. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Hca. % 6.67/6.88 cut (((succ (succ (n0))) = (succ (succ (n0))))); [idtac | apply NNPP; zenon_intro zenon_Hcb]. % 6.67/6.88 cut (((succ (succ (n0))) = (n2))); [idtac | apply NNPP; zenon_intro zenon_Hc6]. % 6.67/6.88 congruence. % 6.67/6.88 exact (zenon_Hc6 successor_2). % 6.67/6.88 apply zenon_Hcb. apply refl_equal. % 6.67/6.88 apply zenon_Hcb. apply refl_equal. % 6.67/6.88 apply zenon_Hc8. zenon_intro zenon_Hcc. % 6.67/6.88 generalize (zenon_H82 (succ (succ (n0)))). zenon_intro zenon_Hcd. % 6.67/6.88 generalize (zenon_Hcd (n2)). zenon_intro zenon_Hce. % 6.67/6.88 generalize (zenon_Hce (n1)). zenon_intro zenon_Hcf. % 6.67/6.88 apply (zenon_imply_s _ _ zenon_Hcf); [ zenon_intro zenon_Hc5 | zenon_intro zenon_Hd0 ]. % 6.67/6.88 exact (zenon_Hc5 zenon_Hcc). % 6.67/6.88 apply (zenon_imply_s _ _ zenon_Hd0); [ zenon_intro zenon_Hd2 | zenon_intro zenon_Hd1 ]. % 6.67/6.88 exact (zenon_Hd2 gt_2_1). % 6.67/6.88 exact (zenon_Hc2 zenon_Hd1). % 6.67/6.88 apply zenon_Hc1. apply refl_equal. % 6.67/6.88 (* end of lemma zenon_L19_ *) % 6.67/6.88 assert (zenon_L20_ : forall (zenon_TE_dq : zenon_U), (~(gt (succ (succ (n0))) (succ zenon_TE_dq))) -> (gt (succ zenon_TE_dq) (n0)) -> (~((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))) -> ((a_select2 (xinit_mean_defuse) (n5)) = (use)) -> (gt (succ (n5)) zenon_TE_dq) -> ((a_select2 (xinit_mean_defuse) (n4)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n1)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n2)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n3)) = (use)) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((gt x y)->((gt y z)->(gt x z)))))) -> False). % 6.67/6.88 do 1 intro. intros zenon_Hd3 zenon_H5c zenon_H86 zenon_H85 zenon_H67 zenon_H84 zenon_Hab zenon_Haf zenon_Hb3 zenon_H82. % 6.67/6.88 elim (classic ((n1) = (succ (n0)))); [ zenon_intro zenon_Hd4 | zenon_intro zenon_Hd5 ]. % 6.67/6.88 elim (classic (gt (succ (succ (n0))) (n1))); [ zenon_intro zenon_Hd1 | zenon_intro zenon_Hc2 ]. % 6.67/6.88 elim (classic (gt (succ (succ (n0))) (succ (n0)))); [ zenon_intro zenon_Hd6 | zenon_intro zenon_Hd7 ]. % 6.67/6.88 cut ((gt (succ (succ (n0))) (succ (n0))) = (gt (succ (succ (n0))) (succ zenon_TE_dq))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Hd3. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Hd6. % 6.67/6.88 cut (((succ (n0)) = (succ zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_Hc0]. % 6.67/6.88 cut (((succ (succ (n0))) = (succ (succ (n0))))); [idtac | apply NNPP; zenon_intro zenon_Hcb]. % 6.67/6.88 congruence. % 6.67/6.88 apply zenon_Hcb. apply refl_equal. % 6.67/6.88 apply (zenon_L17_ zenon_TE_dq); trivial. % 6.67/6.88 cut ((gt (succ (succ (n0))) (n1)) = (gt (succ (succ (n0))) (succ (n0)))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Hd7. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Hd1. % 6.67/6.88 cut (((n1) = (succ (n0)))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 6.67/6.88 cut (((succ (succ (n0))) = (succ (succ (n0))))); [idtac | apply NNPP; zenon_intro zenon_Hcb]. % 6.67/6.88 congruence. % 6.67/6.88 apply zenon_Hcb. apply refl_equal. % 6.67/6.88 exact (zenon_Hd5 zenon_Hd4). % 6.67/6.88 apply (zenon_L19_); trivial. % 6.67/6.88 elim (classic ((succ (n0)) = (succ (n0)))); [ zenon_intro zenon_Hd8 | zenon_intro zenon_Hd9 ]. % 6.67/6.88 cut (((succ (n0)) = (succ (n0))) = ((n1) = (succ (n0)))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Hd5. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Hd8. % 6.67/6.88 cut (((succ (n0)) = (succ (n0)))); [idtac | apply NNPP; zenon_intro zenon_Hd9]. % 6.67/6.88 cut (((succ (n0)) = (n1))); [idtac | apply NNPP; zenon_intro zenon_Hda]. % 6.67/6.88 congruence. % 6.67/6.88 exact (zenon_Hda successor_1). % 6.67/6.88 apply zenon_Hd9. apply refl_equal. % 6.67/6.88 apply zenon_Hd9. apply refl_equal. % 6.67/6.88 (* end of lemma zenon_L20_ *) % 6.67/6.88 assert (zenon_L21_ : forall (zenon_TE_dq : zenon_U), ((a_select2 (xinit_mean_defuse) (n3)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n2)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n1)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n4)) = (use)) -> (gt (succ (n5)) zenon_TE_dq) -> ((a_select2 (xinit_mean_defuse) (n5)) = (use)) -> (~((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))) -> (gt (succ zenon_TE_dq) (n0)) -> (~(gt (n2) (succ zenon_TE_dq))) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((gt x y)->((gt y z)->(gt x z)))))) -> False). % 6.67/6.88 do 1 intro. intros zenon_Hb3 zenon_Haf zenon_Hab zenon_H84 zenon_H67 zenon_H85 zenon_H86 zenon_H5c zenon_Hdb zenon_H82. % 6.67/6.88 elim (classic ((n2) = (succ (succ (n0))))); [ zenon_intro zenon_Hdc | zenon_intro zenon_Hc7 ]. % 6.67/6.88 elim (classic (gt (succ (succ (n0))) (succ zenon_TE_dq))); [ zenon_intro zenon_Hdd | zenon_intro zenon_Hd3 ]. % 6.67/6.88 cut ((gt (succ (succ (n0))) (succ zenon_TE_dq)) = (gt (n2) (succ zenon_TE_dq))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Hdb. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Hdd. % 6.67/6.88 cut (((succ zenon_TE_dq) = (succ zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_Hde]. % 6.67/6.88 cut (((succ (succ (n0))) = (n2))); [idtac | apply NNPP; zenon_intro zenon_Hc6]. % 6.67/6.88 congruence. % 6.67/6.88 elim (classic ((n2) = (n2))); [ zenon_intro zenon_Hdf | zenon_intro zenon_H65 ]. % 6.67/6.88 cut (((n2) = (n2)) = ((succ (succ (n0))) = (n2))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Hc6. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Hdf. % 6.67/6.88 cut (((n2) = (n2))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 6.67/6.88 cut (((n2) = (succ (succ (n0))))); [idtac | apply NNPP; zenon_intro zenon_Hc7]. % 6.67/6.88 congruence. % 6.67/6.88 exact (zenon_Hc7 zenon_Hdc). % 6.67/6.88 apply zenon_H65. apply refl_equal. % 6.67/6.88 apply zenon_H65. apply refl_equal. % 6.67/6.88 apply zenon_Hde. apply refl_equal. % 6.67/6.88 apply (zenon_L20_ zenon_TE_dq); trivial. % 6.67/6.88 elim (classic ((succ (succ (n0))) = (succ (succ (n0))))); [ zenon_intro zenon_Hca | zenon_intro zenon_Hcb ]. % 6.67/6.88 cut (((succ (succ (n0))) = (succ (succ (n0)))) = ((n2) = (succ (succ (n0))))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Hc7. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Hca. % 6.67/6.88 cut (((succ (succ (n0))) = (succ (succ (n0))))); [idtac | apply NNPP; zenon_intro zenon_Hcb]. % 6.67/6.88 cut (((succ (succ (n0))) = (n2))); [idtac | apply NNPP; zenon_intro zenon_Hc6]. % 6.67/6.88 congruence. % 6.67/6.88 exact (zenon_Hc6 successor_2). % 6.67/6.88 apply zenon_Hcb. apply refl_equal. % 6.67/6.88 apply zenon_Hcb. apply refl_equal. % 6.67/6.88 (* end of lemma zenon_L21_ *) % 6.67/6.88 assert (zenon_L22_ : forall (zenon_TE_dq : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((gt x y)->((gt y z)->(gt x z)))))) -> (~(gt (n4) (succ zenon_TE_dq))) -> (gt (succ zenon_TE_dq) (n0)) -> (~((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))) -> ((a_select2 (xinit_mean_defuse) (n5)) = (use)) -> (gt (succ (n5)) zenon_TE_dq) -> ((a_select2 (xinit_mean_defuse) (n4)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n1)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n2)) = (use)) -> ((a_select2 (xinit_mean_defuse) (n3)) = (use)) -> False). % 6.67/6.88 do 1 intro. intros zenon_H82 zenon_He0 zenon_H5c zenon_H86 zenon_H85 zenon_H67 zenon_H84 zenon_Hab zenon_Haf zenon_Hb3. % 6.67/6.88 elim (classic (gt (n3) (succ zenon_TE_dq))); [ zenon_intro zenon_He1 | zenon_intro zenon_He2 ]. % 6.67/6.88 generalize (zenon_H82 (n4)). zenon_intro zenon_H8a. % 6.67/6.88 generalize (zenon_H8a (n3)). zenon_intro zenon_H8b. % 6.67/6.88 generalize (zenon_H8b (succ zenon_TE_dq)). zenon_intro zenon_He3. % 6.67/6.88 apply (zenon_imply_s _ _ zenon_He3); [ zenon_intro zenon_H8e | zenon_intro zenon_He4 ]. % 6.67/6.88 exact (zenon_H8e gt_4_3). % 6.67/6.88 apply (zenon_imply_s _ _ zenon_He4); [ zenon_intro zenon_He2 | zenon_intro zenon_He5 ]. % 6.67/6.88 exact (zenon_He2 zenon_He1). % 6.67/6.88 exact (zenon_He0 zenon_He5). % 6.67/6.88 elim (classic (gt (n2) (succ zenon_TE_dq))); [ zenon_intro zenon_He6 | zenon_intro zenon_Hdb ]. % 6.67/6.88 generalize (zenon_H82 (n3)). zenon_intro zenon_H93. % 6.67/6.88 generalize (zenon_H93 (n2)). zenon_intro zenon_H94. % 6.67/6.88 generalize (zenon_H94 (succ zenon_TE_dq)). zenon_intro zenon_He7. % 6.67/6.88 apply (zenon_imply_s _ _ zenon_He7); [ zenon_intro zenon_H97 | zenon_intro zenon_He8 ]. % 6.67/6.88 exact (zenon_H97 gt_3_2). % 6.67/6.88 apply (zenon_imply_s _ _ zenon_He8); [ zenon_intro zenon_Hdb | zenon_intro zenon_He1 ]. % 6.67/6.88 exact (zenon_Hdb zenon_He6). % 6.67/6.88 exact (zenon_He2 zenon_He1). % 6.67/6.88 apply (zenon_L21_ zenon_TE_dq); trivial. % 6.67/6.88 (* end of lemma zenon_L22_ *) % 6.67/6.88 assert (zenon_L23_ : forall (zenon_TE_dq : zenon_U), (~((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))) -> ((a_select2 (xinit_mean_defuse) (n0)) = (use)) -> (zenon_TE_dq = (n0)) -> False). % 6.67/6.88 do 1 intro. intros zenon_H86 zenon_He9 zenon_H77. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) (n0)) = (use)) = ((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (use))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_H86. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_He9. % 6.67/6.88 cut (((use) = (use))); [idtac | apply NNPP; zenon_intro zenon_H81]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) (n0)) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_Hea]. % 6.67/6.88 congruence. % 6.67/6.88 elim (classic ((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [ zenon_intro zenon_H9a | zenon_intro zenon_H9b ]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq)) = ((a_select2 (xinit_mean_defuse) (n0)) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Hea. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_H9a. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_H9b]. % 6.67/6.88 cut (((a_select2 (xinit_mean_defuse) zenon_TE_dq) = (a_select2 (xinit_mean_defuse) (n0)))); [idtac | apply NNPP; zenon_intro zenon_Heb]. % 6.67/6.88 congruence. % 6.67/6.88 cut ((zenon_TE_dq = (n0))); [idtac | apply NNPP; zenon_intro zenon_Hec]. % 6.67/6.88 cut (((xinit_mean_defuse) = (xinit_mean_defuse))); [idtac | apply NNPP; zenon_intro zenon_H66]. % 6.67/6.88 congruence. % 6.67/6.88 apply zenon_H66. apply refl_equal. % 6.67/6.88 exact (zenon_Hec zenon_H77). % 6.67/6.88 apply zenon_H9b. apply refl_equal. % 6.67/6.88 apply zenon_H9b. apply refl_equal. % 6.67/6.88 apply zenon_H81. apply refl_equal. % 6.67/6.88 (* end of lemma zenon_L23_ *) % 6.67/6.88 apply NNPP. intro zenon_G. % 6.67/6.88 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((gt x y)->((gt y z)->(gt x z))))))); [ zenon_intro zenon_H82 | zenon_intro zenon_Hed ]. % 6.67/6.88 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_Hef. zenon_intro zenon_Hee. % 6.67/6.88 apply (zenon_and_s _ _ zenon_Hef). zenon_intro zenon_Hf1. zenon_intro zenon_Hf0. % 6.67/6.88 apply (zenon_and_s _ _ zenon_Hf0). zenon_intro zenon_Hf3. zenon_intro zenon_Hf2. % 6.67/6.88 apply (zenon_and_s _ _ zenon_Hf2). zenon_intro zenon_Hf5. zenon_intro zenon_Hf4. % 6.67/6.88 apply (zenon_and_s _ _ zenon_Hf4). zenon_intro zenon_Hf7. zenon_intro zenon_Hf6. % 6.67/6.88 apply (zenon_and_s _ _ zenon_Hf6). zenon_intro zenon_Hf9. zenon_intro zenon_Hf8. % 6.67/6.88 apply (zenon_and_s _ _ zenon_Hf8). zenon_intro zenon_Hfb. zenon_intro zenon_Hfa. % 6.67/6.88 apply (zenon_and_s _ _ zenon_Hfa). zenon_intro zenon_Hfd. zenon_intro zenon_Hfc. % 6.67/6.88 apply (zenon_and_s _ _ zenon_Hfc). zenon_intro zenon_Hff. zenon_intro zenon_Hfe. % 6.67/6.88 apply (zenon_and_s _ _ zenon_Hfe). zenon_intro zenon_H101. zenon_intro zenon_H100. % 6.67/6.88 apply (zenon_and_s _ _ zenon_H100). zenon_intro zenon_H103. zenon_intro zenon_H102. % 6.67/6.88 apply (zenon_and_s _ _ zenon_H102). zenon_intro zenon_H105. zenon_intro zenon_H104. % 6.67/6.88 apply (zenon_and_s _ _ zenon_H104). zenon_intro zenon_H107. zenon_intro zenon_H106. % 6.67/6.88 apply (zenon_and_s _ _ zenon_H106). zenon_intro zenon_H109. zenon_intro zenon_H108. % 6.67/6.88 apply (zenon_and_s _ _ zenon_H108). zenon_intro zenon_H10b. zenon_intro zenon_H10a. % 6.67/6.88 apply (zenon_and_s _ _ zenon_H10a). zenon_intro zenon_H10d. zenon_intro zenon_H10c. % 6.67/6.88 apply (zenon_and_s _ _ zenon_H10c). zenon_intro zenon_He9. zenon_intro zenon_H10e. % 6.67/6.88 apply (zenon_and_s _ _ zenon_H10e). zenon_intro zenon_Hab. zenon_intro zenon_H10f. % 6.67/6.88 apply (zenon_and_s _ _ zenon_H10f). zenon_intro zenon_Haf. zenon_intro zenon_H110. % 6.67/6.88 apply (zenon_and_s _ _ zenon_H110). zenon_intro zenon_Hb3. zenon_intro zenon_H111. % 6.67/6.88 apply (zenon_and_s _ _ zenon_H111). zenon_intro zenon_H84. zenon_intro zenon_H112. % 6.67/6.88 apply (zenon_and_s _ _ zenon_H112). zenon_intro zenon_H85. zenon_intro zenon_H113. % 6.67/6.88 apply (zenon_notallex_s (fun E : zenon_U => (((leq (n0) E)/\(leq E (n5)))->((a_select2 (xinit_mean_defuse) E) = (use)))) zenon_Hee); [ zenon_intro zenon_H114; idtac ]. % 6.67/6.88 elim zenon_H114. zenon_intro zenon_TE_dq. zenon_intro zenon_H115. % 6.67/6.88 apply (zenon_notimply_s _ _ zenon_H115). zenon_intro zenon_H116. zenon_intro zenon_H86. % 6.67/6.88 apply (zenon_and_s _ _ zenon_H116). zenon_intro zenon_H61. zenon_intro zenon_H6b. % 6.67/6.88 generalize (leq_succ_gt_equiv (n0)). zenon_intro zenon_H5f. % 6.67/6.88 generalize (zenon_H5f zenon_TE_dq). zenon_intro zenon_H60. % 6.67/6.88 apply (zenon_equiv_s _ _ zenon_H60); [ zenon_intro zenon_H5d; zenon_intro zenon_H62 | zenon_intro zenon_H61; zenon_intro zenon_H5c ]. % 6.67/6.88 exact (zenon_H5d zenon_H61). % 6.67/6.88 generalize (leq_succ_gt_equiv zenon_TE_dq). zenon_intro zenon_H69. % 6.67/6.88 generalize (zenon_H69 (n5)). zenon_intro zenon_H6a. % 6.67/6.88 apply (zenon_equiv_s _ _ zenon_H6a); [ zenon_intro zenon_H68; zenon_intro zenon_H6c | zenon_intro zenon_H6b; zenon_intro zenon_H67 ]. % 6.67/6.88 exact (zenon_H68 zenon_H6b). % 6.67/6.88 generalize (finite_domain_3 zenon_TE_dq). zenon_intro zenon_Hb7. % 6.67/6.88 apply (zenon_imply_s _ _ zenon_Hb7); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hb8 ]. % 6.67/6.88 apply (zenon_notand_s _ _ zenon_Hb9); [ zenon_intro zenon_H5d | zenon_intro zenon_Hba ]. % 6.67/6.88 apply (zenon_L1_ zenon_TE_dq); trivial. % 6.67/6.88 generalize (leq_succ_gt_equiv zenon_TE_dq). zenon_intro zenon_H69. % 6.67/6.88 generalize (zenon_H69 (n3)). zenon_intro zenon_Hbb. % 6.67/6.88 apply (zenon_equiv_s _ _ zenon_Hbb); [ zenon_intro zenon_Hba; zenon_intro zenon_Ha0 | zenon_intro zenon_Hbd; zenon_intro zenon_Hbc ]. % 6.67/6.88 elim (classic ((~((succ (n3)) = (succ zenon_TE_dq)))/\(~(gt (succ (n3)) (succ zenon_TE_dq))))); [ zenon_intro zenon_H117 | zenon_intro zenon_H118 ]. % 6.67/6.88 apply (zenon_and_s _ _ zenon_H117). zenon_intro zenon_H11a. zenon_intro zenon_H119. % 6.67/6.88 elim (classic (gt (n4) (succ zenon_TE_dq))); [ zenon_intro zenon_He5 | zenon_intro zenon_He0 ]. % 6.67/6.88 elim (classic (gt (succ (succ (succ (succ (n0))))) (succ zenon_TE_dq))); [ zenon_intro zenon_H11b | zenon_intro zenon_H11c ]. % 6.67/6.88 cut ((gt (succ (succ (succ (succ (n0))))) (succ zenon_TE_dq)) = (gt (succ (n3)) (succ zenon_TE_dq))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_H119. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_H11b. % 6.67/6.88 cut (((succ zenon_TE_dq) = (succ zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_Hde]. % 6.67/6.88 cut (((succ (succ (succ (succ (n0))))) = (succ (n3)))); [idtac | apply NNPP; zenon_intro zenon_Ha4]. % 6.67/6.88 congruence. % 6.67/6.88 elim (classic ((succ (n3)) = (succ (n3)))); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Ha6 ]. % 6.67/6.88 cut (((succ (n3)) = (succ (n3))) = ((succ (succ (succ (succ (n0))))) = (succ (n3)))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Ha4. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Ha5. % 6.67/6.88 cut (((succ (n3)) = (succ (n3)))); [idtac | apply NNPP; zenon_intro zenon_Ha6]. % 6.67/6.88 cut (((succ (n3)) = (succ (succ (succ (succ (n0))))))); [idtac | apply NNPP; zenon_intro zenon_H9e]. % 6.67/6.88 congruence. % 6.67/6.88 apply (zenon_L11_); trivial. % 6.67/6.88 apply zenon_Ha6. apply refl_equal. % 6.67/6.88 apply zenon_Ha6. apply refl_equal. % 6.67/6.88 apply zenon_Hde. apply refl_equal. % 6.67/6.88 cut ((gt (n4) (succ zenon_TE_dq)) = (gt (succ (succ (succ (succ (n0))))) (succ zenon_TE_dq))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_H11c. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_He5. % 6.67/6.88 cut (((succ zenon_TE_dq) = (succ zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_Hde]. % 6.67/6.88 cut (((n4) = (succ (succ (succ (succ (n0))))))); [idtac | apply NNPP; zenon_intro zenon_Ha7]. % 6.67/6.88 congruence. % 6.67/6.88 elim (classic ((succ (succ (succ (succ (n0))))) = (succ (succ (succ (succ (n0))))))); [ zenon_intro zenon_Ha8 | zenon_intro zenon_Ha9 ]. % 6.67/6.88 cut (((succ (succ (succ (succ (n0))))) = (succ (succ (succ (succ (n0)))))) = ((n4) = (succ (succ (succ (succ (n0))))))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Ha7. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Ha8. % 6.67/6.88 cut (((succ (succ (succ (succ (n0))))) = (succ (succ (succ (succ (n0))))))); [idtac | apply NNPP; zenon_intro zenon_Ha9]. % 6.67/6.88 cut (((succ (succ (succ (succ (n0))))) = (n4))); [idtac | apply NNPP; zenon_intro zenon_Haa]. % 6.67/6.88 congruence. % 6.67/6.88 exact (zenon_Haa successor_4). % 6.67/6.88 apply zenon_Ha9. apply refl_equal. % 6.67/6.88 apply zenon_Ha9. apply refl_equal. % 6.67/6.88 apply zenon_Hde. apply refl_equal. % 6.67/6.88 apply (zenon_L22_ zenon_TE_dq); trivial. % 6.67/6.88 elim (classic ((n0) = zenon_TE_dq)); [ zenon_intro zenon_H11d | zenon_intro zenon_H6d ]. % 6.67/6.88 cut ((gt (succ zenon_TE_dq) (n0)) = (gt (succ (n3)) zenon_TE_dq)). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Ha0. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_H5c. % 6.67/6.88 cut (((n0) = zenon_TE_dq)); [idtac | apply NNPP; zenon_intro zenon_H6d]. % 6.67/6.88 cut (((succ zenon_TE_dq) = (succ (n3)))); [idtac | apply NNPP; zenon_intro zenon_H11e]. % 6.67/6.88 congruence. % 6.67/6.88 apply (zenon_notand_s _ _ zenon_H118); [ zenon_intro zenon_H120 | zenon_intro zenon_H11f ]. % 6.67/6.88 apply zenon_H120. zenon_intro zenon_H121. % 6.67/6.88 elim (classic ((succ (n3)) = (succ (n3)))); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Ha6 ]. % 6.67/6.88 cut (((succ (n3)) = (succ (n3))) = ((succ zenon_TE_dq) = (succ (n3)))). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_H11e. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_Ha5. % 6.67/6.88 cut (((succ (n3)) = (succ (n3)))); [idtac | apply NNPP; zenon_intro zenon_Ha6]. % 6.67/6.88 cut (((succ (n3)) = (succ zenon_TE_dq))); [idtac | apply NNPP; zenon_intro zenon_H11a]. % 6.67/6.88 congruence. % 6.67/6.88 exact (zenon_H11a zenon_H121). % 6.67/6.88 apply zenon_Ha6. apply refl_equal. % 6.67/6.88 apply zenon_Ha6. apply refl_equal. % 6.67/6.88 apply zenon_H11f. zenon_intro zenon_H122. % 6.67/6.88 generalize (zenon_H82 (succ (n3))). zenon_intro zenon_H123. % 6.67/6.88 generalize (zenon_H123 (succ zenon_TE_dq)). zenon_intro zenon_H124. % 6.67/6.88 generalize (zenon_H124 (n0)). zenon_intro zenon_H125. % 6.67/6.88 apply (zenon_imply_s _ _ zenon_H125); [ zenon_intro zenon_H119 | zenon_intro zenon_H126 ]. % 6.67/6.88 exact (zenon_H119 zenon_H122). % 6.67/6.88 apply (zenon_imply_s _ _ zenon_H126); [ zenon_intro zenon_H62 | zenon_intro zenon_H127 ]. % 6.67/6.88 exact (zenon_H62 zenon_H5c). % 6.67/6.88 cut ((gt (succ (n3)) (n0)) = (gt (succ (n3)) zenon_TE_dq)). % 6.67/6.88 intro zenon_D_pnotp. % 6.67/6.88 apply zenon_Ha0. % 6.67/6.88 rewrite <- zenon_D_pnotp. % 6.67/6.88 exact zenon_H127. % 6.67/6.88 cut (((n0) = zenon_TE_dq)); [idtac | apply NNPP; zenon_intro zenon_H6d]. % 6.67/6.88 cut (((succ (n3)) = (succ (n3)))); [idtac | apply NNPP; zenon_intro zenon_Ha6]. % 6.67/6.88 congruence. % 6.67/6.88 apply zenon_Ha6. apply refl_equal. % 6.67/6.88 exact (zenon_H6d zenon_H11d). % 6.67/6.88 exact (zenon_H6d zenon_H11d). % 6.67/6.88 apply (zenon_L12_ zenon_TE_dq); trivial. % 6.67/6.88 exact (zenon_Hba zenon_Hbd). % 6.67/6.88 apply (zenon_or_s _ _ zenon_Hb8); [ zenon_intro zenon_H77 | zenon_intro zenon_Hbe ]. % 6.67/6.88 apply (zenon_L23_ zenon_TE_dq); trivial. % 6.67/6.88 apply (zenon_or_s _ _ zenon_Hbe); [ zenon_intro zenon_H79 | zenon_intro zenon_Hbf ]. % 6.67/6.88 apply (zenon_L13_ zenon_TE_dq); trivial. % 6.67/6.88 apply (zenon_or_s _ _ zenon_Hbf); [ zenon_intro zenon_H7b | zenon_intro zenon_H7d ]. % 6.67/6.88 apply (zenon_L14_ zenon_TE_dq); trivial. % 6.67/6.88 apply (zenon_L15_ zenon_TE_dq); trivial. % 6.67/6.88 apply zenon_Hed. zenon_intro zenon_Tx_lk. apply NNPP. zenon_intro zenon_H129. % 6.67/6.88 apply zenon_H129. zenon_intro zenon_Ty_lm. apply NNPP. zenon_intro zenon_H12b. % 6.67/6.88 apply zenon_H12b. zenon_intro zenon_Tz_lo. apply NNPP. zenon_intro zenon_H12d. % 6.67/6.88 apply (zenon_notimply_s _ _ zenon_H12d). zenon_intro zenon_H12f. zenon_intro zenon_H12e. % 6.67/6.88 apply (zenon_notimply_s _ _ zenon_H12e). zenon_intro zenon_H131. zenon_intro zenon_H130. % 6.67/6.88 generalize (transitivity_gt zenon_Tx_lk). zenon_intro zenon_H132. % 6.67/6.88 generalize (zenon_H132 zenon_Ty_lm). zenon_intro zenon_H133. % 6.67/6.88 generalize (zenon_H133 zenon_Tz_lo). zenon_intro zenon_H134. % 6.67/6.88 apply (zenon_imply_s _ _ zenon_H134); [ zenon_intro zenon_H136 | zenon_intro zenon_H135 ]. % 6.67/6.88 apply (zenon_notand_s _ _ zenon_H136); [ zenon_intro zenon_H138 | zenon_intro zenon_H137 ]. % 6.67/6.88 exact (zenon_H138 zenon_H12f). % 6.67/6.88 exact (zenon_H137 zenon_H131). % 6.67/6.88 exact (zenon_H130 zenon_H135). % 6.67/6.88 Qed. % 6.67/6.88 % SZS output end Proof % 6.67/6.88 (* END-PROOF *) % 6.67/6.88 nodes searched: 518512 % 6.67/6.88 max branch formulas: 3213 % 6.67/6.88 proof nodes created: 1230 % 6.67/6.88 formulas created: 311718 % 6.67/6.88 %------------------------------------------------------------------------------