fof(t90_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => k9_rlvect_1(A,k8_rlvect_1(A,k1_rlvect_1(A),k1_rlvect_1(A),k1_rlvect_1(A))) = k1_rlvect_1(A) ) ), inference(mizar_proof,[status(thm)],[t63_rlvect_1,t10_rlvect_1,t10_rlvect_1]), [file(rlvect_1,t90_rlvect_1),interesting(1.00)]). fof(t74_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => k9_rlvect_1(A,k7_rlvect_1(A,k1_rlvect_1(A),k1_rlvect_1(A))) = k1_rlvect_1(A) ) ), inference(mizar_proof,[status(thm)],[t62_rlvect_1,t10_rlvect_1]), [file(rlvect_1,t74_rlvect_1),interesting(0.99)]). fof(t62_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k9_rlvect_1(A,k7_rlvect_1(A,B,C)) = k2_rlvect_1(A,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_finseq_1,t58_rlvect_1,l78_rlvect_1,l78_rlvect_1]), [file(rlvect_1,t62_rlvect_1),interesting(0.98)]). fof(t25_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => k5_rlvect_1(A,k1_rlvect_1(A)) = k1_rlvect_1(A) ) ), inference(mizar_proof,[status(thm)],[d10_rlvect_1,t10_rlvect_1]), [file(rlvect_1,t25_rlvect_1),interesting(0.97)]). fof(t78_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k9_rlvect_1(A,k7_rlvect_1(A,k5_rlvect_1(A,B),k5_rlvect_1(A,C))) = k5_rlvect_1(A,k2_rlvect_1(A,C,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t62_rlvect_1,l55_rlvect_1]), [file(rlvect_1,t78_rlvect_1),interesting(0.96)]). fof(t84_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k9_rlvect_1(A,k8_rlvect_1(A,C,B,D)) = k4_rlvect_1(A,k9_rlvect_1(A,k7_rlvect_1(A,C,D)),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t63_rlvect_1,d6_rlvect_1,t62_rlvect_1]), [file(rlvect_1,t84_rlvect_1),interesting(0.96)]). fof(t33_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( B = k5_rlvect_1(A,B) => B = k1_rlvect_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_rlvect_1,t30_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,t24_rlvect_1]), [file(rlvect_1,t33_rlvect_1),interesting(0.94)]). fof(t48_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => k3_rlvect_1(B,k6_rlvect_1(B,C,D),A) = k6_rlvect_1(B,k3_rlvect_1(B,C,A),k3_rlvect_1(B,D,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,t39_rlvect_1]), [file(rlvect_1,t48_rlvect_1),interesting(0.94)]). fof(t50_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ( k3_rlvect_1(B,C,A) = k3_rlvect_1(B,D,A) => ( A = 0 | C = D ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_rlvect_1,t48_rlvect_1,t24_rlvect_1,t35_rlvect_1]), [file(rlvect_1,t50_rlvect_1),interesting(0.94)]). fof(t79_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k9_rlvect_1(A,k7_rlvect_1(A,B,B)) = k3_rlvect_1(A,B,2) ) ) ), inference(mizar_proof,[status(thm)],[t62_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1]), [file(rlvect_1,t79_rlvect_1),interesting(0.94)]). fof(t93_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k9_rlvect_1(A,k8_rlvect_1(A,B,B,B)) = k3_rlvect_1(A,B,3) ) ) ), inference(mizar_proof,[status(thm)],[t84_rlvect_1,t79_rlvect_1,d9_rlvect_1,d9_rlvect_1]), [file(rlvect_1,t93_rlvect_1),interesting(0.94)]). fof(t75_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k9_rlvect_1(A,k7_rlvect_1(A,k1_rlvect_1(A),B)) = B & k9_rlvect_1(A,k7_rlvect_1(A,B,k1_rlvect_1(A))) = B ) ) ) ), inference(mizar_proof,[status(thm)],[t62_rlvect_1,t10_rlvect_1,t62_rlvect_1,t10_rlvect_1]), [file(rlvect_1,t75_rlvect_1),interesting(0.93)]). fof(t30_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k5_rlvect_1(A,k5_rlvect_1(A,B)) = B ) ) ), inference(mizar_proof,[status(thm)],[d10_rlvect_1,t19_rlvect_1]), [file(rlvect_1,t30_rlvect_1),interesting(0.92)]). fof(l68_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => k9_rlvect_1(A,k6_finseq_1(u1_struct_0(A))) = k1_rlvect_1(A) ) ), inference(mizar_proof,[status(thm)],[d12_rlvect_1,t25_finseq_1]), [file(rlvect_1,l68_rlvect_1),interesting(0.92)]). fof(t59_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_1(B,u1_struct_0(A)) => ! [C] : ( m2_finseq_1(C,u1_struct_0(A)) => ( ( k2_relat_1(B) = k2_relat_1(C) & v2_funct_1(B) & v2_funct_1(C) ) => k9_rlvect_1(A,B) = k9_rlvect_1(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t25_finseq_1,t27_finseq_1,t27_finseq_1,t25_finseq_1,l69_rlvect_1,t65_finseq_1,t23_finseq_1,t6_finseq_1,d3_finseq_1,d5_funct_1,d5_funct_1,d3_finseq_1,t54_rlvect_1,t3_finseq_1,t28_nat_1,t3_finseq_1,t28_nat_1,t23_finseq_1,s1_finseq_1,d3_tarski,d5_funct_1,t3_finseq_1,t37_nat_1,t2_xreal_1,t3_finseq_1,t9_xreal_1,t3_finseq_1,t54_rlvect_1,d4_finseq_1,t37_nat_1,t21_finseq_1,t29_nat_1,t2_xreal_1,t21_finseq_1,d3_finseq_1,t35_finseq_1,t57_finseq_1,d3_finseq_1,t35_finseq_1,t57_finseq_1,d3_finseq_1,t11_finseq_1,t21_finseq_1,t70_funct_1,d7_finseq_1,d1_tarski,t3_finseq_1,t56_finseq_1,d3_finseq_1,d7_finseq_1,t57_finseq_1,d2_xboole_0,t35_finseq_1,t56_finseq_1,d7_finseq_1,t44_finseq_1,t44_finseq_1,t56_finseq_1,t4_xboole_1,t44_finseq_1,t31_xreal_1,d7_xboole_0,d3_xboole_0,t44_finseq_1,d3_xboole_0,d1_tarski,d5_funct_1,t21_finseq_1,t70_funct_1,t3_finseq_1,t3_finseq_1,t2_xreal_1,t3_finseq_1,t3_finseq_1,d3_finseq_1,d1_tarski,d8_funct_1,d5_funct_1,t37_nat_1,t3_finseq_1,t9_xreal_1,t3_finseq_1,d3_finseq_1,d8_funct_1,t3_finseq_1,d2_xboole_0,t88_xboole_1,t12_finseq_1,t148_relat_1,d3_finseq_1,t146_relat_1,t123_funct_1,t117_funct_1,t84_funct_1,d8_funct_1,t84_funct_1,d7_finseq_1,d8_funct_1,t70_funct_1,d7_finseq_1,d7_finseq_1,t21_finseq_1,t3_finseq_1,t2_xreal_1,t37_nat_1,t3_finseq_1,t9_xreal_1,t3_finseq_1,d3_finseq_1,t2_xreal_1,t37_nat_1,d8_funct_1,t70_funct_1,d7_finseq_1,d7_finseq_1,t21_finseq_1,t3_finseq_1,t2_xreal_1,t37_nat_1,t3_finseq_1,t9_xreal_1,t3_finseq_1,d3_finseq_1,t2_xreal_1,t37_nat_1,d8_funct_1,d7_finseq_1,d7_finseq_1,t37_nat_1,t3_finseq_1,t9_xreal_1,t3_finseq_1,d3_finseq_1,d8_funct_1,t38_finseq_1,t56_finseq_1,t70_funct_1,t55_finseq_1,t4_finseq_1,d1_tarski,t57_finseq_1,d7_finseq_1,t58_rlvect_1,t58_rlvect_1,t58_rlvect_1,d6_rlvect_1,t58_rlvect_1,s1_nat_1]), [file(rlvect_1,t59_rlvect_1),interesting(0.92)]). fof(l23_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & k2_rlvect_1(A,B,D) = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_rlvect_1,d10_rlvect_1,t10_rlvect_1]), [file(rlvect_1,l23_rlvect_1),interesting(0.91)]). fof(t72_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k9_rlvect_1(A,k7_rlvect_1(A,B,C)) = k9_rlvect_1(A,k7_rlvect_1(A,C,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t62_rlvect_1,t62_rlvect_1]), [file(rlvect_1,t72_rlvect_1),interesting(0.91)]). fof(t80_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k9_rlvect_1(A,k7_rlvect_1(A,k5_rlvect_1(A,B),k5_rlvect_1(A,B))) = k3_rlvect_1(A,B,k1_real_1(2)) ) ) ), inference(mizar_proof,[status(thm)],[t78_rlvect_1,t62_rlvect_1,t79_rlvect_1,t29_rlvect_1,d9_rlvect_1]), [file(rlvect_1,t80_rlvect_1),interesting(0.91)]). fof(t35_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k6_rlvect_1(A,B,C) = k1_rlvect_1(A) => B = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_rlvect_1,t31_rlvect_1]), [file(rlvect_1,t35_rlvect_1),interesting(0.90)]). fof(l76_rlvect_1,theorem,( ! [A] : ( v4_ordinal2(A) => ( ~ r1_xreal_0(1,A) => A = 0 ) ) ), inference(mizar_proof,[status(thm)],[t39_nat_1]), [file(rlvect_1,l76_rlvect_1),interesting(0.89)]). fof(l69_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_1(B,u1_struct_0(A)) => ( k3_finseq_1(B) = 0 => k9_rlvect_1(A,B) = k1_rlvect_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t32_finseq_1,l68_rlvect_1]), [file(rlvect_1,l69_rlvect_1),interesting(0.88)]). fof(t77_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k9_rlvect_1(A,k7_rlvect_1(A,B,k5_rlvect_1(A,C))) = k6_rlvect_1(A,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[t62_rlvect_1]), [file(rlvect_1,t77_rlvect_1),interesting(0.88)]). fof(t76_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k9_rlvect_1(A,k7_rlvect_1(A,B,k5_rlvect_1(A,B))) = k1_rlvect_1(A) & k9_rlvect_1(A,k7_rlvect_1(A,k5_rlvect_1(A,B),B)) = k1_rlvect_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_rlvect_1,t62_rlvect_1,l18_rlvect_1,t62_rlvect_1]), [file(rlvect_1,t76_rlvect_1),interesting(0.87)]). fof(t19_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k2_rlvect_1(A,B,C) = k1_rlvect_1(A) => B = k5_rlvect_1(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l18_rlvect_1,d10_rlvect_1]), [file(rlvect_1,t19_rlvect_1),interesting(0.86)]). fof(t3_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => r1_rlvect_1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d1_rlvect_1]), [file(rlvect_1,t3_rlvect_1),interesting(0.86)]). fof(t27_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k6_rlvect_1(A,k1_rlvect_1(A),B) = k5_rlvect_1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t10_rlvect_1]), [file(rlvect_1,t27_rlvect_1),interesting(0.86)]). fof(t49_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v7_rlvect_1(C) & l2_rlvect_1(C) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(C)) => k3_rlvect_1(C,D,k5_real_1(A,B)) = k6_rlvect_1(C,k3_rlvect_1(C,D,A),k3_rlvect_1(C,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,t38_rlvect_1,t39_rlvect_1]), [file(rlvect_1,t49_rlvect_1),interesting(0.86)]). fof(t31_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k5_rlvect_1(A,B) = k5_rlvect_1(A,C) => B = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[t30_rlvect_1,t30_rlvect_1]), [file(rlvect_1,t31_rlvect_1),interesting(0.85)]). fof(t83_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k9_rlvect_1(A,k8_rlvect_1(A,C,B,D)) = k4_rlvect_1(A,k9_rlvect_1(A,k7_rlvect_1(A,B,D)),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t63_rlvect_1,d6_rlvect_1,t62_rlvect_1]), [file(rlvect_1,t83_rlvect_1),interesting(0.85)]). fof(t60_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => k9_rlvect_1(A,k6_finseq_1(u1_struct_0(A))) = k1_rlvect_1(A) ) ), inference(mizar_proof,[status(thm)],[l68_rlvect_1]), [file(rlvect_1,t60_rlvect_1),interesting(0.84)]). fof(t70_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k5_rlvect_1(A,k9_rlvect_1(A,k7_rlvect_1(A,B,C))) = k6_rlvect_1(A,k5_rlvect_1(A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[t62_rlvect_1,t44_rlvect_1]), [file(rlvect_1,t70_rlvect_1),interesting(0.84)]). fof(t29_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k5_rlvect_1(A,B) = k3_rlvect_1(A,B,k1_real_1(1)) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d9_rlvect_1,t23_rlvect_1,t10_rlvect_1,d6_rlvect_1,d10_rlvect_1,t10_rlvect_1]), [file(rlvect_1,t29_rlvect_1),interesting(0.83)]). fof(l78_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k9_rlvect_1(A,k12_finseq_1(u1_struct_0(A),B)) = B ) ) ), inference(mizar_proof,[status(thm)],[d12_rlvect_1,t56_finseq_1,l76_rlvect_1,l76_rlvect_1,t57_finseq_1,t10_rlvect_1,t56_finseq_1]), [file(rlvect_1,l78_rlvect_1),interesting(0.83)]). fof(t10_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k2_rlvect_1(A,B,k1_rlvect_1(A)) = B & k2_rlvect_1(A,k1_rlvect_1(A),B) = B ) ) ) ), inference(mizar_proof,[status(thm)],[d7_rlvect_1,d8_rlvect_1,l18_rlvect_1,d6_rlvect_1]), [file(rlvect_1,t10_rlvect_1),interesting(0.82)]). fof(t26_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k6_rlvect_1(A,B,k1_rlvect_1(A)) = B ) ) ), inference(mizar_proof,[status(thm)],[t25_rlvect_1,t10_rlvect_1]), [file(rlvect_1,t26_rlvect_1),interesting(0.82)]). fof(t23_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ( ( A = 0 | C = k1_rlvect_1(B) ) => k3_rlvect_1(B,C,A) = k1_rlvect_1(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,t10_rlvect_1,t21_rlvect_1,d9_rlvect_1,t10_rlvect_1,t10_rlvect_1,t21_rlvect_1]), [file(rlvect_1,t23_rlvect_1),interesting(0.82)]). fof(t34_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k4_rlvect_1(A,B,B) = k1_rlvect_1(A) => B = k1_rlvect_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_rlvect_1,t33_rlvect_1]), [file(rlvect_1,t34_rlvect_1),interesting(0.81)]). fof(t38_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k3_rlvect_1(B,k5_rlvect_1(B,C),A) = k3_rlvect_1(B,C,k1_real_1(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_rlvect_1,d9_rlvect_1]), [file(rlvect_1,t38_rlvect_1),interesting(0.81)]). fof(t20_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & k2_rlvect_1(A,B,D) = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[l23_rlvect_1]), [file(rlvect_1,t20_rlvect_1),interesting(0.80)]). fof(t36_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & k6_rlvect_1(A,C,D) = B ) ) ) ) ), inference(mizar_proof,[status(thm)],[l23_rlvect_1,t30_rlvect_1]), [file(rlvect_1,t36_rlvect_1),interesting(0.80)]). fof(t28_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k6_rlvect_1(A,B,B) = k1_rlvect_1(A) ) ) ), inference(mizar_proof,[status(thm)],[d10_rlvect_1]), [file(rlvect_1,t28_rlvect_1),interesting(0.78)]). fof(t44_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k5_rlvect_1(A,k2_rlvect_1(A,B,C)) = k6_rlvect_1(A,k5_rlvect_1(A,C),B) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_rlvect_1,t41_rlvect_1,t27_rlvect_1]), [file(rlvect_1,t44_rlvect_1),interesting(0.78)]). fof(t24_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ~ ( k3_rlvect_1(B,C,A) = k1_rlvect_1(B) & A != 0 & C != k1_rlvect_1(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d7_xcmplx_0,d9_rlvect_1,t23_rlvect_1]), [file(rlvect_1,t24_rlvect_1),interesting(0.77)]). fof(t61_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k9_rlvect_1(A,k12_finseq_1(u1_struct_0(A),B)) = B ) ) ), inference(mizar_proof,[status(thm)],[l78_rlvect_1]), [file(rlvect_1,t61_rlvect_1),interesting(0.77)]). fof(t42_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k6_rlvect_1(A,k2_rlvect_1(A,B,C),D) = k2_rlvect_1(A,B,k6_rlvect_1(A,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_rlvect_1]), [file(rlvect_1,t42_rlvect_1),interesting(0.75)]). fof(t68_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => k5_rlvect_1(A,k9_rlvect_1(A,k6_finseq_1(u1_struct_0(A)))) = k1_rlvect_1(A) ) ), inference(mizar_proof,[status(thm)],[l68_rlvect_1,t25_rlvect_1]), [file(rlvect_1,t68_rlvect_1),interesting(0.75)]). fof(t47_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k5_rlvect_1(A,k6_rlvect_1(A,B,C)) = k2_rlvect_1(A,C,k5_rlvect_1(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l55_rlvect_1,t30_rlvect_1]), [file(rlvect_1,t47_rlvect_1),interesting(0.74)]). fof(t40_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k3_rlvect_1(B,k5_rlvect_1(B,C),k1_real_1(A)) = k3_rlvect_1(B,C,A) ) ) ) ), inference(mizar_proof,[status(thm)],[t38_rlvect_1]), [file(rlvect_1,t40_rlvect_1),interesting(0.73)]). fof(t69_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k5_rlvect_1(A,k9_rlvect_1(A,k12_finseq_1(u1_struct_0(A),B))) = k5_rlvect_1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[l78_rlvect_1]), [file(rlvect_1,t69_rlvect_1),interesting(0.72)]). fof(t66_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,k9_rlvect_1(A,k7_rlvect_1(A,C,D)),B) = k4_rlvect_1(A,k3_rlvect_1(A,C,B),k3_rlvect_1(A,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t62_rlvect_1,d9_rlvect_1]), [file(rlvect_1,t66_rlvect_1),interesting(0.69)]). fof(t95_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_1(B,u1_struct_0(A)) => ( k3_finseq_1(B) = 1 => k9_rlvect_1(A,B) = k1_funct_1(B,1) ) ) ) ), inference(mizar_proof,[status(thm)],[t4_finseq_1,d3_finseq_1,d1_tarski,d4_finseq_1,d5_funct_1,t57_finseq_1,l78_rlvect_1]), [file(rlvect_1,t95_rlvect_1),interesting(0.68)]). fof(t64_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,k1_numbers) => k3_rlvect_1(A,k9_rlvect_1(A,k6_finseq_1(u1_struct_0(A))),B) = k1_rlvect_1(A) ) ) ), inference(mizar_proof,[status(thm)],[l68_rlvect_1,t23_rlvect_1]), [file(rlvect_1,t64_rlvect_1),interesting(0.67)]). fof(t55_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_1(B,u1_struct_0(A)) => ! [C] : ( m2_finseq_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ( k3_finseq_1(B) = k1_nat_1(k3_finseq_1(C),1) & C = k7_relat_1(B,k4_finseq_1(C)) & D = k1_funct_1(B,k3_finseq_1(B)) ) => k9_rlvect_1(A,B) = k2_rlvect_1(A,k9_rlvect_1(A,C),D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_rlvect_1,d12_rlvect_1,t23_finseq_1,t37_nat_1,t3_finseq_1,t54_rlvect_1,t37_nat_1,t21_finseq_1,t7_finseq_1,t82_funct_1,t2_xreal_1,t2_xreal_1,t31_xreal_1,t2_xreal_1,t37_nat_1,t3_finseq_1,d3_finseq_1,t70_funct_1,t31_xreal_1,t2_xreal_1,d3_finseq_1,s1_nat_1,t31_xreal_1]), [file(rlvect_1,t55_rlvect_1),interesting(0.66)]). fof(t67_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => k3_rlvect_1(A,k9_rlvect_1(A,k8_rlvect_1(A,C,D,E)),B) = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,C,B),k3_rlvect_1(A,D,B)),k3_rlvect_1(A,E,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t63_rlvect_1,d9_rlvect_1,d9_rlvect_1]), [file(rlvect_1,t67_rlvect_1),interesting(0.66)]). fof(t94_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_1(B,u1_struct_0(A)) => ( k3_finseq_1(B) = 0 => k9_rlvect_1(A,B) = k1_rlvect_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[l69_rlvect_1]), [file(rlvect_1,t94_rlvect_1),interesting(0.64)]). fof(t56_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m2_finseq_1(C,u1_struct_0(B)) => ! [D] : ( m2_finseq_1(D,u1_struct_0(B)) => ( ( k3_finseq_1(C) = k3_finseq_1(D) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => ( ( r2_hidden(E,k4_finseq_1(C)) & F = k1_funct_1(D,E) ) => k1_funct_1(C,E) = k3_rlvect_1(B,F,A) ) ) ) ) => k9_rlvect_1(B,C) = k3_rlvect_1(B,k9_rlvect_1(B,D),A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l69_rlvect_1,t23_rlvect_1,t23_finseq_1,t37_nat_1,t21_finseq_1,t21_finseq_1,t7_finseq_1,t21_finseq_1,t70_funct_1,t21_finseq_1,t70_funct_1,t6_finseq_1,t54_rlvect_1,d3_finseq_1,d3_finseq_1,t55_rlvect_1,d9_rlvect_1,t55_rlvect_1,d3_finseq_1,s1_nat_1]), [file(rlvect_1,t56_rlvect_1),interesting(0.34)]). fof(t57_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_1(B,u1_struct_0(A)) => ! [C] : ( m2_finseq_1(C,u1_struct_0(A)) => ( ( k3_finseq_1(B) = k3_finseq_1(C) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( r2_hidden(D,k4_finseq_1(B)) & E = k1_funct_1(C,D) ) => k1_funct_1(B,D) = k5_rlvect_1(A,E) ) ) ) ) => k9_rlvect_1(A,B) = k5_rlvect_1(A,k9_rlvect_1(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l69_rlvect_1,t25_rlvect_1,t23_finseq_1,t37_nat_1,t21_finseq_1,t21_finseq_1,t7_finseq_1,t21_finseq_1,t70_funct_1,t21_finseq_1,t70_funct_1,t6_finseq_1,t54_rlvect_1,d3_finseq_1,d3_finseq_1,t55_rlvect_1,l55_rlvect_1,t55_rlvect_1,d3_finseq_1,s1_nat_1]), [file(rlvect_1,t57_rlvect_1),interesting(0.33)]). 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(s2_binop_1,theorem,( ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(f1_s2_binop_1,f1_s2_binop_1),f1_s2_binop_1) & m2_relset_1(A,k2_zfmisc_1(f1_s2_binop_1,f1_s2_binop_1),f1_s2_binop_1) & ! [B] : ( m1_subset_1(B,f1_s2_binop_1) => ! [C] : ( m1_subset_1(C,f1_s2_binop_1) => k2_binop_1(f1_s2_binop_1,f1_s2_binop_1,f1_s2_binop_1,A,B,C) = f2_s2_binop_1(B,C) ) ) ) ), file(binop_1,s2_binop_1), [interesting(0.00)]). fof(s8_funct_2,theorem,( ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(f1_s8_funct_2,f2_s8_funct_2),f3_s8_funct_2) & m2_relset_1(A,k2_zfmisc_1(f1_s8_funct_2,f2_s8_funct_2),f3_s8_funct_2) & ! [B] : ( m1_subset_1(B,f1_s8_funct_2) => ! [C] : ( m1_subset_1(C,f2_s8_funct_2) => k1_funct_1(A,k4_tarski(B,C)) = f4_s8_funct_2(B,C) ) ) ) ), file(funct_2,s8_funct_2), [interesting(0.00)]). fof(l10_rlvect_1,theorem,( ? [A] : ( m1_subset_1(A,k1_zfmisc_1(k5_numbers)) & ? [B] : ( m2_subset_1(B,k5_numbers,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) & ? [D] : ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(k1_numbers,A),A) & m2_relset_1(D,k2_zfmisc_1(k1_numbers,A),A) & ! [E] : ( m1_subset_1(E,u1_struct_0(g2_rlvect_1(A,B,C,D))) => ! [F] : ( m1_subset_1(F,u1_struct_0(g2_rlvect_1(A,B,C,D))) => k2_rlvect_1(g2_rlvect_1(A,B,C,D),E,F) = k2_rlvect_1(g2_rlvect_1(A,B,C,D),F,E) ) ) & ! [E] : ( m1_subset_1(E,u1_struct_0(g2_rlvect_1(A,B,C,D))) => ! [F] : ( m1_subset_1(F,u1_struct_0(g2_rlvect_1(A,B,C,D))) => ! [G] : ( m1_subset_1(G,u1_struct_0(g2_rlvect_1(A,B,C,D))) => k2_rlvect_1(g2_rlvect_1(A,B,C,D),k2_rlvect_1(g2_rlvect_1(A,B,C,D),E,F),G) = k2_rlvect_1(g2_rlvect_1(A,B,C,D),E,k2_rlvect_1(g2_rlvect_1(A,B,C,D),F,G)) ) ) ) & ! [E] : ( m1_subset_1(E,u1_struct_0(g2_rlvect_1(A,B,C,D))) => k2_rlvect_1(g2_rlvect_1(A,B,C,D),E,k1_rlvect_1(g2_rlvect_1(A,B,C,D))) = E ) & ! [E] : ( m1_subset_1(E,u1_struct_0(g2_rlvect_1(A,B,C,D))) => ? [F] : ( m1_subset_1(F,u1_struct_0(g2_rlvect_1(A,B,C,D))) & k2_rlvect_1(g2_rlvect_1(A,B,C,D),E,F) = k1_rlvect_1(g2_rlvect_1(A,B,C,D)) ) ) & ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,u1_struct_0(g2_rlvect_1(A,B,C,D))) => ! [G] : ( m1_subset_1(G,u1_struct_0(g2_rlvect_1(A,B,C,D))) => k3_rlvect_1(g2_rlvect_1(A,B,C,D),k2_rlvect_1(g2_rlvect_1(A,B,C,D),F,G),E) = k2_rlvect_1(g2_rlvect_1(A,B,C,D),k3_rlvect_1(g2_rlvect_1(A,B,C,D),F,E),k3_rlvect_1(g2_rlvect_1(A,B,C,D),G,E)) ) ) ) & ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,u1_struct_0(g2_rlvect_1(A,B,C,D))) => k3_rlvect_1(g2_rlvect_1(A,B,C,D),G,k3_real_1(E,F)) = k2_rlvect_1(g2_rlvect_1(A,B,C,D),k3_rlvect_1(g2_rlvect_1(A,B,C,D),G,E),k3_rlvect_1(g2_rlvect_1(A,B,C,D),G,F)) ) ) ) & ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,u1_struct_0(g2_rlvect_1(A,B,C,D))) => k3_rlvect_1(g2_rlvect_1(A,B,C,D),G,k4_real_1(E,F)) = k3_rlvect_1(g2_rlvect_1(A,B,C,D),k3_rlvect_1(g2_rlvect_1(A,B,C,D),G,F),E) ) ) ) & ! [E] : ( m1_subset_1(E,u1_struct_0(g2_rlvect_1(A,B,C,D))) => k3_rlvect_1(g2_rlvect_1(A,B,C,D),E,1) = E ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_tarski,s2_binop_1,s8_funct_2,d1_tarski,d1_tarski]), [file(rlvect_1,l10_rlvect_1),interesting(0.00)]). fof(t11_rlvect_1,theorem,( $true ), file(rlvect_1,t11_rlvect_1), [interesting(0.00)]). fof(t12_rlvect_1,theorem,( $true ), file(rlvect_1,t12_rlvect_1), [interesting(0.00)]). fof(t13_rlvect_1,theorem,( $true ), file(rlvect_1,t13_rlvect_1), [interesting(0.00)]). fof(t14_rlvect_1,theorem,( $true ), file(rlvect_1,t14_rlvect_1), [interesting(0.00)]). fof(t15_rlvect_1,theorem,( $true ), file(rlvect_1,t15_rlvect_1), [interesting(0.00)]). fof(t17_rlvect_1,theorem,( $true ), file(rlvect_1,t17_rlvect_1), [interesting(0.00)]). fof(t18_rlvect_1,theorem,( $true ), file(rlvect_1,t18_rlvect_1), [interesting(0.00)]). fof(t1_rlvect_1,theorem,( $true ), file(rlvect_1,t1_rlvect_1), [interesting(0.00)]). fof(d6_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ( v4_rlvect_1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k2_rlvect_1(A,k2_rlvect_1(A,B,C),D) = k2_rlvect_1(A,B,k2_rlvect_1(A,C,D)) ) ) ) ) ) ), file(rlvect_1,d6_rlvect_1), [interesting(0.00)]). fof(d10_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( ( v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( C = k5_rlvect_1(A,B) <=> k2_rlvect_1(A,B,C) = k1_rlvect_1(A) ) ) ) ) ) ), file(rlvect_1,d10_rlvect_1), [interesting(0.00)]). fof(d7_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ( v5_rlvect_1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k2_rlvect_1(A,B,k1_rlvect_1(A)) = B ) ) ) ), file(rlvect_1,d7_rlvect_1), [interesting(0.00)]). fof(d8_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ( v6_rlvect_1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & k2_rlvect_1(A,B,C) = k1_rlvect_1(A) ) ) ) ) ), file(rlvect_1,d8_rlvect_1), [interesting(0.00)]). fof(l18_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k2_rlvect_1(A,B,C) = k1_rlvect_1(A) => k2_rlvect_1(A,C,B) = k1_rlvect_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_rlvect_1,d7_rlvect_1,d6_rlvect_1,d6_rlvect_1,d7_rlvect_1]), [file(rlvect_1,l18_rlvect_1),interesting(0.00)]). fof(t16_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k2_rlvect_1(A,B,k5_rlvect_1(A,B)) = k1_rlvect_1(A) & k2_rlvect_1(A,k5_rlvect_1(A,B),B) = k1_rlvect_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_rlvect_1,l18_rlvect_1]), [file(rlvect_1,t16_rlvect_1),interesting(0.00)]). fof(t21_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( k2_rlvect_1(A,B,D) = k2_rlvect_1(A,B,E) | k2_rlvect_1(A,D,B) = k2_rlvect_1(A,E,B) ) => D = E ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_rlvect_1,t16_rlvect_1,d6_rlvect_1,d6_rlvect_1,t16_rlvect_1,t10_rlvect_1,t10_rlvect_1,t16_rlvect_1,d6_rlvect_1,d6_rlvect_1,t16_rlvect_1,t10_rlvect_1]), [file(rlvect_1,t21_rlvect_1),interesting(0.00)]). fof(t22_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ( k2_rlvect_1(A,B,C) = B | k2_rlvect_1(A,C,B) = B ) => C = k1_rlvect_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_rlvect_1,t21_rlvect_1]), [file(rlvect_1,t22_rlvect_1),interesting(0.00)]). fof(t2_rlvect_1,theorem,( $true ), file(rlvect_1,t2_rlvect_1), [interesting(0.00)]). fof(t32_rlvect_1,theorem,( $true ), file(rlvect_1,t32_rlvect_1), [interesting(0.00)]). fof(d9_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l2_rlvect_1(A) ) => ( v7_rlvect_1(A) <=> ( ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,k2_rlvect_1(A,C,D),B) = k2_rlvect_1(A,k3_rlvect_1(A,C,B),k3_rlvect_1(A,D,B)) ) ) ) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,D,k3_real_1(B,C)) = k2_rlvect_1(A,k3_rlvect_1(A,D,B),k3_rlvect_1(A,D,C)) ) ) ) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,D,k4_real_1(B,C)) = k3_rlvect_1(A,k3_rlvect_1(A,D,C),B) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_rlvect_1(A,B,1) = B ) ) ) ) ), file(rlvect_1,d9_rlvect_1), [interesting(0.00)]). fof(d7_xcmplx_0,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( ( A != 0 => ( B = k5_xcmplx_0(A) <=> k3_xcmplx_0(A,B) = 1 ) ) & ( A = 0 => ( B = k5_xcmplx_0(A) <=> B = 0 ) ) ) ) ) ), file(xcmplx_0,d7_xcmplx_0), [interesting(0.00)]). fof(t37_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( k6_rlvect_1(A,B,C) = k6_rlvect_1(A,B,D) => C = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_rlvect_1,t31_rlvect_1]), [file(rlvect_1,t37_rlvect_1),interesting(0.00)]). fof(d1_rlvect_1,definition,( ! [A] : ( l1_struct_0(A) => ! [B] : ( r1_rlvect_1(A,B) <=> r2_hidden(B,u1_struct_0(A)) ) ) ), file(rlvect_1,d1_rlvect_1), [interesting(0.00)]). fof(l55_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k5_rlvect_1(A,k2_rlvect_1(A,B,C)) = k2_rlvect_1(A,k5_rlvect_1(A,C),k5_rlvect_1(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_rlvect_1,d6_rlvect_1,d10_rlvect_1,t10_rlvect_1,d10_rlvect_1,d10_rlvect_1]), [file(rlvect_1,l55_rlvect_1),interesting(0.00)]). fof(t41_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k6_rlvect_1(A,B,k2_rlvect_1(A,C,D)) = k6_rlvect_1(A,k6_rlvect_1(A,B,D),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l55_rlvect_1,d6_rlvect_1]), [file(rlvect_1,t41_rlvect_1),interesting(0.00)]). fof(t43_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k6_rlvect_1(A,B,k6_rlvect_1(A,C,D)) = k4_rlvect_1(A,k6_rlvect_1(A,B,C),D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t41_rlvect_1,t30_rlvect_1]), [file(rlvect_1,t43_rlvect_1),interesting(0.00)]). fof(t45_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k5_rlvect_1(A,k2_rlvect_1(A,B,C)) = k2_rlvect_1(A,k5_rlvect_1(A,C),k5_rlvect_1(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[l55_rlvect_1]), [file(rlvect_1,t45_rlvect_1),interesting(0.00)]). fof(t46_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k6_rlvect_1(A,k5_rlvect_1(A,B),C) = k6_rlvect_1(A,k5_rlvect_1(A,C),B) ) ) ) ), inference(mizar_proof,[status(thm)],[t44_rlvect_1,t44_rlvect_1]), [file(rlvect_1,t46_rlvect_1),interesting(0.00)]). fof(t4_rlvect_1,theorem,( $true ), file(rlvect_1,t4_rlvect_1), [interesting(0.00)]). fof(t39_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k3_rlvect_1(B,k5_rlvect_1(B,C),A) = k5_rlvect_1(B,k3_rlvect_1(B,C,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t38_rlvect_1,d9_rlvect_1,t29_rlvect_1]), [file(rlvect_1,t39_rlvect_1),interesting(0.00)]). fof(t51_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v7_rlvect_1(C) & l2_rlvect_1(C) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(C)) => ( k3_rlvect_1(C,D,A) = k3_rlvect_1(C,D,B) => ( D = k1_rlvect_1(C) | A = B ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_rlvect_1,t49_rlvect_1,t24_rlvect_1]), [file(rlvect_1,t51_rlvect_1),interesting(0.00)]). fof(t52_rlvect_1,theorem,( $true ), file(rlvect_1,t52_rlvect_1), [interesting(0.00)]). fof(t53_rlvect_1,theorem,( $true ), file(rlvect_1,t53_rlvect_1), [interesting(0.00)]). fof(t32_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( A = k6_finseq_1(B) <=> k3_finseq_1(A) = 0 ) ) ), file(finseq_1,t32_finseq_1), [interesting(0.00)]). fof(d12_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( C = k9_rlvect_1(A,B) <=> ? [D] : ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) & C = k8_funct_2(k5_numbers,u1_struct_0(A),D,k3_finseq_1(B)) & k8_funct_2(k5_numbers,u1_struct_0(A),D,0) = k1_rlvect_1(A) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ( F = k1_funct_1(B,k1_nat_1(E,1)) => ( r1_xreal_0(k3_finseq_1(B),E) | k8_funct_2(k5_numbers,u1_struct_0(A),D,k1_nat_1(E,1)) = k2_rlvect_1(A,k8_funct_2(k5_numbers,u1_struct_0(A),D,E),F) ) ) ) ) ) ) ) ) ) ), file(rlvect_1,d12_rlvect_1), [interesting(0.00)]). fof(t25_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( k3_finseq_1(A) = 0 <=> A = k1_xboole_0 ) ) ), file(finseq_1,t25_finseq_1), [interesting(0.00)]). fof(t23_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B,C] : ( m2_finseq_1(C,B) => m2_finseq_1(k7_relat_1(C,k2_finseq_1(A)),B) ) ) ), file(finseq_1,t23_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(t21_finseq_1,theorem,( ! [A] : ( v4_ordinal2(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) ) => ( ( r1_xreal_0(A,k3_finseq_1(B)) & C = k7_relat_1(B,k2_finseq_1(A)) ) => ( k3_finseq_1(C) = A & k4_finseq_1(C) = k2_finseq_1(A) ) ) ) ) ) ), file(finseq_1,t21_finseq_1), [interesting(0.00)]). fof(t7_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(A,B) <=> r1_tarski(k2_finseq_1(A),k2_finseq_1(B)) ) ) ) ), file(finseq_1,t7_finseq_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)]). fof(t6_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => r2_hidden(k2_xcmplx_0(A,1),k2_finseq_1(k2_xcmplx_0(A,1))) ) ), file(finseq_1,t6_finseq_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(t54_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_1(B,u1_struct_0(A)) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( ( r2_hidden(C,k2_finseq_1(D)) & k3_finseq_1(B) = D ) => m1_subset_1(k1_funct_1(B,C),u1_struct_0(A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_1,d4_finseq_1,d5_funct_1]), [file(rlvect_1,t54_rlvect_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(t82_funct_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r1_tarski(A,B) => ( k7_relat_1(k7_relat_1(C,A),B) = k7_relat_1(C,A) & k7_relat_1(k7_relat_1(C,B),A) = k7_relat_1(C,A) ) ) ) ), file(funct_1,t82_funct_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(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(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(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(t65_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) ) => ( ( k2_relat_1(A) = k2_relat_1(B) & v2_funct_1(A) & v2_funct_1(B) ) => k3_finseq_1(A) = k3_finseq_1(B) ) ) ) ), file(finseq_1,t65_finseq_1), [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(s1_finseq_1,theorem, ( ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B,C] : ( ( r2_hidden(A,k2_finseq_1(f1_s1_finseq_1)) & p1_s1_finseq_1(A,B) & p1_s1_finseq_1(A,C) ) => B = C ) ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ~ ( r2_hidden(A,k2_finseq_1(f1_s1_finseq_1)) & ! [B] : ~ p1_s1_finseq_1(A,B) ) ) ) => ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) & k4_finseq_1(A) = k2_finseq_1(f1_s1_finseq_1) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r2_hidden(B,k2_finseq_1(f1_s1_finseq_1)) => p1_s1_finseq_1(B,k1_funct_1(A,B)) ) ) ) ), file(finseq_1,s1_finseq_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(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(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(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(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(t11_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => k2_xboole_0(k2_finseq_1(A),k1_tarski(k2_xcmplx_0(A,1))) = k2_finseq_1(k2_xcmplx_0(A,1)) ) ), file(finseq_1,t11_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(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(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(t44_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) ) => k2_relat_1(k7_finseq_1(A,B)) = k2_xboole_0(k2_relat_1(A),k2_relat_1(B)) ) ) ), file(finseq_1,t44_finseq_1), [interesting(0.00)]). fof(t4_xboole_1,theorem,( ! [A,B,C] : k2_xboole_0(k2_xboole_0(A,B),C) = k2_xboole_0(A,k2_xboole_0(B,C)) ), file(xboole_1,t4_xboole_1), [interesting(0.00)]). fof(d7_xboole_0,definition,( ! [A,B] : ( r1_xboole_0(A,B) <=> k3_xboole_0(A,B) = k1_xboole_0 ) ), file(xboole_0,d7_xboole_0), [interesting(0.00)]). fof(d3_xboole_0,definition,( ! [A,B,C] : ( C = k3_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & r2_hidden(D,B) ) ) ) ), file(xboole_0,d3_xboole_0), [interesting(0.00)]). fof(d8_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v2_funct_1(A) <=> ! [B,C] : ( ( r2_hidden(B,k1_relat_1(A)) & r2_hidden(C,k1_relat_1(A)) & k1_funct_1(A,B) = k1_funct_1(A,C) ) => B = C ) ) ) ), file(funct_1,d8_funct_1), [interesting(0.00)]). fof(t88_xboole_1,theorem,( ! [A,B] : ( r1_xboole_0(A,B) => k4_xboole_0(k2_xboole_0(A,B),B) = A ) ), file(xboole_1,t88_xboole_1), [interesting(0.00)]). fof(t12_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => k2_finseq_1(A) = k4_xboole_0(k2_finseq_1(k2_xcmplx_0(A,1)),k1_tarski(k2_xcmplx_0(A,1))) ) ), file(finseq_1,t12_finseq_1), [interesting(0.00)]). fof(t148_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => k2_relat_1(k7_relat_1(B,A)) = k9_relat_1(B,A) ) ), file(relat_1,t148_relat_1), [interesting(0.00)]). fof(t146_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => k9_relat_1(A,k1_relat_1(A)) = k2_relat_1(A) ) ), file(relat_1,t146_relat_1), [interesting(0.00)]). fof(t123_funct_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( v2_funct_1(C) => k9_relat_1(C,k4_xboole_0(A,B)) = k4_xboole_0(k9_relat_1(C,A),k9_relat_1(C,B)) ) ) ), file(funct_1,t123_funct_1), [interesting(0.00)]). fof(t117_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r2_hidden(A,k1_relat_1(B)) => k9_relat_1(B,k1_tarski(A)) = k1_tarski(k1_funct_1(B,A)) ) ) ), file(funct_1,t117_funct_1), [interesting(0.00)]). fof(t84_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( v2_funct_1(B) => v2_funct_1(k7_relat_1(B,A)) ) ) ), file(funct_1,t84_funct_1), [interesting(0.00)]). fof(t38_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] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ ( r2_hidden(C,k4_finseq_1(k7_finseq_1(A,B))) & ~ r2_hidden(C,k4_finseq_1(A)) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ~ ( r2_hidden(D,k4_finseq_1(B)) & C = k1_nat_1(k3_finseq_1(A),D) ) ) ) ) ) ) ), file(finseq_1,t38_finseq_1), [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(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_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(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(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(t28_xboole_1,theorem,( ! [A,B] : ( r1_tarski(A,B) => k3_xboole_0(A,B) = A ) ), file(xboole_1,t28_xboole_1), [interesting(0.00)]). fof(t39_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ( ~ r1_xreal_0(1,A) => A = 0 ) ) ), file(nat_1,t39_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(t68_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( B = k7_relat_1(C,A) <=> ( k1_relat_1(B) = k3_xboole_0(k1_relat_1(C),A) & ! [D] : ( r2_hidden(D,k1_relat_1(B)) => k1_funct_1(B,D) = k1_funct_1(C,D) ) ) ) ) ) ), file(funct_1,t68_funct_1), [interesting(0.00)]). fof(t58_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_1(B,u1_struct_0(A)) => ! [C] : ( m2_finseq_1(C,u1_struct_0(A)) => k9_rlvect_1(A,k8_finseq_1(u1_struct_0(A),B,C)) = k2_rlvect_1(A,k9_rlvect_1(A,B),k9_rlvect_1(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t25_finseq_1,l68_rlvect_1,t47_finseq_1,d7_rlvect_1,t23_finseq_1,d3_finseq_1,t6_finseq_1,d4_finseq_1,d5_funct_1,t37_nat_1,t21_finseq_1,t56_finseq_1,t21_finseq_1,t7_finseq_1,t21_finseq_1,t72_funct_1,t4_finseq_1,t55_finseq_1,d1_tarski,d8_finseq_1,d7_finseq_1,t45_finseq_1,t35_finseq_1,t56_finseq_1,d3_finseq_1,d3_finseq_1,t35_finseq_1,t35_finseq_1,t9_xreal_1,t7_finseq_1,t28_xboole_1,d7_finseq_1,d3_finseq_1,t3_finseq_1,t3_finseq_1,t28_nat_1,l76_rlvect_1,t3_finseq_1,t3_finseq_1,t8_xreal_1,t21_finseq_1,t3_finseq_1,t21_finseq_1,d7_finseq_1,t68_funct_1,d3_finseq_1,d3_finseq_1,d7_finseq_1,t35_finseq_1,t55_rlvect_1,d6_rlvect_1,t55_rlvect_1,s1_nat_1]), [file(rlvect_1,t58_rlvect_1),interesting(0.00)]). fof(t5_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k2_rlvect_1(A,B,C) = k2_binop_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),u1_rlvect_1(A),B,C) ) ) ) ), file(rlvect_1,t5_rlvect_1), [interesting(0.00)]). fof(t65_rlvect_1,theorem,( $true ), file(rlvect_1,t65_rlvect_1), [interesting(0.00)]). fof(d9_finseq_1,definition,( ! [A,B] : k10_finseq_1(A,B) = k7_finseq_1(k9_finseq_1(A),k9_finseq_1(B)) ), file(finseq_1,d9_finseq_1), [interesting(0.00)]). fof(t60_finseq_1,theorem,( ! [A,B,C] : ( k11_finseq_1(A,B,C) = k7_finseq_1(k9_finseq_1(A),k10_finseq_1(B,C)) & k11_finseq_1(A,B,C) = k7_finseq_1(k10_finseq_1(A,B),k9_finseq_1(C)) ) ), file(finseq_1,t60_finseq_1), [interesting(0.00)]). fof(t63_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k9_rlvect_1(A,k8_rlvect_1(A,B,C,D)) = k2_rlvect_1(A,k2_rlvect_1(A,B,C),D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t60_finseq_1,t58_rlvect_1,l78_rlvect_1,t62_rlvect_1]), [file(rlvect_1,t63_rlvect_1),interesting(0.00)]). fof(t6_rlvect_1,theorem,( $true ), file(rlvect_1,t6_rlvect_1), [interesting(0.00)]). fof(t71_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k5_rlvect_1(A,k9_rlvect_1(A,k8_rlvect_1(A,B,C,D))) = k6_rlvect_1(A,k6_rlvect_1(A,k5_rlvect_1(A,B),C),D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t63_rlvect_1,t44_rlvect_1,t44_rlvect_1]), [file(rlvect_1,t71_rlvect_1),interesting(0.00)]). fof(t73_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k9_rlvect_1(A,k7_rlvect_1(A,B,C)) = k2_rlvect_1(A,k9_rlvect_1(A,k12_finseq_1(u1_struct_0(A),B)),k9_rlvect_1(A,k12_finseq_1(u1_struct_0(A),C))) ) ) ) ), inference(mizar_proof,[status(thm)],[t62_rlvect_1,l78_rlvect_1,l78_rlvect_1]), [file(rlvect_1,t73_rlvect_1),interesting(0.00)]). fof(d5_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ( v3_rlvect_1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k2_rlvect_1(A,B,C) = k2_rlvect_1(A,C,B) ) ) ) ) ), file(rlvect_1,d5_rlvect_1), [interesting(0.00)]). fof(t7_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_rlvect_1(A) ) => ( ( ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k2_rlvect_1(A,B,C) = k2_rlvect_1(A,C,B) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k2_rlvect_1(A,k2_rlvect_1(A,B,C),D) = k2_rlvect_1(A,B,k2_rlvect_1(A,C,D)) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k2_rlvect_1(A,B,k1_rlvect_1(A)) = B ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & k2_rlvect_1(A,B,C) = k1_rlvect_1(A) ) ) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,k2_rlvect_1(A,C,D),B) = k2_rlvect_1(A,k3_rlvect_1(A,C,B),k3_rlvect_1(A,D,B)) ) ) ) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,D,k3_real_1(B,C)) = k2_rlvect_1(A,k3_rlvect_1(A,D,B),k3_rlvect_1(A,D,C)) ) ) ) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,D,k4_real_1(B,C)) = k3_rlvect_1(A,k3_rlvect_1(A,D,C),B) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_rlvect_1(A,B,1) = B ) ) => ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_rlvect_1,d6_rlvect_1,d7_rlvect_1,d8_rlvect_1,d9_rlvect_1]), [file(rlvect_1,t7_rlvect_1),interesting(0.00)]). fof(t81_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k9_rlvect_1(A,k8_rlvect_1(A,B,C,D)) = k2_rlvect_1(A,k2_rlvect_1(A,k9_rlvect_1(A,k12_finseq_1(u1_struct_0(A),B)),k9_rlvect_1(A,k12_finseq_1(u1_struct_0(A),C))),k9_rlvect_1(A,k12_finseq_1(u1_struct_0(A),D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t63_rlvect_1,l78_rlvect_1,l78_rlvect_1,l78_rlvect_1]), [file(rlvect_1,t81_rlvect_1),interesting(0.00)]). fof(t82_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k9_rlvect_1(A,k8_rlvect_1(A,B,C,D)) = k2_rlvect_1(A,k9_rlvect_1(A,k7_rlvect_1(A,B,C)),D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t63_rlvect_1,t62_rlvect_1]), [file(rlvect_1,t82_rlvect_1),interesting(0.00)]). fof(t88_rlvect_1,theorem,( $true ), file(rlvect_1,t88_rlvect_1), [interesting(0.00)]). fof(t86_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k9_rlvect_1(A,k8_rlvect_1(A,C,B,D)) = k9_rlvect_1(A,k8_rlvect_1(A,B,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t63_rlvect_1,t63_rlvect_1]), [file(rlvect_1,t86_rlvect_1),interesting(0.00)]). fof(t85_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k9_rlvect_1(A,k8_rlvect_1(A,C,B,D)) = k9_rlvect_1(A,k8_rlvect_1(A,C,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t63_rlvect_1,d6_rlvect_1,t63_rlvect_1]), [file(rlvect_1,t85_rlvect_1),interesting(0.00)]). fof(t87_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k9_rlvect_1(A,k8_rlvect_1(A,C,B,D)) = k9_rlvect_1(A,k8_rlvect_1(A,B,D,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t86_rlvect_1,t85_rlvect_1]), [file(rlvect_1,t87_rlvect_1),interesting(0.00)]). fof(t89_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k9_rlvect_1(A,k8_rlvect_1(A,C,B,D)) = k9_rlvect_1(A,k8_rlvect_1(A,D,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t87_rlvect_1,t85_rlvect_1]), [file(rlvect_1,t89_rlvect_1),interesting(0.00)]). fof(t8_rlvect_1,theorem,( $true ), file(rlvect_1,t8_rlvect_1), [interesting(0.00)]). fof(t91_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k9_rlvect_1(A,k8_rlvect_1(A,k1_rlvect_1(A),k1_rlvect_1(A),B)) = B & k9_rlvect_1(A,k8_rlvect_1(A,k1_rlvect_1(A),B,k1_rlvect_1(A))) = B & k9_rlvect_1(A,k8_rlvect_1(A,B,k1_rlvect_1(A),k1_rlvect_1(A))) = B ) ) ) ), inference(mizar_proof,[status(thm)],[t63_rlvect_1,t10_rlvect_1,t10_rlvect_1,t63_rlvect_1,t10_rlvect_1,t10_rlvect_1,t63_rlvect_1,t10_rlvect_1,t10_rlvect_1]), [file(rlvect_1,t91_rlvect_1),interesting(0.00)]). fof(t92_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k9_rlvect_1(A,k8_rlvect_1(A,k1_rlvect_1(A),B,C)) = k2_rlvect_1(A,B,C) & k9_rlvect_1(A,k8_rlvect_1(A,B,C,k1_rlvect_1(A))) = k2_rlvect_1(A,B,C) & k9_rlvect_1(A,k8_rlvect_1(A,B,k1_rlvect_1(A),C)) = k2_rlvect_1(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t63_rlvect_1,t10_rlvect_1,t63_rlvect_1,t10_rlvect_1,t63_rlvect_1,t10_rlvect_1]), [file(rlvect_1,t92_rlvect_1),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(t96_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ( k3_finseq_1(B) = 2 & C = k1_funct_1(B,1) & D = k1_funct_1(B,2) ) => k9_rlvect_1(A,B) = k2_rlvect_1(A,C,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t61_finseq_1,t62_rlvect_1]), [file(rlvect_1,t96_rlvect_1),interesting(0.00)]). fof(t62_finseq_1,theorem,( ! [A,B,C,D] : ( ( v1_relat_1(D) & v1_funct_1(D) & v1_finseq_1(D) ) => ( D = k11_finseq_1(A,B,C) <=> ( k3_finseq_1(D) = 3 & k1_funct_1(D,1) = A & k1_funct_1(D,2) = B & k1_funct_1(D,3) = C ) ) ) ), file(finseq_1,t62_finseq_1), [interesting(0.00)]). fof(t97_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( k3_finseq_1(B) = 3 & C = k1_funct_1(B,1) & D = k1_funct_1(B,2) & E = k1_funct_1(B,3) ) => k9_rlvect_1(A,B) = k2_rlvect_1(A,k2_rlvect_1(A,C,D),E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t62_finseq_1,t63_rlvect_1]), [file(rlvect_1,t97_rlvect_1),interesting(0.00)]). fof(t9_rlvect_1,theorem,( $true ), file(rlvect_1,t9_rlvect_1), [interesting(0.00)]).