fof(t17_dtconstr,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_dtconstr)) => ( ( A = 0 => k20_dtconstr(k5_dtconstr,A) = k6_domain_1(k3_finseq_2(k5_numbers),k3_lang1(k5_numbers,0)) ) & ( A = 1 => k20_dtconstr(k5_dtconstr,A) = a_0_0_dtconstr ) ) ) ), inference(mizar_proof,[status(thm)],[t79_trees_1,t3_trees_4,t16_dtconstr,t72_finseq_2,t47_finseq_1,t9_dtconstr,d1_tarski,d3_tarski,d10_xboole_0,d3_tarski,d1_tarski,t3_trees_4,t10_dtconstr,d5_dtconstr,t57_finseq_1,t5_dtconstr,d5_trees_4,t13_trees_4,t83_trees_3,t16_dtconstr,d3_tarski,d10_xboole_0,d3_tarski,t16_dtconstr,t46_finseq_1,t69_finseq_2,t69_finseq_2,d5_trees_4,t13_trees_4,t83_trees_3,t16_dtconstr,d4_trees_4,d5_trees_4,t13_trees_4,t83_trees_3,t79_trees_1,t3_trees_4,t16_dtconstr,d4_trees_4,s1_nat_1]), [file(dtconstr,t17_dtconstr),interesting(1.00)]). fof(t19_dtconstr,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_dtconstr)) => ( ( A = 0 => k21_dtconstr(k5_dtconstr,A) = k6_domain_1(k3_finseq_2(k5_numbers),k3_lang1(k5_numbers,0)) ) & ( A = 1 => k21_dtconstr(k5_dtconstr,A) = a_0_1_dtconstr ) ) ) ), inference(mizar_proof,[status(thm)],[t79_trees_1,t3_trees_4,t18_dtconstr,t72_finseq_2,t47_finseq_1,t9_dtconstr,d1_tarski,d3_tarski,d10_xboole_0,d3_tarski,d1_tarski,t3_trees_4,t10_dtconstr,d5_dtconstr,t57_finseq_1,t5_dtconstr,d5_trees_4,t13_trees_4,t83_trees_3,t18_dtconstr,d3_tarski,d10_xboole_0,d3_tarski,t18_dtconstr,t46_finseq_1,t69_finseq_2,t69_finseq_2,d5_trees_4,t13_trees_4,t83_trees_3,t18_dtconstr,d4_trees_4,d5_trees_4,t13_trees_4,t83_trees_3,t79_trees_1,t3_trees_4,t18_dtconstr,d4_trees_4,s1_nat_1]), [file(dtconstr,t19_dtconstr),interesting(1.00)]). fof(t15_dtconstr,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_dtconstr)) => k19_dtconstr(k5_dtconstr,A) = k6_domain_1(k3_finseq_2(k5_numbers),k3_lang1(k5_numbers,0)) ) ), inference(mizar_proof,[status(thm)],[l15_dtconstr,d2_tarski,t14_dtconstr,d1_tarski,d3_tarski,d10_xboole_0,d3_tarski,d1_tarski,t3_trees_4,l18_dtconstr,t4_dtconstr,d4_dtconstr,t14_dtconstr,d4_trees_4]), [file(dtconstr,t15_dtconstr),interesting(0.89)]). fof(t14_dtconstr,theorem,( ! [A] : ( ( v1_funct_1(A) & v3_trees_2(A) & m3_trees_2(A,u1_struct_0(k5_dtconstr)) ) => ( r2_hidden(A,k4_dtconstr(k5_dtconstr)) => k16_dtconstr(k5_dtconstr,A) = k3_lang1(k5_numbers,0) ) ) ), inference(mizar_proof,[status(thm)],[d15_dtconstr,l23_dtconstr,d1_tarski,d4_dtconstr,d5_dtconstr,t57_finseq_1,t5_dtconstr,t56_finseq_1,d1_tarski,d15_dtconstr,t39_finseq_2,t13_dtconstr,d15_dtconstr,s7_dtconstr]), [file(dtconstr,t14_dtconstr),interesting(0.87)]). fof(t16_dtconstr,theorem,( ! [A] : ( m1_dtconstr(A,u1_struct_0(k5_dtconstr),k5_trees_3(u1_struct_0(k5_dtconstr)),k4_dtconstr(k5_dtconstr)) => k17_dtconstr(k5_dtconstr,A) = k8_finseq_1(k5_numbers,k4_finseqop(k5_numbers,k6_trees_1(k1_relat_1(A)),1),k3_lang1(k5_numbers,0)) ) ), inference(mizar_proof,[status(thm)],[d16_dtconstr,l23_dtconstr,d1_tarski,t47_finseq_1,t72_finseq_2,t79_trees_1,t3_trees_4,d4_dtconstr,d5_dtconstr,t57_finseq_1,t5_dtconstr,t56_finseq_1,d1_tarski,d16_dtconstr,t39_finseq_2,t13_dtconstr,t45_finseq_1,t73_finseq_2,t143_finseq_2,t83_trees_3,t13_trees_4,d5_trees_4,d16_dtconstr,s7_dtconstr]), [file(dtconstr,t16_dtconstr),interesting(0.79)]). fof(t18_dtconstr,theorem,( ! [A] : ( m1_dtconstr(A,u1_struct_0(k5_dtconstr),k5_trees_3(u1_struct_0(k5_dtconstr)),k4_dtconstr(k5_dtconstr)) => k18_dtconstr(k5_dtconstr,A) = k8_finseq_1(k5_numbers,k3_lang1(k5_numbers,0),k4_finseqop(k5_numbers,k6_trees_1(k1_relat_1(A)),1)) ) ), inference(mizar_proof,[status(thm)],[d17_dtconstr,l23_dtconstr,d1_tarski,t47_finseq_1,t72_finseq_2,t79_trees_1,t3_trees_4,d4_dtconstr,d5_dtconstr,t57_finseq_1,t5_dtconstr,t56_finseq_1,d1_tarski,d17_dtconstr,t39_finseq_2,t13_dtconstr,t45_finseq_1,t73_finseq_2,t143_finseq_2,t83_trees_3,t13_trees_4,d5_trees_4,d17_dtconstr,s7_dtconstr]), [file(dtconstr,t18_dtconstr),interesting(0.79)]). fof(l22_dtconstr,theorem,( r2_hidden(c2,k5_lang1(k5_dtconstr)) ), inference(mizar_proof,[status(thm)],[l21_dtconstr,l20_dtconstr]), [file(dtconstr,l22_dtconstr),interesting(0.69)]). fof(l25_dtconstr,theorem,( r2_hidden(c3,k6_lang1(k5_dtconstr)) ), inference(mizar_proof,[status(thm)],[l24_dtconstr,l18_dtconstr]), [file(dtconstr,l25_dtconstr),interesting(0.68)]). fof(l3_dtconstr,theorem,( k5_finsop_1(k16_trees_3(k1_xboole_0)) = k1_xboole_0 ), inference(mizar_proof,[status(thm)],[t23_trees_3,d18_trees_3,t26_finseq_1]), [file(dtconstr,l3_dtconstr),interesting(0.68)]). fof(t3_dtconstr,theorem,( k16_trees_3(k1_xboole_0) = k1_xboole_0 ), inference(mizar_proof,[status(thm)],[l3_dtconstr,t26_finseq_1]), [file(dtconstr,t3_dtconstr),interesting(0.68)]). fof(t13_dtconstr,theorem,( ! [A,B] : ( m2_finseq_2(B,A,k3_finseq_2(A)) => k15_dtconstr(A,k3_lang1(k3_finseq_2(A),B)) = B ) ), inference(mizar_proof,[status(thm)],[d14_dtconstr,t12_finsop_1]), [file(dtconstr,t13_dtconstr),interesting(0.68)]). fof(l21_dtconstr,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ~ r1_lang1(k5_dtconstr,c2,A) ) ), inference(mizar_proof,[status(thm)],[d1_lang1,t106_zfmisc_1,d3_finseq_2,d5_dtconstr]), [file(dtconstr,l21_dtconstr),interesting(0.66)]). fof(l27_dtconstr,theorem,( r1_tarski(k6_lang1(k5_dtconstr),k6_domain_1(u1_struct_0(k5_dtconstr),c3)) ), inference(mizar_proof,[status(thm)],[d3_tarski,l24_dtconstr,l15_dtconstr,d2_tarski,l21_dtconstr,d1_tarski]), [file(dtconstr,l27_dtconstr),interesting(0.66)]). fof(l33_dtconstr,theorem, ( v1_dtconstr(k5_dtconstr) & v2_dtconstr(k5_dtconstr) & v3_dtconstr(k5_dtconstr) ), inference(mizar_proof,[status(thm)],[l22_dtconstr,d6_dtconstr,l25_dtconstr,d7_dtconstr,d4_dtconstr,l22_dtconstr,d8_dtconstr,l27_dtconstr,d1_tarski,t55_finseq_1,t4_finseq_1,t57_finseq_1,d1_tarski,t57_finseq_1,t3_trees_4,l18_dtconstr,d18_trees_3]), [file(dtconstr,l33_dtconstr),interesting(0.65)]). fof(l23_dtconstr,theorem,( r1_tarski(k5_lang1(k5_dtconstr),k6_domain_1(u1_struct_0(k5_dtconstr),c2)) ), inference(mizar_proof,[status(thm)],[d3_tarski,l20_dtconstr,l15_dtconstr,d2_tarski,l18_dtconstr,d1_tarski]), [file(dtconstr,l23_dtconstr),interesting(0.65)]). fof(t11_dtconstr,theorem,( ! [A] : ( m1_dtconstr(A,u1_struct_0(k5_dtconstr),k5_trees_3(u1_struct_0(k5_dtconstr)),k4_dtconstr(k5_dtconstr)) => A = k8_funct_2(k5_numbers,k4_dtconstr(k5_dtconstr),k14_dtconstr,k8_funct_2(k4_dtconstr(k5_dtconstr),k5_numbers,k12_dtconstr,A)) ) ), inference(mizar_proof,[status(thm)],[d11_dtconstr,d13_dtconstr,l23_dtconstr,d1_tarski,l21_dtconstr,l15_dtconstr,d2_tarski,d5_dtconstr,t57_finseq_1,t5_dtconstr,t55_finseq_1,d1_tarski,t39_finseq_2,d10_dtconstr,t57_finseq_1,d13_dtconstr,d11_dtconstr,s7_dtconstr]), [file(dtconstr,t11_dtconstr),interesting(0.65)]). fof(t4_dtconstr,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v3_trees_2(A) ) => k16_trees_3(k9_finseq_1(A)) = k9_finseq_1(k1_funct_1(A,k1_xboole_0)) ) ), inference(mizar_proof,[status(thm)],[d8_finseq_1,t4_finseq_1,d1_tarski,d18_trees_3]), [file(dtconstr,t4_dtconstr),interesting(0.65)]). fof(l15_dtconstr,theorem,( u1_struct_0(k5_dtconstr) = k7_domain_1(k5_numbers,0,1) ), inference(mizar_proof,[status(thm)],[d5_dtconstr]), [file(dtconstr,l15_dtconstr),interesting(0.64)]). fof(t7_dtconstr,theorem, ( k15_mcart_1(k1_xboole_0) = k1_xboole_0 & k16_mcart_1(k1_xboole_0) = k1_xboole_0 ), inference(mizar_proof,[status(thm)],[t29_finseq_1,d12_mcart_1,t26_finseq_1,t26_finseq_1,d13_mcart_1,t26_finseq_1,t26_finseq_1]), [file(dtconstr,t7_dtconstr),interesting(0.64)]). fof(l18_dtconstr,theorem,( r1_lang1(k5_dtconstr,c3,k3_lang1(u1_struct_0(k5_dtconstr),c2)) ), inference(mizar_proof,[status(thm)],[d5_dtconstr]), [file(dtconstr,l18_dtconstr),interesting(0.63)]). fof(l26_dtconstr,theorem,( r1_tarski(k6_domain_1(u1_struct_0(k5_dtconstr),c3),k6_lang1(k5_dtconstr)) ), inference(mizar_proof,[status(thm)],[l25_dtconstr,t37_zfmisc_1]), [file(dtconstr,l26_dtconstr),interesting(0.63)]). fof(t2_dtconstr,theorem,( ! [A,B,C] : ( m2_finseq_1(C,A) => ( r2_hidden(B,k5_finsop_1(C)) => r2_hidden(k1_funct_1(C,B),A) ) ) ), inference(mizar_proof,[status(thm)],[d4_finseq_1,d5_funct_1]), [file(dtconstr,t2_dtconstr),interesting(0.63)]). fof(l24_dtconstr,theorem,( k6_lang1(k5_dtconstr) = a_0_8_dtconstr ), inference(mizar_proof,[status(thm)],[d3_lang1]), [file(dtconstr,l24_dtconstr),interesting(0.62)]). fof(l20_dtconstr,theorem,( k5_lang1(k5_dtconstr) = a_0_7_dtconstr ), inference(mizar_proof,[status(thm)],[d2_lang1]), [file(dtconstr,l20_dtconstr),interesting(0.62)]). fof(t1_dtconstr,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,k5_trees_3(A)) => m2_finseq_1(B,k4_trees_3(A)) ) ) ), inference(mizar_proof,[status(thm)],[t22_trees_3,t27_finseq_2]), [file(dtconstr,t1_dtconstr),interesting(0.62)]). fof(l44_dtconstr,theorem,( 0 = k8_funct_2(k4_dtconstr(k5_dtconstr),k5_numbers,k12_dtconstr,k8_funct_2(k5_numbers,k4_dtconstr(k5_dtconstr),k14_dtconstr,0)) ), inference(mizar_proof,[status(thm)],[d11_dtconstr,d13_dtconstr]), [file(dtconstr,l44_dtconstr),interesting(0.61)]). fof(t5_dtconstr,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k5_trees_3(A))) => ! [C] : ( m1_trees_4(C,k5_trees_3(A),B) => ~ ( k3_finseq_1(k1_dtconstr(A,k5_trees_3(A),C)) = 1 & ! [D] : ( m5_trees_3(D,A,k5_trees_3(A)) => ~ ( C = k3_lang1(k5_trees_3(A),D) & r2_hidden(D,B) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_1,d18_trees_3,t2_dtconstr,t2_dtconstr,d8_finseq_1]), [file(dtconstr,t5_dtconstr),interesting(0.58)]). fof(l28_dtconstr,theorem,( k6_lang1(k5_dtconstr) = k6_domain_1(u1_struct_0(k5_dtconstr),c3) ), inference(mizar_proof,[status(thm)],[l27_dtconstr,l26_dtconstr,d10_xboole_0]), [file(dtconstr,l28_dtconstr),interesting(0.57)]). fof(l17_dtconstr,theorem, ( r1_lang1(k5_dtconstr,c3,k3_lang1(u1_struct_0(k5_dtconstr),c2)) & r1_lang1(k5_dtconstr,c3,k3_lang1(u1_struct_0(k5_dtconstr),c3)) ), inference(mizar_proof,[status(thm)],[d5_dtconstr]), [file(dtconstr,l17_dtconstr),interesting(0.57)]). fof(t12_dtconstr,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => A = k8_funct_2(k4_dtconstr(k5_dtconstr),k5_numbers,k12_dtconstr,k8_funct_2(k5_numbers,k4_dtconstr(k5_dtconstr),k14_dtconstr,A)) ) ), inference(mizar_proof,[status(thm)],[l44_dtconstr,l45_dtconstr,s1_nat_1]), [file(dtconstr,t12_dtconstr),interesting(0.56)]). fof(l29_dtconstr,theorem, ( ~ v1_xboole_0(k4_dtconstr(k5_dtconstr)) & m1_subset_1(k4_dtconstr(k5_dtconstr),k1_zfmisc_1(k5_trees_3(u1_struct_0(k5_dtconstr)))) ), inference(mizar_proof,[status(thm)],[d4_dtconstr,l22_dtconstr]), [file(dtconstr,l29_dtconstr),interesting(0.55)]). fof(l37_dtconstr,theorem,( m1_struct_0(c2,k5_dtconstr,k6_dtconstr(k5_dtconstr)) ), inference(mizar_proof,[status(thm)],[l22_dtconstr]), [file(dtconstr,l37_dtconstr),interesting(0.55)]). fof(l45_dtconstr,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( A = k8_funct_2(k4_dtconstr(k5_dtconstr),k5_numbers,k12_dtconstr,k8_funct_2(k5_numbers,k4_dtconstr(k5_dtconstr),k14_dtconstr,A)) => k1_nat_1(A,1) = k8_funct_2(k4_dtconstr(k5_dtconstr),k5_numbers,k12_dtconstr,k8_funct_2(k5_numbers,k4_dtconstr(k5_dtconstr),k14_dtconstr,k1_nat_1(A,1))) ) ) ), inference(mizar_proof,[status(thm)],[t47_trees_1,l15_dtconstr,d2_tarski,d13_dtconstr,l17_dtconstr,t4_dtconstr,d10_dtconstr,t39_finseq_2,d11_dtconstr,t57_finseq_1]), [file(dtconstr,l45_dtconstr),interesting(0.55)]). fof(l38_dtconstr,theorem,( m1_struct_0(c3,k5_dtconstr,k7_dtconstr(k5_dtconstr)) ), inference(mizar_proof,[status(thm)],[l25_dtconstr]), [file(dtconstr,l38_dtconstr),interesting(0.54)]). fof(t8_dtconstr,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_lang1(A) ) => r1_xboole_0(k5_lang1(A),k6_lang1(A)) ) ), inference(mizar_proof,[status(thm)],[d2_lang1,d3_lang1,t3_xboole_0]), [file(dtconstr,t8_dtconstr),interesting(0.54)]). fof(s5_dtconstr,theorem, ( ( k1_relat_1(f1_s5_dtconstr) = k5_numbers & k1_funct_1(f1_s5_dtconstr,0) = a_0_5_dtconstr & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k1_funct_1(f1_s5_dtconstr,k1_nat_1(A,1)) = k2_xboole_0(k1_funct_1(f1_s5_dtconstr,A),a_1_2_dtconstr(A)) ) ) => ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m5_trees_3(B,k2_zfmisc_1(u1_struct_0(f2_s5_dtconstr),f3_s5_dtconstr),k5_trees_3(k2_zfmisc_1(u1_struct_0(f2_s5_dtconstr),f3_s5_dtconstr))) => ( r2_hidden(B,k3_card_3(f1_s5_dtconstr)) => ( r2_hidden(B,k1_funct_1(f1_s5_dtconstr,A)) <=> r1_xreal_0(k6_trees_1(k1_relat_1(B)),A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t79_trees_1,t3_trees_4,t80_trees_1,d2_xboole_0,t5_trees_4,t17_trees_4,t3_dtconstr,t7_dtconstr,d4_trees_4,t3_dtconstr,t7_dtconstr,s1_nat_1,t10_card_5,d2_xboole_0,t29_nat_1,t2_xreal_1,t10_trees_4,d5_funct_1,t39_trees_3,d4_finseq_1,d5_funct_1,d4_finseq_1,t31_funct_6,t10_card_5,t80_trees_3,t10_card_5,s5_nat_1,t7_xboole_1,t29_nat_1,t22_measure2,t38_nat_1,d2_xboole_0,t10_trees_4,d3_tarski,d5_funct_1,d4_finseq_1,d5_funct_1,t31_funct_6,d5_funct_1,t81_trees_3,t2_xreal_1,t38_nat_1,d4_finseq_1,d5_funct_1,t10_card_5,d4_finseq_1,d11_finseq_1,d2_xboole_0,t22_nat_1,s1_nat_1]), [file(dtconstr,s5_dtconstr),interesting(0.53)]). fof(s6_dtconstr,theorem, ( ( k1_relat_1(f1_s6_dtconstr) = k5_numbers & k1_funct_1(f1_s6_dtconstr,0) = a_0_6_dtconstr & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k1_funct_1(f1_s6_dtconstr,k1_nat_1(A,1)) = k2_xboole_0(k1_funct_1(f1_s6_dtconstr,A),a_1_3_dtconstr(A)) ) ) => ! [A] : ( ( v1_funct_1(A) & v3_trees_2(A) & m3_trees_2(A,k2_zfmisc_1(u1_struct_0(f2_s6_dtconstr),f3_s6_dtconstr)) ) => ! [B] : ( ( v1_funct_1(B) & v3_trees_2(B) & m3_trees_2(B,k2_zfmisc_1(u1_struct_0(f2_s6_dtconstr),f3_s6_dtconstr)) ) => ( ( r2_hidden(A,k3_card_3(f1_s6_dtconstr)) & r2_hidden(B,k3_card_3(f1_s6_dtconstr)) & k10_trees_3(u1_struct_0(f2_s6_dtconstr),f3_s6_dtconstr,A) = k10_trees_3(u1_struct_0(f2_s6_dtconstr),f3_s6_dtconstr,B) ) => A = B ) ) ) ), inference(mizar_proof,[status(thm)],[t25_trees_4,t4_trees_4,d2_lang1,t24_trees_4,t10_card_5,s3_dtconstr,s5_dtconstr,d2_xboole_0,d2_xboole_0,t31_trees_4,t31_trees_4,t15_trees_4,t2_dtconstr,t17_finseq_1,s1_nat_1,t10_card_5,t10_card_5,t7_xboole_1,t29_nat_1,t22_measure2,t28_nat_1]), [file(dtconstr,s6_dtconstr),interesting(0.52)]). fof(s7_dtconstr,theorem, ( ( ! [A] : ( m1_subset_1(A,u1_struct_0(f1_s7_dtconstr)) => ( r2_hidden(A,k5_lang1(f1_s7_dtconstr)) => p1_s7_dtconstr(k2_trees_4(u1_struct_0(f1_s7_dtconstr),A)) ) ) & ! [A] : ( m1_subset_1(A,u1_struct_0(f1_s7_dtconstr)) => ! [B] : ( m1_trees_4(B,k5_trees_3(u1_struct_0(f1_s7_dtconstr)),k4_dtconstr(f1_s7_dtconstr)) => ( ( r1_lang1(f1_s7_dtconstr,A,k1_dtconstr(u1_struct_0(f1_s7_dtconstr),k5_trees_3(u1_struct_0(f1_s7_dtconstr)),B)) & ! [C] : ( ( v1_funct_1(C) & v3_trees_2(C) & m3_trees_2(C,u1_struct_0(f1_s7_dtconstr)) ) => ( r2_hidden(C,k2_relat_1(B)) => p1_s7_dtconstr(C) ) ) ) => p1_s7_dtconstr(k12_trees_4(u1_struct_0(f1_s7_dtconstr),A,B)) ) ) ) ) => ! [A] : ( ( v1_funct_1(A) & v3_trees_2(A) & m3_trees_2(A,u1_struct_0(f1_s7_dtconstr)) ) => ( r2_hidden(A,k4_dtconstr(f1_s7_dtconstr)) => p1_s7_dtconstr(A) ) ) ), inference(mizar_proof,[status(thm)],[s3_recdef_1,s3_dtconstr,s4_dtconstr,d4_dtconstr,t29_finseq_1,t3_dtconstr,t20_trees_4,t25_trees_4,t27_finseq_1,d2_xboole_0,d5_funct_1,d4_card_3,d4_finseq_1,t92_zfmisc_1,d3_finseq_1,d5_funct_1,t1_xboole_1,d1_funct_2,d9_trees_2,d12_trees_3,t46_relat_1,d8_trees_3,s5_finseq_1,t1_dtconstr,d18_trees_3,d12_mcart_1,d18_trees_3,t47_trees_1,d18_trees_3,t41_trees_3,d18_trees_3,d12_mcart_1,t17_finseq_1,d3_tarski,d5_funct_1,t25_finseq_3,d4_finseq_1,d5_funct_1,t25_finseq_3,d5_funct_1,t1_dtconstr,t27_trees_4,s1_nat_1,t10_card_5]), [file(dtconstr,s7_dtconstr),interesting(0.52)]). fof(l19_dtconstr,theorem,( r1_lang1(k5_dtconstr,c3,k3_lang1(u1_struct_0(k5_dtconstr),c3)) ), inference(mizar_proof,[status(thm)],[d5_dtconstr]), [file(dtconstr,l19_dtconstr),interesting(0.50)]). fof(t9_dtconstr,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v1_dtconstr(A) & l1_lang1(A) ) => ! [B] : ( m1_dtconstr(B,u1_struct_0(A),k5_trees_3(u1_struct_0(A)),k4_dtconstr(A)) => ! [C] : ( m1_struct_0(C,A,k6_dtconstr(A)) => ( k1_funct_1(B,k1_xboole_0) = C => B = k8_dtconstr(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t3_trees_4,d4_trees_4,d2_lang1,s7_dtconstr]), [file(dtconstr,t9_dtconstr),interesting(0.50)]). fof(l16_dtconstr,theorem, ( m1_subset_1(0,u1_struct_0(k5_dtconstr)) & m1_subset_1(1,u1_struct_0(k5_dtconstr)) ), inference(mizar_proof,[status(thm)],[l15_dtconstr,d2_tarski]), [file(dtconstr,l16_dtconstr),interesting(0.49)]). fof(t6_dtconstr,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v3_trees_2(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v3_trees_2(B) ) => k16_trees_3(k10_finseq_1(A,B)) = k10_finseq_1(k1_funct_1(A,k1_xboole_0),k1_funct_1(B,k1_xboole_0)) ) ) ), inference(mizar_proof,[status(thm)],[t61_finseq_1,d3_finseq_1,d3_finseq_1,t4_finseq_1,d2_tarski,d18_trees_3]), [file(dtconstr,t6_dtconstr),interesting(0.48)]). fof(s1_dtconstr,theorem,( ? [A] : ( ~ v3_struct_0(A) & v1_lang1(A) & l1_lang1(A) & u1_struct_0(A) = f1_s1_dtconstr & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m2_finseq_1(C,u1_struct_0(A)) => ( r1_lang1(A,B,C) <=> p1_s1_dtconstr(B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[s1_relset_1,d1_lang1,d11_finseq_1,d1_lang1]), [file(dtconstr,s1_dtconstr),interesting(0.42)]). fof(s8_dtconstr,theorem,( ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k4_dtconstr(f1_s8_dtconstr),f2_s8_dtconstr) & m2_relset_1(A,k4_dtconstr(f1_s8_dtconstr),f2_s8_dtconstr) & ! [B] : ( m1_subset_1(B,u1_struct_0(f1_s8_dtconstr)) => ( r2_hidden(B,k5_lang1(f1_s8_dtconstr)) => k1_funct_1(A,k2_trees_4(u1_struct_0(f1_s8_dtconstr),B)) = f3_s8_dtconstr(B) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(f1_s8_dtconstr)) => ! [C] : ( m1_trees_4(C,k5_trees_3(u1_struct_0(f1_s8_dtconstr)),k4_dtconstr(f1_s8_dtconstr)) => ( r1_lang1(f1_s8_dtconstr,B,k1_dtconstr(u1_struct_0(f1_s8_dtconstr),k5_trees_3(u1_struct_0(f1_s8_dtconstr)),C)) => k1_funct_1(A,k12_trees_4(u1_struct_0(f1_s8_dtconstr),B,C)) = f4_s8_dtconstr(B,k1_dtconstr(u1_struct_0(f1_s8_dtconstr),k5_trees_3(u1_struct_0(f1_s8_dtconstr)),C),k5_finseqop(k4_dtconstr(f1_s8_dtconstr),f2_s8_dtconstr,C,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[s3_recdef_1,s4_dtconstr,d4_dtconstr,t47_trees_1,s6_dtconstr,s1_wellord2,d1_funct_2,t11_relset_1,s3_dtconstr,t25_trees_4,t3_trees_4,d3_finseq_1,d4_finseq_1,d5_funct_1,s5_finseq_1,d3_tarski,d5_funct_1,t25_finseq_3,d4_finseq_1,d18_trees_3,d12_mcart_1,d13_mcart_1,d18_trees_3,t47_trees_1,d18_trees_3,t41_trees_3,d18_trees_3,d12_mcart_1,t17_finseq_1,d4_finseq_1,t22_trees_3,t1_xboole_1,d4_finseq_1,d4_finseq_1,t22_trees_3,t1_xboole_1,d4_finseq_1,t27_trees_4,d4_finseq_1,t46_relat_1,t47_trees_1,d5_funct_1,t22_funct_1,t41_trees_3,d18_trees_3,d13_mcart_1,t17_finseq_1,t47_trees_1,t41_trees_3,d4_trees_4,t7_mcart_1]), [file(dtconstr,s8_dtconstr),interesting(0.40)]). fof(t10_dtconstr,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v1_dtconstr(A) & v2_dtconstr(A) & l1_lang1(A) ) => ! [B] : ( m1_dtconstr(B,u1_struct_0(A),k5_trees_3(u1_struct_0(A)),k4_dtconstr(A)) => ! [C] : ( m1_struct_0(C,A,k7_dtconstr(A)) => ~ ( k1_funct_1(B,k1_xboole_0) = C & ! [D] : ( m1_trees_4(D,k5_trees_3(u1_struct_0(A)),k4_dtconstr(A)) => ~ ( B = k12_trees_4(u1_struct_0(A),C,D) & r1_lang1(A,C,k1_dtconstr(u1_struct_0(A),k5_trees_3(u1_struct_0(A)),D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t3_trees_4,d2_lang1,d3_lang1,d4_trees_4,s7_dtconstr]), [file(dtconstr,t10_dtconstr),interesting(0.35)]). fof(s4_dtconstr,theorem, ( ( k1_relat_1(f1_s4_dtconstr) = k5_numbers & k1_funct_1(f1_s4_dtconstr,0) = a_0_3_dtconstr & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k1_funct_1(f1_s4_dtconstr,k1_nat_1(A,1)) = k2_xboole_0(k1_funct_1(f1_s4_dtconstr,A),a_1_1_dtconstr(A)) ) ) => ? [A] : ( m1_subset_1(A,k1_zfmisc_1(k5_trees_3(u1_struct_0(f2_s4_dtconstr)))) & A = a_0_4_dtconstr & ! [B] : ( m1_subset_1(B,u1_struct_0(f2_s4_dtconstr)) => ( r2_hidden(B,k5_lang1(f2_s4_dtconstr)) => r2_hidden(k2_trees_4(u1_struct_0(f2_s4_dtconstr),B),A) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(f2_s4_dtconstr)) => ! [C] : ( m1_trees_4(C,k5_trees_3(u1_struct_0(f2_s4_dtconstr)),A) => ( r1_lang1(f2_s4_dtconstr,B,k1_dtconstr(u1_struct_0(f2_s4_dtconstr),k5_trees_3(u1_struct_0(f2_s4_dtconstr)),C)) => r2_hidden(k12_trees_4(u1_struct_0(f2_s4_dtconstr),B,C),A) ) ) ) & ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k5_trees_3(u1_struct_0(f2_s4_dtconstr)))) => ( ( ! [C] : ( m1_subset_1(C,u1_struct_0(f2_s4_dtconstr)) => ( r2_hidden(C,k5_lang1(f2_s4_dtconstr)) => r2_hidden(k2_trees_4(u1_struct_0(f2_s4_dtconstr),C),B) ) ) & ! [C] : ( m1_subset_1(C,u1_struct_0(f2_s4_dtconstr)) => ! [D] : ( m1_trees_4(D,k5_trees_3(u1_struct_0(f2_s4_dtconstr)),B) => ( r1_lang1(f2_s4_dtconstr,C,k1_dtconstr(u1_struct_0(f2_s4_dtconstr),k5_trees_3(u1_struct_0(f2_s4_dtconstr)),D)) => r2_hidden(k12_trees_4(u1_struct_0(f2_s4_dtconstr),C,D),B) ) ) ) ) => r1_tarski(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[s3_dtconstr,d3_tarski,d1_funct_2,d9_trees_2,d12_trees_3,t46_relat_1,d8_trees_3,t25_trees_4,d3_finseq_1,d4_finseq_1,d5_funct_1,s5_finseq_1,d3_tarski,d5_funct_1,t25_finseq_3,d4_finseq_1,d18_trees_3,d12_mcart_1,d13_mcart_1,d18_trees_3,t47_trees_1,d18_trees_3,t41_trees_3,d18_trees_3,d12_mcart_1,t17_finseq_1,d4_finseq_1,t22_trees_3,t1_xboole_1,d4_finseq_1,d4_finseq_1,t22_trees_3,t1_xboole_1,d4_finseq_1,t27_trees_4,d3_tarski,d3_tarski,t25_trees_4,t31_trees_4,d3_tarski,d5_funct_1,t25_finseq_3,d5_funct_1,d4_finseq_1,d4_finseq_1,d18_trees_3,d12_mcart_1,d18_trees_3,d5_funct_1,d4_finseq_1,t47_trees_1,d18_trees_3,t41_trees_3,d18_trees_3,d12_mcart_1,t17_finseq_1]), [file(dtconstr,s4_dtconstr),interesting(0.30)]). fof(s9_dtconstr,theorem, ( ( ! [A] : ( m1_subset_1(A,u1_struct_0(f1_s9_dtconstr)) => ( r2_hidden(A,k5_lang1(f1_s9_dtconstr)) => k1_funct_1(f5_s9_dtconstr,k2_trees_4(u1_struct_0(f1_s9_dtconstr),A)) = f3_s9_dtconstr(A) ) ) & ! [A] : ( m1_subset_1(A,u1_struct_0(f1_s9_dtconstr)) => ! [B] : ( m1_trees_4(B,k5_trees_3(u1_struct_0(f1_s9_dtconstr)),k4_dtconstr(f1_s9_dtconstr)) => ( r1_lang1(f1_s9_dtconstr,A,k1_dtconstr(u1_struct_0(f1_s9_dtconstr),k5_trees_3(u1_struct_0(f1_s9_dtconstr)),B)) => k1_funct_1(f5_s9_dtconstr,k12_trees_4(u1_struct_0(f1_s9_dtconstr),A,B)) = f4_s9_dtconstr(A,k1_dtconstr(u1_struct_0(f1_s9_dtconstr),k5_trees_3(u1_struct_0(f1_s9_dtconstr)),B),k5_finseqop(k4_dtconstr(f1_s9_dtconstr),f2_s9_dtconstr,B,f5_s9_dtconstr)) ) ) ) & ! [A] : ( m1_subset_1(A,u1_struct_0(f1_s9_dtconstr)) => ( r2_hidden(A,k5_lang1(f1_s9_dtconstr)) => k1_funct_1(f6_s9_dtconstr,k2_trees_4(u1_struct_0(f1_s9_dtconstr),A)) = f3_s9_dtconstr(A) ) ) & ! [A] : ( m1_subset_1(A,u1_struct_0(f1_s9_dtconstr)) => ! [B] : ( m1_trees_4(B,k5_trees_3(u1_struct_0(f1_s9_dtconstr)),k4_dtconstr(f1_s9_dtconstr)) => ( r1_lang1(f1_s9_dtconstr,A,k1_dtconstr(u1_struct_0(f1_s9_dtconstr),k5_trees_3(u1_struct_0(f1_s9_dtconstr)),B)) => k1_funct_1(f6_s9_dtconstr,k12_trees_4(u1_struct_0(f1_s9_dtconstr),A,B)) = f4_s9_dtconstr(A,k1_dtconstr(u1_struct_0(f1_s9_dtconstr),k5_trees_3(u1_struct_0(f1_s9_dtconstr)),B),k5_finseqop(k4_dtconstr(f1_s9_dtconstr),f2_s9_dtconstr,B,f6_s9_dtconstr)) ) ) ) ) => f5_s9_dtconstr = f6_s9_dtconstr ), inference(mizar_proof,[status(thm)],[d4_finseq_1,d1_funct_2,d3_finseq_1,t46_relat_1,d1_funct_2,t46_relat_1,t2_dtconstr,d5_funct_1,t22_funct_1,t22_funct_1,t9_funct_1,s7_dtconstr,t18_funct_2]), [file(dtconstr,s9_dtconstr),interesting(0.18)]). fof(d5_dtconstr,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v1_lang1(A) & l1_lang1(A) ) => ( A = k5_dtconstr <=> ( u1_struct_0(A) = k7_domain_1(k5_numbers,0,1) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m2_finseq_1(C,u1_struct_0(A)) => ( r1_lang1(A,B,C) <=> ( B = 1 & ( C = k3_lang1(k5_numbers,0) | C = k3_lang1(k5_numbers,1) ) ) ) ) ) ) ) ) ), file(dtconstr,d5_dtconstr), [interesting(0.00)]). fof(d2_tarski,definition,( ! [A,B,C] : ( C = k2_tarski(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( D = A | D = B ) ) ) ), file(tarski,d2_tarski), [interesting(0.00)]). fof(d3_tarski,definition,( ! [A,B] : ( r1_tarski(A,B) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(C,B) ) ) ), file(tarski,d3_tarski), [interesting(0.00)]). fof(d3_lang1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_lang1(A) ) => k6_lang1(A) = a_1_1_lang1(A) ) ), file(lang1,d3_lang1), [interesting(0.00)]). fof(d1_lang1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_lang1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( r1_lang1(A,B,C) <=> r2_hidden(k4_tarski(B,C),u1_lang1(A)) ) ) ) ) ), file(lang1,d1_lang1), [interesting(0.00)]). fof(t106_zfmisc_1,theorem,( ! [A,B,C,D] : ( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) <=> ( r2_hidden(A,C) & r2_hidden(B,D) ) ) ), file(zfmisc_1,t106_zfmisc_1), [interesting(0.00)]). fof(d3_finseq_2,definition,( ! [A,B] : ( m1_finseq_2(B,A) <=> ! [C] : ( r2_hidden(C,B) => m2_finseq_1(C,A) ) ) ), file(finseq_2,d3_finseq_2), [interesting(0.00)]). fof(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [interesting(0.00)]). fof(t37_zfmisc_1,theorem,( ! [A,B] : ( r1_tarski(k1_tarski(A),B) <=> r2_hidden(A,B) ) ), file(zfmisc_1,t37_zfmisc_1), [interesting(0.00)]). fof(d10_xboole_0,definition,( ! [A,B] : ( A = B <=> ( r1_tarski(A,B) & r1_tarski(B,A) ) ) ), file(xboole_0,d10_xboole_0), [interesting(0.00)]). fof(d4_dtconstr,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_lang1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k5_trees_3(u1_struct_0(A)))) => ( B = k4_dtconstr(A) <=> ( ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r2_hidden(C,k5_lang1(A)) => r2_hidden(k2_trees_4(u1_struct_0(A),C),B) ) ) & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_trees_4(D,k5_trees_3(u1_struct_0(A)),B) => ( r1_lang1(A,C,k1_dtconstr(u1_struct_0(A),k5_trees_3(u1_struct_0(A)),D)) => r2_hidden(k12_trees_4(u1_struct_0(A),C,D),B) ) ) ) & ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k5_trees_3(u1_struct_0(A)))) => ( ( ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_hidden(D,k5_lang1(A)) => r2_hidden(k2_trees_4(u1_struct_0(A),D),C) ) ) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_trees_4(E,k5_trees_3(u1_struct_0(A)),C) => ( r1_lang1(A,D,k1_dtconstr(u1_struct_0(A),k5_trees_3(u1_struct_0(A)),E)) => r2_hidden(k12_trees_4(u1_struct_0(A),D,E),C) ) ) ) ) => r1_tarski(B,C) ) ) ) ) ) ) ), file(dtconstr,d4_dtconstr), [interesting(0.00)]). fof(d2_lang1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_lang1(A) ) => k5_lang1(A) = a_1_0_lang1(A) ) ), file(lang1,d2_lang1), [interesting(0.00)]). fof(d6_dtconstr,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_lang1(A) ) => ( v1_dtconstr(A) <=> k5_lang1(A) != k1_xboole_0 ) ) ), file(dtconstr,d6_dtconstr), [interesting(0.00)]). fof(d7_dtconstr,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_lang1(A) ) => ( v2_dtconstr(A) <=> k6_lang1(A) != k1_xboole_0 ) ) ), file(dtconstr,d7_dtconstr), [interesting(0.00)]). fof(d8_dtconstr,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_lang1(A) ) => ( v3_dtconstr(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ~ ( r2_hidden(B,k6_lang1(A)) & ! [C] : ( m1_trees_4(C,k5_trees_3(u1_struct_0(A)),k4_dtconstr(A)) => ~ r1_lang1(A,B,k1_dtconstr(u1_struct_0(A),k5_trees_3(u1_struct_0(A)),C)) ) ) ) ) ) ), file(dtconstr,d8_dtconstr), [interesting(0.00)]). fof(t55_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( B = k9_finseq_1(A) <=> ( k4_finseq_1(B) = k2_finseq_1(1) & k2_relat_1(B) = k1_tarski(A) ) ) ) ), file(finseq_1,t55_finseq_1), [interesting(0.00)]). fof(t4_finseq_1,theorem, ( k2_finseq_1(0) = k1_xboole_0 & k2_finseq_1(1) = k1_tarski(1) & k2_finseq_1(2) = k2_tarski(1,2) ), file(finseq_1,t4_finseq_1), [interesting(0.00)]). fof(t57_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( B = k9_finseq_1(A) <=> ( k3_finseq_1(B) = 1 & k1_funct_1(B,1) = A ) ) ) ), file(finseq_1,t57_finseq_1), [interesting(0.00)]). fof(t3_trees_4,theorem,( ! [A] : ( k1_relat_1(k1_trees_4(A)) = k2_trees_1(0) & k1_funct_1(k1_trees_4(A),k1_xboole_0) = A ) ), file(trees_4,t3_trees_4), [interesting(0.00)]). fof(d18_trees_3,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( v6_trees_3(A) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( B = k16_trees_3(A) <=> ( k4_finseq_1(B) = k4_finseq_1(A) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ ( r2_hidden(C,k4_finseq_1(A)) & ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) & v3_trees_2(D) ) => ~ ( D = k1_funct_1(A,C) & k1_funct_1(B,C) = k1_funct_1(D,k1_xboole_0) ) ) ) ) ) ) ) ) ) ), file(trees_3,d18_trees_3), [interesting(0.00)]). fof(s1_relset_1,theorem,( ? [A] : ( m2_relset_1(A,f1_s1_relset_1,f2_s1_relset_1) & ! [B,C] : ( r2_hidden(k4_tarski(B,C),A) <=> ( r2_hidden(B,f1_s1_relset_1) & r2_hidden(C,f2_s1_relset_1) & p1_s1_relset_1(B,C) ) ) ) ), file(relset_1,s1_relset_1), [interesting(0.00)]). fof(d11_finseq_1,definition,( ! [A,B] : ( B = k13_finseq_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> m2_finseq_1(C,A) ) ) ), file(finseq_1,d11_finseq_1), [interesting(0.00)]). fof(d2_relat_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ( A = B <=> ! [C,D] : ( r2_hidden(k4_tarski(C,D),A) <=> r2_hidden(k4_tarski(C,D),B) ) ) ) ) ), file(relat_1,d2_relat_1), [interesting(0.00)]). fof(s2_dtconstr,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v1_lang1(A) & l1_lang1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v1_lang1(B) & l1_lang1(B) ) => ( ( u1_struct_0(A) = f1_s2_dtconstr & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m2_finseq_1(D,u1_struct_0(A)) => ( r1_lang1(A,C,D) <=> p1_s2_dtconstr(C,D) ) ) ) & u1_struct_0(B) = f1_s2_dtconstr & ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m2_finseq_1(D,u1_struct_0(B)) => ( r1_lang1(B,C,D) <=> p1_s2_dtconstr(C,D) ) ) ) ) => A = B ) ) ) ), inference(mizar_proof,[status(thm)],[t106_zfmisc_1,t106_zfmisc_1,d3_finseq_2,t106_zfmisc_1,d3_finseq_2,d1_lang1,d1_lang1,t106_zfmisc_1,t106_zfmisc_1,d3_finseq_2,t106_zfmisc_1,d3_finseq_2,d1_lang1,d1_lang1,d2_relat_1]), [file(dtconstr,s2_dtconstr),interesting(0.00)]). fof(s3_recdef_1,theorem,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & k1_relat_1(A) = k5_numbers & k1_funct_1(A,0) = f1_s3_recdef_1 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => k1_funct_1(A,k1_nat_1(B,1)) = f2_s3_recdef_1(B,k1_funct_1(A,B)) ) ) ), file(recdef_1,s3_recdef_1), [interesting(0.00)]). fof(t10_card_5,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r2_hidden(A,k3_card_3(B)) <=> ? [C] : ( r2_hidden(C,k1_relat_1(B)) & r2_hidden(A,k1_funct_1(B,C)) ) ) ) ), file(card_5,t10_card_5), [interesting(0.00)]). fof(d2_xboole_0,definition,( ! [A,B,C] : ( C = k2_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) | r2_hidden(D,B) ) ) ) ), file(xboole_0,d2_xboole_0), [interesting(0.00)]). fof(s1_nat_1,theorem, ( ( p1_s1_nat_1(0) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( p1_s1_nat_1(A) => p1_s1_nat_1(k1_nat_1(A,1)) ) ) ) => ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => p1_s1_nat_1(A) ) ), file(nat_1,s1_nat_1), [interesting(0.00)]). fof(d3_finseq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( B = k3_finseq_1(A) <=> k2_finseq_1(B) = k1_relat_1(A) ) ) ) ), file(finseq_1,d3_finseq_1), [interesting(0.00)]). fof(d4_finseq_1,definition,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( m1_finseq_1(B,A) <=> r1_tarski(k2_relat_1(B),A) ) ) ), file(finseq_1,d4_finseq_1), [interesting(0.00)]). fof(d5_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( B = k2_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(D,k1_relat_1(A)) & C = k1_funct_1(A,D) ) ) ) ) ), file(funct_1,d5_funct_1), [interesting(0.00)]). fof(s5_finseq_1,theorem, ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ~ ( r2_hidden(A,k2_finseq_1(f2_s5_finseq_1)) & ! [B] : ( m1_subset_1(B,f1_s5_finseq_1) => ~ p1_s5_finseq_1(A,B) ) ) ) => ? [A] : ( m2_finseq_1(A,f1_s5_finseq_1) & k4_finseq_1(A) = k2_finseq_1(f2_s5_finseq_1) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r2_hidden(B,k2_finseq_1(f2_s5_finseq_1)) => p1_s5_finseq_1(B,k1_funct_1(A,B)) ) ) ) ), file(finseq_1,s5_finseq_1), [interesting(0.00)]). fof(t2_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,C) ) => r1_xreal_0(A,C) ) ) ) ) ), file(xreal_1,t2_xreal_1), [interesting(0.00)]). fof(s4_cqc_sim1,theorem, ( ( v1_finset_1(f2_s4_cqc_sim1) & f2_s4_cqc_sim1 != k1_xboole_0 & r1_tarski(f2_s4_cqc_sim1,f1_s4_cqc_sim1) & ! [A] : ( m1_subset_1(A,f1_s4_cqc_sim1) => ! [B] : ( m1_subset_1(B,f1_s4_cqc_sim1) => ( p1_s4_cqc_sim1(A,B) | p1_s4_cqc_sim1(B,A) ) ) ) & ! [A] : ( m1_subset_1(A,f1_s4_cqc_sim1) => ! [B] : ( m1_subset_1(B,f1_s4_cqc_sim1) => ! [C] : ( m1_subset_1(C,f1_s4_cqc_sim1) => ( ( p1_s4_cqc_sim1(A,B) & p1_s4_cqc_sim1(B,C) ) => p1_s4_cqc_sim1(A,C) ) ) ) ) ) => ? [A] : ( m1_subset_1(A,f1_s4_cqc_sim1) & r2_hidden(A,f2_s4_cqc_sim1) & ! [B] : ( m1_subset_1(B,f1_s4_cqc_sim1) => ( r2_hidden(B,f2_s4_cqc_sim1) => p1_s4_cqc_sim1(A,B) ) ) ) ), file(cqc_sim1,s4_cqc_sim1), [interesting(0.00)]). fof(t25_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k4_finseq_1(A)) => m2_subset_1(B,k1_numbers,k5_numbers) ) ) ), file(finseq_3,t25_finseq_3), [interesting(0.00)]). fof(t28_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ~ ( r1_xreal_0(A,B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => B != k2_xcmplx_0(A,C) ) ) ) ) ), file(nat_1,t28_nat_1), [interesting(0.00)]). fof(t7_xboole_1,theorem,( ! [A,B] : r1_tarski(A,k2_xboole_0(A,B)) ), file(xboole_1,t7_xboole_1), [interesting(0.00)]). fof(t29_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => r1_xreal_0(A,k2_xcmplx_0(A,B)) ) ) ), file(nat_1,t29_nat_1), [interesting(0.00)]). fof(t22_measure2,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => r1_tarski(k1_funct_1(A,B),k1_funct_1(A,k1_nat_1(B,1))) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(C,B) => r1_tarski(k1_funct_1(A,C),k1_funct_1(A,B)) ) ) ) ) ) ), file(measure2,t22_measure2), [interesting(0.00)]). fof(t27_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( A = k1_xboole_0 <=> k2_relat_1(A) = k1_xboole_0 ) ) ), file(finseq_1,t27_finseq_1), [interesting(0.00)]). fof(t26_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( A = k1_xboole_0 <=> k4_finseq_1(A) = k1_xboole_0 ) ) ), file(finseq_1,t26_finseq_1), [interesting(0.00)]). fof(t2_xboole_1,theorem,( ! [A] : r1_tarski(k1_xboole_0,A) ), file(xboole_1,t2_xboole_1), [interesting(0.00)]). fof(d4_card_3,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => k3_card_3(A) = k3_tarski(k2_relat_1(A)) ) ), file(card_3,d4_card_3), [interesting(0.00)]). fof(t92_zfmisc_1,theorem,( ! [A,B] : ( r2_hidden(A,B) => r1_tarski(A,k3_tarski(B)) ) ), file(zfmisc_1,t92_zfmisc_1), [interesting(0.00)]). fof(t1_xboole_1,theorem,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_tarski(B,C) ) => r1_tarski(A,C) ) ), file(xboole_1,t1_xboole_1), [interesting(0.00)]). fof(t29_finseq_1,theorem,( ! [A] : m2_finseq_1(k1_xboole_0,A) ), file(finseq_1,t29_finseq_1), [interesting(0.00)]). fof(t23_trees_3,theorem, ( v4_trees_3(k1_xboole_0) & v5_trees_3(k1_xboole_0) & v6_trees_3(k1_xboole_0) ), file(trees_3,t23_trees_3), [interesting(0.00)]). fof(d12_mcart_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( B = k15_mcart_1(A) <=> ( k1_relat_1(B) = k1_relat_1(A) & ! [C] : ( r2_hidden(C,k1_relat_1(A)) => k1_funct_1(B,C) = k1_mcart_1(k1_funct_1(A,C)) ) ) ) ) ) ), file(mcart_1,d12_mcart_1), [interesting(0.00)]). fof(d13_mcart_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( B = k16_mcart_1(A) <=> ( k1_relat_1(B) = k1_relat_1(A) & ! [C] : ( r2_hidden(C,k1_relat_1(A)) => k1_funct_1(B,C) = k2_mcart_1(k1_funct_1(A,C)) ) ) ) ) ) ), file(mcart_1,d13_mcart_1), [interesting(0.00)]). fof(t20_trees_4,theorem,( ! [A] : ( k3_trees_4(A,k1_xboole_0) = k1_trees_4(A) & k4_trees_4(A,k1_xboole_0) = k1_trees_4(A) ) ), file(trees_4,t20_trees_4), [interesting(0.00)]). fof(s3_dtconstr,theorem, ( ( k1_relat_1(f1_s3_dtconstr) = k5_numbers & k1_funct_1(f1_s3_dtconstr,0) = a_0_2_dtconstr & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k1_funct_1(f1_s3_dtconstr,k1_nat_1(A,1)) = k2_xboole_0(k1_funct_1(f1_s3_dtconstr,A),a_1_0_dtconstr(A)) ) ) => ? [A] : ( m1_subset_1(A,k1_zfmisc_1(k5_trees_3(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr)))) & A = k3_card_3(f1_s3_dtconstr) & ! [B] : ( m1_subset_1(B,u1_struct_0(f2_s3_dtconstr)) => ( r2_hidden(B,k5_lang1(f2_s3_dtconstr)) => r2_hidden(k2_trees_4(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr),k1_domain_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr,B,f4_s3_dtconstr(B))),A) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(f2_s3_dtconstr)) => ! [C] : ( m1_trees_4(C,k5_trees_3(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr)),A) => ( r1_lang1(f2_s3_dtconstr,B,k2_dtconstr(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr,k1_dtconstr(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr),k5_trees_3(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr)),C))) => r2_hidden(k12_trees_4(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr),k1_domain_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr,B,f5_s3_dtconstr(B,k2_dtconstr(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr,k1_dtconstr(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr),k5_trees_3(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr)),C)),k3_dtconstr(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr,k1_dtconstr(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr),k5_trees_3(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr)),C)))),C),A) ) ) ) & ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k5_trees_3(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr)))) => ( ( ! [C] : ( m1_subset_1(C,u1_struct_0(f2_s3_dtconstr)) => ( r2_hidden(C,k5_lang1(f2_s3_dtconstr)) => r2_hidden(k2_trees_4(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr),k1_domain_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr,C,f4_s3_dtconstr(C))),B) ) ) & ! [C] : ( m1_subset_1(C,u1_struct_0(f2_s3_dtconstr)) => ! [D] : ( m1_trees_4(D,k5_trees_3(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr)),B) => ( r1_lang1(f2_s3_dtconstr,C,k2_dtconstr(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr,k1_dtconstr(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr),k5_trees_3(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr)),D))) => r2_hidden(k12_trees_4(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr),k1_domain_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr,C,f5_s3_dtconstr(C,k2_dtconstr(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr,k1_dtconstr(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr),k5_trees_3(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr)),D)),k3_dtconstr(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr,k1_dtconstr(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr),k5_trees_3(k2_zfmisc_1(u1_struct_0(f2_s3_dtconstr),f3_s3_dtconstr)),D)))),D),B) ) ) ) ) => r1_tarski(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t10_card_5,d2_xboole_0,s1_nat_1,t10_card_5,d3_finseq_1,d4_finseq_1,d5_funct_1,t10_card_5,s5_finseq_1,d4_finseq_1,t2_xreal_1,s4_cqc_sim1,d3_tarski,d5_funct_1,t25_finseq_3,d5_funct_1,t28_nat_1,t7_xboole_1,t29_nat_1,t22_measure2,t27_finseq_1,t26_finseq_1,t26_finseq_1,t27_finseq_1,t2_xboole_1,d5_funct_1,d4_card_3,t92_zfmisc_1,t1_xboole_1,d4_finseq_1,d11_finseq_1,d2_xboole_0,t10_card_5,d3_tarski,t29_finseq_1,t3_dtconstr,t7_dtconstr,t20_trees_4,d3_tarski,d2_xboole_0,d4_finseq_1,t1_xboole_1,d4_finseq_1,s1_nat_1,d3_tarski,t10_card_5]), [file(dtconstr,s3_dtconstr),interesting(0.00)]). fof(d1_funct_2,definition,( ! [A,B,C] : ( m2_relset_1(C,A,B) => ( ( ( B = k1_xboole_0 => A = k1_xboole_0 ) => ( v1_funct_2(C,A,B) <=> A = k4_relset_1(A,B,C) ) ) & ( B = k1_xboole_0 => ( A = k1_xboole_0 | ( v1_funct_2(C,A,B) <=> C = k1_xboole_0 ) ) ) ) ) ), file(funct_2,d1_funct_2), [interesting(0.00)]). fof(d9_trees_2,definition,( ! [A,B] : ( v1_relat_1(B) => ( m3_trees_2(B,A) <=> r1_tarski(k2_relat_1(B),A) ) ) ), file(trees_2,d9_trees_2), [interesting(0.00)]). fof(d12_trees_3,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v3_trees_2(C) & m3_trees_2(C,k2_zfmisc_1(A,B)) ) => k10_trees_3(A,B,C) = k7_trees_3(k2_zfmisc_1(A,B),A,C,k8_trees_3(A,B)) ) ) ) ), file(trees_3,d12_trees_3), [interesting(0.00)]). fof(t46_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ( r1_tarski(k2_relat_1(A),k1_relat_1(B)) => k1_relat_1(k5_relat_1(A,B)) = k1_relat_1(A) ) ) ) ), file(relat_1,t46_relat_1), [interesting(0.00)]). fof(d8_trees_3,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m4_trees_3(B,A) => ( B = k5_trees_3(A) <=> ! [C] : ( ( v1_funct_1(C) & v3_trees_2(C) & m3_trees_2(C,A) ) => ( v1_finset_1(k1_relat_1(C)) <=> r2_hidden(C,B) ) ) ) ) ) ), file(trees_3,d8_trees_3), [interesting(0.00)]). fof(t25_trees_4,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,B) => ( k10_trees_3(A,B,k2_trees_4(k2_zfmisc_1(A,B),k1_domain_1(A,B,C,D))) = k2_trees_4(A,C) & k11_trees_3(A,B,k2_trees_4(k2_zfmisc_1(A,B),k1_domain_1(A,B,C,D))) = k2_trees_4(B,D) ) ) ) ) ) ), file(trees_4,t25_trees_4), [interesting(0.00)]). fof(t47_trees_1,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & v1_trees_1(A) ) => ( r2_hidden(k1_xboole_0,A) & r2_hidden(k6_finseq_1(k5_numbers),A) ) ) ), file(trees_1,t47_trees_1), [interesting(0.00)]). fof(t41_trees_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v3_trees_2(C) & m3_trees_2(C,k2_zfmisc_1(A,B)) ) => ! [D] : ( m1_trees_1(D,k1_relat_1(C)) => ( k2_domain_1(A,B,k3_trees_2(k2_zfmisc_1(A,B),C,D)) = k1_funct_1(k10_trees_3(A,B,C),D) & k1_funct_1(k11_trees_3(A,B,C),D) = k3_domain_1(A,B,k3_trees_2(k2_zfmisc_1(A,B),C,D)) ) ) ) ) ) ), file(trees_3,t41_trees_3), [interesting(0.00)]). fof(t17_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( ( k4_finseq_1(A) = k4_finseq_1(B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r2_hidden(C,k4_finseq_1(A)) => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) ) => A = B ) ) ) ), file(finseq_1,t17_finseq_1), [interesting(0.00)]). fof(t22_trees_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => r1_tarski(k5_trees_3(A),k4_trees_3(A)) ) ), file(trees_3,t22_trees_3), [interesting(0.00)]). fof(t27_trees_4,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,B) => ! [E] : ( ( ~ v1_xboole_0(E) & m4_trees_3(E,k2_zfmisc_1(A,B)) ) => ! [F] : ( ( ~ v1_xboole_0(F) & m4_trees_3(F,A) ) => ! [G] : ( m2_finseq_1(G,E) => ! [H] : ( m2_finseq_1(H,F) => ( ( k4_finseq_1(H) = k4_finseq_1(G) & ! [I] : ( m2_subset_1(I,k1_numbers,k5_numbers) => ( r2_hidden(I,k4_finseq_1(G)) => ! [J] : ( ( v1_funct_1(J) & v3_trees_2(J) & m3_trees_2(J,k2_zfmisc_1(A,B)) ) => ( J = k1_funct_1(G,I) => k1_funct_1(H,I) = k10_trees_3(A,B,J) ) ) ) ) ) => k10_trees_3(A,B,k8_trees_4(k2_zfmisc_1(A,B),E,k1_domain_1(A,B,C,D),G)) = k8_trees_4(A,F,C,H) ) ) ) ) ) ) ) ) ) ), file(trees_4,t27_trees_4), [interesting(0.00)]). fof(t31_trees_4,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,B) => ! [E] : ( m2_finseq_1(E,k5_trees_3(k2_zfmisc_1(A,B))) => ? [F] : ( m2_finseq_1(F,k5_trees_3(A)) & k4_finseq_1(F) = k4_finseq_1(E) & ! [G] : ( m2_subset_1(G,k1_numbers,k5_numbers) => ~ ( r2_hidden(G,k4_finseq_1(E)) & ! [H] : ( m5_trees_3(H,k2_zfmisc_1(A,B),k5_trees_3(k2_zfmisc_1(A,B))) => ~ ( H = k1_funct_1(E,G) & k1_funct_1(F,G) = k10_trees_3(A,B,H) ) ) ) ) & k10_trees_3(A,B,k12_trees_4(k2_zfmisc_1(A,B),k1_domain_1(A,B,C,D),E)) = k12_trees_4(A,C,F) ) ) ) ) ) ) ), file(trees_4,t31_trees_4), [interesting(0.00)]). fof(t4_trees_4,theorem,( ! [A,B] : ( k1_trees_4(A) = k1_trees_4(B) => A = B ) ), file(trees_4,t4_trees_4), [interesting(0.00)]). fof(t24_trees_4,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v3_trees_2(C) & m3_trees_2(C,k2_zfmisc_1(A,B)) ) => ( k1_relat_1(k10_trees_3(A,B,C)) = k1_relat_1(C) & k1_relat_1(k11_trees_3(A,B,C)) = k1_relat_1(C) ) ) ) ) ), file(trees_4,t24_trees_4), [interesting(0.00)]). fof(t79_trees_1,theorem,( k6_trees_1(k2_trees_1(0)) = 0 ), file(trees_1,t79_trees_1), [interesting(0.00)]). fof(t80_trees_1,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & v1_finset_1(A) & v1_trees_1(A) ) => ( k6_trees_1(A) = 0 => A = k2_trees_1(0) ) ) ), file(trees_1,t80_trees_1), [interesting(0.00)]). fof(t5_trees_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v3_trees_2(A) ) => ( k1_relat_1(A) = k2_trees_1(0) => A = k1_trees_4(k1_funct_1(A,k1_xboole_0)) ) ) ), file(trees_4,t5_trees_4), [interesting(0.00)]). fof(t17_trees_4,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( ( k1_trees_4(A) = k4_trees_4(B,C) & v6_trees_3(C) ) => ( A = B & C = k1_xboole_0 ) ) ) ), file(trees_4,t17_trees_4), [interesting(0.00)]). fof(d4_trees_4,definition,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( v6_trees_3(B) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v3_trees_2(C) ) => ( C = k4_trees_4(A,B) <=> ( ? [D] : ( v1_relat_1(D) & v1_funct_1(D) & v1_finseq_1(D) & v6_trees_3(D) & B = D & k1_relat_1(C) = k13_trees_3(k2_funct_6(D)) ) & k1_funct_1(C,k1_xboole_0) = A & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( ~ r1_xreal_0(k3_finseq_1(B),D) => k5_trees_2(C,k12_finseq_1(k5_numbers,D)) = k1_funct_1(B,k1_nat_1(D,1)) ) ) ) ) ) ) ) ), file(trees_4,d4_trees_4), [interesting(0.00)]). fof(t10_trees_4,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) & v6_trees_3(B) ) => k1_relat_1(k4_trees_4(A,B)) = k13_trees_3(k2_funct_6(B)) ) ), file(trees_4,t10_trees_4), [interesting(0.00)]). fof(t39_trees_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v6_trees_3(A) ) => ( k1_relat_1(k2_funct_6(A)) = k1_relat_1(A) & v4_trees_3(k2_funct_6(A)) ) ) ), file(trees_3,t39_trees_3), [interesting(0.00)]). fof(t31_funct_6,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( ( r2_hidden(A,k1_relat_1(B)) & C = k1_funct_1(B,A) ) => ( r2_hidden(A,k1_relat_1(k2_funct_6(B))) & k1_funct_1(k2_funct_6(B),A) = k1_relat_1(C) & r2_hidden(A,k1_relat_1(k3_funct_6(B))) & k1_funct_1(k3_funct_6(B),A) = k2_relat_1(C) ) ) ) ) ), file(funct_6,t31_funct_6), [interesting(0.00)]). fof(t80_trees_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) & v5_trees_3(B) ) => ( ! [C] : ( ( ~ v1_xboole_0(C) & v1_finset_1(C) & v1_trees_1(C) ) => ( r2_hidden(C,k2_relat_1(B)) => r1_xreal_0(k6_trees_1(C),A) ) ) => r1_xreal_0(k6_trees_1(k13_trees_3(B)),k1_nat_1(A,1)) ) ) ) ), file(trees_3,t80_trees_3), [interesting(0.00)]). fof(s5_nat_1,theorem, ( ? [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) & p1_s5_nat_1(A) ) => ? [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) & p1_s5_nat_1(A) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( p1_s5_nat_1(B) => r1_xreal_0(A,B) ) ) ) ), file(nat_1,s5_nat_1), [interesting(0.00)]). fof(t38_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ~ r1_xreal_0(k2_xcmplx_0(B,1),A) <=> r1_xreal_0(A,B) ) ) ) ), file(nat_1,t38_nat_1), [interesting(0.00)]). fof(t81_trees_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) & v5_trees_3(A) ) => ! [B] : ( ( ~ v1_xboole_0(B) & v1_finset_1(B) & v1_trees_1(B) ) => ~ ( r2_hidden(B,k2_relat_1(A)) & r1_xreal_0(k6_trees_1(k13_trees_3(A)),k6_trees_1(B)) ) ) ) ), file(trees_3,t81_trees_3), [interesting(0.00)]). fof(t22_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ~ ( A != 0 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => A != k1_nat_1(B,1) ) ) ) ), file(nat_1,t22_nat_1), [interesting(0.00)]). fof(t15_trees_4,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) & v6_trees_3(C) ) => ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) & v1_finseq_1(D) & v6_trees_3(D) ) => ( k4_trees_4(A,C) = k4_trees_4(B,D) => ( A = B & C = D ) ) ) ) ), file(trees_4,t15_trees_4), [interesting(0.00)]). fof(s1_wellord2,theorem, ( ! [A] : ~ ( r2_hidden(A,f1_s1_wellord2) & ! [B] : ~ ( r2_hidden(B,f2_s1_wellord2) & p1_s1_wellord2(A,B) ) ) => ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & k1_relat_1(A) = f1_s1_wellord2 & r1_tarski(k2_relat_1(A),f2_s1_wellord2) & ! [B] : ( r2_hidden(B,f1_s1_wellord2) => p1_s1_wellord2(B,k1_funct_1(A,B)) ) ) ), file(wellord2,s1_wellord2), [interesting(0.00)]). fof(t11_relset_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( ( r1_tarski(k1_relat_1(C),A) & r1_tarski(k2_relat_1(C),B) ) => m2_relset_1(C,A,B) ) ) ), file(relset_1,t11_relset_1), [interesting(0.00)]). fof(t22_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(A,k1_relat_1(k5_relat_1(C,B))) => k1_funct_1(k5_relat_1(C,B),A) = k1_funct_1(B,k1_funct_1(C,A)) ) ) ) ), file(funct_1,t22_funct_1), [interesting(0.00)]). fof(t7_mcart_1,theorem,( ! [A,B] : ( k1_mcart_1(k4_tarski(A,B)) = A & k2_mcart_1(k4_tarski(A,B)) = B ) ), file(mcart_1,t7_mcart_1), [interesting(0.00)]). fof(t9_funct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( ( k1_relat_1(A) = k1_relat_1(B) & ! [C] : ( r2_hidden(C,k1_relat_1(A)) => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) => A = B ) ) ) ), file(funct_1,t9_funct_1), [interesting(0.00)]). fof(t27_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( ~ v1_xboole_0(B) & m1_subset_1(B,k1_zfmisc_1(A)) ) => ! [C] : ( m2_finseq_1(C,B) => m2_finseq_1(C,A) ) ) ) ), file(finseq_2,t27_finseq_2), [interesting(0.00)]). fof(t18_funct_2,theorem,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( ! [E] : ( r2_hidden(E,A) => k1_funct_1(C,E) = k1_funct_1(D,E) ) => C = D ) ) ) ), file(funct_2,t18_funct_2), [interesting(0.00)]). fof(d11_dtconstr,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k4_dtconstr(k5_dtconstr),k5_numbers) & m2_relset_1(A,k4_dtconstr(k5_dtconstr),k5_numbers) ) => ( A = k12_dtconstr <=> ( ! [B] : ( m1_subset_1(B,u1_struct_0(k5_dtconstr)) => ( r2_hidden(B,k6_dtconstr(k5_dtconstr)) => k1_funct_1(A,k2_trees_4(u1_struct_0(k5_dtconstr),B)) = 0 ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(k5_dtconstr)) => ! [C] : ( m1_trees_4(C,k5_trees_3(u1_struct_0(k5_dtconstr)),k4_dtconstr(k5_dtconstr)) => ( r1_lang1(k5_dtconstr,B,k1_dtconstr(u1_struct_0(k5_dtconstr),k5_trees_3(u1_struct_0(k5_dtconstr)),C)) => k1_funct_1(A,k12_trees_4(u1_struct_0(k5_dtconstr),B,C)) = k11_dtconstr(k5_finseqop(k4_dtconstr(k5_dtconstr),k5_numbers,C,A)) ) ) ) ) ) ) ), file(dtconstr,d11_dtconstr), [interesting(0.00)]). fof(d13_dtconstr,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k4_dtconstr(k5_dtconstr)) & m2_relset_1(A,k5_numbers,k4_dtconstr(k5_dtconstr)) ) => ( A = k14_dtconstr <=> ( k8_funct_2(k5_numbers,k4_dtconstr(k5_dtconstr),A,0) = k2_trees_4(k5_numbers,0) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k4_dtconstr(k5_dtconstr),A,k1_nat_1(B,1)) = k13_dtconstr(k8_funct_2(k5_numbers,k4_dtconstr(k5_dtconstr),A,B)) ) ) ) ) ), file(dtconstr,d13_dtconstr), [interesting(0.00)]). fof(d8_finseq_1,definition,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( B = k9_finseq_1(A) <=> ( k1_relat_1(B) = k2_finseq_1(1) & k1_funct_1(B,1) = A ) ) ) ), file(finseq_1,d8_finseq_1), [interesting(0.00)]). fof(t39_finseq_2,theorem,( ! [A,B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m2_finseq_1(D,B) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,B,C) & m2_relset_1(E,B,C) ) => ( D = k9_finseq_1(A) => k1_partfun1(k5_numbers,B,B,C,D,E) = k9_finseq_1(k1_funct_1(E,A)) ) ) ) ) ) ), file(finseq_2,t39_finseq_2), [interesting(0.00)]). fof(d10_dtconstr,definition,( ! [A] : ( m2_finseq_1(A,k5_numbers) => ( A != k1_xboole_0 => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( B = k11_dtconstr(A) <=> ? [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) & B = k1_nat_1(C,1) & k1_funct_1(A,1) = C ) ) ) ) ) ), file(dtconstr,d10_dtconstr), [interesting(0.00)]). fof(d15_dtconstr,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_lang1(A) ) => ! [B] : ( ( v1_funct_1(B) & v3_trees_2(B) & m3_trees_2(B,u1_struct_0(A)) ) => ( r2_hidden(B,k4_dtconstr(A)) => ! [C] : ( m2_finseq_1(C,k5_lang1(A)) => ( C = k16_dtconstr(A,B) <=> ? [D] : ( v1_funct_1(D) & v1_funct_2(D,k4_dtconstr(A),k3_finseq_2(k5_lang1(A))) & m2_relset_1(D,k4_dtconstr(A),k3_finseq_2(k5_lang1(A))) & C = k1_funct_1(D,B) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_hidden(E,k5_lang1(A)) => k1_funct_1(D,k2_trees_4(u1_struct_0(A),E)) = k3_lang1(u1_struct_0(A),E) ) ) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_trees_4(F,k5_trees_3(u1_struct_0(A)),k4_dtconstr(A)) => ( r1_lang1(A,E,k1_dtconstr(u1_struct_0(A),k5_trees_3(u1_struct_0(A)),F)) => k1_funct_1(D,k12_trees_4(u1_struct_0(A),E,F)) = k15_dtconstr(k5_lang1(A),k5_finseqop(k4_dtconstr(A),k3_finseq_2(k5_lang1(A)),F,D)) ) ) ) ) ) ) ) ) ) ), file(dtconstr,d15_dtconstr), [interesting(0.00)]). fof(t56_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( B = k9_finseq_1(A) <=> ( k3_finseq_1(B) = 1 & k2_relat_1(B) = k1_tarski(A) ) ) ) ), file(finseq_1,t56_finseq_1), [interesting(0.00)]). fof(d14_dtconstr,definition,( ! [A,B] : ( m2_finseq_1(B,k3_finseq_2(A)) => ! [C] : ( m2_finseq_2(C,A,k3_finseq_2(A)) => ( C = k15_dtconstr(A,B) <=> ? [D] : ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(k3_finseq_2(A),k3_finseq_2(A)),k3_finseq_2(A)) & m2_relset_1(D,k2_zfmisc_1(k3_finseq_2(A),k3_finseq_2(A)),k3_finseq_2(A)) & ! [E] : ( m2_finseq_2(E,A,k3_finseq_2(A)) => ! [F] : ( m2_finseq_2(F,A,k3_finseq_2(A)) => k2_binop_1(k3_finseq_2(A),k3_finseq_2(A),k3_finseq_2(A),D,E,F) = k1_lang1(A,E,F) ) ) & C = k2_finsop_1(k3_finseq_2(A),B,D) ) ) ) ) ), file(dtconstr,d14_dtconstr), [interesting(0.00)]). fof(t12_finsop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => k2_finsop_1(A,k12_finseq_1(A,B),C) = B ) ) ) ), file(finsop_1,t12_finsop_1), [interesting(0.00)]). fof(d16_dtconstr,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_lang1(A) ) => ! [B] : ( ( v1_funct_1(B) & v3_trees_2(B) & m3_trees_2(B,u1_struct_0(A)) ) => ( r2_hidden(B,k4_dtconstr(A)) => ! [C] : ( m2_finseq_1(C,u1_struct_0(A)) => ( C = k17_dtconstr(A,B) <=> ? [D] : ( v1_funct_1(D) & v1_funct_2(D,k4_dtconstr(A),k3_finseq_2(u1_struct_0(A))) & m2_relset_1(D,k4_dtconstr(A),k3_finseq_2(u1_struct_0(A))) & C = k1_funct_1(D,B) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_hidden(E,k5_lang1(A)) => k1_funct_1(D,k2_trees_4(u1_struct_0(A),E)) = k3_lang1(u1_struct_0(A),E) ) ) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_trees_4(F,k5_trees_3(u1_struct_0(A)),k4_dtconstr(A)) => ! [G] : ( ( v1_relat_1(G) & v1_funct_1(G) & v1_finseq_1(G) ) => ( ( G = k1_dtconstr(u1_struct_0(A),k5_trees_3(u1_struct_0(A)),F) & r1_lang1(A,E,G) ) => ! [H] : ( m2_finseq_1(H,k3_finseq_2(u1_struct_0(A))) => ( H = k5_finseqop(k4_dtconstr(A),k3_finseq_2(u1_struct_0(A)),F,D) => k1_funct_1(D,k12_trees_4(u1_struct_0(A),E,F)) = k1_lang1(u1_struct_0(A),k3_lang1(u1_struct_0(A),E),k15_dtconstr(u1_struct_0(A),H)) ) ) ) ) ) ) ) ) ) ) ) ) ), file(dtconstr,d16_dtconstr), [interesting(0.00)]). fof(t47_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( k7_finseq_1(A,k1_xboole_0) = A & k7_finseq_1(k1_xboole_0,A) = A ) ) ), file(finseq_1,t47_finseq_1), [interesting(0.00)]). fof(t72_finseq_2,theorem,( ! [A] : k2_finseq_2(0,A) = k1_xboole_0 ), file(finseq_2,t72_finseq_2), [interesting(0.00)]). fof(t45_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => k7_finseq_1(k7_finseq_1(A,B),C) = k7_finseq_1(A,k7_finseq_1(B,C)) ) ) ) ), file(finseq_1,t45_finseq_1), [interesting(0.00)]). fof(t73_finseq_2,theorem,( ! [A] : k2_finseq_2(1,A) = k9_finseq_1(A) ), file(finseq_2,t73_finseq_2), [interesting(0.00)]). fof(t143_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : k2_finseq_2(k1_nat_1(A,B),C) = k7_finseq_1(k2_finseq_2(A,C),k2_finseq_2(B,C)) ) ) ), file(finseq_2,t143_finseq_2), [interesting(0.00)]). fof(t83_trees_3,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & v1_finset_1(A) & v1_trees_1(A) ) => k6_trees_1(k14_trees_3(A)) = k1_nat_1(k6_trees_1(A),1) ) ), file(trees_3,t83_trees_3), [interesting(0.00)]). fof(t13_trees_4,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v3_trees_2(B) ) => k1_relat_1(k5_trees_4(A,B)) = k14_trees_3(k1_relat_1(B)) ) ), file(trees_4,t13_trees_4), [interesting(0.00)]). fof(d5_trees_4,definition,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v3_trees_2(B) ) => k5_trees_4(A,B) = k4_trees_4(A,k9_finseq_1(B)) ) ), file(trees_4,d5_trees_4), [interesting(0.00)]). fof(t46_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( ( k7_finseq_1(A,B) = k7_finseq_1(C,B) | k7_finseq_1(B,A) = k7_finseq_1(B,C) ) => A = C ) ) ) ) ), file(finseq_1,t46_finseq_1), [interesting(0.00)]). fof(t69_finseq_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : k3_finseq_1(k2_finseq_2(A,B)) = A ) ), file(finseq_2,t69_finseq_2), [interesting(0.00)]). fof(d17_dtconstr,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_lang1(A) ) => ! [B] : ( ( v1_funct_1(B) & v3_trees_2(B) & m3_trees_2(B,u1_struct_0(A)) ) => ( r2_hidden(B,k4_dtconstr(A)) => ! [C] : ( m2_finseq_1(C,u1_struct_0(A)) => ( C = k18_dtconstr(A,B) <=> ? [D] : ( v1_funct_1(D) & v1_funct_2(D,k4_dtconstr(A),k3_finseq_2(u1_struct_0(A))) & m2_relset_1(D,k4_dtconstr(A),k3_finseq_2(u1_struct_0(A))) & C = k1_funct_1(D,B) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_hidden(E,k5_lang1(A)) => k1_funct_1(D,k2_trees_4(u1_struct_0(A),E)) = k3_lang1(u1_struct_0(A),E) ) ) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_trees_4(F,k5_trees_3(u1_struct_0(A)),k4_dtconstr(A)) => ! [G] : ( ( v1_relat_1(G) & v1_funct_1(G) & v1_finseq_1(G) ) => ( ( G = k1_dtconstr(u1_struct_0(A),k5_trees_3(u1_struct_0(A)),F) & r1_lang1(A,E,G) ) => ! [H] : ( m2_finseq_1(H,k3_finseq_2(u1_struct_0(A))) => ( H = k5_finseqop(k4_dtconstr(A),k3_finseq_2(u1_struct_0(A)),F,D) => k1_funct_1(D,k12_trees_4(u1_struct_0(A),E,F)) = k1_lang1(u1_struct_0(A),k15_dtconstr(u1_struct_0(A),H),k3_lang1(u1_struct_0(A),E)) ) ) ) ) ) ) ) ) ) ) ) ) ), file(dtconstr,d17_dtconstr), [interesting(0.00)]). fof(t61_finseq_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( C = k10_finseq_1(A,B) <=> ( k3_finseq_1(C) = 2 & k1_funct_1(C,1) = A & k1_funct_1(C,2) = B ) ) ) ), file(finseq_1,t61_finseq_1), [interesting(0.00)]). fof(t3_xboole_0,theorem,( ! [A,B] : ( ~ ( ~ r1_xboole_0(A,B) & ! [C] : ~ ( r2_hidden(C,A) & r2_hidden(C,B) ) ) & ~ ( ? [C] : ( r2_hidden(C,A) & r2_hidden(C,B) ) & r1_xboole_0(A,B) ) ) ), file(xboole_0,t3_xboole_0), [interesting(0.00)]).