fof(l1_recdef_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_1(C,B) => ( ( r1_xreal_0(1,A) & r1_xreal_0(A,k3_finseq_1(C)) ) => m1_subset_1(k1_funct_1(C,A),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t3_finseq_1,d3_finseq_1,d5_funct_1,d4_finseq_1]), [file(recdef_1,l1_recdef_1),interesting(1.00)]). fof(s8_recdef_1,theorem,( ? [A,B] : ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) & A = k1_funct_1(B,k3_finseq_1(B)) & k3_finseq_1(B) = k3_finseq_1(f1_s8_recdef_1) & k1_funct_1(B,1) = k1_funct_1(f1_s8_recdef_1,1) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(1,C) => ( r1_xreal_0(k3_finseq_1(f1_s8_recdef_1),C) | k1_funct_1(B,k1_nat_1(C,1)) = f2_s8_recdef_1(k1_funct_1(f1_s8_recdef_1,k1_nat_1(C,1)),k1_funct_1(B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[s7_recdef_1]), [file(recdef_1,s8_recdef_1),interesting(0.77)]). 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)) ) ) ), inference(mizar_proof,[status(thm)],[s1_recdef_1]), [file(recdef_1,s3_recdef_1),interesting(0.75)]). fof(s1_recdef_1,theorem, ( ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ? [C] : p1_s1_recdef_1(A,B,C) ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B,C,D] : ( ( p1_s1_recdef_1(A,B,C) & p1_s1_recdef_1(A,B,D) ) => C = D ) ) ) => ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & k1_relat_1(A) = k5_numbers & k1_funct_1(A,0) = f1_s1_recdef_1 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => p1_s1_recdef_1(B,k1_funct_1(A,B),k1_funct_1(A,k1_nat_1(B,1))) ) ) ), inference(mizar_proof,[status(thm)],[t38_nat_1,s1_nat_1,t9_funct_1,t13_funcop_1,t19_funcop_1,t18_nat_1,t26_nat_1,t8_xreal_1,t8_xreal_1,t26_nat_1,s2_funct_1,t18_nat_1,t18_nat_1,t29_nat_1,t38_nat_1,t26_nat_1,t38_nat_1,s1_nat_1,t38_nat_1,s1_nat_1,s2_funct_1,t29_nat_1,t2_xreal_1,t31_xreal_1]), [file(recdef_1,s1_recdef_1),interesting(0.74)]). fof(s4_recdef_1,theorem,( ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,f1_s4_recdef_1) & m2_relset_1(A,k5_numbers,f1_s4_recdef_1) & k8_funct_2(k5_numbers,f1_s4_recdef_1,A,0) = f2_s4_recdef_1 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,f1_s4_recdef_1,A,k1_nat_1(B,1)) = f3_s4_recdef_1(B,k8_funct_2(k5_numbers,f1_s4_recdef_1,A,B)) ) ) ), inference(mizar_proof,[status(thm)],[s2_recdef_1]), [file(recdef_1,s4_recdef_1),interesting(0.71)]). fof(s2_recdef_1,theorem, ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,f1_s2_recdef_1) => ? [C] : ( m1_subset_1(C,f1_s2_recdef_1) & p1_s2_recdef_1(A,B,C) ) ) ) => ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,f1_s2_recdef_1) & m2_relset_1(A,k5_numbers,f1_s2_recdef_1) & k8_funct_2(k5_numbers,f1_s2_recdef_1,A,0) = f2_s2_recdef_1 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => p1_s2_recdef_1(B,k8_funct_2(k5_numbers,f1_s2_recdef_1,A,B),k8_funct_2(k5_numbers,f1_s2_recdef_1,A,k1_nat_1(B,1))) ) ) ), inference(mizar_proof,[status(thm)],[s7_funct_2,s4_finseq_1,s5_nat_1,t22_nat_1,d5_real_1,t38_nat_1,t9_xreal_1,t2_xreal_1,t8_xreal_1,t22_nat_1,t2_xreal_1,t16_finseq_1,d3_finseq_1,t3_finseq_1,t2_xreal_1,t3_finseq_1,d3_finseq_1,t8_funct_1,d3_tarski,d4_tarski,d11_finseq_1,d4_tarski,d11_finseq_1,d1_funct_1,d1_funct_1,s1_funct_1,d4_tarski,d11_finseq_1,d4_relat_1,d1_relat_1,d4_tarski,d11_finseq_1,d1_relat_1,t2_tarski,d5_funct_1,t8_funct_1,d4_tarski,d11_finseq_1,t8_funct_1,t8_funct_1,d5_funct_1,d4_finseq_1,d3_tarski,t4_funct_2,d8_finseq_1,d11_finseq_1,t56_finseq_1,t37_nat_1,t8_xreal_1,t52_finseq_1,d1_tarski,d4_tarski,t8_funct_1,t8_funct_1,d4_tarski,d11_finseq_1,t35_finseq_1,t56_finseq_1,t37_nat_1,t3_finseq_1,d3_finseq_1,t8_funct_1,t37_nat_1,t3_finseq_1,d3_finseq_1,d7_finseq_1,t37_nat_1,t3_finseq_1,d3_finseq_1,d5_funct_1,d4_finseq_1,d11_finseq_1,t35_finseq_1,t57_finseq_1,t36_finseq_1,t57_finseq_1,t37_nat_1,t57_finseq_1,t8_xreal_1,t3_finseq_1,d3_finseq_1,d7_finseq_1,t26_nat_1,t37_nat_1,t3_finseq_1,d3_finseq_1,d7_finseq_1,t37_nat_1,t57_finseq_1,t8_xreal_1,t3_finseq_1,d3_finseq_1,d7_finseq_1,d4_tarski,t8_funct_1,t8_funct_1,d3_finseq_1,t3_finseq_1,d5_real_1,t38_nat_1,t37_nat_1,t3_finseq_1,d3_finseq_1,t8_funct_1,d4_tarski,t8_funct_1,s1_nat_1,s2_funct_1,d3_tarski,d5_funct_1,d5_funct_1,t4_funct_2,d4_funct_1,d4_tarski,d11_finseq_1,t8_funct_1,d3_finseq_1,t3_finseq_1,t37_nat_1,t9_xreal_1,t2_xreal_1,t3_finseq_1,d3_finseq_1,t8_funct_1,d4_tarski,t8_funct_1,t8_funct_1,d11_finseq_1,d8_finseq_1,t56_finseq_1,t8_xreal_1,t37_nat_1,t8_xreal_1,t52_finseq_1,d1_tarski,d4_tarski,t8_funct_1]), [file(recdef_1,s2_recdef_1),interesting(0.63)]). fof(s7_recdef_1,theorem, ( ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ~ ( r1_xreal_0(1,A) & ~ r1_xreal_0(k3_finseq_1(f1_s7_recdef_1),A) & ! [C] : ~ p1_s7_recdef_1(k1_funct_1(f1_s7_recdef_1,k1_nat_1(A,1)),B,C) ) ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B,C,D,E] : ( ( r1_xreal_0(1,A) & E = k1_funct_1(f1_s7_recdef_1,k1_nat_1(A,1)) & p1_s7_recdef_1(E,B,C) & p1_s7_recdef_1(E,B,D) ) => ( r1_xreal_0(k3_finseq_1(f1_s7_recdef_1),A) | C = D ) ) ) ) => ? [A,B] : ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) & A = k1_funct_1(B,k3_finseq_1(B)) & k3_finseq_1(B) = k3_finseq_1(f1_s7_recdef_1) & k1_funct_1(B,1) = k1_funct_1(f1_s7_recdef_1,1) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(1,C) => ( r1_xreal_0(k3_finseq_1(f1_s7_recdef_1),C) | p1_s7_recdef_1(k1_funct_1(f1_s7_recdef_1,k1_nat_1(C,1)),k1_funct_1(B,C),k1_funct_1(B,k1_nat_1(C,1))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[s5_recdef_1,t2_xreal_1]), [file(recdef_1,s7_recdef_1),interesting(0.58)]). fof(s18_recdef_1,theorem, ( ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ? [C] : p1_s18_recdef_1(A,B,C) ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B,C,D] : ( ( p1_s18_recdef_1(A,B,C) & p1_s18_recdef_1(A,B,D) ) => C = D ) ) ) => ( ? [A,B] : ( v1_relat_1(B) & v1_funct_1(B) & A = k1_funct_1(B,f2_s18_recdef_1) & k1_relat_1(B) = k5_numbers & k1_funct_1(B,0) = f1_s18_recdef_1 & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => p1_s18_recdef_1(C,k1_funct_1(B,C),k1_funct_1(B,k1_nat_1(C,1))) ) ) & ! [A,B] : ~ ( ? [C] : ( v1_relat_1(C) & v1_funct_1(C) & A = k1_funct_1(C,f2_s18_recdef_1) & k1_relat_1(C) = k5_numbers & k1_funct_1(C,0) = f1_s18_recdef_1 & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => p1_s18_recdef_1(D,k1_funct_1(C,D),k1_funct_1(C,k1_nat_1(D,1))) ) ) & ? [C] : ( v1_relat_1(C) & v1_funct_1(C) & B = k1_funct_1(C,f2_s18_recdef_1) & k1_relat_1(C) = k5_numbers & k1_funct_1(C,0) = f1_s18_recdef_1 & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => p1_s18_recdef_1(D,k1_funct_1(C,D),k1_funct_1(C,k1_nat_1(D,1))) ) ) & A != B ) ) ), inference(mizar_proof,[status(thm)],[s1_recdef_1,s9_recdef_1]), [file(recdef_1,s18_recdef_1),interesting(0.52)]). fof(s5_recdef_1,theorem, ( ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( r1_xreal_0(1,A) => ( r1_xreal_0(f2_s5_recdef_1,A) | ! [B] : ? [C] : p1_s5_recdef_1(A,B,C) ) ) ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( r1_xreal_0(1,A) => ( r1_xreal_0(f2_s5_recdef_1,A) | ! [B,C,D] : ( ( p1_s5_recdef_1(A,B,C) & p1_s5_recdef_1(A,B,D) ) => C = D ) ) ) ) ) => ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) & k3_finseq_1(A) = f2_s5_recdef_1 & ( k1_funct_1(A,1) = f1_s5_recdef_1 | f2_s5_recdef_1 = 0 ) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r1_xreal_0(1,B) => ( r1_xreal_0(f2_s5_recdef_1,B) | p1_s5_recdef_1(B,k1_funct_1(A,B),k1_funct_1(A,k1_nat_1(B,1))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_xreal_1,t29_nat_1,t22_xreal_1,t29_nat_1,s1_recdef_1,s2_funct_1,t1_xboole_1,t91_relat_1,d2_finseq_1,t29_nat_1,t38_nat_1,t3_finseq_1,t72_funct_1,d3_finseq_1,t22_nat_1,t18_nat_1,t9_xreal_1,t3_finseq_1,t72_funct_1,t22_nat_1,t22_xreal_1,t29_nat_1,t2_xreal_1]), [file(recdef_1,s5_recdef_1),interesting(0.45)]). fof(s23_recdef_1,theorem, ( ? [A,B] : ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) & A = k1_funct_1(B,k3_finseq_1(B)) & k3_finseq_1(B) = k3_finseq_1(f1_s23_recdef_1) & k1_funct_1(B,1) = k1_funct_1(f1_s23_recdef_1,1) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(1,C) => ( r1_xreal_0(k3_finseq_1(f1_s23_recdef_1),C) | k1_funct_1(B,k1_nat_1(C,1)) = f2_s23_recdef_1(k1_funct_1(f1_s23_recdef_1,k1_nat_1(C,1)),k1_funct_1(B,C)) ) ) ) ) & ! [A,B] : ~ ( ? [C] : ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) & A = k1_funct_1(C,k3_finseq_1(C)) & k3_finseq_1(C) = k3_finseq_1(f1_s23_recdef_1) & k1_funct_1(C,1) = k1_funct_1(f1_s23_recdef_1,1) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r1_xreal_0(1,D) => ( r1_xreal_0(k3_finseq_1(f1_s23_recdef_1),D) | k1_funct_1(C,k1_nat_1(D,1)) = f2_s23_recdef_1(k1_funct_1(f1_s23_recdef_1,k1_nat_1(D,1)),k1_funct_1(C,D)) ) ) ) ) & ? [C] : ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) & B = k1_funct_1(C,k3_finseq_1(C)) & k3_finseq_1(C) = k3_finseq_1(f1_s23_recdef_1) & k1_funct_1(C,1) = k1_funct_1(f1_s23_recdef_1,1) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r1_xreal_0(1,D) => ( r1_xreal_0(k3_finseq_1(f1_s23_recdef_1),D) | k1_funct_1(C,k1_nat_1(D,1)) = f2_s23_recdef_1(k1_funct_1(f1_s23_recdef_1,k1_nat_1(D,1)),k1_funct_1(C,D)) ) ) ) ) & A != B ) ), inference(mizar_proof,[status(thm)],[s8_recdef_1,s17_recdef_1]), [file(recdef_1,s23_recdef_1),interesting(0.44)]). fof(s6_recdef_1,theorem, ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( r1_xreal_0(1,A) => ( r1_xreal_0(f3_s6_recdef_1,A) | ! [B] : ( m1_subset_1(B,f1_s6_recdef_1) => ? [C] : ( m1_subset_1(C,f1_s6_recdef_1) & p1_s6_recdef_1(A,B,C) ) ) ) ) ) => ? [A] : ( m2_finseq_1(A,f1_s6_recdef_1) & k3_finseq_1(A) = f3_s6_recdef_1 & ( k1_funct_1(A,1) = f2_s6_recdef_1 | f3_s6_recdef_1 = 0 ) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r1_xreal_0(1,B) => ( r1_xreal_0(f3_s6_recdef_1,B) | p1_s6_recdef_1(B,k1_funct_1(A,B),k1_funct_1(A,k1_nat_1(B,1))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_nat_1,t22_xreal_1,s2_recdef_1,s2_funct_1,t1_xboole_1,t91_relat_1,d2_finseq_1,d3_tarski,d5_funct_1,t3_finseq_1,t22_nat_1,t70_funct_1,d4_finseq_1,t29_nat_1,t38_nat_1,t3_finseq_1,t72_funct_1,d3_finseq_1,t22_nat_1,t18_nat_1,t9_xreal_1,t3_finseq_1,t72_funct_1,t22_nat_1,t22_xreal_1,t29_nat_1,t2_xreal_1]), [file(recdef_1,s6_recdef_1),interesting(0.41)]). fof(s19_recdef_1,theorem, ( ? [A,B] : ( v1_relat_1(B) & v1_funct_1(B) & A = k1_funct_1(B,f2_s19_recdef_1) & k1_relat_1(B) = k5_numbers & k1_funct_1(B,0) = f1_s19_recdef_1 & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k1_funct_1(B,k1_nat_1(C,1)) = f3_s19_recdef_1(C,k1_funct_1(B,C)) ) ) & ! [A,B] : ~ ( ? [C] : ( v1_relat_1(C) & v1_funct_1(C) & A = k1_funct_1(C,f2_s19_recdef_1) & k1_relat_1(C) = k5_numbers & k1_funct_1(C,0) = f1_s19_recdef_1 & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k1_funct_1(C,k1_nat_1(D,1)) = f3_s19_recdef_1(D,k1_funct_1(C,D)) ) ) & ? [C] : ( v1_relat_1(C) & v1_funct_1(C) & B = k1_funct_1(C,f2_s19_recdef_1) & k1_relat_1(C) = k5_numbers & k1_funct_1(C,0) = f1_s19_recdef_1 & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k1_funct_1(C,k1_nat_1(D,1)) = f3_s19_recdef_1(D,k1_funct_1(C,D)) ) ) & A != B ) ), inference(mizar_proof,[status(thm)],[s18_recdef_1]), [file(recdef_1,s19_recdef_1),interesting(0.36)]). fof(s14_recdef_1,theorem, ( ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( r1_xreal_0(1,A) => ( r1_xreal_0(f2_s14_recdef_1,A) | ! [B,C,D] : ( ( p1_s14_recdef_1(A,B,C) & p1_s14_recdef_1(A,B,D) ) => C = D ) ) ) ) & k3_finseq_1(f3_s14_recdef_1) = f2_s14_recdef_1 & ( k1_funct_1(f3_s14_recdef_1,1) = f1_s14_recdef_1 | f2_s14_recdef_1 = 0 ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( r1_xreal_0(1,A) => ( r1_xreal_0(f2_s14_recdef_1,A) | p1_s14_recdef_1(A,k1_funct_1(f3_s14_recdef_1,A),k1_funct_1(f3_s14_recdef_1,k1_nat_1(A,1))) ) ) ) & k3_finseq_1(f4_s14_recdef_1) = f2_s14_recdef_1 & ( k1_funct_1(f4_s14_recdef_1,1) = f1_s14_recdef_1 | f2_s14_recdef_1 = 0 ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( r1_xreal_0(1,A) => ( r1_xreal_0(f2_s14_recdef_1,A) | p1_s14_recdef_1(A,k1_funct_1(f4_s14_recdef_1,A),k1_funct_1(f4_s14_recdef_1,k1_nat_1(A,1))) ) ) ) ) => f3_s14_recdef_1 = f4_s14_recdef_1 ), inference(mizar_proof,[status(thm)],[d3_finseq_1,d3_finseq_1,t9_funct_1,d3_finseq_1,t3_finseq_1,s5_nat_1,d5_real_1,t22_nat_1,t38_nat_1,t31_xreal_1,t2_xreal_1,t38_nat_1]), [file(recdef_1,s14_recdef_1),interesting(0.36)]). fof(s17_recdef_1,theorem, ( ( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) & f3_s17_recdef_1 = k1_funct_1(A,k3_finseq_1(A)) & k3_finseq_1(A) = k3_finseq_1(f1_s17_recdef_1) & k1_funct_1(A,1) = k1_funct_1(f1_s17_recdef_1,1) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r1_xreal_0(1,B) => ( r1_xreal_0(k3_finseq_1(f1_s17_recdef_1),B) | k1_funct_1(A,k1_nat_1(B,1)) = f2_s17_recdef_1(k1_funct_1(f1_s17_recdef_1,k1_nat_1(B,1)),k1_funct_1(A,B)) ) ) ) ) & ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) & f4_s17_recdef_1 = k1_funct_1(A,k3_finseq_1(A)) & k3_finseq_1(A) = k3_finseq_1(f1_s17_recdef_1) & k1_funct_1(A,1) = k1_funct_1(f1_s17_recdef_1,1) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r1_xreal_0(1,B) => ( r1_xreal_0(k3_finseq_1(f1_s17_recdef_1),B) | k1_funct_1(A,k1_nat_1(B,1)) = f2_s17_recdef_1(k1_funct_1(f1_s17_recdef_1,k1_nat_1(B,1)),k1_funct_1(A,B)) ) ) ) ) ) => f3_s17_recdef_1 = f4_s17_recdef_1 ), inference(mizar_proof,[status(thm)],[s16_recdef_1]), [file(recdef_1,s17_recdef_1),interesting(0.28)]). fof(s22_recdef_1,theorem, ( ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ~ ( r1_xreal_0(1,A) & ~ r1_xreal_0(k3_finseq_1(f1_s22_recdef_1),A) & ! [C] : ~ p1_s22_recdef_1(k1_funct_1(f1_s22_recdef_1,k1_nat_1(A,1)),B,C) ) ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B,C,D,E] : ( ( r1_xreal_0(1,A) & E = k1_funct_1(f1_s22_recdef_1,k1_nat_1(A,1)) & p1_s22_recdef_1(E,B,C) & p1_s22_recdef_1(E,B,D) ) => ( r1_xreal_0(k3_finseq_1(f1_s22_recdef_1),A) | C = D ) ) ) ) => ( ? [A,B] : ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) & A = k1_funct_1(B,k3_finseq_1(B)) & k3_finseq_1(B) = k3_finseq_1(f1_s22_recdef_1) & k1_funct_1(B,1) = k1_funct_1(f1_s22_recdef_1,1) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(1,C) => ( r1_xreal_0(k3_finseq_1(f1_s22_recdef_1),C) | p1_s22_recdef_1(k1_funct_1(f1_s22_recdef_1,k1_nat_1(C,1)),k1_funct_1(B,C),k1_funct_1(B,k1_nat_1(C,1))) ) ) ) ) & ! [A,B] : ~ ( ? [C] : ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) & A = k1_funct_1(C,k3_finseq_1(C)) & k3_finseq_1(C) = k3_finseq_1(f1_s22_recdef_1) & k1_funct_1(C,1) = k1_funct_1(f1_s22_recdef_1,1) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r1_xreal_0(1,D) => ( r1_xreal_0(k3_finseq_1(f1_s22_recdef_1),D) | p1_s22_recdef_1(k1_funct_1(f1_s22_recdef_1,k1_nat_1(D,1)),k1_funct_1(C,D),k1_funct_1(C,k1_nat_1(D,1))) ) ) ) ) & ? [C] : ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) & B = k1_funct_1(C,k3_finseq_1(C)) & k3_finseq_1(C) = k3_finseq_1(f1_s22_recdef_1) & k1_funct_1(C,1) = k1_funct_1(f1_s22_recdef_1,1) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r1_xreal_0(1,D) => ( r1_xreal_0(k3_finseq_1(f1_s22_recdef_1),D) | p1_s22_recdef_1(k1_funct_1(f1_s22_recdef_1,k1_nat_1(D,1)),k1_funct_1(C,D),k1_funct_1(C,k1_nat_1(D,1))) ) ) ) ) & A != B ) ) ), inference(mizar_proof,[status(thm)],[s7_recdef_1,s16_recdef_1]), [file(recdef_1,s22_recdef_1),interesting(0.26)]). fof(s16_recdef_1,theorem, ( ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B,C,D,E] : ( ( r1_xreal_0(1,A) & E = k1_funct_1(f1_s16_recdef_1,k1_nat_1(A,1)) & p1_s16_recdef_1(E,B,C) & p1_s16_recdef_1(E,B,D) ) => ( r1_xreal_0(k3_finseq_1(f1_s16_recdef_1),A) | C = D ) ) ) & ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) & f2_s16_recdef_1 = k1_funct_1(A,k3_finseq_1(A)) & k3_finseq_1(A) = k3_finseq_1(f1_s16_recdef_1) & k1_funct_1(A,1) = k1_funct_1(f1_s16_recdef_1,1) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r1_xreal_0(1,B) => ( r1_xreal_0(k3_finseq_1(f1_s16_recdef_1),B) | p1_s16_recdef_1(k1_funct_1(f1_s16_recdef_1,k1_nat_1(B,1)),k1_funct_1(A,B),k1_funct_1(A,k1_nat_1(B,1))) ) ) ) ) & ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) & f3_s16_recdef_1 = k1_funct_1(A,k3_finseq_1(A)) & k3_finseq_1(A) = k3_finseq_1(f1_s16_recdef_1) & k1_funct_1(A,1) = k1_funct_1(f1_s16_recdef_1,1) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r1_xreal_0(1,B) => ( r1_xreal_0(k3_finseq_1(f1_s16_recdef_1),B) | p1_s16_recdef_1(k1_funct_1(f1_s16_recdef_1,k1_nat_1(B,1)),k1_funct_1(A,B),k1_funct_1(A,k1_nat_1(B,1))) ) ) ) ) ) => f2_s16_recdef_1 = f3_s16_recdef_1 ), inference(mizar_proof,[status(thm)],[s14_recdef_1]), [file(recdef_1,s16_recdef_1),interesting(0.22)]). fof(s20_recdef_1,theorem, ( ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,f1_s20_recdef_1) => ? [C] : ( m1_subset_1(C,f1_s20_recdef_1) & p1_s20_recdef_1(A,B,C) ) ) ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,f1_s20_recdef_1) => ! [C] : ( m1_subset_1(C,f1_s20_recdef_1) => ! [D] : ( m1_subset_1(D,f1_s20_recdef_1) => ( ( p1_s20_recdef_1(A,B,C) & p1_s20_recdef_1(A,B,D) ) => C = D ) ) ) ) ) ) => ( ? [A] : ( m1_subset_1(A,f1_s20_recdef_1) & ? [B] : ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,f1_s20_recdef_1) & m2_relset_1(B,k5_numbers,f1_s20_recdef_1) & A = k8_funct_2(k5_numbers,f1_s20_recdef_1,B,f3_s20_recdef_1) & k8_funct_2(k5_numbers,f1_s20_recdef_1,B,0) = f2_s20_recdef_1 & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => p1_s20_recdef_1(C,k8_funct_2(k5_numbers,f1_s20_recdef_1,B,C),k8_funct_2(k5_numbers,f1_s20_recdef_1,B,k1_nat_1(C,1))) ) ) ) & ! [A] : ( m1_subset_1(A,f1_s20_recdef_1) => ! [B] : ( m1_subset_1(B,f1_s20_recdef_1) => ~ ( ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,f1_s20_recdef_1) & m2_relset_1(C,k5_numbers,f1_s20_recdef_1) & A = k8_funct_2(k5_numbers,f1_s20_recdef_1,C,f3_s20_recdef_1) & k8_funct_2(k5_numbers,f1_s20_recdef_1,C,0) = f2_s20_recdef_1 & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => p1_s20_recdef_1(D,k8_funct_2(k5_numbers,f1_s20_recdef_1,C,D),k8_funct_2(k5_numbers,f1_s20_recdef_1,C,k1_nat_1(D,1))) ) ) & ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,f1_s20_recdef_1) & m2_relset_1(C,k5_numbers,f1_s20_recdef_1) & B = k8_funct_2(k5_numbers,f1_s20_recdef_1,C,f3_s20_recdef_1) & k8_funct_2(k5_numbers,f1_s20_recdef_1,C,0) = f2_s20_recdef_1 & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => p1_s20_recdef_1(D,k8_funct_2(k5_numbers,f1_s20_recdef_1,C,D),k8_funct_2(k5_numbers,f1_s20_recdef_1,C,k1_nat_1(D,1))) ) ) & A != B ) ) ) ) ), inference(mizar_proof,[status(thm)],[s2_recdef_1,s10_recdef_1]), [file(recdef_1,s20_recdef_1),interesting(0.18)]). fof(s15_recdef_1,theorem, ( ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( r1_xreal_0(1,A) => ( r1_xreal_0(f3_s15_recdef_1,A) | ! [B] : ( m1_subset_1(B,f1_s15_recdef_1) => ! [C] : ( m1_subset_1(C,f1_s15_recdef_1) => ! [D] : ( m1_subset_1(D,f1_s15_recdef_1) => ( ( p1_s15_recdef_1(A,B,C) & p1_s15_recdef_1(A,B,D) ) => C = D ) ) ) ) ) ) ) & k3_finseq_1(f4_s15_recdef_1) = f3_s15_recdef_1 & ( k1_funct_1(f4_s15_recdef_1,1) = f2_s15_recdef_1 | f3_s15_recdef_1 = 0 ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( r1_xreal_0(1,A) => ( r1_xreal_0(f3_s15_recdef_1,A) | p1_s15_recdef_1(A,k1_funct_1(f4_s15_recdef_1,A),k1_funct_1(f4_s15_recdef_1,k1_nat_1(A,1))) ) ) ) & k3_finseq_1(f5_s15_recdef_1) = f3_s15_recdef_1 & ( k1_funct_1(f5_s15_recdef_1,1) = f2_s15_recdef_1 | f3_s15_recdef_1 = 0 ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( r1_xreal_0(1,A) => ( r1_xreal_0(f3_s15_recdef_1,A) | p1_s15_recdef_1(A,k1_funct_1(f5_s15_recdef_1,A),k1_funct_1(f5_s15_recdef_1,k1_nat_1(A,1))) ) ) ) ) => f4_s15_recdef_1 = f5_s15_recdef_1 ), inference(mizar_proof,[status(thm)],[d3_finseq_1,d3_finseq_1,t9_funct_1,d3_finseq_1,t3_finseq_1,s5_nat_1,d5_real_1,t22_nat_1,t38_nat_1,t31_xreal_1,t2_xreal_1,t38_nat_1,l1_recdef_1,l1_recdef_1,l1_recdef_1]), [file(recdef_1,s15_recdef_1),interesting(0.02)]). 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(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(s9_recdef_1,theorem, ( ( k1_relat_1(f2_s9_recdef_1) = k5_numbers & k1_funct_1(f2_s9_recdef_1,0) = f1_s9_recdef_1 & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => p1_s9_recdef_1(A,k1_funct_1(f2_s9_recdef_1,A),k1_funct_1(f2_s9_recdef_1,k1_nat_1(A,1))) ) & k1_relat_1(f3_s9_recdef_1) = k5_numbers & k1_funct_1(f3_s9_recdef_1,0) = f1_s9_recdef_1 & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => p1_s9_recdef_1(A,k1_funct_1(f3_s9_recdef_1,A),k1_funct_1(f3_s9_recdef_1,k1_nat_1(A,1))) ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B,C,D] : ( ( p1_s9_recdef_1(A,B,C) & p1_s9_recdef_1(A,B,D) ) => C = D ) ) ) => f2_s9_recdef_1 = f3_s9_recdef_1 ), inference(mizar_proof,[status(thm)],[s1_nat_1,t9_funct_1]), [file(recdef_1,s9_recdef_1),interesting(0.00)]). fof(s11_recdef_1,theorem, ( ( k1_relat_1(f3_s11_recdef_1) = k5_numbers & k1_funct_1(f3_s11_recdef_1,0) = f1_s11_recdef_1 & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k1_funct_1(f3_s11_recdef_1,k1_nat_1(A,1)) = f2_s11_recdef_1(A,k1_funct_1(f3_s11_recdef_1,A)) ) & k1_relat_1(f4_s11_recdef_1) = k5_numbers & k1_funct_1(f4_s11_recdef_1,0) = f1_s11_recdef_1 & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k1_funct_1(f4_s11_recdef_1,k1_nat_1(A,1)) = f2_s11_recdef_1(A,k1_funct_1(f4_s11_recdef_1,A)) ) ) => f3_s11_recdef_1 = f4_s11_recdef_1 ), inference(mizar_proof,[status(thm)],[s9_recdef_1]), [file(recdef_1,s11_recdef_1),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(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(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(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(s10_recdef_1,theorem, ( ( k8_funct_2(k5_numbers,f1_s10_recdef_1,f3_s10_recdef_1,0) = f2_s10_recdef_1 & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => p1_s10_recdef_1(A,k8_funct_2(k5_numbers,f1_s10_recdef_1,f3_s10_recdef_1,A),k8_funct_2(k5_numbers,f1_s10_recdef_1,f3_s10_recdef_1,k1_nat_1(A,1))) ) & k8_funct_2(k5_numbers,f1_s10_recdef_1,f4_s10_recdef_1,0) = f2_s10_recdef_1 & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => p1_s10_recdef_1(A,k8_funct_2(k5_numbers,f1_s10_recdef_1,f4_s10_recdef_1,A),k8_funct_2(k5_numbers,f1_s10_recdef_1,f4_s10_recdef_1,k1_nat_1(A,1))) ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,f1_s10_recdef_1) => ! [C] : ( m1_subset_1(C,f1_s10_recdef_1) => ! [D] : ( m1_subset_1(D,f1_s10_recdef_1) => ( ( p1_s10_recdef_1(A,B,C) & p1_s10_recdef_1(A,B,D) ) => C = D ) ) ) ) ) ) => f3_s10_recdef_1 = f4_s10_recdef_1 ), inference(mizar_proof,[status(thm)],[d1_funct_2,d1_funct_2,t9_funct_1,s5_nat_1,t22_nat_1,t38_nat_1]), [file(recdef_1,s10_recdef_1),interesting(0.00)]). fof(s12_recdef_1,theorem, ( ( k8_funct_2(k5_numbers,f1_s12_recdef_1,f4_s12_recdef_1,0) = f2_s12_recdef_1 & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,f1_s12_recdef_1,f4_s12_recdef_1,k1_nat_1(A,1)) = f3_s12_recdef_1(A,k8_funct_2(k5_numbers,f1_s12_recdef_1,f4_s12_recdef_1,A)) ) & k8_funct_2(k5_numbers,f1_s12_recdef_1,f5_s12_recdef_1,0) = f2_s12_recdef_1 & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,f1_s12_recdef_1,f5_s12_recdef_1,k1_nat_1(A,1)) = f3_s12_recdef_1(A,k8_funct_2(k5_numbers,f1_s12_recdef_1,f5_s12_recdef_1,A)) ) ) => f4_s12_recdef_1 = f5_s12_recdef_1 ), inference(mizar_proof,[status(thm)],[s10_recdef_1]), [file(recdef_1,s12_recdef_1),interesting(0.00)]). fof(s13_recdef_1,theorem, ( ( k8_funct_2(k5_numbers,k1_numbers,f3_s13_recdef_1,0) = f1_s13_recdef_1 & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k1_numbers,f3_s13_recdef_1,k1_nat_1(A,1)) = f2_s13_recdef_1(A,k8_funct_2(k5_numbers,k1_numbers,f3_s13_recdef_1,A)) ) & k8_funct_2(k5_numbers,k1_numbers,f4_s13_recdef_1,0) = f1_s13_recdef_1 & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k1_numbers,f4_s13_recdef_1,k1_nat_1(A,1)) = f2_s13_recdef_1(A,k8_funct_2(k5_numbers,k1_numbers,f4_s13_recdef_1,A)) ) ) => f3_s13_recdef_1 = f4_s13_recdef_1 ), inference(mizar_proof,[status(thm)],[s10_recdef_1]), [file(recdef_1,s13_recdef_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(t3_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r2_hidden(A,k2_finseq_1(B)) <=> ( r1_xreal_0(1,A) & r1_xreal_0(A,B) ) ) ) ) ), file(finseq_1,t3_finseq_1), [interesting(0.00)]). fof(d5_real_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) <=> ~ ( r1_xreal_0(B,A) & B != A ) ) ) ) ), file(real_1,d5_real_1), [interesting(0.00)]). fof(t31_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k2_xcmplx_0(B,A),B) ) ) ) ), file(xreal_1,t31_xreal_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(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(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(t13_funcop_1,theorem,( ! [A,B,C] : ( r2_hidden(B,A) => k1_funct_1(k2_funcop_1(A,C),B) = C ) ), file(funcop_1,t13_funcop_1), [interesting(0.00)]). fof(t19_funcop_1,theorem,( ! [A,B] : ( k1_relat_1(k2_funcop_1(A,B)) = A & r1_tarski(k2_relat_1(k2_funcop_1(A,B)),k1_tarski(B)) ) ), file(funcop_1,t19_funcop_1), [interesting(0.00)]). fof(t18_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => r1_xreal_0(0,A) ) ), file(nat_1,t18_nat_1), [interesting(0.00)]). fof(t26_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ~ ( r1_xreal_0(A,k2_xcmplx_0(B,1)) & ~ r1_xreal_0(A,B) & A != k2_xcmplx_0(B,1) ) ) ) ), file(nat_1,t26_nat_1), [interesting(0.00)]). fof(t8_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(k2_xcmplx_0(A,C),k2_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t8_xreal_1), [interesting(0.00)]). fof(s2_funct_1,theorem, ( ( ! [A,B,C] : ( ( r2_hidden(A,f1_s2_funct_1) & p1_s2_funct_1(A,B) & p1_s2_funct_1(A,C) ) => B = C ) & ! [A] : ~ ( r2_hidden(A,f1_s2_funct_1) & ! [B] : ~ p1_s2_funct_1(A,B) ) ) => ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & k1_relat_1(A) = f1_s2_funct_1 & ! [B] : ( r2_hidden(B,f1_s2_funct_1) => p1_s2_funct_1(B,k1_funct_1(A,B)) ) ) ), file(funct_1,s2_funct_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(s7_funct_2,theorem, ( ! [A] : ( m1_subset_1(A,f1_s7_funct_2) => ! [B] : ( m1_subset_1(B,f2_s7_funct_2) => ? [C] : ( m1_subset_1(C,f3_s7_funct_2) & p1_s7_funct_2(A,B,C) ) ) ) => ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(f1_s7_funct_2,f2_s7_funct_2),f3_s7_funct_2) & m2_relset_1(A,k2_zfmisc_1(f1_s7_funct_2,f2_s7_funct_2),f3_s7_funct_2) & ! [B] : ( m1_subset_1(B,f1_s7_funct_2) => ! [C] : ( m1_subset_1(C,f2_s7_funct_2) => p1_s7_funct_2(B,C,k1_funct_1(A,k4_tarski(B,C))) ) ) ) ), file(funct_2,s7_funct_2), [interesting(0.00)]). fof(s4_finseq_1,theorem,( ? [A] : ! [B] : ( r2_hidden(B,A) <=> ? [C] : ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) & r2_hidden(C,k13_finseq_1(f1_s4_finseq_1)) & p1_s4_finseq_1(C) & B = C ) ) ), file(finseq_1,s4_finseq_1), [interesting(0.00)]). fof(t9_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( ( r1_xreal_0(A,B) & r1_xreal_0(C,D) ) => r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,D)) ) ) ) ) ) ), file(xreal_1,t9_xreal_1), [interesting(0.00)]). fof(t16_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ~ ( r2_hidden(A,B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ ( r2_hidden(C,k4_finseq_1(B)) & A = k4_tarski(C,k1_funct_1(B,C)) ) ) ) ) ), file(finseq_1,t16_finseq_1), [interesting(0.00)]). fof(t8_funct_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(k4_tarski(A,B),C) <=> ( r2_hidden(A,k1_relat_1(C)) & B = k1_funct_1(C,A) ) ) ) ), file(funct_1,t8_funct_1), [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(d4_tarski,definition,( ! [A,B] : ( B = k3_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(C,D) & r2_hidden(D,A) ) ) ) ), file(tarski,d4_tarski), [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(d1_funct_1,definition,( ! [A] : ( v1_funct_1(A) <=> ! [B,C,D] : ( ( r2_hidden(k4_tarski(B,C),A) & r2_hidden(k4_tarski(B,D),A) ) => C = D ) ) ), file(funct_1,d1_funct_1), [interesting(0.00)]). fof(s1_funct_1,theorem, ( ! [A,B,C] : ( ( p1_s1_funct_1(A,B) & p1_s1_funct_1(A,C) ) => B = C ) => ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & ! [B,C] : ( r2_hidden(k4_tarski(B,C),A) <=> ( r2_hidden(B,f1_s1_funct_1) & p1_s1_funct_1(B,C) ) ) ) ), file(funct_1,s1_funct_1), [interesting(0.00)]). fof(d4_relat_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( B = k1_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : r2_hidden(k4_tarski(C,D),A) ) ) ) ), file(relat_1,d4_relat_1), [interesting(0.00)]). fof(d1_relat_1,definition,( ! [A] : ( v1_relat_1(A) <=> ! [B] : ~ ( r2_hidden(B,A) & ! [C,D] : B != k4_tarski(C,D) ) ) ), file(relat_1,d1_relat_1), [interesting(0.00)]). fof(t2_tarski,theorem,( ! [A,B] : ( ! [C] : ( r2_hidden(C,A) <=> r2_hidden(C,B) ) => A = B ) ), file(tarski,t2_tarski), [interesting(0.00)]). fof(t4_funct_2,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r1_tarski(k2_relat_1(B),A) => ( v1_funct_1(B) & v1_funct_2(B,k1_relat_1(B),A) & m2_relset_1(B,k1_relat_1(B),A) ) ) ) ), file(funct_2,t4_funct_2), [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(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(t37_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v4_ordinal2(C) => ( r1_xreal_0(A,B) => r1_xreal_0(A,k2_xcmplx_0(B,C)) ) ) ) ) ), file(nat_1,t37_nat_1), [interesting(0.00)]). fof(t52_finseq_1,theorem,( ! [A] : k9_finseq_1(A) = k1_tarski(k4_tarski(1,A)) ), file(finseq_1,t52_finseq_1), [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(t35_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) ) => k3_finseq_1(k7_finseq_1(A,B)) = k1_nat_1(k3_finseq_1(A),k3_finseq_1(B)) ) ) ), file(finseq_1,t35_finseq_1), [interesting(0.00)]). fof(d7_finseq_1,definition,( ! [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) ) => ( C = k7_finseq_1(A,B) <=> ( k4_finseq_1(C) = k2_finseq_1(k1_nat_1(k3_finseq_1(A),k3_finseq_1(B))) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(A)) => k1_funct_1(C,D) = k1_funct_1(A,D) ) ) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(B)) => k1_funct_1(C,k1_nat_1(k3_finseq_1(A),D)) = k1_funct_1(B,D) ) ) ) ) ) ) ) ), file(finseq_1,d7_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(t36_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] : ( v4_ordinal2(C) => ( ( r1_xreal_0(k1_nat_1(k3_finseq_1(A),1),C) & r1_xreal_0(C,k1_nat_1(k3_finseq_1(A),k3_finseq_1(B))) ) => k1_funct_1(k7_finseq_1(A,B),C) = k1_funct_1(B,k6_xcmplx_0(C,k3_finseq_1(A))) ) ) ) ) ), file(finseq_1,t36_finseq_1), [interesting(0.00)]). fof(d4_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C] : ( ( r2_hidden(B,k1_relat_1(A)) => ( C = k1_funct_1(A,B) <=> r2_hidden(k4_tarski(B,C),A) ) ) & ( ~ r2_hidden(B,k1_relat_1(A)) => ( C = k1_funct_1(A,B) <=> C = k1_xboole_0 ) ) ) ) ), file(funct_1,d4_funct_1), [interesting(0.00)]). fof(s21_recdef_1,theorem, ( ? [A] : ( m1_subset_1(A,f1_s21_recdef_1) & ? [B] : ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,f1_s21_recdef_1) & m2_relset_1(B,k5_numbers,f1_s21_recdef_1) & A = k8_funct_2(k5_numbers,f1_s21_recdef_1,B,f3_s21_recdef_1) & k8_funct_2(k5_numbers,f1_s21_recdef_1,B,0) = f2_s21_recdef_1 & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,f1_s21_recdef_1,B,k1_nat_1(C,1)) = f4_s21_recdef_1(C,k8_funct_2(k5_numbers,f1_s21_recdef_1,B,C)) ) ) ) & ! [A] : ( m1_subset_1(A,f1_s21_recdef_1) => ! [B] : ( m1_subset_1(B,f1_s21_recdef_1) => ~ ( ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,f1_s21_recdef_1) & m2_relset_1(C,k5_numbers,f1_s21_recdef_1) & A = k8_funct_2(k5_numbers,f1_s21_recdef_1,C,f3_s21_recdef_1) & k8_funct_2(k5_numbers,f1_s21_recdef_1,C,0) = f2_s21_recdef_1 & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,f1_s21_recdef_1,C,k1_nat_1(D,1)) = f4_s21_recdef_1(D,k8_funct_2(k5_numbers,f1_s21_recdef_1,C,D)) ) ) & ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,f1_s21_recdef_1) & m2_relset_1(C,k5_numbers,f1_s21_recdef_1) & B = k8_funct_2(k5_numbers,f1_s21_recdef_1,C,f3_s21_recdef_1) & k8_funct_2(k5_numbers,f1_s21_recdef_1,C,0) = f2_s21_recdef_1 & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,f1_s21_recdef_1,C,k1_nat_1(D,1)) = f4_s21_recdef_1(D,k8_funct_2(k5_numbers,f1_s21_recdef_1,C,D)) ) ) & A != B ) ) ) ), inference(mizar_proof,[status(thm)],[s20_recdef_1]), [file(recdef_1,s21_recdef_1),interesting(0.00)]). fof(t22_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,k2_xcmplx_0(B,C)) <=> r1_xreal_0(k6_xcmplx_0(A,B),C) ) ) ) ) ), file(xreal_1,t22_xreal_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(t91_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r1_tarski(A,k1_relat_1(B)) => k1_relat_1(k7_relat_1(B,A)) = A ) ) ), file(relat_1,t91_relat_1), [interesting(0.00)]). fof(d2_finseq_1,definition,( ! [A] : ( v1_relat_1(A) => ( v1_finseq_1(A) <=> ? [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) & k1_relat_1(A) = k2_finseq_1(B) ) ) ) ), file(finseq_1,d2_finseq_1), [interesting(0.00)]). fof(t72_funct_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(B,A) => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ), file(funct_1,t72_funct_1), [interesting(0.00)]). fof(t70_funct_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(B,k1_relat_1(k7_relat_1(C,A))) => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ), file(funct_1,t70_funct_1), [interesting(0.00)]).