%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : LAT380+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n005.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 : Sun Jul 17 07:24:26 EDT 2022 % Result : Theorem 0.53s 0.70s % Output : Proof 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : LAT380+1 : TPTP v8.1.0. Released v3.4.0. % 0.06/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n005.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 : Thu Jun 30 06:34:07 EDT 2022 % 0.12/0.33 % CPUTime : % 0.53/0.70 Zenon warning: unused variable (B : zenon_U) in reflexivity_r1_tarski % 0.53/0.70 (* PROOF-FOUND *) % 0.53/0.70 % SZS status Theorem % 0.53/0.70 (* BEGIN-PROOF *) % 0.53/0.70 % SZS output start Proof % 0.53/0.70 Theorem t71_waybel34 : (forall A : zenon_U, (((v2_orders_2 A)/\((v3_orders_2 A)/\((v4_orders_2 A)/\((v1_lattice3 A)/\((v2_lattice3 A)/\((v3_lattice3 A)/\(l1_orders_2 A)))))))->(forall B : zenon_U, (((v2_orders_2 B)/\((v3_orders_2 B)/\((v4_orders_2 B)/\((v1_lattice3 B)/\((v2_lattice3 B)/\((v3_lattice3 B)/\(l1_orders_2 B)))))))->((v2_waybel_8 B)->(forall C : zenon_U, (((v1_funct_1 C)/\((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B))/\((v17_waybel_0 C A B)/\(m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))->((v22_waybel_0 C A B)<->((v1_funct_1 (k8_relset_1 (u1_struct_0 B) (u1_struct_0 A) (k1_waybel34 A B C) (u1_struct_0 (k1_waybel_8 B))))/\((v1_funct_2 (k8_relset_1 (u1_struct_0 B) (u1_struct_0 A) (k1_waybel34 A B C) (u1_struct_0 (k1_waybel_8 B))) (u1_struct_0 (k1_waybel_8 B)) (u1_struct_0 (k1_waybel_8 A)))/\((v4_waybel34 (k8_relset_1 (u1_struct_0 B) (u1_struct_0 A) (k1_waybel34 A B C) (u1_struct_0 (k1_waybel_8 B))) (k1_waybel_8 B) (k1_waybel_8 A))/\(m2_relset_1 (k8_relset_1 (u1_struct_0 B) (u1_struct_0 A) (k1_waybel34 A B C) (u1_struct_0 (k1_waybel_8 B))) (u1_struct_0 (k1_waybel_8 B)) (u1_struct_0 (k1_waybel_8 A)))))))))))))). % 0.53/0.70 Proof. % 0.53/0.70 assert (zenon_L1_ : forall (zenon_TB_fd : zenon_U) (zenon_TA_fe : zenon_U) (zenon_TC_ff : zenon_U), (m1_relset_1 zenon_TC_ff (u1_struct_0 zenon_TA_fe) (u1_struct_0 zenon_TB_fd)) -> (~(m2_relset_1 zenon_TC_ff (u1_struct_0 zenon_TA_fe) (u1_struct_0 zenon_TB_fd))) -> False). % 0.53/0.70 do 3 intro. intros zenon_H83 zenon_H84. % 0.53/0.70 generalize (redefinition_m2_relset_1 (u1_struct_0 zenon_TA_fe)). zenon_intro zenon_H88. % 0.53/0.70 generalize (zenon_H88 (u1_struct_0 zenon_TB_fd)). zenon_intro zenon_H89. % 0.53/0.70 generalize (zenon_H89 zenon_TC_ff). zenon_intro zenon_H8a. % 0.53/0.70 apply (zenon_equiv_s _ _ zenon_H8a); [ zenon_intro zenon_H84; zenon_intro zenon_H8c | zenon_intro zenon_H8b; zenon_intro zenon_H83 ]. % 0.53/0.70 exact (zenon_H8c zenon_H83). % 0.53/0.70 exact (zenon_H84 zenon_H8b). % 0.53/0.70 (* end of lemma zenon_L1_ *) % 0.53/0.70 assert (zenon_L2_ : forall (zenon_TC_ff : zenon_U) (zenon_TB_fd : zenon_U) (zenon_TA_fe : zenon_U), (v2_orders_2 zenon_TA_fe) -> (v3_orders_2 zenon_TA_fe) -> (v4_orders_2 zenon_TA_fe) -> (v1_lattice3 zenon_TA_fe) -> (v2_lattice3 zenon_TA_fe) -> (v3_lattice3 zenon_TA_fe) -> (l1_orders_2 zenon_TA_fe) -> (v2_orders_2 zenon_TB_fd) -> (v3_orders_2 zenon_TB_fd) -> (v4_orders_2 zenon_TB_fd) -> (v1_lattice3 zenon_TB_fd) -> (v2_lattice3 zenon_TB_fd) -> (v3_lattice3 zenon_TB_fd) -> (l1_orders_2 zenon_TB_fd) -> (v1_funct_1 zenon_TC_ff) -> (v1_funct_2 zenon_TC_ff (u1_struct_0 zenon_TA_fe) (u1_struct_0 zenon_TB_fd)) -> (v17_waybel_0 zenon_TC_ff zenon_TA_fe zenon_TB_fd) -> (m1_relset_1 zenon_TC_ff (u1_struct_0 zenon_TA_fe) (u1_struct_0 zenon_TB_fd)) -> (~(v1_funct_1 (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff))) -> False). % 0.53/0.70 do 3 intro. intros zenon_H8d zenon_H8e zenon_H8f zenon_H90 zenon_H91 zenon_H92 zenon_H93 zenon_H94 zenon_H95 zenon_H96 zenon_H97 zenon_H98 zenon_H99 zenon_H9a zenon_H9b zenon_H9c zenon_H9d zenon_H83 zenon_H9e. % 0.53/0.70 generalize (fc1_waybel34 zenon_TA_fe). zenon_intro zenon_H9f. % 0.53/0.70 generalize (zenon_H9f zenon_TB_fd). zenon_intro zenon_Ha0. % 0.53/0.70 generalize (zenon_Ha0 zenon_TC_ff). zenon_intro zenon_Ha1. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_Ha1); [ zenon_intro zenon_Ha3 | zenon_intro zenon_Ha2 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Ha3); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Ha4 ]. % 0.53/0.70 exact (zenon_Ha5 zenon_H8d). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Ha4); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Ha6 ]. % 0.53/0.70 exact (zenon_Ha7 zenon_H8e). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Ha6); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Ha8 ]. % 0.53/0.70 exact (zenon_Ha9 zenon_H8f). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Ha8); [ zenon_intro zenon_Hab | zenon_intro zenon_Haa ]. % 0.53/0.70 exact (zenon_Hab zenon_H90). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Haa); [ zenon_intro zenon_Had | zenon_intro zenon_Hac ]. % 0.53/0.70 exact (zenon_Had zenon_H91). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hac); [ zenon_intro zenon_Haf | zenon_intro zenon_Hae ]. % 0.53/0.70 exact (zenon_Haf zenon_H92). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hae); [ zenon_intro zenon_Hb1 | zenon_intro zenon_Hb0 ]. % 0.53/0.70 exact (zenon_Hb1 zenon_H93). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hb0); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hb2 ]. % 0.53/0.70 exact (zenon_Hb3 zenon_H94). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hb2); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hb4 ]. % 0.53/0.70 exact (zenon_Hb5 zenon_H95). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hb4); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb6 ]. % 0.53/0.70 exact (zenon_Hb7 zenon_H96). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hb6); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hb8 ]. % 0.53/0.70 exact (zenon_Hb9 zenon_H97). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hb8); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hba ]. % 0.53/0.70 exact (zenon_Hbb zenon_H98). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hba); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hbc ]. % 0.53/0.70 exact (zenon_Hbd zenon_H99). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hbc); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hbe ]. % 0.53/0.70 exact (zenon_Hbf zenon_H9a). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hbe); [ zenon_intro zenon_Hc1 | zenon_intro zenon_Hc0 ]. % 0.53/0.70 exact (zenon_Hc1 zenon_H9b). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hc0); [ zenon_intro zenon_Hc3 | zenon_intro zenon_Hc2 ]. % 0.53/0.70 exact (zenon_Hc3 zenon_H9c). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hc2); [ zenon_intro zenon_Hc4 | zenon_intro zenon_H8c ]. % 0.53/0.70 exact (zenon_Hc4 zenon_H9d). % 0.53/0.70 exact (zenon_H8c zenon_H83). % 0.53/0.70 apply (zenon_and_s _ _ zenon_Ha2). zenon_intro zenon_Hc6. zenon_intro zenon_Hc5. % 0.53/0.70 apply (zenon_and_s _ _ zenon_Hc5). zenon_intro zenon_Hc8. zenon_intro zenon_Hc7. % 0.53/0.70 exact (zenon_H9e zenon_Hc8). % 0.53/0.70 (* end of lemma zenon_L2_ *) % 0.53/0.70 assert (zenon_L3_ : forall (zenon_TC_ff : zenon_U) (zenon_TB_fd : zenon_U) (zenon_TA_fe : zenon_U), (v2_orders_2 zenon_TA_fe) -> (v3_orders_2 zenon_TA_fe) -> (v4_orders_2 zenon_TA_fe) -> (v1_lattice3 zenon_TA_fe) -> (v2_lattice3 zenon_TA_fe) -> (v3_lattice3 zenon_TA_fe) -> (l1_orders_2 zenon_TA_fe) -> (v2_orders_2 zenon_TB_fd) -> (v3_orders_2 zenon_TB_fd) -> (v4_orders_2 zenon_TB_fd) -> (v1_lattice3 zenon_TB_fd) -> (v2_lattice3 zenon_TB_fd) -> (v3_lattice3 zenon_TB_fd) -> (l1_orders_2 zenon_TB_fd) -> (v1_funct_1 zenon_TC_ff) -> (v1_funct_2 zenon_TC_ff (u1_struct_0 zenon_TA_fe) (u1_struct_0 zenon_TB_fd)) -> (v17_waybel_0 zenon_TC_ff zenon_TA_fe zenon_TB_fd) -> (m1_relset_1 zenon_TC_ff (u1_struct_0 zenon_TA_fe) (u1_struct_0 zenon_TB_fd)) -> (~(v1_funct_2 (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff) (u1_struct_0 zenon_TB_fd) (u1_struct_0 zenon_TA_fe))) -> False). % 0.53/0.70 do 3 intro. intros zenon_H8d zenon_H8e zenon_H8f zenon_H90 zenon_H91 zenon_H92 zenon_H93 zenon_H94 zenon_H95 zenon_H96 zenon_H97 zenon_H98 zenon_H99 zenon_H9a zenon_H9b zenon_H9c zenon_H9d zenon_H83 zenon_Hc9. % 0.53/0.70 generalize (fc1_waybel34 zenon_TA_fe). zenon_intro zenon_H9f. % 0.53/0.70 generalize (zenon_H9f zenon_TB_fd). zenon_intro zenon_Ha0. % 0.53/0.70 generalize (zenon_Ha0 zenon_TC_ff). zenon_intro zenon_Ha1. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_Ha1); [ zenon_intro zenon_Ha3 | zenon_intro zenon_Ha2 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Ha3); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Ha4 ]. % 0.53/0.70 exact (zenon_Ha5 zenon_H8d). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Ha4); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Ha6 ]. % 0.53/0.70 exact (zenon_Ha7 zenon_H8e). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Ha6); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Ha8 ]. % 0.53/0.70 exact (zenon_Ha9 zenon_H8f). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Ha8); [ zenon_intro zenon_Hab | zenon_intro zenon_Haa ]. % 0.53/0.70 exact (zenon_Hab zenon_H90). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Haa); [ zenon_intro zenon_Had | zenon_intro zenon_Hac ]. % 0.53/0.70 exact (zenon_Had zenon_H91). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hac); [ zenon_intro zenon_Haf | zenon_intro zenon_Hae ]. % 0.53/0.70 exact (zenon_Haf zenon_H92). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hae); [ zenon_intro zenon_Hb1 | zenon_intro zenon_Hb0 ]. % 0.53/0.70 exact (zenon_Hb1 zenon_H93). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hb0); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hb2 ]. % 0.53/0.70 exact (zenon_Hb3 zenon_H94). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hb2); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hb4 ]. % 0.53/0.70 exact (zenon_Hb5 zenon_H95). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hb4); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb6 ]. % 0.53/0.70 exact (zenon_Hb7 zenon_H96). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hb6); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hb8 ]. % 0.53/0.70 exact (zenon_Hb9 zenon_H97). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hb8); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hba ]. % 0.53/0.70 exact (zenon_Hbb zenon_H98). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hba); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hbc ]. % 0.53/0.70 exact (zenon_Hbd zenon_H99). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hbc); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hbe ]. % 0.53/0.70 exact (zenon_Hbf zenon_H9a). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hbe); [ zenon_intro zenon_Hc1 | zenon_intro zenon_Hc0 ]. % 0.53/0.70 exact (zenon_Hc1 zenon_H9b). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hc0); [ zenon_intro zenon_Hc3 | zenon_intro zenon_Hc2 ]. % 0.53/0.70 exact (zenon_Hc3 zenon_H9c). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hc2); [ zenon_intro zenon_Hc4 | zenon_intro zenon_H8c ]. % 0.53/0.70 exact (zenon_Hc4 zenon_H9d). % 0.53/0.70 exact (zenon_H8c zenon_H83). % 0.53/0.70 apply (zenon_and_s _ _ zenon_Ha2). zenon_intro zenon_Hc6. zenon_intro zenon_Hc5. % 0.53/0.70 apply (zenon_and_s _ _ zenon_Hc5). zenon_intro zenon_Hc8. zenon_intro zenon_Hc7. % 0.53/0.70 apply (zenon_and_s _ _ zenon_Hc7). zenon_intro zenon_Hcb. zenon_intro zenon_Hca. % 0.53/0.70 apply (zenon_and_s _ _ zenon_Hca). zenon_intro zenon_Hcd. zenon_intro zenon_Hcc. % 0.53/0.70 exact (zenon_Hc9 zenon_Hcd). % 0.53/0.70 (* end of lemma zenon_L3_ *) % 0.53/0.70 assert (zenon_L4_ : forall (zenon_TC_ff : zenon_U) (zenon_TB_fd : zenon_U) (zenon_TA_fe : zenon_U), (v2_orders_2 zenon_TA_fe) -> (v3_orders_2 zenon_TA_fe) -> (v4_orders_2 zenon_TA_fe) -> (v1_lattice3 zenon_TA_fe) -> (v2_lattice3 zenon_TA_fe) -> (v3_lattice3 zenon_TA_fe) -> (l1_orders_2 zenon_TA_fe) -> (v2_orders_2 zenon_TB_fd) -> (v3_orders_2 zenon_TB_fd) -> (v4_orders_2 zenon_TB_fd) -> (v1_lattice3 zenon_TB_fd) -> (v2_lattice3 zenon_TB_fd) -> (v3_lattice3 zenon_TB_fd) -> (l1_orders_2 zenon_TB_fd) -> (v1_funct_1 zenon_TC_ff) -> (v1_funct_2 zenon_TC_ff (u1_struct_0 zenon_TA_fe) (u1_struct_0 zenon_TB_fd)) -> (v17_waybel_0 zenon_TC_ff zenon_TA_fe zenon_TB_fd) -> (m1_relset_1 zenon_TC_ff (u1_struct_0 zenon_TA_fe) (u1_struct_0 zenon_TB_fd)) -> (~(v18_waybel_0 (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff) zenon_TB_fd zenon_TA_fe)) -> False). % 0.53/0.70 do 3 intro. intros zenon_H8d zenon_H8e zenon_H8f zenon_H90 zenon_H91 zenon_H92 zenon_H93 zenon_H94 zenon_H95 zenon_H96 zenon_H97 zenon_H98 zenon_H99 zenon_H9a zenon_H9b zenon_H9c zenon_H9d zenon_H83 zenon_Hce. % 0.53/0.70 generalize (fc1_waybel34 zenon_TA_fe). zenon_intro zenon_H9f. % 0.53/0.70 generalize (zenon_H9f zenon_TB_fd). zenon_intro zenon_Ha0. % 0.53/0.70 generalize (zenon_Ha0 zenon_TC_ff). zenon_intro zenon_Ha1. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_Ha1); [ zenon_intro zenon_Ha3 | zenon_intro zenon_Ha2 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Ha3); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Ha4 ]. % 0.53/0.70 exact (zenon_Ha5 zenon_H8d). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Ha4); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Ha6 ]. % 0.53/0.70 exact (zenon_Ha7 zenon_H8e). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Ha6); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Ha8 ]. % 0.53/0.70 exact (zenon_Ha9 zenon_H8f). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Ha8); [ zenon_intro zenon_Hab | zenon_intro zenon_Haa ]. % 0.53/0.70 exact (zenon_Hab zenon_H90). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Haa); [ zenon_intro zenon_Had | zenon_intro zenon_Hac ]. % 0.53/0.70 exact (zenon_Had zenon_H91). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hac); [ zenon_intro zenon_Haf | zenon_intro zenon_Hae ]. % 0.53/0.70 exact (zenon_Haf zenon_H92). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hae); [ zenon_intro zenon_Hb1 | zenon_intro zenon_Hb0 ]. % 0.53/0.70 exact (zenon_Hb1 zenon_H93). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hb0); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hb2 ]. % 0.53/0.70 exact (zenon_Hb3 zenon_H94). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hb2); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hb4 ]. % 0.53/0.70 exact (zenon_Hb5 zenon_H95). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hb4); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb6 ]. % 0.53/0.70 exact (zenon_Hb7 zenon_H96). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hb6); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hb8 ]. % 0.53/0.70 exact (zenon_Hb9 zenon_H97). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hb8); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hba ]. % 0.53/0.70 exact (zenon_Hbb zenon_H98). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hba); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hbc ]. % 0.53/0.70 exact (zenon_Hbd zenon_H99). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hbc); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hbe ]. % 0.53/0.70 exact (zenon_Hbf zenon_H9a). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hbe); [ zenon_intro zenon_Hc1 | zenon_intro zenon_Hc0 ]. % 0.53/0.70 exact (zenon_Hc1 zenon_H9b). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hc0); [ zenon_intro zenon_Hc3 | zenon_intro zenon_Hc2 ]. % 0.53/0.70 exact (zenon_Hc3 zenon_H9c). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hc2); [ zenon_intro zenon_Hc4 | zenon_intro zenon_H8c ]. % 0.53/0.70 exact (zenon_Hc4 zenon_H9d). % 0.53/0.70 exact (zenon_H8c zenon_H83). % 0.53/0.70 apply (zenon_and_s _ _ zenon_Ha2). zenon_intro zenon_Hc6. zenon_intro zenon_Hc5. % 0.53/0.70 apply (zenon_and_s _ _ zenon_Hc5). zenon_intro zenon_Hc8. zenon_intro zenon_Hc7. % 0.53/0.70 apply (zenon_and_s _ _ zenon_Hc7). zenon_intro zenon_Hcb. zenon_intro zenon_Hca. % 0.53/0.70 apply (zenon_and_s _ _ zenon_Hca). zenon_intro zenon_Hcd. zenon_intro zenon_Hcc. % 0.53/0.70 apply (zenon_and_s _ _ zenon_Hcc). zenon_intro zenon_Hd0. zenon_intro zenon_Hcf. % 0.53/0.70 apply (zenon_and_s _ _ zenon_Hcf). zenon_intro zenon_Hd2. zenon_intro zenon_Hd1. % 0.53/0.70 exact (zenon_Hce zenon_Hd2). % 0.53/0.70 (* end of lemma zenon_L4_ *) % 0.53/0.70 assert (zenon_L5_ : forall (zenon_TB_fd : zenon_U) (zenon_TA_fe : zenon_U) (zenon_TC_ff : zenon_U), (m1_relset_1 zenon_TC_ff (u1_struct_0 zenon_TA_fe) (u1_struct_0 zenon_TB_fd)) -> (v1_funct_2 zenon_TC_ff (u1_struct_0 zenon_TA_fe) (u1_struct_0 zenon_TB_fd)) -> (v1_funct_1 zenon_TC_ff) -> (l1_orders_2 zenon_TB_fd) -> (v2_lattice3 zenon_TB_fd) -> (v1_lattice3 zenon_TB_fd) -> (v4_orders_2 zenon_TB_fd) -> (v3_orders_2 zenon_TB_fd) -> (v2_orders_2 zenon_TB_fd) -> (l1_orders_2 zenon_TA_fe) -> (v2_lattice3 zenon_TA_fe) -> (v1_lattice3 zenon_TA_fe) -> (v4_orders_2 zenon_TA_fe) -> (v3_orders_2 zenon_TA_fe) -> (v2_orders_2 zenon_TA_fe) -> (~(m2_relset_1 (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff) (u1_struct_0 zenon_TB_fd) (u1_struct_0 zenon_TA_fe))) -> False). % 0.53/0.70 do 3 intro. intros zenon_H83 zenon_H9c zenon_H9b zenon_H9a zenon_H98 zenon_H97 zenon_H96 zenon_H95 zenon_H94 zenon_H93 zenon_H91 zenon_H90 zenon_H8f zenon_H8e zenon_H8d zenon_Hd3. % 0.53/0.70 generalize (redefinition_m2_relset_1 (u1_struct_0 zenon_TB_fd)). zenon_intro zenon_Hd4. % 0.53/0.70 generalize (zenon_Hd4 (u1_struct_0 zenon_TA_fe)). zenon_intro zenon_Hd5. % 0.53/0.70 generalize (zenon_Hd5 (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff)). zenon_intro zenon_Hd6. % 0.53/0.70 apply (zenon_equiv_s _ _ zenon_Hd6); [ zenon_intro zenon_Hd3; zenon_intro zenon_Hd9 | zenon_intro zenon_Hd8; zenon_intro zenon_Hd7 ]. % 0.53/0.70 generalize (dt_k1_waybel34 zenon_TA_fe). zenon_intro zenon_Hda. % 0.53/0.70 generalize (zenon_Hda zenon_TB_fd). zenon_intro zenon_Hdb. % 0.53/0.70 generalize (zenon_Hdb zenon_TC_ff). zenon_intro zenon_Hdc. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_Hdc); [ zenon_intro zenon_Hde | zenon_intro zenon_Hdd ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hde); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Hdf ]. % 0.53/0.70 exact (zenon_Ha5 zenon_H8d). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hdf); [ zenon_intro zenon_Ha7 | zenon_intro zenon_He0 ]. % 0.53/0.70 exact (zenon_Ha7 zenon_H8e). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_He0); [ zenon_intro zenon_Ha9 | zenon_intro zenon_He1 ]. % 0.53/0.70 exact (zenon_Ha9 zenon_H8f). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_He1); [ zenon_intro zenon_Hab | zenon_intro zenon_He2 ]. % 0.53/0.70 exact (zenon_Hab zenon_H90). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_He2); [ zenon_intro zenon_Had | zenon_intro zenon_He3 ]. % 0.53/0.70 exact (zenon_Had zenon_H91). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_He3); [ zenon_intro zenon_Hb1 | zenon_intro zenon_He4 ]. % 0.53/0.70 exact (zenon_Hb1 zenon_H93). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_He4); [ zenon_intro zenon_Hb3 | zenon_intro zenon_He5 ]. % 0.53/0.70 exact (zenon_Hb3 zenon_H94). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_He5); [ zenon_intro zenon_Hb5 | zenon_intro zenon_He6 ]. % 0.53/0.70 exact (zenon_Hb5 zenon_H95). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_He6); [ zenon_intro zenon_Hb7 | zenon_intro zenon_He7 ]. % 0.53/0.70 exact (zenon_Hb7 zenon_H96). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_He7); [ zenon_intro zenon_Hb9 | zenon_intro zenon_He8 ]. % 0.53/0.70 exact (zenon_Hb9 zenon_H97). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_He8); [ zenon_intro zenon_Hbb | zenon_intro zenon_He9 ]. % 0.53/0.70 exact (zenon_Hbb zenon_H98). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_He9); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hea ]. % 0.53/0.70 exact (zenon_Hbf zenon_H9a). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hea); [ zenon_intro zenon_Hc1 | zenon_intro zenon_Heb ]. % 0.53/0.70 exact (zenon_Hc1 zenon_H9b). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Heb); [ zenon_intro zenon_Hc3 | zenon_intro zenon_H8c ]. % 0.53/0.70 exact (zenon_Hc3 zenon_H9c). % 0.53/0.70 exact (zenon_H8c zenon_H83). % 0.53/0.70 apply (zenon_and_s _ _ zenon_Hdd). zenon_intro zenon_Hc8. zenon_intro zenon_Hec. % 0.53/0.70 apply (zenon_and_s _ _ zenon_Hec). zenon_intro zenon_Hcd. zenon_intro zenon_Hd8. % 0.53/0.70 generalize (redefinition_m2_relset_1 (u1_struct_0 zenon_TB_fd)). zenon_intro zenon_Hd4. % 0.53/0.70 generalize (zenon_Hd4 (u1_struct_0 zenon_TA_fe)). zenon_intro zenon_Hd5. % 0.53/0.70 generalize (zenon_Hd5 (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff)). zenon_intro zenon_Hd6. % 0.53/0.70 apply (zenon_equiv_s _ _ zenon_Hd6); [ zenon_intro zenon_Hd3; zenon_intro zenon_Hd9 | zenon_intro zenon_Hd8; zenon_intro zenon_Hd7 ]. % 0.53/0.70 exact (zenon_Hd3 zenon_Hd8). % 0.53/0.70 exact (zenon_Hd9 zenon_Hd7). % 0.53/0.70 exact (zenon_Hd3 zenon_Hd8). % 0.53/0.70 (* end of lemma zenon_L5_ *) % 0.53/0.70 assert (zenon_L6_ : forall (zenon_TC_ff : zenon_U) (zenon_TB_fd : zenon_U) (zenon_TA_fe : zenon_U), (v2_orders_2 zenon_TA_fe) -> (v3_orders_2 zenon_TA_fe) -> (v4_orders_2 zenon_TA_fe) -> (v1_lattice3 zenon_TA_fe) -> (v2_lattice3 zenon_TA_fe) -> (v3_lattice3 zenon_TA_fe) -> (l1_orders_2 zenon_TA_fe) -> (v2_orders_2 zenon_TB_fd) -> (v3_orders_2 zenon_TB_fd) -> (v4_orders_2 zenon_TB_fd) -> (v1_lattice3 zenon_TB_fd) -> (v2_lattice3 zenon_TB_fd) -> (v3_lattice3 zenon_TB_fd) -> (l1_orders_2 zenon_TB_fd) -> (v1_funct_1 zenon_TC_ff) -> (v1_funct_2 zenon_TC_ff (u1_struct_0 zenon_TA_fe) (u1_struct_0 zenon_TB_fd)) -> (v17_waybel_0 zenon_TC_ff zenon_TA_fe zenon_TB_fd) -> (m1_relset_1 zenon_TC_ff (u1_struct_0 zenon_TA_fe) (u1_struct_0 zenon_TB_fd)) -> (v22_waybel_0 zenon_TC_ff zenon_TA_fe zenon_TB_fd) -> (~(v3_waybel34 (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff) zenon_TB_fd zenon_TA_fe)) -> False). % 0.53/0.70 do 3 intro. intros zenon_H8d zenon_H8e zenon_H8f zenon_H90 zenon_H91 zenon_H92 zenon_H93 zenon_H94 zenon_H95 zenon_H96 zenon_H97 zenon_H98 zenon_H99 zenon_H9a zenon_H9b zenon_H9c zenon_H9d zenon_H83 zenon_Hed zenon_Hee. % 0.53/0.70 generalize (t60_waybel34 zenon_TA_fe). zenon_intro zenon_Hef. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_Hef); [ zenon_intro zenon_Hf1 | zenon_intro zenon_Hf0 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf1); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Hf2 ]. % 0.53/0.70 exact (zenon_Ha5 zenon_H8d). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf2); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Hf3 ]. % 0.53/0.70 exact (zenon_Ha7 zenon_H8e). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf3); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Hf4 ]. % 0.53/0.70 exact (zenon_Ha9 zenon_H8f). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf4); [ zenon_intro zenon_Hab | zenon_intro zenon_Hf5 ]. % 0.53/0.70 exact (zenon_Hab zenon_H90). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf5); [ zenon_intro zenon_Had | zenon_intro zenon_Hf6 ]. % 0.53/0.70 exact (zenon_Had zenon_H91). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf6); [ zenon_intro zenon_Haf | zenon_intro zenon_Hb1 ]. % 0.53/0.70 exact (zenon_Haf zenon_H92). % 0.53/0.70 exact (zenon_Hb1 zenon_H93). % 0.53/0.70 generalize (zenon_Hf0 zenon_TB_fd). zenon_intro zenon_Hf7. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_Hf7); [ zenon_intro zenon_Hf9 | zenon_intro zenon_Hf8 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf9); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hfa ]. % 0.53/0.70 exact (zenon_Hb3 zenon_H94). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfa); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hfb ]. % 0.53/0.70 exact (zenon_Hb5 zenon_H95). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfb); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hfc ]. % 0.53/0.70 exact (zenon_Hb7 zenon_H96). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfc); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hfd ]. % 0.53/0.70 exact (zenon_Hb9 zenon_H97). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfd); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hfe ]. % 0.53/0.70 exact (zenon_Hbb zenon_H98). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfe); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hbf ]. % 0.53/0.70 exact (zenon_Hbd zenon_H99). % 0.53/0.70 exact (zenon_Hbf zenon_H9a). % 0.53/0.70 generalize (zenon_Hf8 (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff)). zenon_intro zenon_Hff. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_Hff); [ zenon_intro zenon_H101 | zenon_intro zenon_H100 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H101); [ zenon_intro zenon_H9e | zenon_intro zenon_H102 ]. % 0.53/0.70 apply (zenon_L2_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H102); [ zenon_intro zenon_Hc9 | zenon_intro zenon_H103 ]. % 0.53/0.70 apply (zenon_L3_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H103); [ zenon_intro zenon_Hce | zenon_intro zenon_Hd3 ]. % 0.53/0.70 apply (zenon_L4_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_L5_ zenon_TB_fd zenon_TA_fe zenon_TC_ff); trivial. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H100); [ zenon_intro zenon_H105 | zenon_intro zenon_H104 ]. % 0.53/0.70 generalize (t24_waybel34 zenon_TA_fe). zenon_intro zenon_H106. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H106); [ zenon_intro zenon_Hf1 | zenon_intro zenon_H107 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf1); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Hf2 ]. % 0.53/0.70 exact (zenon_Ha5 zenon_H8d). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf2); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Hf3 ]. % 0.53/0.70 exact (zenon_Ha7 zenon_H8e). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf3); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Hf4 ]. % 0.53/0.70 exact (zenon_Ha9 zenon_H8f). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf4); [ zenon_intro zenon_Hab | zenon_intro zenon_Hf5 ]. % 0.53/0.70 exact (zenon_Hab zenon_H90). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf5); [ zenon_intro zenon_Had | zenon_intro zenon_Hf6 ]. % 0.53/0.70 exact (zenon_Had zenon_H91). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf6); [ zenon_intro zenon_Haf | zenon_intro zenon_Hb1 ]. % 0.53/0.70 exact (zenon_Haf zenon_H92). % 0.53/0.70 exact (zenon_Hb1 zenon_H93). % 0.53/0.70 generalize (zenon_H107 zenon_TB_fd). zenon_intro zenon_H108. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H108); [ zenon_intro zenon_Hf9 | zenon_intro zenon_H109 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf9); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hfa ]. % 0.53/0.70 exact (zenon_Hb3 zenon_H94). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfa); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hfb ]. % 0.53/0.70 exact (zenon_Hb5 zenon_H95). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfb); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hfc ]. % 0.53/0.70 exact (zenon_Hb7 zenon_H96). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfc); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hfd ]. % 0.53/0.70 exact (zenon_Hb9 zenon_H97). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfd); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hfe ]. % 0.53/0.70 exact (zenon_Hbb zenon_H98). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfe); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hbf ]. % 0.53/0.70 exact (zenon_Hbd zenon_H99). % 0.53/0.70 exact (zenon_Hbf zenon_H9a). % 0.53/0.70 generalize (zenon_H109 zenon_TC_ff). zenon_intro zenon_H10a. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H10a); [ zenon_intro zenon_H10c | zenon_intro zenon_H10b ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H10c); [ zenon_intro zenon_Hc1 | zenon_intro zenon_H10d ]. % 0.53/0.70 exact (zenon_Hc1 zenon_H9b). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H10d); [ zenon_intro zenon_Hc3 | zenon_intro zenon_H10e ]. % 0.53/0.70 exact (zenon_Hc3 zenon_H9c). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H10e); [ zenon_intro zenon_Hc4 | zenon_intro zenon_H84 ]. % 0.53/0.70 exact (zenon_Hc4 zenon_H9d). % 0.53/0.70 apply (zenon_L1_ zenon_TB_fd zenon_TA_fe zenon_TC_ff); trivial. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H10b); [ zenon_intro zenon_H110 | zenon_intro zenon_H10f ]. % 0.53/0.70 exact (zenon_H110 zenon_Hed). % 0.53/0.70 exact (zenon_H105 zenon_H10f). % 0.53/0.70 exact (zenon_Hee zenon_H104). % 0.53/0.70 (* end of lemma zenon_L6_ *) % 0.53/0.70 apply NNPP. intro zenon_G. % 0.53/0.70 apply (zenon_notallex_s (fun A : zenon_U => (((v2_orders_2 A)/\((v3_orders_2 A)/\((v4_orders_2 A)/\((v1_lattice3 A)/\((v2_lattice3 A)/\((v3_lattice3 A)/\(l1_orders_2 A)))))))->(forall B : zenon_U, (((v2_orders_2 B)/\((v3_orders_2 B)/\((v4_orders_2 B)/\((v1_lattice3 B)/\((v2_lattice3 B)/\((v3_lattice3 B)/\(l1_orders_2 B)))))))->((v2_waybel_8 B)->(forall C : zenon_U, (((v1_funct_1 C)/\((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B))/\((v17_waybel_0 C A B)/\(m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))->((v22_waybel_0 C A B)<->((v1_funct_1 (k8_relset_1 (u1_struct_0 B) (u1_struct_0 A) (k1_waybel34 A B C) (u1_struct_0 (k1_waybel_8 B))))/\((v1_funct_2 (k8_relset_1 (u1_struct_0 B) (u1_struct_0 A) (k1_waybel34 A B C) (u1_struct_0 (k1_waybel_8 B))) (u1_struct_0 (k1_waybel_8 B)) (u1_struct_0 (k1_waybel_8 A)))/\((v4_waybel34 (k8_relset_1 (u1_struct_0 B) (u1_struct_0 A) (k1_waybel34 A B C) (u1_struct_0 (k1_waybel_8 B))) (k1_waybel_8 B) (k1_waybel_8 A))/\(m2_relset_1 (k8_relset_1 (u1_struct_0 B) (u1_struct_0 A) (k1_waybel34 A B C) (u1_struct_0 (k1_waybel_8 B))) (u1_struct_0 (k1_waybel_8 B)) (u1_struct_0 (k1_waybel_8 A)))))))))))))) zenon_G); [ zenon_intro zenon_H111; idtac ]. % 0.53/0.70 elim zenon_H111. zenon_intro zenon_TA_fe. zenon_intro zenon_H112. % 0.53/0.70 apply (zenon_notimply_s _ _ zenon_H112). zenon_intro zenon_H114. zenon_intro zenon_H113. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H114). zenon_intro zenon_H8d. zenon_intro zenon_H115. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H115). zenon_intro zenon_H8e. zenon_intro zenon_H116. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H116). zenon_intro zenon_H8f. zenon_intro zenon_H117. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H117). zenon_intro zenon_H90. zenon_intro zenon_H118. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H118). zenon_intro zenon_H91. zenon_intro zenon_H119. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H119). zenon_intro zenon_H92. zenon_intro zenon_H93. % 0.53/0.70 apply (zenon_notallex_s (fun B : zenon_U => (((v2_orders_2 B)/\((v3_orders_2 B)/\((v4_orders_2 B)/\((v1_lattice3 B)/\((v2_lattice3 B)/\((v3_lattice3 B)/\(l1_orders_2 B)))))))->((v2_waybel_8 B)->(forall C : zenon_U, (((v1_funct_1 C)/\((v1_funct_2 C (u1_struct_0 zenon_TA_fe) (u1_struct_0 B))/\((v17_waybel_0 C zenon_TA_fe B)/\(m2_relset_1 C (u1_struct_0 zenon_TA_fe) (u1_struct_0 B)))))->((v22_waybel_0 C zenon_TA_fe B)<->((v1_funct_1 (k8_relset_1 (u1_struct_0 B) (u1_struct_0 zenon_TA_fe) (k1_waybel34 zenon_TA_fe B C) (u1_struct_0 (k1_waybel_8 B))))/\((v1_funct_2 (k8_relset_1 (u1_struct_0 B) (u1_struct_0 zenon_TA_fe) (k1_waybel34 zenon_TA_fe B C) (u1_struct_0 (k1_waybel_8 B))) (u1_struct_0 (k1_waybel_8 B)) (u1_struct_0 (k1_waybel_8 zenon_TA_fe)))/\((v4_waybel34 (k8_relset_1 (u1_struct_0 B) (u1_struct_0 zenon_TA_fe) (k1_waybel34 zenon_TA_fe B C) (u1_struct_0 (k1_waybel_8 B))) (k1_waybel_8 B) (k1_waybel_8 zenon_TA_fe))/\(m2_relset_1 (k8_relset_1 (u1_struct_0 B) (u1_struct_0 zenon_TA_fe) (k1_waybel34 zenon_TA_fe B C) (u1_struct_0 (k1_waybel_8 B))) (u1_struct_0 (k1_waybel_8 B)) (u1_struct_0 (k1_waybel_8 zenon_TA_fe)))))))))))) zenon_H113); [ zenon_intro zenon_H11a; idtac ]. % 0.53/0.70 elim zenon_H11a. zenon_intro zenon_TB_fd. zenon_intro zenon_H11b. % 0.53/0.70 apply (zenon_notimply_s _ _ zenon_H11b). zenon_intro zenon_H11d. zenon_intro zenon_H11c. % 0.53/0.70 apply (zenon_notimply_s _ _ zenon_H11c). zenon_intro zenon_H11f. zenon_intro zenon_H11e. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H11d). zenon_intro zenon_H94. zenon_intro zenon_H120. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H120). zenon_intro zenon_H95. zenon_intro zenon_H121. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H121). zenon_intro zenon_H96. zenon_intro zenon_H122. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H122). zenon_intro zenon_H97. zenon_intro zenon_H123. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H123). zenon_intro zenon_H98. zenon_intro zenon_H124. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H124). zenon_intro zenon_H99. zenon_intro zenon_H9a. % 0.53/0.70 apply (zenon_notallex_s (fun C : zenon_U => (((v1_funct_1 C)/\((v1_funct_2 C (u1_struct_0 zenon_TA_fe) (u1_struct_0 zenon_TB_fd))/\((v17_waybel_0 C zenon_TA_fe zenon_TB_fd)/\(m2_relset_1 C (u1_struct_0 zenon_TA_fe) (u1_struct_0 zenon_TB_fd)))))->((v22_waybel_0 C zenon_TA_fe zenon_TB_fd)<->((v1_funct_1 (k8_relset_1 (u1_struct_0 zenon_TB_fd) (u1_struct_0 zenon_TA_fe) (k1_waybel34 zenon_TA_fe zenon_TB_fd C) (u1_struct_0 (k1_waybel_8 zenon_TB_fd))))/\((v1_funct_2 (k8_relset_1 (u1_struct_0 zenon_TB_fd) (u1_struct_0 zenon_TA_fe) (k1_waybel34 zenon_TA_fe zenon_TB_fd C) (u1_struct_0 (k1_waybel_8 zenon_TB_fd))) (u1_struct_0 (k1_waybel_8 zenon_TB_fd)) (u1_struct_0 (k1_waybel_8 zenon_TA_fe)))/\((v4_waybel34 (k8_relset_1 (u1_struct_0 zenon_TB_fd) (u1_struct_0 zenon_TA_fe) (k1_waybel34 zenon_TA_fe zenon_TB_fd C) (u1_struct_0 (k1_waybel_8 zenon_TB_fd))) (k1_waybel_8 zenon_TB_fd) (k1_waybel_8 zenon_TA_fe))/\(m2_relset_1 (k8_relset_1 (u1_struct_0 zenon_TB_fd) (u1_struct_0 zenon_TA_fe) (k1_waybel34 zenon_TA_fe zenon_TB_fd C) (u1_struct_0 (k1_waybel_8 zenon_TB_fd))) (u1_struct_0 (k1_waybel_8 zenon_TB_fd)) (u1_struct_0 (k1_waybel_8 zenon_TA_fe))))))))) zenon_H11e); [ zenon_intro zenon_H125; idtac ]. % 0.53/0.70 elim zenon_H125. zenon_intro zenon_TC_ff. zenon_intro zenon_H126. % 0.53/0.70 apply (zenon_notimply_s _ _ zenon_H126). zenon_intro zenon_H128. zenon_intro zenon_H127. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H128). zenon_intro zenon_H9b. zenon_intro zenon_H129. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H129). zenon_intro zenon_H9c. zenon_intro zenon_H12a. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H12a). zenon_intro zenon_H9d. zenon_intro zenon_H8b. % 0.53/0.70 generalize (redefinition_m2_relset_1 (u1_struct_0 zenon_TA_fe)). zenon_intro zenon_H88. % 0.53/0.70 generalize (zenon_H88 (u1_struct_0 zenon_TB_fd)). zenon_intro zenon_H89. % 0.53/0.70 generalize (zenon_H89 zenon_TC_ff). zenon_intro zenon_H8a. % 0.53/0.70 apply (zenon_equiv_s _ _ zenon_H8a); [ zenon_intro zenon_H84; zenon_intro zenon_H8c | zenon_intro zenon_H8b; zenon_intro zenon_H83 ]. % 0.53/0.70 exact (zenon_H84 zenon_H8b). % 0.53/0.70 apply (zenon_notequiv_s _ _ zenon_H127); [ zenon_intro zenon_H110; zenon_intro zenon_H12c | zenon_intro zenon_Hed; zenon_intro zenon_H12b ]. % 0.53/0.70 generalize (t25_waybel34 zenon_TA_fe). zenon_intro zenon_H12d. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H12d); [ zenon_intro zenon_Hf1 | zenon_intro zenon_H12e ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf1); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Hf2 ]. % 0.53/0.70 exact (zenon_Ha5 zenon_H8d). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf2); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Hf3 ]. % 0.53/0.70 exact (zenon_Ha7 zenon_H8e). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf3); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Hf4 ]. % 0.53/0.70 exact (zenon_Ha9 zenon_H8f). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf4); [ zenon_intro zenon_Hab | zenon_intro zenon_Hf5 ]. % 0.53/0.70 exact (zenon_Hab zenon_H90). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf5); [ zenon_intro zenon_Had | zenon_intro zenon_Hf6 ]. % 0.53/0.70 exact (zenon_Had zenon_H91). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf6); [ zenon_intro zenon_Haf | zenon_intro zenon_Hb1 ]. % 0.53/0.70 exact (zenon_Haf zenon_H92). % 0.53/0.70 exact (zenon_Hb1 zenon_H93). % 0.53/0.70 generalize (zenon_H12e zenon_TB_fd). zenon_intro zenon_H12f. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H12f); [ zenon_intro zenon_H131 | zenon_intro zenon_H130 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H131); [ zenon_intro zenon_Hb3 | zenon_intro zenon_H132 ]. % 0.53/0.70 exact (zenon_Hb3 zenon_H94). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H132); [ zenon_intro zenon_Hb5 | zenon_intro zenon_H133 ]. % 0.53/0.70 exact (zenon_Hb5 zenon_H95). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H133); [ zenon_intro zenon_Hb7 | zenon_intro zenon_H134 ]. % 0.53/0.70 exact (zenon_Hb7 zenon_H96). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H134); [ zenon_intro zenon_Hb9 | zenon_intro zenon_H135 ]. % 0.53/0.70 exact (zenon_Hb9 zenon_H97). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H135); [ zenon_intro zenon_Hbb | zenon_intro zenon_H136 ]. % 0.53/0.70 exact (zenon_Hbb zenon_H98). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H136); [ zenon_intro zenon_Hbd | zenon_intro zenon_H137 ]. % 0.53/0.70 exact (zenon_Hbd zenon_H99). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H137); [ zenon_intro zenon_H138 | zenon_intro zenon_Hbf ]. % 0.53/0.70 generalize (cc1_waybel_8 zenon_TB_fd). zenon_intro zenon_H139. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H139); [ zenon_intro zenon_Hbf | zenon_intro zenon_H13a ]. % 0.53/0.70 exact (zenon_Hbf zenon_H9a). % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H13a); [ zenon_intro zenon_H13c | zenon_intro zenon_H13b ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H13c); [ zenon_intro zenon_Hb3 | zenon_intro zenon_H13d ]. % 0.53/0.70 exact (zenon_Hb3 zenon_H94). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H13d); [ zenon_intro zenon_Hb5 | zenon_intro zenon_H13e ]. % 0.53/0.70 exact (zenon_Hb5 zenon_H95). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H13e); [ zenon_intro zenon_Hb7 | zenon_intro zenon_H13f ]. % 0.53/0.70 exact (zenon_Hb7 zenon_H96). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H13f); [ zenon_intro zenon_Hb9 | zenon_intro zenon_H140 ]. % 0.53/0.70 exact (zenon_Hb9 zenon_H97). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H140); [ zenon_intro zenon_Hbb | zenon_intro zenon_H141 ]. % 0.53/0.70 exact (zenon_Hbb zenon_H98). % 0.53/0.70 exact (zenon_H141 zenon_H11f). % 0.53/0.70 apply (zenon_and_s _ _ zenon_H13b). zenon_intro zenon_H143. zenon_intro zenon_H142. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H142). zenon_intro zenon_H94. zenon_intro zenon_H144. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H144). zenon_intro zenon_H95. zenon_intro zenon_H145. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H145). zenon_intro zenon_H96. zenon_intro zenon_H146. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H146). zenon_intro zenon_H97. zenon_intro zenon_H147. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H147). zenon_intro zenon_H98. zenon_intro zenon_H148. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H148). zenon_intro zenon_H14a. zenon_intro zenon_H149. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H149). zenon_intro zenon_H14c. zenon_intro zenon_H14b. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H14b). zenon_intro zenon_H14e. zenon_intro zenon_H14d. % 0.53/0.70 exact (zenon_H138 zenon_H14d). % 0.53/0.70 exact (zenon_Hbf zenon_H9a). % 0.53/0.70 generalize (zenon_H130 zenon_TC_ff). zenon_intro zenon_H14f. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H14f); [ zenon_intro zenon_H10c | zenon_intro zenon_H150 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H10c); [ zenon_intro zenon_Hc1 | zenon_intro zenon_H10d ]. % 0.53/0.70 exact (zenon_Hc1 zenon_H9b). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H10d); [ zenon_intro zenon_Hc3 | zenon_intro zenon_H10e ]. % 0.53/0.70 exact (zenon_Hc3 zenon_H9c). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H10e); [ zenon_intro zenon_Hc4 | zenon_intro zenon_H84 ]. % 0.53/0.70 exact (zenon_Hc4 zenon_H9d). % 0.53/0.70 apply (zenon_L1_ zenon_TB_fd zenon_TA_fe zenon_TC_ff); trivial. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H150); [ zenon_intro zenon_H105 | zenon_intro zenon_Hed ]. % 0.53/0.70 generalize (t61_waybel34 zenon_TA_fe). zenon_intro zenon_H151. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H151); [ zenon_intro zenon_Hf1 | zenon_intro zenon_H152 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf1); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Hf2 ]. % 0.53/0.70 exact (zenon_Ha5 zenon_H8d). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf2); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Hf3 ]. % 0.53/0.70 exact (zenon_Ha7 zenon_H8e). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf3); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Hf4 ]. % 0.53/0.70 exact (zenon_Ha9 zenon_H8f). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf4); [ zenon_intro zenon_Hab | zenon_intro zenon_Hf5 ]. % 0.53/0.70 exact (zenon_Hab zenon_H90). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf5); [ zenon_intro zenon_Had | zenon_intro zenon_Hf6 ]. % 0.53/0.70 exact (zenon_Had zenon_H91). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf6); [ zenon_intro zenon_Haf | zenon_intro zenon_Hb1 ]. % 0.53/0.70 exact (zenon_Haf zenon_H92). % 0.53/0.70 exact (zenon_Hb1 zenon_H93). % 0.53/0.70 generalize (zenon_H152 zenon_TB_fd). zenon_intro zenon_H153. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H153); [ zenon_intro zenon_Hf9 | zenon_intro zenon_H154 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf9); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hfa ]. % 0.53/0.70 exact (zenon_Hb3 zenon_H94). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfa); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hfb ]. % 0.53/0.70 exact (zenon_Hb5 zenon_H95). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfb); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hfc ]. % 0.53/0.70 exact (zenon_Hb7 zenon_H96). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfc); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hfd ]. % 0.53/0.70 exact (zenon_Hb9 zenon_H97). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfd); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hfe ]. % 0.53/0.70 exact (zenon_Hbb zenon_H98). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfe); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hbf ]. % 0.53/0.70 exact (zenon_Hbd zenon_H99). % 0.53/0.70 exact (zenon_Hbf zenon_H9a). % 0.53/0.70 generalize (zenon_H154 (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff)). zenon_intro zenon_H155. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H155); [ zenon_intro zenon_H101 | zenon_intro zenon_H156 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H101); [ zenon_intro zenon_H9e | zenon_intro zenon_H102 ]. % 0.53/0.70 apply (zenon_L2_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H102); [ zenon_intro zenon_Hc9 | zenon_intro zenon_H103 ]. % 0.53/0.70 apply (zenon_L3_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H103); [ zenon_intro zenon_Hce | zenon_intro zenon_Hd3 ]. % 0.53/0.70 apply (zenon_L4_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_L5_ zenon_TB_fd zenon_TA_fe zenon_TC_ff); trivial. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H156); [ zenon_intro zenon_H157 | zenon_intro zenon_H10f ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H157); [ zenon_intro zenon_H141 | zenon_intro zenon_Hee ]. % 0.53/0.70 exact (zenon_H141 zenon_H11f). % 0.53/0.70 generalize (t70_waybel34 zenon_TA_fe). zenon_intro zenon_H158. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H158); [ zenon_intro zenon_Hf1 | zenon_intro zenon_H159 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf1); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Hf2 ]. % 0.53/0.70 exact (zenon_Ha5 zenon_H8d). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf2); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Hf3 ]. % 0.53/0.70 exact (zenon_Ha7 zenon_H8e). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf3); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Hf4 ]. % 0.53/0.70 exact (zenon_Ha9 zenon_H8f). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf4); [ zenon_intro zenon_Hab | zenon_intro zenon_Hf5 ]. % 0.53/0.70 exact (zenon_Hab zenon_H90). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf5); [ zenon_intro zenon_Had | zenon_intro zenon_Hf6 ]. % 0.53/0.70 exact (zenon_Had zenon_H91). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf6); [ zenon_intro zenon_Haf | zenon_intro zenon_Hb1 ]. % 0.53/0.70 exact (zenon_Haf zenon_H92). % 0.53/0.70 exact (zenon_Hb1 zenon_H93). % 0.53/0.70 generalize (zenon_H159 zenon_TB_fd). zenon_intro zenon_H15a. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H15a); [ zenon_intro zenon_Hf9 | zenon_intro zenon_H15b ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf9); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hfa ]. % 0.53/0.70 exact (zenon_Hb3 zenon_H94). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfa); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hfb ]. % 0.53/0.70 exact (zenon_Hb5 zenon_H95). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfb); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hfc ]. % 0.53/0.70 exact (zenon_Hb7 zenon_H96). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfc); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hfd ]. % 0.53/0.70 exact (zenon_Hb9 zenon_H97). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfd); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hfe ]. % 0.53/0.70 exact (zenon_Hbb zenon_H98). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfe); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hbf ]. % 0.53/0.70 exact (zenon_Hbd zenon_H99). % 0.53/0.70 exact (zenon_Hbf zenon_H9a). % 0.53/0.70 generalize (zenon_H15b (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff)). zenon_intro zenon_H15c. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H15c); [ zenon_intro zenon_H101 | zenon_intro zenon_H15d ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H101); [ zenon_intro zenon_H9e | zenon_intro zenon_H102 ]. % 0.53/0.70 apply (zenon_L2_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H102); [ zenon_intro zenon_Hc9 | zenon_intro zenon_H103 ]. % 0.53/0.70 apply (zenon_L3_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H103); [ zenon_intro zenon_Hce | zenon_intro zenon_Hd3 ]. % 0.53/0.70 apply (zenon_L4_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_L5_ zenon_TB_fd zenon_TA_fe zenon_TC_ff); trivial. % 0.53/0.70 apply (zenon_equiv_s _ _ zenon_H15d); [ zenon_intro zenon_Hee; zenon_intro zenon_H12b | zenon_intro zenon_H104; zenon_intro zenon_H12c ]. % 0.53/0.70 exact (zenon_H12b zenon_H12c). % 0.53/0.70 exact (zenon_Hee zenon_H104). % 0.53/0.70 exact (zenon_H105 zenon_H10f). % 0.53/0.70 exact (zenon_H110 zenon_Hed). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H12b); [ zenon_intro zenon_H15f | zenon_intro zenon_H15e ]. % 0.53/0.70 generalize (t70_waybel34 zenon_TA_fe). zenon_intro zenon_H158. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H158); [ zenon_intro zenon_Hf1 | zenon_intro zenon_H159 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf1); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Hf2 ]. % 0.53/0.70 exact (zenon_Ha5 zenon_H8d). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf2); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Hf3 ]. % 0.53/0.70 exact (zenon_Ha7 zenon_H8e). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf3); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Hf4 ]. % 0.53/0.70 exact (zenon_Ha9 zenon_H8f). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf4); [ zenon_intro zenon_Hab | zenon_intro zenon_Hf5 ]. % 0.53/0.70 exact (zenon_Hab zenon_H90). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf5); [ zenon_intro zenon_Had | zenon_intro zenon_Hf6 ]. % 0.53/0.70 exact (zenon_Had zenon_H91). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf6); [ zenon_intro zenon_Haf | zenon_intro zenon_Hb1 ]. % 0.53/0.70 exact (zenon_Haf zenon_H92). % 0.53/0.70 exact (zenon_Hb1 zenon_H93). % 0.53/0.70 generalize (zenon_H159 zenon_TB_fd). zenon_intro zenon_H15a. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H15a); [ zenon_intro zenon_Hf9 | zenon_intro zenon_H15b ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf9); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hfa ]. % 0.53/0.70 exact (zenon_Hb3 zenon_H94). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfa); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hfb ]. % 0.53/0.70 exact (zenon_Hb5 zenon_H95). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfb); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hfc ]. % 0.53/0.70 exact (zenon_Hb7 zenon_H96). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfc); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hfd ]. % 0.53/0.70 exact (zenon_Hb9 zenon_H97). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfd); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hfe ]. % 0.53/0.70 exact (zenon_Hbb zenon_H98). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfe); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hbf ]. % 0.53/0.70 exact (zenon_Hbd zenon_H99). % 0.53/0.70 exact (zenon_Hbf zenon_H9a). % 0.53/0.70 generalize (zenon_H15b (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff)). zenon_intro zenon_H15c. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H15c); [ zenon_intro zenon_H101 | zenon_intro zenon_H15d ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H101); [ zenon_intro zenon_H9e | zenon_intro zenon_H102 ]. % 0.53/0.70 apply (zenon_L2_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H102); [ zenon_intro zenon_Hc9 | zenon_intro zenon_H103 ]. % 0.53/0.70 apply (zenon_L3_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H103); [ zenon_intro zenon_Hce | zenon_intro zenon_Hd3 ]. % 0.53/0.70 apply (zenon_L4_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_L5_ zenon_TB_fd zenon_TA_fe zenon_TC_ff); trivial. % 0.53/0.70 apply (zenon_equiv_s _ _ zenon_H15d); [ zenon_intro zenon_Hee; zenon_intro zenon_H12b | zenon_intro zenon_H104; zenon_intro zenon_H12c ]. % 0.53/0.70 apply (zenon_L6_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H12c). zenon_intro zenon_H161. zenon_intro zenon_H160. % 0.53/0.70 exact (zenon_H15f zenon_H161). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H15e); [ zenon_intro zenon_H163 | zenon_intro zenon_H162 ]. % 0.53/0.70 generalize (t70_waybel34 zenon_TA_fe). zenon_intro zenon_H158. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H158); [ zenon_intro zenon_Hf1 | zenon_intro zenon_H159 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf1); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Hf2 ]. % 0.53/0.70 exact (zenon_Ha5 zenon_H8d). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf2); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Hf3 ]. % 0.53/0.70 exact (zenon_Ha7 zenon_H8e). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf3); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Hf4 ]. % 0.53/0.70 exact (zenon_Ha9 zenon_H8f). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf4); [ zenon_intro zenon_Hab | zenon_intro zenon_Hf5 ]. % 0.53/0.70 exact (zenon_Hab zenon_H90). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf5); [ zenon_intro zenon_Had | zenon_intro zenon_Hf6 ]. % 0.53/0.70 exact (zenon_Had zenon_H91). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf6); [ zenon_intro zenon_Haf | zenon_intro zenon_Hb1 ]. % 0.53/0.70 exact (zenon_Haf zenon_H92). % 0.53/0.70 exact (zenon_Hb1 zenon_H93). % 0.53/0.70 generalize (zenon_H159 zenon_TB_fd). zenon_intro zenon_H15a. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H15a); [ zenon_intro zenon_Hf9 | zenon_intro zenon_H15b ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf9); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hfa ]. % 0.53/0.70 exact (zenon_Hb3 zenon_H94). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfa); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hfb ]. % 0.53/0.70 exact (zenon_Hb5 zenon_H95). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfb); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hfc ]. % 0.53/0.70 exact (zenon_Hb7 zenon_H96). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfc); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hfd ]. % 0.53/0.70 exact (zenon_Hb9 zenon_H97). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfd); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hfe ]. % 0.53/0.70 exact (zenon_Hbb zenon_H98). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfe); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hbf ]. % 0.53/0.70 exact (zenon_Hbd zenon_H99). % 0.53/0.70 exact (zenon_Hbf zenon_H9a). % 0.53/0.70 generalize (zenon_H15b (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff)). zenon_intro zenon_H15c. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H15c); [ zenon_intro zenon_H101 | zenon_intro zenon_H15d ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H101); [ zenon_intro zenon_H9e | zenon_intro zenon_H102 ]. % 0.53/0.70 apply (zenon_L2_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H102); [ zenon_intro zenon_Hc9 | zenon_intro zenon_H103 ]. % 0.53/0.70 apply (zenon_L3_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H103); [ zenon_intro zenon_Hce | zenon_intro zenon_Hd3 ]. % 0.53/0.70 apply (zenon_L4_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_L5_ zenon_TB_fd zenon_TA_fe zenon_TC_ff); trivial. % 0.53/0.70 apply (zenon_equiv_s _ _ zenon_H15d); [ zenon_intro zenon_Hee; zenon_intro zenon_H12b | zenon_intro zenon_H104; zenon_intro zenon_H12c ]. % 0.53/0.70 apply (zenon_L6_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H12c). zenon_intro zenon_H161. zenon_intro zenon_H160. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H160). zenon_intro zenon_H165. zenon_intro zenon_H164. % 0.53/0.70 exact (zenon_H163 zenon_H165). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H162); [ zenon_intro zenon_H167 | zenon_intro zenon_H166 ]. % 0.53/0.70 generalize (t70_waybel34 zenon_TA_fe). zenon_intro zenon_H158. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H158); [ zenon_intro zenon_Hf1 | zenon_intro zenon_H159 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf1); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Hf2 ]. % 0.53/0.70 exact (zenon_Ha5 zenon_H8d). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf2); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Hf3 ]. % 0.53/0.70 exact (zenon_Ha7 zenon_H8e). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf3); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Hf4 ]. % 0.53/0.70 exact (zenon_Ha9 zenon_H8f). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf4); [ zenon_intro zenon_Hab | zenon_intro zenon_Hf5 ]. % 0.53/0.70 exact (zenon_Hab zenon_H90). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf5); [ zenon_intro zenon_Had | zenon_intro zenon_Hf6 ]. % 0.53/0.70 exact (zenon_Had zenon_H91). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf6); [ zenon_intro zenon_Haf | zenon_intro zenon_Hb1 ]. % 0.53/0.70 exact (zenon_Haf zenon_H92). % 0.53/0.70 exact (zenon_Hb1 zenon_H93). % 0.53/0.70 generalize (zenon_H159 zenon_TB_fd). zenon_intro zenon_H15a. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H15a); [ zenon_intro zenon_Hf9 | zenon_intro zenon_H15b ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf9); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hfa ]. % 0.53/0.70 exact (zenon_Hb3 zenon_H94). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfa); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hfb ]. % 0.53/0.70 exact (zenon_Hb5 zenon_H95). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfb); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hfc ]. % 0.53/0.70 exact (zenon_Hb7 zenon_H96). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfc); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hfd ]. % 0.53/0.70 exact (zenon_Hb9 zenon_H97). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfd); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hfe ]. % 0.53/0.70 exact (zenon_Hbb zenon_H98). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfe); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hbf ]. % 0.53/0.70 exact (zenon_Hbd zenon_H99). % 0.53/0.70 exact (zenon_Hbf zenon_H9a). % 0.53/0.70 generalize (zenon_H15b (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff)). zenon_intro zenon_H15c. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H15c); [ zenon_intro zenon_H101 | zenon_intro zenon_H15d ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H101); [ zenon_intro zenon_H9e | zenon_intro zenon_H102 ]. % 0.53/0.70 apply (zenon_L2_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H102); [ zenon_intro zenon_Hc9 | zenon_intro zenon_H103 ]. % 0.53/0.70 apply (zenon_L3_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H103); [ zenon_intro zenon_Hce | zenon_intro zenon_Hd3 ]. % 0.53/0.70 apply (zenon_L4_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_L5_ zenon_TB_fd zenon_TA_fe zenon_TC_ff); trivial. % 0.53/0.70 apply (zenon_equiv_s _ _ zenon_H15d); [ zenon_intro zenon_Hee; zenon_intro zenon_H12b | zenon_intro zenon_H104; zenon_intro zenon_H12c ]. % 0.53/0.70 apply (zenon_L6_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H12c). zenon_intro zenon_H161. zenon_intro zenon_H160. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H160). zenon_intro zenon_H165. zenon_intro zenon_H164. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H164). zenon_intro zenon_H169. zenon_intro zenon_H168. % 0.53/0.70 exact (zenon_H167 zenon_H169). % 0.53/0.70 generalize (redefinition_m2_relset_1 (u1_struct_0 (k1_waybel_8 zenon_TB_fd))). zenon_intro zenon_H16a. % 0.53/0.70 generalize (zenon_H16a (u1_struct_0 (k1_waybel_8 zenon_TA_fe))). zenon_intro zenon_H16b. % 0.53/0.70 generalize (zenon_H16b (k8_relset_1 (u1_struct_0 zenon_TB_fd) (u1_struct_0 zenon_TA_fe) (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff) (u1_struct_0 (k1_waybel_8 zenon_TB_fd)))). zenon_intro zenon_H16c. % 0.53/0.70 apply (zenon_equiv_s _ _ zenon_H16c); [ zenon_intro zenon_H166; zenon_intro zenon_H16e | zenon_intro zenon_H168; zenon_intro zenon_H16d ]. % 0.53/0.70 generalize (t70_waybel34 zenon_TA_fe). zenon_intro zenon_H158. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H158); [ zenon_intro zenon_Hf1 | zenon_intro zenon_H159 ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf1); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Hf2 ]. % 0.53/0.70 exact (zenon_Ha5 zenon_H8d). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf2); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Hf3 ]. % 0.53/0.70 exact (zenon_Ha7 zenon_H8e). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf3); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Hf4 ]. % 0.53/0.70 exact (zenon_Ha9 zenon_H8f). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf4); [ zenon_intro zenon_Hab | zenon_intro zenon_Hf5 ]. % 0.53/0.70 exact (zenon_Hab zenon_H90). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf5); [ zenon_intro zenon_Had | zenon_intro zenon_Hf6 ]. % 0.53/0.70 exact (zenon_Had zenon_H91). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf6); [ zenon_intro zenon_Haf | zenon_intro zenon_Hb1 ]. % 0.53/0.70 exact (zenon_Haf zenon_H92). % 0.53/0.70 exact (zenon_Hb1 zenon_H93). % 0.53/0.70 generalize (zenon_H159 zenon_TB_fd). zenon_intro zenon_H15a. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H15a); [ zenon_intro zenon_Hf9 | zenon_intro zenon_H15b ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hf9); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hfa ]. % 0.53/0.70 exact (zenon_Hb3 zenon_H94). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfa); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hfb ]. % 0.53/0.70 exact (zenon_Hb5 zenon_H95). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfb); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hfc ]. % 0.53/0.70 exact (zenon_Hb7 zenon_H96). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfc); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hfd ]. % 0.53/0.70 exact (zenon_Hb9 zenon_H97). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfd); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hfe ]. % 0.53/0.70 exact (zenon_Hbb zenon_H98). % 0.53/0.70 apply (zenon_notand_s _ _ zenon_Hfe); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hbf ]. % 0.53/0.70 exact (zenon_Hbd zenon_H99). % 0.53/0.70 exact (zenon_Hbf zenon_H9a). % 0.53/0.70 generalize (zenon_H15b (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff)). zenon_intro zenon_H15c. % 0.53/0.70 apply (zenon_imply_s _ _ zenon_H15c); [ zenon_intro zenon_H101 | zenon_intro zenon_H15d ]. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H101); [ zenon_intro zenon_H9e | zenon_intro zenon_H102 ]. % 0.53/0.70 apply (zenon_L2_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H102); [ zenon_intro zenon_Hc9 | zenon_intro zenon_H103 ]. % 0.53/0.70 apply (zenon_L3_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_notand_s _ _ zenon_H103); [ zenon_intro zenon_Hce | zenon_intro zenon_Hd3 ]. % 0.53/0.70 apply (zenon_L4_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_L5_ zenon_TB_fd zenon_TA_fe zenon_TC_ff); trivial. % 0.53/0.70 apply (zenon_equiv_s _ _ zenon_H15d); [ zenon_intro zenon_Hee; zenon_intro zenon_H12b | zenon_intro zenon_H104; zenon_intro zenon_H12c ]. % 0.53/0.70 apply (zenon_L6_ zenon_TC_ff zenon_TB_fd zenon_TA_fe); trivial. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H12c). zenon_intro zenon_H161. zenon_intro zenon_H160. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H160). zenon_intro zenon_H165. zenon_intro zenon_H164. % 0.53/0.70 apply (zenon_and_s _ _ zenon_H164). zenon_intro zenon_H169. zenon_intro zenon_H168. % 0.53/0.70 generalize (redefinition_m2_relset_1 (u1_struct_0 (k1_waybel_8 zenon_TB_fd))). zenon_intro zenon_H16a. % 0.53/0.70 generalize (zenon_H16a (u1_struct_0 (k1_waybel_8 zenon_TA_fe))). zenon_intro zenon_H16b. % 0.53/0.70 generalize (zenon_H16b (k8_relset_1 (u1_struct_0 zenon_TB_fd) (u1_struct_0 zenon_TA_fe) (k1_waybel34 zenon_TA_fe zenon_TB_fd zenon_TC_ff) (u1_struct_0 (k1_waybel_8 zenon_TB_fd)))). zenon_intro zenon_H16c. % 0.53/0.70 apply (zenon_equiv_s _ _ zenon_H16c); [ zenon_intro zenon_H166; zenon_intro zenon_H16e | zenon_intro zenon_H168; zenon_intro zenon_H16d ]. % 0.53/0.70 exact (zenon_H166 zenon_H168). % 0.53/0.70 exact (zenon_H16e zenon_H16d). % 0.53/0.70 exact (zenon_H166 zenon_H168). % 0.53/0.70 Qed. % 0.53/0.70 % SZS output end Proof % 0.53/0.70 (* END-PROOF *) % 0.53/0.70 nodes searched: 5891 % 0.53/0.70 max branch formulas: 1552 % 0.53/0.70 proof nodes created: 687 % 0.53/0.70 formulas created: 26028 % 0.53/0.70 %------------------------------------------------------------------------------