fof(t90_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v2_group_1(B) & v4_group_1(B) & v7_vectsp_1(B) & ~ v3_realset2(B) & l3_vectsp_1(B) ) => k2_group_1(k30_polynom1(A,B)) = k27_polynom1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d27_polynom1,l122_polynom1,d5_group_1]), [file(polynom1,t90_polynom1),interesting(1.00)]). fof(l122_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v2_group_1(B) & v4_group_1(B) & v7_vectsp_1(B) & ~ v3_realset2(B) & l3_vectsp_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(k30_polynom1(A,B))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k30_polynom1(A,B))) => ( D = k2_vectsp_1(k30_polynom1(A,B)) => ( k1_group_1(k30_polynom1(A,B),C,D) = C & k1_group_1(k30_polynom1(A,B),D,C) = C ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d27_polynom1,d27_polynom1,d27_polynom1,t88_polynom1,d27_polynom1,t89_polynom1]), [file(polynom1,l122_polynom1),interesting(0.88)]). fof(t88_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( ~ v3_struct_0(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v2_group_1(B) & v7_vectsp_1(B) & ~ v3_realset2(B) & l3_vectsp_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(C,k14_polynom1(A),u1_struct_0(B)) ) => k28_polynom1(A,B,C,k27_polynom1(A,B)) = C ) ) ) ), inference(mizar_proof,[status(thm)],[d26_polynom1,t25_finseq_1,t22_finseq_2,t58_rlvect_1,t25_finseq_1,t6_finseq_5,t75_polynom1,t2_group_7,t19_finseq_2,t59_finseq_1,d4_finseq_4,t61_rlvect_1,t84_polynom1,d5_group_1,t60_rlvect_1,d4_finseq_4,d7_finseq_1,t27_finseq_3,t31_finseq_3,t35_finseq_1,t56_finseq_1,t27_finseq_3,t38_nat_1,t27_finseq_3,d4_finseq_4,t76_polynom1,t84_polynom1,t36_vectsp_1,t75_polynom1,t2_group_7,t77_polynom1,t56_finseq_1,t25_finseq_1,t84_polynom1,t36_vectsp_1,t1_xreal_1,t15_matrlin,t10_rlvect_1,t113_funct_2]), [file(polynom1,t88_polynom1),interesting(0.81)]). fof(t89_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( ~ v3_struct_0(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v2_group_1(B) & v7_vectsp_1(B) & ~ v3_realset2(B) & l3_vectsp_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(C,k14_polynom1(A),u1_struct_0(B)) ) => k28_polynom1(A,B,k27_polynom1(A,B),C) = C ) ) ) ), inference(mizar_proof,[status(thm)],[d26_polynom1,t25_finseq_1,t25_finseq_1,t111_finseq_3,t58_rlvect_1,t25_finseq_1,t6_finseq_5,t75_polynom1,t2_group_7,d4_finseq_4,t61_rlvect_1,t84_polynom1,d5_group_1,t60_rlvect_1,d4_finseq_4,t112_finseq_3,t27_finseq_3,t38_nat_1,t31_finseq_3,t35_finseq_1,t56_finseq_1,t27_finseq_3,t8_xreal_1,t27_finseq_3,d4_finseq_4,t76_polynom1,t84_polynom1,t39_vectsp_1,t75_polynom1,t2_group_7,t77_polynom1,t56_finseq_1,t25_finseq_1,t84_polynom1,t39_vectsp_1,t1_xreal_1,t15_matrlin,t10_rlvect_1,t113_funct_2]), [file(polynom1,t89_polynom1),interesting(0.80)]). fof(t86_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v2_group_1(B) & v4_group_1(B) & v7_vectsp_1(B) & l3_vectsp_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(C,k14_polynom1(A),u1_struct_0(B)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(D,k14_polynom1(A),u1_struct_0(B)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(E,k14_polynom1(A),u1_struct_0(B)) ) => k28_polynom1(A,B,k28_polynom1(A,B,C,D),E) = k28_polynom1(A,B,C,k28_polynom1(A,B,D,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d26_polynom1,d26_polynom1,s1_finseq_5,s1_finseq_5,d3_tarski,d5_funct_1,d2_matrlin,t68_finseq_2,d3_finseq_1,d4_finseq_1,d3_finseq_1,d3_tarski,d5_funct_1,d5_funct_1,t70_finseq_2,d2_matrlin,d4_finseq_1,d11_finseq_1,d3_tarski,d5_funct_1,d2_matrlin,t68_finseq_2,d3_finseq_1,d4_finseq_1,d3_finseq_1,d3_tarski,d5_funct_1,d5_funct_1,t70_finseq_2,d2_matrlin,d4_finseq_1,d11_finseq_1,d4_finseq_1,s4_funct_2,d1_funct_2,t36_finseq_2,t36_polynom1,t34_polynom1,t15_polynom1,d24_pboole,t19_funcop_1,t31_finseq_3,t31_finseq_3,t27_finseq_3,d14_polynom1,d26_polynom1,t29_polynom1,t27_finseq_3,t61_finseq_1,t27_finseq_3,d4_finseq_4,t61_finseq_1,d4_finseq_4,t61_finseq_1,d2_matrlin,t68_finseq_2,d3_finseq_1,t27_finseq_3,d5_funct_1,d4_finseq_1,d3_finseq_1,d4_finseq_1,t46_relat_1,d3_finseq_1,d2_finseq_1,d3_polynom1,t31_finseq_3,t31_finseq_3,t31_finseq_3,t27_finseq_3,t70_finseq_2,d4_finseq_4,d2_matrlin,t60_finseq_1,d14_polynom1,t124_finseq_2,t27_finseq_3,d3_polynom1,t22_funct_1,t27_finseq_4,t27_finseq_4,t27_finseq_4,d3_polynom1,d4_finseq_4,t18_finseq_1,d4_finseq_4,d24_pboole,t13_funcop_1,d4_finseq_4,d4_finseq_4,d8_matrlin,t18_finseq_1,t36_polynom1,t34_polynom1,t15_polynom1,d24_pboole,t19_funcop_1,t31_finseq_3,t31_finseq_3,t27_finseq_3,d14_polynom1,d26_polynom1,t28_polynom1,t27_finseq_3,t61_finseq_1,t27_finseq_3,d4_finseq_4,t61_finseq_1,d4_finseq_4,t61_finseq_1,d2_matrlin,t68_finseq_2,d3_finseq_1,t27_finseq_3,d5_funct_1,d4_finseq_1,d3_finseq_1,d4_finseq_1,t46_relat_1,d3_finseq_1,d2_finseq_1,d2_polynom1,t31_finseq_3,t31_finseq_3,t31_finseq_3,t27_finseq_3,t70_finseq_2,d4_finseq_4,d2_matrlin,t60_finseq_1,d14_polynom1,t124_finseq_2,t27_finseq_3,t22_funct_1,t27_finseq_4,t27_finseq_4,t27_finseq_4,d4_group_1,d2_polynom1,d4_finseq_4,t18_finseq_1,d4_finseq_4,d24_pboole,t13_funcop_1,d4_finseq_4,d4_finseq_4,d8_matrlin,t18_finseq_1,t31_finseq_3,t78_polynom1,d4_finseq_1,t46_relat_1,t55_relat_1,t9_rlvect_2,t113_funct_2]), [file(polynom1,t86_polynom1),interesting(0.77)]). fof(t30_polynom1,theorem,( ! [A,B] : ( m2_finseq_1(B,k3_finseq_2(A)) => k3_finseq_1(k15_dtconstr(A,B)) = k9_wsierp_1(k5_polynom1(A,B)) ) ), inference(mizar_proof,[status(thm)],[t25_finseq_1,t102_rvsum_1,t14_scmfsa_7,t35_finseq_1,t13_dtconstr,t104_rvsum_1,t12_polynom1,t13_polynom1,s2_finseq_2]), [file(polynom1,t30_polynom1),interesting(0.73)]). fof(t36_polynom1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_1(C,k3_finseq_2(A)) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ? [E] : ( m2_finseq_1(E,k3_finseq_2(B)) & E = k13_pboole(C,k2_funcop_1(k4_finseq_1(C),D)) & k1_partfun1(k5_numbers,A,A,B,k15_dtconstr(A,C),D) = k15_dtconstr(B,E) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t35_polynom1,t36_finseq_2,t37_finseq_2,t31_finseq_3,d2_card_3,d24_pboole,t19_funcop_1,d2_card_3,d24_pboole,t13_funcop_1,t13_finseq_2,d11_finseq_1,d2_card_3,t37_finseq_2,d2_card_3,t9_funct_1,t31_polynom1,t31_finseq_3,t32_polynom1,d1_funct_2,t13_finseq_2,d11_finseq_1,d4_finseq_1,t46_relat_1,d24_pboole,t13_funcop_1,t13_finseq_2,d11_finseq_1,t37_finseq_2,t31_finseq_3,d15_finseq_1,t11_polynom1,t11_polynom1,d15_finseq_1,t33_polynom1,d24_pboole,t13_funcop_1,t22_funct_1,t22_funct_1,t17_finseq_1]), [file(polynom1,t36_polynom1),interesting(0.72)]). fof(t71_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => k20_polynom1(A,k16_polynom1(A)) = k13_binarith(k14_polynom1(A),k16_polynom1(A)) ) ), inference(mizar_proof,[status(thm)],[d18_polynom1,l85_polynom1,t134_orders_1,t37_zfmisc_1,d3_tarski,d14_polynom1,t62_polynom1,d1_tarski,d10_xboole_0,d2_triang_1,t7_polynom1,t79_card_1,t56_finseq_1]), [file(polynom1,t71_polynom1),interesting(0.71)]). fof(l84_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => r8_relat_2(k17_polynom1(A),k14_polynom1(A)) ) ), inference(mizar_proof,[status(thm)],[d8_relat_2,d14_polynom1,d16_polynom1,d14_polynom1,d16_polynom1,t46_polynom1,d16_polynom1]), [file(polynom1,l84_polynom1),interesting(0.70)]). fof(l85_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => r3_orders_1(k17_polynom1(A),k14_polynom1(A)) ) ), inference(mizar_proof,[status(thm)],[l82_polynom1,l83_polynom1,l84_polynom1,d6_relat_2,d14_polynom1,d16_polynom1,t49_polynom1,d16_polynom1,d8_orders_1]), [file(polynom1,l85_polynom1),interesting(0.70)]). fof(t77_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => k21_polynom1(A,k16_polynom1(A)) = k3_matrlin(k14_polynom1(A),k2_finseq_4(k14_polynom1(A),k16_polynom1(A),k16_polynom1(A))) ) ), inference(mizar_proof,[status(thm)],[t61_finseq_1,t110_finseq_2,d3_tarski,t56_finseq_1,d1_tarski,d4_finseq_1,t71_polynom1,t55_finseq_1,t55_finseq_1,t4_finseq_1,d1_tarski,t25_finseq_4,t25_finseq_4,t58_polynom1,d19_polynom1]), [file(polynom1,t77_polynom1),interesting(0.69)]). fof(t12_polynom1,theorem,( ! [A] : k1_card_3(k9_finseq_1(A)) = k9_finseq_1(k1_card_1(A)) ), inference(mizar_proof,[status(thm)],[t4_finseq_1,t55_finseq_1,d1_tarski,t57_finseq_1,d1_card_3,t4_finseq_1,t55_finseq_1,d1_tarski,t57_finseq_1,t57_finseq_1,d2_card_3]), [file(polynom1,t12_polynom1),interesting(0.66)]). fof(l83_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => r4_relat_2(k17_polynom1(A),k14_polynom1(A)) ) ), inference(mizar_proof,[status(thm)],[d4_relat_2,d14_polynom1,d16_polynom1,d14_polynom1,d16_polynom1,d12_polynom1]), [file(polynom1,l83_polynom1),interesting(0.66)]). fof(t41_polynom1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => r1_tarski(k11_polynom1(A),k1_relat_1(A)) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d7_polynom1,d4_funct_1]), [file(polynom1,t41_polynom1),interesting(0.65)]). fof(t34_polynom1,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,k3_finseq_2(u1_struct_0(A))) => k9_rlvect_1(A,k15_dtconstr(u1_struct_0(A),B)) = k9_rlvect_1(A,k8_matrlin(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t16_polynom1,t14_scmfsa_7,t13_dtconstr,t58_rlvect_1,t61_rlvect_1,t58_rlvect_1,t17_polynom1,t18_polynom1,s2_finseq_2]), [file(polynom1,t34_polynom1),interesting(0.65)]). fof(t56_polynom1,theorem,( ! [A,B] : k8_polynom1(k16_polynom1(A),B) = 0 ), inference(mizar_proof,[status(thm)],[t19_funcop_1,t13_funcop_1,d4_funct_1]), [file(polynom1,t56_polynom1),interesting(0.65)]). fof(t31_polynom1,theorem,( ! [A,B,C] : ( m2_finseq_1(C,k3_finseq_2(A)) => ! [D] : ( m2_finseq_1(D,k3_finseq_2(B)) => ( k5_polynom1(A,C) = k5_polynom1(B,D) => k3_finseq_1(k15_dtconstr(A,C)) = k3_finseq_1(k15_dtconstr(B,D)) ) ) ) ), inference(mizar_proof,[status(thm)],[t30_polynom1,t30_polynom1]), [file(polynom1,t31_polynom1),interesting(0.64)]). fof(t11_polynom1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : k1_card_3(k7_relat_1(A,B)) = k7_relat_1(k1_card_3(A),B) ) ), inference(mizar_proof,[status(thm)],[t90_relat_1,d2_card_3,t90_relat_1,t89_relat_1,t70_funct_1,d2_card_3,t70_funct_1,d2_card_3]), [file(polynom1,t11_polynom1),interesting(0.64)]). fof(l82_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => r1_relat_2(k17_polynom1(A),k14_polynom1(A)) ) ), inference(mizar_proof,[status(thm)],[d1_relat_2,d14_polynom1,d16_polynom1]), [file(polynom1,l82_polynom1),interesting(0.64)]). fof(t58_polynom1,theorem,( ! [A,B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => r6_pboole(A,k10_polynom1(A,B,k16_polynom1(A)),B) ) ), inference(mizar_proof,[status(thm)],[t13_funcop_1,d6_polynom1,t2_jordan3,t3_pboole]), [file(polynom1,t58_polynom1),interesting(0.64)]). fof(t60_polynom1,theorem,( ! [A,B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => r6_pboole(A,k10_polynom1(A,B,B),k16_polynom1(A)) ) ), inference(mizar_proof,[status(thm)],[d6_polynom1,t51_binarith,t56_polynom1,t3_pboole]), [file(polynom1,t60_polynom1),interesting(0.64)]). fof(t2_polynom1,theorem,( ! [A,B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(B,B),B) & m2_relset_1(C,k2_zfmisc_1(B,B),B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( m1_subset_1(E,B) => k1_relat_1(k4_funcop_1(C,D,E)) = A ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_funcop_1,t37_zfmisc_1,t1_xboole_1,t12_relset_1,t71_funct_3,t119_zfmisc_1,d1_funct_2,t1_xboole_1,t19_funcop_1,d4_funcop_1,t46_relat_1,t70_funct_3,d1_funct_2]), [file(polynom1,t2_polynom1),interesting(0.63)]). fof(t13_polynom1,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) ) => k1_card_3(k7_finseq_1(A,B)) = k7_finseq_1(k1_card_3(A),k1_card_3(B)) ) ) ), inference(mizar_proof,[status(thm)],[d2_card_3,d2_card_3,t31_finseq_3,t31_finseq_3,d7_finseq_1,d7_finseq_1,d7_finseq_1,t3_finseq_1,t27_finseq_3,d7_finseq_1,d2_card_3,d7_finseq_1,t27_finseq_3,t38_finseq_1,d7_finseq_1,d2_card_3,d7_finseq_1,d2_card_3]), [file(polynom1,t13_polynom1),interesting(0.63)]). fof(t29_polynom1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v2_group_1(A) & v7_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m2_finseq_1(C,u1_struct_0(A)) => k9_rlvect_1(A,k7_polynom1(A,C,B)) = k1_group_1(A,k9_rlvect_1(A,C),B) ) ) ) ), inference(mizar_proof,[status(thm)],[t60_rlvect_1,t20_polynom1,t39_vectsp_1,t24_polynom1,t58_rlvect_1,t22_polynom1,t61_rlvect_1,t61_rlvect_1,d18_vectsp_1,t58_rlvect_1,s2_finseq_2]), [file(polynom1,t29_polynom1),interesting(0.63)]). fof(t28_polynom1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v2_group_1(A) & v7_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m2_finseq_1(C,u1_struct_0(A)) => k9_rlvect_1(A,k6_polynom1(A,C,B)) = k1_group_1(A,B,k9_rlvect_1(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t60_rlvect_1,t19_polynom1,t36_vectsp_1,t23_polynom1,t58_rlvect_1,t21_polynom1,t61_rlvect_1,t61_rlvect_1,d18_vectsp_1,t58_rlvect_1,s2_finseq_2]), [file(polynom1,t28_polynom1),interesting(0.63)]). fof(t7_polynom1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v2_funct_1(A) ) => k1_card_1(A) = k1_card_1(k2_relat_1(A)) ) ), inference(mizar_proof,[status(thm)],[t80_card_2,t80_card_2,t55_funct_1,d10_xboole_0,t21_pre_circ]), [file(polynom1,t7_polynom1),interesting(0.63)]). fof(t65_polynom1,theorem,( ! [A,B] : ( ( v1_funct_1(B) & v1_funct_2(B,A,k5_numbers) & m2_relset_1(B,A,k5_numbers) ) => r2_hidden(B,k18_polynom1(A,B)) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,d3_pboole,d17_polynom1]), [file(polynom1,t65_polynom1),interesting(0.62)]). fof(t49_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ( r2_polynom1(A,B,C) | r2_polynom1(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_polynom1,t3_pboole,t23_ordinal1,s1_ordinal1,t7_ordinal1,d11_polynom1,t7_ordinal1,d11_polynom1,d12_polynom1,t1_xreal_1]), [file(polynom1,t49_polynom1),interesting(0.62)]). fof(t62_polynom1,theorem,( ! [A,B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ( r3_polynom1(A,B,k16_polynom1(A)) => r6_pboole(A,k16_polynom1(A),B) ) ) ), inference(mizar_proof,[status(thm)],[t56_polynom1,d13_polynom1,t3_pboole]), [file(polynom1,t62_polynom1),interesting(0.62)]). fof(t68_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ( r2_hidden(B,k4_finseq_1(k20_polynom1(A,C))) => r3_polynom1(A,k4_finseq_4(k5_numbers,k13_polynom1(A),k20_polynom1(A,C),B),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d18_polynom1,l85_polynom1,t134_orders_1,d4_finseq_4,d5_funct_1,d2_triang_1]), [file(polynom1,t68_polynom1),interesting(0.61)]). fof(t52_polynom1,theorem,( ! [A,B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => r6_pboole(A,k10_polynom1(A,k9_polynom1(A,C,B),B),C) ) ) ), inference(mizar_proof,[status(thm)],[d6_polynom1,d5_polynom1,t39_binarith,t3_pboole]), [file(polynom1,t52_polynom1),interesting(0.61)]). fof(t3_polynom1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k5_binarith(k5_binarith(A,B),C) = k5_binarith(A,k1_nat_1(B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t37_nat_1,t10_nat_2,t10_nat_2,t10_nat_2,t22_xreal_1,t50_binarith,t10_nat_2,t10_nat_2,t21_xreal_1,t50_binarith,t50_binarith,t50_binarith]), [file(polynom1,t3_polynom1),interesting(0.60)]). fof(t5_polynom1,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)) => ( k4_finseq_1(B) = k4_finseq_1(C) => k4_finseq_1(k3_fvsum_1(A,B,C)) = k4_finseq_1(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_finseq_1,d4_finseq_1,t71_funct_3,t119_zfmisc_1,d1_funct_2,t1_xboole_1,d3_fvsum_1,d3_funcop_1,t46_relat_1,d8_funct_3]), [file(polynom1,t5_polynom1),interesting(0.60)]). fof(t35_polynom1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_1(C,k3_finseq_2(A)) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => m2_finseq_1(k13_pboole(C,k2_funcop_1(k4_finseq_1(C),D)),k3_finseq_2(B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d24_pboole,t19_funcop_1,d3_finseq_1,d2_finseq_1,d3_tarski,d5_funct_1,d24_pboole,t13_funcop_1,t13_finseq_2,d11_finseq_1,t36_finseq_2,d11_finseq_1,d4_finseq_1]), [file(polynom1,t35_polynom1),interesting(0.60)]). fof(t46_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ! [D] : ( ( v7_seqm_3(D) & v1_polynom1(D) & m1_pboole(D,A) ) => ( ( r2_polynom1(A,B,C) & r2_polynom1(A,C,D) ) => r2_polynom1(A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_polynom1,t45_polynom1,d12_polynom1]), [file(polynom1,t46_polynom1),interesting(0.60)]). fof(t51_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ( r3_polynom1(A,B,C) => r6_pboole(A,k9_polynom1(A,k10_polynom1(A,C,B),B),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_ordinal1,d13_polynom1,d5_polynom1,d6_polynom1,t3_jordan4,t39_binarith,t3_pboole]), [file(polynom1,t51_polynom1),interesting(0.60)]). fof(t61_polynom1,theorem,( ! [A,B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ( ( r3_polynom1(A,B,C) & r6_pboole(A,k10_polynom1(A,C,B),k16_polynom1(A)) ) => r6_pboole(A,C,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_polynom1,t56_polynom1,d6_polynom1,t1_jordan4,t1_xreal_1,t3_pboole]), [file(polynom1,t61_polynom1),interesting(0.60)]). fof(t45_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ! [D] : ( ( v7_seqm_3(D) & v1_polynom1(D) & m1_pboole(D,A) ) => ( ( r1_polynom1(A,B,C) & r1_polynom1(A,C,D) ) => r1_polynom1(A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_polynom1,d11_polynom1,d11_polynom1,t17_xboole_1,d8_xboole_0,t21_ordinal1,t16_ordinal3,t17_xboole_1,t21_ordinal1,t16_ordinal3,t17_xboole_1,t2_xreal_1,t24_ordinal1]), [file(polynom1,t45_polynom1),interesting(0.59)]). fof(t4_polynom1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r1_tarski(k3_relat_1(B),A) => m2_relset_1(B,A,A) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d1_relset_1,d1_relat_1,t30_relat_1,d2_zfmisc_1]), [file(polynom1,t4_polynom1),interesting(0.59)]). fof(t39_polynom1,theorem,( ! [A,B] : ( ( v1_seq_1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v1_seq_1(C) & m1_pboole(C,A) ) => ! [D] : ( ( v1_seq_1(D) & m1_pboole(D,A) ) => r6_pboole(A,k9_polynom1(A,k9_polynom1(A,B,C),D),k9_polynom1(A,B,k9_polynom1(A,C,D))) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_polynom1,d5_polynom1,d5_polynom1,d5_polynom1,t3_pboole]), [file(polynom1,t39_polynom1),interesting(0.59)]). fof(t16_polynom1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_1(B,k3_finseq_2(u1_struct_0(A))) => k8_matrlin(A,k6_finseq_1(k3_finseq_2(u1_struct_0(A)))) = k6_finseq_1(u1_struct_0(A)) ) ) ), inference(mizar_proof,[status(thm)],[t15_polynom1,t26_finseq_1]), [file(polynom1,t16_polynom1),interesting(0.58)]). fof(t20_polynom1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k7_polynom1(A,k6_finseq_1(u1_struct_0(A)),B) = k6_finseq_1(u1_struct_0(A)) ) ) ), inference(mizar_proof,[status(thm)],[d3_polynom1,t64_relat_1]), [file(polynom1,t20_polynom1),interesting(0.58)]). fof(t19_polynom1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k6_polynom1(A,k6_finseq_1(u1_struct_0(A)),B) = k6_finseq_1(u1_struct_0(A)) ) ) ), inference(mizar_proof,[status(thm)],[d2_polynom1,t64_relat_1]), [file(polynom1,t19_polynom1),interesting(0.58)]). fof(t50_polynom1,theorem,( ! [A,B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ( ! [D] : ( r2_hidden(D,A) => r1_xreal_0(k8_polynom1(B,D),k8_polynom1(C,D)) ) => r3_polynom1(A,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_polynom1,d3_pboole,d4_funct_1]), [file(polynom1,t50_polynom1),interesting(0.58)]). fof(t54_polynom1,theorem,( ! [A,B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ! [D] : ( ( v7_seqm_3(D) & v1_polynom1(D) & m1_pboole(D,A) ) => ( r6_pboole(A,B,k9_polynom1(A,C,D)) => r3_polynom1(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_polynom1,t29_nat_1,t50_polynom1]), [file(polynom1,t54_polynom1),interesting(0.58)]). fof(t38_polynom1,theorem,( ! [A,B] : ( ( v7_seqm_3(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & m1_pboole(C,A) ) => ! [D] : ( ( v7_seqm_3(D) & m1_pboole(D,A) ) => ( ! [E] : ( r2_hidden(E,A) => k8_polynom1(B,E) = k5_binarith(k8_polynom1(C,E),k8_polynom1(D,E)) ) => r6_pboole(A,B,k10_polynom1(A,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_pboole,d3_pboole,d3_pboole,d4_funct_1,t51_binarith,d4_funct_1,d4_funct_1,d6_polynom1]), [file(polynom1,t38_polynom1),interesting(0.57)]). fof(l1_polynom1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => k2_binop_1(k5_numbers,k5_numbers,k5_numbers,k48_binop_2,A,B) = k2_nat_1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d24_binop_2]), [file(polynom1,l1_polynom1),interesting(0.57)]). fof(t17_polynom1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_2(B,u1_struct_0(A),k3_finseq_2(u1_struct_0(A))) => k13_binarith(u1_struct_0(A),k9_rlvect_1(A,B)) = k8_matrlin(A,k3_matrlin(u1_struct_0(A),B)) ) ) ), inference(mizar_proof,[status(thm)],[t55_finseq_1,t55_finseq_1,t31_finseq_3,t4_finseq_1,t55_finseq_1,d1_tarski,t25_finseq_4,t25_finseq_4,d8_matrlin]), [file(polynom1,t17_polynom1),interesting(0.57)]). fof(t22_polynom1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k7_polynom1(A,k13_binarith(u1_struct_0(A),C),B) = k13_binarith(u1_struct_0(A),k1_group_1(A,C,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t55_finseq_1,t55_finseq_1,t4_finseq_1,t55_finseq_1,d1_tarski,t25_finseq_4,t25_finseq_4,d3_polynom1]), [file(polynom1,t22_polynom1),interesting(0.57)]). fof(t21_polynom1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k6_polynom1(A,k13_binarith(u1_struct_0(A),C),B) = k13_binarith(u1_struct_0(A),k1_group_1(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t55_finseq_1,t55_finseq_1,t4_finseq_1,t55_finseq_1,d1_tarski,t25_finseq_4,t25_finseq_4,d2_polynom1]), [file(polynom1,t21_polynom1),interesting(0.57)]). fof(t63_polynom1,theorem,( ! [A,B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => r3_polynom1(A,k16_polynom1(A),B) ) ), inference(mizar_proof,[status(thm)],[d13_polynom1,t56_polynom1]), [file(polynom1,t63_polynom1),interesting(0.57)]). fof(t75_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ( k3_polynom1(k14_polynom1(A),k5_numbers,k4_finseq_2(2,k14_polynom1(A)),k21_polynom1(A,B),1) = k10_finseq_1(k16_polynom1(A),B) & k3_polynom1(k14_polynom1(A),k5_numbers,k4_finseq_2(2,k14_polynom1(A)),k21_polynom1(A,B),k3_finseq_1(k21_polynom1(A,B))) = k10_finseq_1(B,k16_polynom1(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d19_polynom1,t31_finseq_3,d14_polynom1,t69_polynom1,t6_finseq_5,d19_polynom1,t58_polynom1,d14_polynom1,t69_polynom1,t6_finseq_5,d19_polynom1,t60_polynom1]), [file(polynom1,t75_polynom1),interesting(0.57)]). fof(t53_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ( r3_polynom1(A,B,C) => r2_polynom1(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_polynom1,t23_ordinal1,d13_polynom1,t1_xreal_1,s1_ordinal1,t7_ordinal1,d13_polynom1,t1_xreal_1,d11_polynom1,t3_pboole]), [file(polynom1,t53_polynom1),interesting(0.56)]). fof(t55_polynom1,theorem,( k14_polynom1(k1_xboole_0) = k1_tarski(k1_xboole_0) ), inference(mizar_proof,[status(thm)],[d1_tarski,d3_pboole,t60_relat_1,d3_pboole,t64_relat_1,d1_tarski,d14_polynom1]), [file(polynom1,t55_polynom1),interesting(0.55)]). fof(t32_polynom1,theorem,( ! [A,B] : ( m2_finseq_1(B,k3_finseq_2(A)) => ! [C] : ~ ( r2_hidden(C,k4_finseq_1(k15_dtconstr(A,B))) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ~ ( r2_hidden(D,k4_finseq_1(B)) & r2_hidden(E,k4_finseq_1(k1_funct_1(B,D))) & C = k1_nat_1(k9_wsierp_1(k5_polynom1(A,k16_finseq_1(k3_finseq_2(A),B,k5_binarith(D,1)))),E) & k1_funct_1(k1_funct_1(B,D),E) = k1_funct_1(k15_dtconstr(A,B),C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_scmfsa_7,t13_dtconstr,t30_polynom1,t26_finseq_5,t39_binarith,t27_finseq_3,t27_finseq_3,t35_finseq_1,t56_finseq_1,t6_finseq_5,d7_finseq_1,t57_finseq_1,t29_nat_1,t27_finseq_3,t38_nat_1,t8_sprect_3,t27_finseq_3,t35_finseq_1,t6_sprect_3,t27_finseq_3,t53_binarith,d7_finseq_1,t39_finseq_1,d7_finseq_1,d7_finseq_1,t27_finseq_3,t52_binarith,t2_xreal_1,t25_finseq_5,d7_finseq_1,s2_finseq_2]), [file(polynom1,t32_polynom1),interesting(0.55)]). fof(t76_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ! [D] : ( ( v7_seqm_3(D) & v1_polynom1(D) & m1_pboole(D,A) ) => ! [E] : ( ( v7_seqm_3(E) & v1_polynom1(E) & m1_pboole(E,A) ) => ( k3_polynom1(k14_polynom1(A),k5_numbers,k4_finseq_2(2,k14_polynom1(A)),k21_polynom1(A,C),B) = k10_finseq_1(D,E) => ( r1_xreal_0(B,1) | r1_xreal_0(k3_finseq_1(k21_polynom1(A,C)),B) | ( D != k16_polynom1(A) & E != k16_polynom1(A) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d19_polynom1,t31_finseq_3,d14_polynom1,t27_finseq_3,d19_polynom1,t2_group_7,t70_polynom1,t68_polynom1,t61_polynom1,t70_polynom1]), [file(polynom1,t76_polynom1),interesting(0.55)]). fof(t57_polynom1,theorem,( ! [A,B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => r6_pboole(A,k9_polynom1(A,B,k16_polynom1(A)),B) ) ), inference(mizar_proof,[status(thm)],[t13_funcop_1,d5_polynom1,t3_pboole]), [file(polynom1,t57_polynom1),interesting(0.54)]). fof(t67_polynom1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,A,k5_numbers) & v1_polynom1(B) & m2_relset_1(B,A,k5_numbers) ) => k1_card_1(k18_polynom1(A,B)) = k7_setwiseo(A,k5_numbers,k48_binop_2,k19_polynom1(A,B),k7_funcop_1(k5_numbers,A,k47_binop_2,B,1)) ) ) ), inference(mizar_proof,[status(thm)],[t121_funct_2,d1_funct_2,t12_relset_1,d3_pboole,d17_polynom1,t113_funct_2,t65_polynom1,d1_tarski,t50_card_1,t20_card_2,t10_binop_2,t40_setwiseo,t2_polynom1,t35_funcop_1,d23_binop_2,d1_funct_2,t33_funct_7,d2_xboole_0,d1_tarski,t34_funct_7,t1_card_4,t4_scmfsa6a,t36_funcop_1,t9_setwop_2,t31_xreal_1,d2_ordinal1,t169_funct_2,t32_funct_7,d3_pboole,t33_funct_7,t1_euler_1,t38_nat_1,t34_funct_7,d3_pboole,d17_polynom1,t34_funct_7,d17_polynom1,s1_funct_7,d4_wellord2,d8_funct_1,t102_zfmisc_1,t106_zfmisc_1,t102_zfmisc_1,t106_zfmisc_1,t106_zfmisc_1,t106_zfmisc_1,t169_funct_2,t169_funct_2,d3_pboole,t33_funct_7,d17_polynom1,t34_funct_7,t34_funct_7,t33_funct_7,t33_funct_7,t3_pboole,d1_funct_2,t12_relset_1,d10_xboole_0,d3_tarski,t169_funct_2,d3_pboole,t32_funct_7,d3_pboole,t33_funct_7,t34_funct_7,d17_polynom1,t34_funct_7,d17_polynom1,d17_polynom1,t2_xreal_1,t1_euler_1,t106_zfmisc_1,t37_funct_7,t36_funct_7,d5_funct_1,t21_card_1,t65_card_2,d5_card_1,l1_polynom1,t4_setwop_2,s2_setwiseo,d7_polynom1]), [file(polynom1,t67_polynom1),interesting(0.54)]). fof(t15_polynom1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_1(B,k3_finseq_2(u1_struct_0(A))) => k4_finseq_1(k8_matrlin(A,B)) = k4_finseq_1(B) ) ) ), inference(mizar_proof,[status(thm)],[d8_matrlin,t31_finseq_3]), [file(polynom1,t15_polynom1),interesting(0.54)]). fof(t64_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => r2_polynom1(A,k16_polynom1(A),B) ) ) ), inference(mizar_proof,[status(thm)],[t63_polynom1,t53_polynom1]), [file(polynom1,t64_polynom1),interesting(0.54)]). fof(t70_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ! [D] : ( ( v7_seqm_3(D) & v1_polynom1(D) & m1_pboole(D,A) ) => ! [E] : ( ( v7_seqm_3(E) & v1_polynom1(E) & m1_pboole(E,A) ) => ~ ( ~ r1_xreal_0(B,1) & ~ r1_xreal_0(k3_finseq_1(k20_polynom1(A,C)),B) & ~ ( k4_finseq_4(k5_numbers,k13_polynom1(A),k20_polynom1(A,C),B) != k16_polynom1(A) & k4_finseq_4(k5_numbers,k13_polynom1(A),k20_polynom1(A,C),B) != C ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t69_polynom1,t6_finseq_5,t27_finseq_3,t17_partfun2]), [file(polynom1,t70_polynom1),interesting(0.53)]). fof(t59_polynom1,theorem,( ! [A,B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => r6_pboole(A,k10_polynom1(A,k16_polynom1(A),B),k16_polynom1(A)) ) ), inference(mizar_proof,[status(thm)],[t13_funcop_1,d6_polynom1,t10_nat_2,t3_pboole]), [file(polynom1,t59_polynom1),interesting(0.52)]). fof(t6_polynom1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C] : r1_tarski(k2_relat_1(k2_funct_7(A,B,C)),k2_xboole_0(k2_relat_1(A),k1_tarski(C))) ) ), inference(mizar_proof,[status(thm)],[d3_funct_7,t7_xboole_1,d3_funct_7,t18_funct_4,t5_cqc_lang]), [file(polynom1,t6_polynom1),interesting(0.52)]). fof(t72_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ~ ( r2_hidden(B,k4_finseq_1(k21_polynom1(A,C))) & ! [D] : ( ( v7_seqm_3(D) & v1_polynom1(D) & m1_pboole(D,A) ) => ! [E] : ( ( v7_seqm_3(E) & v1_polynom1(E) & m1_pboole(E,A) ) => ~ ( k3_polynom1(k14_polynom1(A),k5_numbers,k4_finseq_2(2,k14_polynom1(A)),k21_polynom1(A,C),B) = k10_finseq_1(D,E) & r6_pboole(A,C,k9_polynom1(A,D,E)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d19_polynom1,d14_polynom1,d19_polynom1,t68_polynom1,t51_polynom1]), [file(polynom1,t72_polynom1),interesting(0.52)]). fof(t73_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ! [D] : ( ( v7_seqm_3(D) & v1_polynom1(D) & m1_pboole(D,A) ) => ~ ( r6_pboole(A,B,k9_polynom1(A,C,D)) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ~ ( r2_hidden(E,k4_finseq_1(k21_polynom1(A,B))) & k3_polynom1(k14_polynom1(A),k5_numbers,k4_finseq_2(2,k14_polynom1(A)),k21_polynom1(A,B),E) = k10_finseq_1(C,D) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d18_polynom1,l85_polynom1,t134_orders_1,t54_polynom1,d2_triang_1,t4_partfun2,d19_polynom1,d19_polynom1,t52_polynom1]), [file(polynom1,t73_polynom1),interesting(0.52)]). fof(t10_polynom1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v1_card_3(A) <=> ! [B] : ( r2_hidden(B,k2_relat_1(A)) => v1_card_1(B) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_funct_1,d1_card_3,d1_card_3,d5_funct_1]), [file(polynom1,t10_polynom1),interesting(0.51)]). fof(t44_polynom1,theorem,( ! [A] : ( v7_seqm_3(k2_funcop_1(A,0)) & v1_polynom1(k2_funcop_1(A,0)) & m1_pboole(k2_funcop_1(A,0),A) ) ), inference(mizar_proof,[status(thm)],[t19_funcop_1,t19_funcop_1,t37_zfmisc_1,t1_xboole_1,d1_xboole_0,t41_polynom1,t13_funcop_1,d7_polynom1,d8_polynom1,d3_pboole,d8_seqm_3]), [file(polynom1,t44_polynom1),interesting(0.51)]). fof(t81_polynom1,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & l2_struct_0(B) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => k15_polynom1(A,B,k26_polynom1(A,B),C) = k1_rlvect_1(B) ) ) ), inference(mizar_proof,[status(thm)],[d14_polynom1,t13_funcop_1]), [file(polynom1,t81_polynom1),interesting(0.51)]). fof(t33_polynom1,theorem,( ! [A,B] : ( m2_finseq_1(B,k3_finseq_2(A)) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( ( r2_hidden(C,k4_finseq_1(B)) & r2_hidden(D,k4_finseq_1(k1_funct_1(B,C))) ) => ( r2_hidden(k1_nat_1(k9_wsierp_1(k5_polynom1(A,k16_finseq_1(k3_finseq_2(A),B,k5_binarith(C,1)))),D),k4_finseq_1(k15_dtconstr(A,B))) & k1_funct_1(k1_funct_1(B,C),D) = k1_funct_1(k15_dtconstr(A,B),k1_nat_1(k9_wsierp_1(k5_polynom1(A,k16_finseq_1(k3_finseq_2(A),B,k5_binarith(C,1)))),D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_scmfsa_7,t13_dtconstr,t35_finseq_1,t57_finseq_1,t27_finseq_3,t27_finseq_3,t38_nat_1,t1_xreal_1,t39_binarith,t6_finseq_5,d7_finseq_1,t57_finseq_1,t26_finseq_5,t30_polynom1,t41_finseq_1,d7_finseq_1,t27_finseq_3,t52_binarith,t2_xreal_1,t25_finseq_5,t39_finseq_1,d7_finseq_1,d7_finseq_1,d7_finseq_1,s2_finseq_2]), [file(polynom1,t33_polynom1),interesting(0.51)]). fof(t14_polynom1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v1_matrlin(A) <=> ! [B] : ( r2_hidden(B,k2_relat_1(A)) => ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_funct_1,d1_matrlin,d1_matrlin,d5_funct_1]), [file(polynom1,t14_polynom1),interesting(0.50)]). fof(t40_polynom1,theorem,( ! [A,B] : ( ( v7_seqm_3(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & m1_pboole(C,A) ) => ! [D] : ( ( v7_seqm_3(D) & m1_pboole(D,A) ) => r6_pboole(A,k10_polynom1(A,k10_polynom1(A,B,C),D),k10_polynom1(A,B,k9_polynom1(A,C,D))) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_polynom1,d6_polynom1,t3_polynom1,d5_polynom1,t38_polynom1]), [file(polynom1,t40_polynom1),interesting(0.50)]). fof(t66_polynom1,theorem,( ! [A,B] : ( ( v1_funct_1(B) & v1_funct_2(B,A,k5_numbers) & v1_polynom1(B) & m2_relset_1(B,A,k5_numbers) ) => r1_tarski(k18_polynom1(A,B),k14_polynom1(A)) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t169_funct_2,d3_pboole,d3_tarski,d7_polynom1,t41_polynom1,d17_polynom1,d7_polynom1,t13_finset_1,d8_polynom1,d3_pboole,d14_polynom1]), [file(polynom1,t66_polynom1),interesting(0.50)]). fof(t43_polynom1,theorem,( ! [A,B] : ( ( v7_seqm_3(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & m1_pboole(C,A) ) => r1_tarski(k11_polynom1(k10_polynom1(A,B,C)),k11_polynom1(B)) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d7_polynom1,t10_nat_2,d6_polynom1,d7_polynom1]), [file(polynom1,t43_polynom1),interesting(0.49)]). fof(t42_polynom1,theorem,( ! [A,B] : ( ( v7_seqm_3(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & m1_pboole(C,A) ) => k11_polynom1(k9_polynom1(A,B,C)) = k2_xboole_0(k11_polynom1(B),k11_polynom1(C)) ) ) ), inference(mizar_proof,[status(thm)],[d2_xboole_0,d7_polynom1,t23_nat_1,d5_polynom1,d2_xboole_0,d7_polynom1,d5_polynom1,d7_polynom1]), [file(polynom1,t42_polynom1),interesting(0.48)]). fof(t47_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ! [D] : ( ( v7_seqm_3(D) & v1_polynom1(D) & m1_pboole(D,A) ) => ( ( r1_polynom1(A,B,C) & r2_polynom1(A,C,D) ) => r1_polynom1(A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_polynom1,t45_polynom1]), [file(polynom1,t47_polynom1),interesting(0.48)]). fof(t48_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ! [D] : ( ( v7_seqm_3(D) & v1_polynom1(D) & m1_pboole(D,A) ) => ( ( r2_polynom1(A,B,C) & r1_polynom1(A,C,D) ) => r1_polynom1(A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_polynom1,t45_polynom1]), [file(polynom1,t48_polynom1),interesting(0.48)]). fof(t82_polynom1,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v5_rlvect_1(B) & l1_rlvect_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(C,k14_polynom1(A),u1_struct_0(B)) ) => k22_polynom1(A,B,C,k26_polynom1(A,B)) = C ) ) ), inference(mizar_proof,[status(thm)],[d21_polynom1,t81_polynom1,d7_rlvect_1,t113_funct_2]), [file(polynom1,t82_polynom1),interesting(0.47)]). fof(t91_polynom1,theorem,( ! [A,B] : ( ( v1_seq_1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v1_seq_1(C) & m1_pboole(C,A) ) => r1_tarski(k11_polynom1(k9_polynom1(A,B,C)),k2_xboole_0(k11_polynom1(B),k11_polynom1(C))) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d7_polynom1,d2_xboole_0,d7_polynom1,d5_polynom1]), [file(polynom1,t91_polynom1),interesting(0.47)]). fof(t27_polynom1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v2_group_1(A) & v4_vectsp_1(A) & l3_vectsp_1(A) ) => ( k1_rlvect_1(A) = k2_group_1(A) => v3_realset2(A) ) ) ), inference(mizar_proof,[status(thm)],[d8_anproj_1,d5_group_1,t36_vectsp_1]), [file(polynom1,t27_polynom1),interesting(0.45)]). fof(t37_polynom1,theorem,( ! [A,B] : ( ( v1_seq_1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v1_seq_1(C) & m1_pboole(C,A) ) => ! [D] : ( ( v1_seq_1(D) & m1_pboole(D,A) ) => ( ! [E] : ( r2_hidden(E,A) => k1_seq_1(B,E) = k9_binop_2(k1_seq_1(C,E),k1_seq_1(D,E)) ) => r6_pboole(A,B,k9_polynom1(A,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_pboole,d3_pboole,d3_pboole,d4_funct_1,d4_funct_1,d4_funct_1,d5_polynom1]), [file(polynom1,t37_polynom1),interesting(0.45)]). fof(t87_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( ~ v3_struct_0(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v2_group_1(B) & v7_vectsp_1(B) & l3_vectsp_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(C,k14_polynom1(A),u1_struct_0(B)) ) => k28_polynom1(A,B,C,k26_polynom1(A,B)) = k26_polynom1(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d26_polynom1,t81_polynom1,t36_vectsp_1,t15_matrlin,t81_polynom1,t113_funct_2]), [file(polynom1,t87_polynom1),interesting(0.40)]). fof(t85_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v4_group_1(B) & v7_vectsp_1(B) & l3_vectsp_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(C,k14_polynom1(A),u1_struct_0(B)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(D,k14_polynom1(A),u1_struct_0(B)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(E,k14_polynom1(A),u1_struct_0(B)) ) => k28_polynom1(A,B,C,k23_polynom1(A,B,D,E)) = k23_polynom1(A,B,k28_polynom1(A,B,C,D),k28_polynom1(A,B,C,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d26_polynom1,d26_polynom1,d26_polynom1,t110_finseq_2,t31_finseq_3,t5_polynom1,t31_finseq_3,t3_finseq_1,t27_finseq_3,t2_group_7,d4_finseq_4,d21_polynom1,d18_vectsp_1,t21_fvsum_1,t10_finseq_2,t95_fvsum_1,d21_polynom1,t113_funct_2]), [file(polynom1,t85_polynom1),interesting(0.35)]). 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(d1_card_3,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v1_card_3(A) <=> ! [B] : ( r2_hidden(B,k1_relat_1(A)) => v1_card_1(k1_funct_1(A,B)) ) ) ) ), file(card_3,d1_card_3), [interesting(0.00)]). fof(d1_matrlin,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v1_matrlin(A) <=> ! [B] : ( r2_hidden(B,k1_relat_1(A)) => ( v1_relat_1(k1_funct_1(A,B)) & v1_funct_1(k1_funct_1(A,B)) & v1_finseq_1(k1_funct_1(A,B)) ) ) ) ) ), file(matrlin,d1_matrlin), [interesting(0.00)]). fof(t1_polynom1,theorem,( $true ), file(polynom1,t1_polynom1), [interesting(0.00)]). fof(t25_polynom1,theorem,( $true ), file(polynom1,t25_polynom1), [interesting(0.00)]). fof(t26_polynom1,theorem,( $true ), file(polynom1,t26_polynom1), [interesting(0.00)]). fof(d8_anproj_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l2_struct_0(A) ) => ( v3_realset2(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => B = k1_rlvect_1(A) ) ) ) ), file(anproj_1,d8_anproj_1), [interesting(0.00)]). fof(d5_group_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ( v2_group_1(A) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( B = k2_group_1(A) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k1_group_1(A,C,B) = C & k1_group_1(A,B,C) = C ) ) ) ) ) ) ), file(group_1,d5_group_1), [interesting(0.00)]). fof(t36_vectsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k1_group_1(A,B,k1_rlvect_1(A)) = k1_rlvect_1(A) ) ) ), file(vectsp_1,t36_vectsp_1), [interesting(0.00)]). fof(d3_pboole,definition,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( m1_pboole(B,A) <=> k1_relat_1(B) = A ) ) ), file(pboole,d3_pboole), [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(d5_polynom1,definition,( ! [A,B] : ( ( v1_seq_1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v1_seq_1(C) & m1_pboole(C,A) ) => ! [D] : ( m1_pboole(D,A) => ( D = k9_polynom1(A,B,C) <=> ! [E] : k1_funct_1(D,E) = k9_binop_2(k1_seq_1(B,E),k1_seq_1(C,E)) ) ) ) ) ), file(polynom1,d5_polynom1), [interesting(0.00)]). fof(d6_polynom1,definition,( ! [A,B] : ( ( v7_seqm_3(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & m1_pboole(C,A) ) => ! [D] : ( m1_pboole(D,A) => ( D = k10_polynom1(A,B,C) <=> ! [E] : k1_funct_1(D,E) = k5_binarith(k8_polynom1(B,E),k8_polynom1(C,E)) ) ) ) ) ), file(polynom1,d6_polynom1), [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(t10_nat_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(B,A) => k5_binarith(B,A) = 0 ) ) ) ), file(nat_2,t10_nat_2), [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(t50_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(A,B) => k5_binarith(B,A) = k6_xcmplx_0(B,A) ) ) ) ), file(binarith,t50_binarith), [interesting(0.00)]). fof(t21_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(k2_xcmplx_0(A,B),C) <=> r1_xreal_0(A,k6_xcmplx_0(C,B)) ) ) ) ) ), file(xreal_1,t21_xreal_1), [interesting(0.00)]). fof(t51_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => k5_binarith(A,A) = 0 ) ), file(binarith,t51_binarith), [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(d7_polynom1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( B = k11_polynom1(A) <=> ! [C] : ( r2_hidden(C,B) <=> k1_funct_1(A,C) != 0 ) ) ) ), file(polynom1,d7_polynom1), [interesting(0.00)]). fof(t23_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( k2_xcmplx_0(A,B) = 0 => ( A = 0 & B = 0 ) ) ) ) ), file(nat_1,t23_nat_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(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(t37_zfmisc_1,theorem,( ! [A,B] : ( r1_tarski(k1_tarski(A),B) <=> r2_hidden(A,B) ) ), file(zfmisc_1,t37_zfmisc_1), [interesting(0.00)]). fof(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(d1_xboole_0,definition,( ! [A] : ( A = k1_xboole_0 <=> ! [B] : ~ r2_hidden(B,A) ) ), file(xboole_0,d1_xboole_0), [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(d8_polynom1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v1_polynom1(A) <=> v1_finset_1(k11_polynom1(A)) ) ) ), file(polynom1,d8_polynom1), [interesting(0.00)]). fof(d8_seqm_3,definition,( ! [A] : ( v1_relat_1(A) => ( v7_seqm_3(A) <=> r1_tarski(k2_relat_1(A),k5_numbers) ) ) ), file(seqm_3,d8_seqm_3), [interesting(0.00)]). fof(d12_polynom1,definition,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ( r2_polynom1(A,B,C) <=> ( r1_polynom1(A,B,C) | r6_pboole(A,B,C) ) ) ) ) ) ), file(polynom1,d12_polynom1), [interesting(0.00)]). fof(d11_polynom1,definition,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ( r1_polynom1(A,B,C) <=> ? [D] : ( v3_ordinal1(D) & ~ r1_xreal_0(k8_polynom1(C,D),k8_polynom1(B,D)) & ! [E] : ( v3_ordinal1(E) => ( r2_hidden(E,D) => k8_polynom1(B,E) = k8_polynom1(C,E) ) ) ) ) ) ) ) ), file(polynom1,d11_polynom1), [interesting(0.00)]). fof(t17_xboole_1,theorem,( ! [A,B] : r1_tarski(k3_xboole_0(A,B),A) ), file(xboole_1,t17_xboole_1), [interesting(0.00)]). fof(d8_xboole_0,definition,( ! [A,B] : ( r2_xboole_0(A,B) <=> ( r1_tarski(A,B) & A != B ) ) ), file(xboole_0,d8_xboole_0), [interesting(0.00)]). fof(t21_ordinal1,theorem,( ! [A] : ( v1_ordinal1(A) => ! [B] : ( v3_ordinal1(B) => ( r2_xboole_0(A,B) => r2_hidden(A,B) ) ) ) ), file(ordinal1,t21_ordinal1), [interesting(0.00)]). fof(t16_ordinal3,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( v3_ordinal1(B) => ( k3_xboole_0(A,B) = A | k3_xboole_0(A,B) = B ) ) ) ), file(ordinal3,t16_ordinal3), [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(t24_ordinal1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( v3_ordinal1(B) => ~ ( ~ r2_hidden(A,B) & A != B & ~ r2_hidden(B,A) ) ) ) ), file(ordinal1,t24_ordinal1), [interesting(0.00)]). fof(d1_relset_1,definition,( ! [A,B,C] : ( m1_relset_1(C,A,B) <=> r1_tarski(C,k2_zfmisc_1(A,B)) ) ), file(relset_1,d1_relset_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(t30_relat_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( r2_hidden(k4_tarski(A,B),C) => ( r2_hidden(A,k3_relat_1(C)) & r2_hidden(B,k3_relat_1(C)) ) ) ) ), file(relat_1,t30_relat_1), [interesting(0.00)]). fof(d2_zfmisc_1,definition,( ! [A,B,C] : ( C = k2_zfmisc_1(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ? [E,F] : ( r2_hidden(E,A) & r2_hidden(F,B) & D = k4_tarski(E,F) ) ) ) ), file(zfmisc_1,d2_zfmisc_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(t60_relat_1,theorem, ( k1_relat_1(k1_xboole_0) = k1_xboole_0 & k2_relat_1(k1_xboole_0) = k1_xboole_0 ), file(relat_1,t60_relat_1), [interesting(0.00)]). fof(t64_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ( ( k1_relat_1(A) = k1_xboole_0 | k2_relat_1(A) = k1_xboole_0 ) => A = k1_xboole_0 ) ) ), file(relat_1,t64_relat_1), [interesting(0.00)]). fof(d14_polynom1,definition,( ! [A,B] : ( B = k13_polynom1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) ) ) ), file(polynom1,d14_polynom1), [interesting(0.00)]). fof(t3_pboole,theorem,( ! [A,B] : ( m1_pboole(B,A) => ! [C] : ( m1_pboole(C,A) => ( ! [D] : ( r2_hidden(D,A) => k1_funct_1(B,D) = k1_funct_1(C,D) ) => B = C ) ) ) ), file(pboole,t3_pboole), [interesting(0.00)]). fof(t169_funct_2,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(C,k1_funct_2(A,B)) => ( k1_relat_1(C) = A & r1_tarski(k2_relat_1(C),B) ) ) ) ), file(funct_2,t169_funct_2), [interesting(0.00)]). fof(d17_polynom1,definition,( ! [A,B] : ( ( v1_funct_1(B) & v1_funct_2(B,A,k5_numbers) & m2_relset_1(B,A,k5_numbers) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_fraenkel(A,k5_numbers))) => ( C = k18_polynom1(A,B) <=> ! [D] : ( ( v7_seqm_3(D) & m1_pboole(D,A) ) => ( r2_hidden(D,C) <=> ! [E] : ( r2_hidden(E,A) => r1_xreal_0(k8_polynom1(D,E),k8_polynom1(B,E)) ) ) ) ) ) ) ), file(polynom1,d17_polynom1), [interesting(0.00)]). fof(t13_finset_1,theorem,( ! [A,B] : ( ( r1_tarski(A,B) & v1_finset_1(B) ) => v1_finset_1(A) ) ), file(finset_1,t13_finset_1), [interesting(0.00)]). fof(t121_funct_2,theorem,( ! [A,B,C] : ( r2_hidden(C,k1_funct_2(A,B)) => ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) ) ), file(funct_2,t121_funct_2), [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(t12_relset_1,theorem,( ! [A,B,C] : ( m2_relset_1(C,A,B) => ( r1_tarski(k1_relat_1(C),A) & r1_tarski(k2_relat_1(C),B) ) ) ), file(relset_1,t12_relset_1), [interesting(0.00)]). fof(t113_funct_2,theorem,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( ! [E] : ( m1_subset_1(E,A) => k1_funct_1(C,E) = k1_funct_1(D,E) ) => C = D ) ) ) ), file(funct_2,t113_funct_2), [interesting(0.00)]). fof(t50_card_1,theorem,( ! [A] : k1_card_1(k1_tarski(A)) = k4_ordinal2 ), file(card_1,t50_card_1), [interesting(0.00)]). fof(t20_card_2,theorem,( 1 = k4_ordinal2 ), file(card_2,t20_card_2), [interesting(0.00)]). fof(t10_binop_2,theorem,( k3_binop_1(k5_numbers,k48_binop_2) = 1 ), file(binop_2,t10_binop_2), [interesting(0.00)]). fof(t40_setwiseo,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [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) ) => ( ( v1_binop_1(C,A) & v2_binop_1(C,A) & v1_setwiseo(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,B,A) & m2_relset_1(D,B,A) ) => k7_setwiseo(B,A,C,k1_setwiseo(B),D) = k3_binop_1(A,C) ) ) ) ) ) ), file(setwiseo,t40_setwiseo), [interesting(0.00)]). fof(t71_funct_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => r1_tarski(k2_relat_1(k13_funct_3(A,B)),k2_zfmisc_1(k2_relat_1(A),k2_relat_1(B))) ) ) ), file(funct_3,t71_funct_3), [interesting(0.00)]). fof(t119_zfmisc_1,theorem,( ! [A,B,C,D] : ( ( r1_tarski(A,B) & r1_tarski(C,D) ) => r1_tarski(k2_zfmisc_1(A,C),k2_zfmisc_1(B,D)) ) ), file(zfmisc_1,t119_zfmisc_1), [interesting(0.00)]). fof(d4_funcop_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : k4_funcop_1(A,B,C) = k5_relat_1(k13_funct_3(B,k2_funcop_1(k1_relat_1(B),C)),A) ) ) ), file(funcop_1,d4_funcop_1), [interesting(0.00)]). fof(t46_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ( r1_tarski(k2_relat_1(A),k1_relat_1(B)) => k1_relat_1(k5_relat_1(A,B)) = k1_relat_1(A) ) ) ) ), file(relat_1,t46_relat_1), [interesting(0.00)]). fof(t70_funct_3,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( ( k1_relat_1(B) = A & k1_relat_1(C) = A ) => k1_relat_1(k13_funct_3(B,C)) = A ) ) ) ), file(funct_3,t70_funct_3), [interesting(0.00)]). fof(t35_funcop_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C,D] : ( r2_hidden(C,k1_relat_1(k4_funcop_1(B,A,D))) => k1_funct_1(k4_funcop_1(B,A,D),C) = k1_binop_1(B,k1_funct_1(A,C),D) ) ) ) ), file(funcop_1,t35_funcop_1), [interesting(0.00)]). fof(d23_binop_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(k5_numbers,k5_numbers),k5_numbers) & m2_relset_1(A,k2_zfmisc_1(k5_numbers,k5_numbers),k5_numbers) ) => ( A = k47_binop_2 <=> ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k2_binop_1(k5_numbers,k5_numbers,k5_numbers,A,B,C) = k23_binop_2(B,C) ) ) ) ) ), file(binop_2,d23_binop_2), [interesting(0.00)]). fof(t33_funct_7,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C] : ( r2_hidden(C,k1_relat_1(A)) => k1_funct_1(k2_funct_7(A,C,B),C) = B ) ) ), file(funct_7,t33_funct_7), [interesting(0.00)]). fof(t34_funct_7,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C,D] : ( C != D => k1_funct_1(k2_funct_7(A,C,B),D) = k1_funct_1(A,D) ) ) ), file(funct_7,t34_funct_7), [interesting(0.00)]). fof(t1_card_4,theorem,( ! [A] : ( v1_finset_1(A) <=> v1_finset_1(k1_card_1(A)) ) ), file(card_4,t1_card_4), [interesting(0.00)]). fof(t4_scmfsa6a,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C,D] : ( r2_hidden(B,D) | k7_relat_1(k2_funct_7(A,B,C),D) = k7_relat_1(A,D) ) ) ), file(scmfsa6a,t4_scmfsa6a), [interesting(0.00)]). fof(t36_funcop_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C,D] : ( ( v1_relat_1(D) & v1_funct_1(D) ) => ! [E] : ( k7_relat_1(A,C) = k7_relat_1(B,C) => k7_relat_1(k4_funcop_1(D,A,E),C) = k7_relat_1(k4_funcop_1(D,B,E),C) ) ) ) ) ), file(funcop_1,t36_funcop_1), [interesting(0.00)]). fof(t9_setwop_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,k5_finsub_1(A)) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(B,B),B) & m2_relset_1(D,k2_zfmisc_1(B,B),B) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,A,B) & m2_relset_1(F,A,B) ) => ( ( v1_binop_1(D,B) & v2_binop_1(D,B) & k2_partfun1(A,B,E,C) = k2_partfun1(A,B,F,C) ) => ( ( C = k1_xboole_0 & ~ v1_setwiseo(D,B) ) | k7_setwiseo(A,B,D,C,E) = k7_setwiseo(A,B,D,C,F) ) ) ) ) ) ) ) ) ), file(setwop_2,t9_setwop_2), [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(d2_ordinal1,definition,( ! [A] : ( v1_ordinal1(A) <=> ! [B] : ( r2_hidden(B,A) => r1_tarski(B,A) ) ) ), file(ordinal1,d2_ordinal1), [interesting(0.00)]). fof(t32_funct_7,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C] : k1_relat_1(k2_funct_7(A,C,B)) = k1_relat_1(A) ) ), file(funct_7,t32_funct_7), [interesting(0.00)]). fof(t1_euler_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r2_hidden(A,B) <=> ~ r1_xreal_0(B,A) ) ) ) ), file(euler_1,t1_euler_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(s1_funct_7,theorem, ( ! [A] : ( m1_subset_1(A,f1_s1_funct_7) => ! [B] : ( m1_subset_1(B,f2_s1_funct_7) => r2_hidden(f4_s1_funct_7(A,B),f3_s1_funct_7) ) ) => ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(f1_s1_funct_7,f2_s1_funct_7),f3_s1_funct_7) & m2_relset_1(A,k2_zfmisc_1(f1_s1_funct_7,f2_s1_funct_7),f3_s1_funct_7) & ! [B] : ( m1_subset_1(B,f1_s1_funct_7) => ! [C] : ( m1_subset_1(C,f2_s1_funct_7) => k8_funct_2(k2_zfmisc_1(f1_s1_funct_7,f2_s1_funct_7),f3_s1_funct_7,A,k1_domain_1(f1_s1_funct_7,f2_s1_funct_7,B,C)) = f4_s1_funct_7(B,C) ) ) ) ), file(funct_7,s1_funct_7), [interesting(0.00)]). fof(d4_wellord2,definition,( ! [A,B] : ( r2_wellord2(A,B) <=> ? [C] : ( v1_relat_1(C) & v1_funct_1(C) & v2_funct_1(C) & k1_relat_1(C) = A & k2_relat_1(C) = B ) ) ), file(wellord2,d4_wellord2), [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(t102_zfmisc_1,theorem,( ! [A,B,C] : ~ ( r2_hidden(A,k2_zfmisc_1(B,C)) & ! [D,E] : k4_tarski(D,E) != A ) ), file(zfmisc_1,t102_zfmisc_1), [interesting(0.00)]). fof(t106_zfmisc_1,theorem,( ! [A,B,C,D] : ( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) <=> ( r2_hidden(A,C) & r2_hidden(B,D) ) ) ), file(zfmisc_1,t106_zfmisc_1), [interesting(0.00)]). fof(d10_xboole_0,definition,( ! [A,B] : ( A = B <=> ( r1_tarski(A,B) & r1_tarski(B,A) ) ) ), file(xboole_0,d10_xboole_0), [interesting(0.00)]). fof(t37_funct_7,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : k2_funct_7(A,B,k1_funct_1(A,B)) = A ) ), file(funct_7,t37_funct_7), [interesting(0.00)]). fof(t36_funct_7,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C,D] : k2_funct_7(k2_funct_7(A,D,B),D,C) = k2_funct_7(A,D,C) ) ), file(funct_7,t36_funct_7), [interesting(0.00)]). fof(t21_card_1,theorem,( ! [A,B] : ( r2_wellord2(A,B) <=> k1_card_1(A) = k1_card_1(B) ) ), file(card_1,t21_card_1), [interesting(0.00)]). fof(t65_card_2,theorem,( ! [A] : ( v1_finset_1(A) => ! [B] : ( v1_finset_1(B) => k4_card_1(k2_zfmisc_1(A,B)) = k2_nat_1(k4_card_1(A),k4_card_1(B)) ) ) ), file(card_2,t65_card_2), [interesting(0.00)]). fof(d5_card_1,definition,( ! [A,B] : ( v1_card_1(B) => ( B = k1_card_1(A) <=> r2_wellord2(A,B) ) ) ), file(card_1,d5_card_1), [interesting(0.00)]). fof(d24_binop_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(k5_numbers,k5_numbers),k5_numbers) & m2_relset_1(A,k2_zfmisc_1(k5_numbers,k5_numbers),k5_numbers) ) => ( A = k48_binop_2 <=> ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k2_binop_1(k5_numbers,k5_numbers,k5_numbers,A,B,C) = k24_binop_2(B,C) ) ) ) ) ), file(binop_2,d24_binop_2), [interesting(0.00)]). fof(t4_setwop_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,k5_finsub_1(A)) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(B,B),B) & m2_relset_1(E,k2_zfmisc_1(B,B),B) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,A,B) & m2_relset_1(F,A,B) ) => ( ( v1_binop_1(E,B) & v2_binop_1(E,B) ) => ( ( D = k1_xboole_0 & ~ v1_setwiseo(E,B) ) | r2_hidden(C,D) | k7_setwiseo(A,B,E,k5_setwiseo(A,D,k2_setwiseo(A,C)),F) = k2_binop_1(B,B,B,E,k7_setwiseo(A,B,E,D,F),k8_funct_2(A,B,F,C)) ) ) ) ) ) ) ) ) ), file(setwop_2,t4_setwop_2), [interesting(0.00)]). fof(s2_setwiseo,theorem, ( ( p1_s2_setwiseo(k1_setwiseo(f1_s2_setwiseo)) & ! [A] : ( m1_subset_1(A,k5_finsub_1(f1_s2_setwiseo)) => ! [B] : ( m1_subset_1(B,f1_s2_setwiseo) => ( p1_s2_setwiseo(A) => ( r2_hidden(B,A) | p1_s2_setwiseo(k5_setwiseo(f1_s2_setwiseo,A,k2_setwiseo(f1_s2_setwiseo,B))) ) ) ) ) ) => ! [A] : ( m1_subset_1(A,k5_finsub_1(f1_s2_setwiseo)) => p1_s2_setwiseo(A) ) ), file(setwiseo,s2_setwiseo), [interesting(0.00)]). fof(d3_funct_7,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C] : ( ( r2_hidden(B,k1_relat_1(A)) => k2_funct_7(A,B,C) = k1_funct_4(A,k3_cqc_lang(B,C)) ) & ( ~ r2_hidden(B,k1_relat_1(A)) => k2_funct_7(A,B,C) = A ) ) ) ), file(funct_7,d3_funct_7), [interesting(0.00)]). fof(t7_xboole_1,theorem,( ! [A,B] : r1_tarski(A,k2_xboole_0(A,B)) ), file(xboole_1,t7_xboole_1), [interesting(0.00)]). fof(t18_funct_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => r1_tarski(k2_relat_1(k1_funct_4(A,B)),k2_xboole_0(k2_relat_1(A),k2_relat_1(B))) ) ) ), file(funct_4,t18_funct_4), [interesting(0.00)]). fof(t5_cqc_lang,theorem,( ! [A,B] : ( k1_relat_1(k3_cqc_lang(A,B)) = k1_tarski(A) & k2_relat_1(k3_cqc_lang(A,B)) = k1_tarski(B) ) ), file(cqc_lang,t5_cqc_lang), [interesting(0.00)]). fof(d19_polynom1,definition,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( m2_finseq_1(C,k4_finseq_2(2,k14_polynom1(A))) => ( C = k21_polynom1(A,B) <=> ( k4_finseq_1(C) = k4_finseq_1(k20_polynom1(A,B)) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( ( v7_seqm_3(E) & v1_polynom1(E) & m1_pboole(E,A) ) => ( ( r2_hidden(D,k4_finseq_1(C)) & E = k4_finseq_4(k5_numbers,k13_polynom1(A),k20_polynom1(A,B),D) ) => k3_polynom1(k14_polynom1(A),k5_numbers,k4_finseq_2(2,k14_polynom1(A)),C,D) = k10_finseq_1(E,k10_polynom1(A,B,E)) ) ) ) ) ) ) ) ) ), file(polynom1,d19_polynom1), [interesting(0.00)]). fof(t2_group_7,theorem,( ! [A,B,C,D] : ( k10_finseq_1(A,B) = k10_finseq_1(C,D) => ( A = C & B = D ) ) ), file(group_7,t2_group_7), [interesting(0.00)]). fof(t74_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ! [D] : ( ( v7_seqm_3(D) & v1_polynom1(D) & m1_pboole(D,A) ) => ! [E] : ( ( v7_seqm_3(E) & v1_polynom1(E) & m1_pboole(E,A) ) => ( ( r2_hidden(B,k4_finseq_1(k21_polynom1(A,C))) & k3_polynom1(k14_polynom1(A),k5_numbers,k4_finseq_2(2,k14_polynom1(A)),k21_polynom1(A,C),B) = k10_finseq_1(D,E) ) => D = k4_finseq_4(k5_numbers,k13_polynom1(A),k20_polynom1(A,C),B) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_polynom1,d19_polynom1,t2_group_7]), [file(polynom1,t74_polynom1),interesting(0.00)]). fof(d9_polynom1,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( l2_struct_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,u1_struct_0(B)) & m2_relset_1(C,A,u1_struct_0(B)) ) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(A)) => ( D = k12_polynom1(A,B,C) <=> ! [E] : ( m1_subset_1(E,A) => ( r2_hidden(E,D) <=> k8_funct_2(A,u1_struct_0(B),C,E) != k1_rlvect_1(B) ) ) ) ) ) ) ) ), file(polynom1,d9_polynom1), [interesting(0.00)]). fof(d21_polynom1,definition,( ! [A,B] : ( ( ~ v3_struct_0(B) & l1_rlvect_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(C,k14_polynom1(A),u1_struct_0(B)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(D,k14_polynom1(A),u1_struct_0(B)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(E,k14_polynom1(A),u1_struct_0(B)) ) => ( E = k22_polynom1(A,B,C,D) <=> ! [F] : ( ( v7_seqm_3(F) & v1_polynom1(F) & m1_pboole(F,A) ) => k15_polynom1(A,B,E,F) = k2_rlvect_1(B,k15_polynom1(A,B,C,F),k15_polynom1(A,B,D,F)) ) ) ) ) ) ) ), file(polynom1,d21_polynom1), [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(t79_polynom1,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v5_rlvect_1(B) & l1_rlvect_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(C,k14_polynom1(A),u1_struct_0(B)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(D,k14_polynom1(A),u1_struct_0(B)) ) => r1_tarski(k12_polynom1(k14_polynom1(A),B,k22_polynom1(A,B,C,D)),k4_subset_1(k14_polynom1(A),k12_polynom1(k14_polynom1(A),B,C),k12_polynom1(k14_polynom1(A),B,D))) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d9_polynom1,d21_polynom1,d7_rlvect_1,d9_polynom1,d2_xboole_0]), [file(polynom1,t79_polynom1),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(t80_polynom1,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & l3_vectsp_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(C,k14_polynom1(A),u1_struct_0(B)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(D,k14_polynom1(A),u1_struct_0(B)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(E,k14_polynom1(A),u1_struct_0(B)) ) => k22_polynom1(A,B,k22_polynom1(A,B,C,D),E) = k22_polynom1(A,B,C,k22_polynom1(A,B,D,E)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d21_polynom1,d21_polynom1,d6_rlvect_1,d21_polynom1,d21_polynom1,t113_funct_2]), [file(polynom1,t80_polynom1),interesting(0.00)]). fof(d22_polynom1,definition,( ! [A,B] : ( ( ~ v3_struct_0(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & l1_rlvect_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(C,k14_polynom1(A),u1_struct_0(B)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(D,k14_polynom1(A),u1_struct_0(B)) ) => ( D = k24_polynom1(A,B,C) <=> ! [E] : ( ( v7_seqm_3(E) & v1_polynom1(E) & m1_pboole(E,A) ) => k15_polynom1(A,B,D,E) = k5_rlvect_1(B,k15_polynom1(A,B,C,E)) ) ) ) ) ) ), file(polynom1,d22_polynom1), [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(t83_polynom1,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & l1_rlvect_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(C,k14_polynom1(A),u1_struct_0(B)) ) => k25_polynom1(A,B,C,C) = k26_polynom1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d21_polynom1,d22_polynom1,d10_rlvect_1,t81_polynom1,t113_funct_2]), [file(polynom1,t83_polynom1),interesting(0.00)]). fof(d26_polynom1,definition,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( ~ v3_struct_0(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & l3_vectsp_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(C,k14_polynom1(A),u1_struct_0(B)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(D,k14_polynom1(A),u1_struct_0(B)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k14_polynom1(A),u1_struct_0(B)) & m2_relset_1(E,k14_polynom1(A),u1_struct_0(B)) ) => ( E = k28_polynom1(A,B,C,D) <=> ! [F] : ( ( v7_seqm_3(F) & v1_polynom1(F) & m1_pboole(F,A) ) => ? [G] : ( m2_finseq_1(G,u1_struct_0(B)) & k15_polynom1(A,B,E,F) = k9_rlvect_1(B,G) & k3_finseq_1(G) = k3_finseq_1(k21_polynom1(A,F)) & ! [H] : ( m2_subset_1(H,k1_numbers,k5_numbers) => ~ ( r2_hidden(H,k4_finseq_1(G)) & ! [I] : ( ( v7_seqm_3(I) & v1_polynom1(I) & m1_pboole(I,A) ) => ! [J] : ( ( v7_seqm_3(J) & v1_polynom1(J) & m1_pboole(J,A) ) => ~ ( k3_polynom1(k14_polynom1(A),k5_numbers,k4_finseq_2(2,k14_polynom1(A)),k21_polynom1(A,F),H) = k10_finseq_1(I,J) & k4_finseq_4(k5_numbers,u1_struct_0(B),G,H) = k1_group_1(B,k15_polynom1(A,B,C,I),k15_polynom1(A,B,D,J)) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(polynom1,d26_polynom1), [interesting(0.00)]). fof(t110_finseq_2,theorem,( ! [A,B] : ( m2_finseq_1(B,A) => m1_subset_1(B,k4_finseq_2(k3_finseq_1(B),A)) ) ), file(finseq_2,t110_finseq_2), [interesting(0.00)]). fof(t31_finseq_3,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(A) = k3_finseq_1(B) <=> k4_finseq_1(A) = k4_finseq_1(B) ) ) ) ), file(finseq_3,t31_finseq_3), [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(d3_fvsum_1,definition,( ! [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)) => k3_fvsum_1(A,B,C) = k1_finseqop(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),u1_rlvect_1(A),B,C) ) ) ) ), file(fvsum_1,d3_fvsum_1), [interesting(0.00)]). fof(d3_funcop_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => k3_funcop_1(A,B,C) = k5_relat_1(k13_funct_3(B,C),A) ) ) ) ), file(funcop_1,d3_funcop_1), [interesting(0.00)]). fof(d8_funct_3,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k13_funct_3(A,B) <=> ( k1_relat_1(C) = k3_xboole_0(k1_relat_1(A),k1_relat_1(B)) & ! [D] : ( r2_hidden(D,k1_relat_1(C)) => k1_funct_1(C,D) = k4_tarski(k1_funct_1(A,D),k1_funct_1(B,D)) ) ) ) ) ) ) ), file(funct_3,d8_funct_3), [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(t27_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( v4_ordinal2(B) => ( r2_hidden(B,k4_finseq_1(A)) <=> ( r1_xreal_0(1,B) & r1_xreal_0(B,k3_finseq_1(A)) ) ) ) ) ), file(finseq_3,t27_finseq_3), [interesting(0.00)]). fof(d4_finseq_4,definition,( ! [A,B,C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,B) ) => ! [D] : ( r2_hidden(D,k1_relat_1(C)) => k4_finseq_4(A,B,C,D) = k1_funct_1(C,D) ) ) ), file(finseq_4,d4_finseq_4), [interesting(0.00)]). fof(d18_vectsp_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l3_vectsp_1(A) ) => ( v7_vectsp_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)) => ( k1_group_1(A,B,k2_rlvect_1(A,C,D)) = k2_rlvect_1(A,k1_group_1(A,B,C),k1_group_1(A,B,D)) & k1_group_1(A,k2_rlvect_1(A,C,D),B) = k2_rlvect_1(A,k1_group_1(A,C,B),k1_group_1(A,D,B)) ) ) ) ) ) ) ), file(vectsp_1,d18_vectsp_1), [interesting(0.00)]). fof(t21_fvsum_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)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ( ( r2_hidden(F,k3_setwop_2(k3_fvsum_1(A,B,C))) & D = k1_funct_1(B,F) & E = k1_funct_1(C,F) ) => k1_funct_1(k3_fvsum_1(A,B,C),F) = k2_rlvect_1(A,D,E) ) ) ) ) ) ) ) ), file(fvsum_1,t21_fvsum_1), [interesting(0.00)]). fof(t10_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [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) ) => ( ( k3_finseq_1(B) = A & k3_finseq_1(C) = A & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k2_finseq_1(A)) => k1_funct_1(B,D) = k1_funct_1(C,D) ) ) ) => B = C ) ) ) ) ), file(finseq_2,t10_finseq_2), [interesting(0.00)]). fof(t95_fvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & l1_rlvect_1(B) ) => ! [C] : ( m2_finseq_2(C,u1_struct_0(B),k4_finseq_2(A,u1_struct_0(B))) => ! [D] : ( m2_finseq_2(D,u1_struct_0(B),k4_finseq_2(A,u1_struct_0(B))) => k9_rlvect_1(B,k4_fvsum_1(A,B,C,D)) = k4_rlvect_1(B,k9_rlvect_1(B,C),k9_rlvect_1(B,D)) ) ) ) ) ), file(fvsum_1,t95_fvsum_1), [interesting(0.00)]). fof(s1_finseq_5,theorem,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) & k3_finseq_1(A) = f1_s1_finseq_5 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r2_hidden(B,k4_finseq_1(A)) => k1_funct_1(A,B) = f2_s1_finseq_5(B) ) ) ) ), file(finseq_5,s1_finseq_5), [interesting(0.00)]). fof(d2_matrlin,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_matrlin(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_matrlin(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_matrlin(C) ) => ( C = k4_matrlin(A,B) <=> ( k1_relat_1(C) = k3_xboole_0(k1_relat_1(A),k1_relat_1(B)) & ! [D] : ( r2_hidden(D,k1_relat_1(C)) => ! [E] : ( ( v1_relat_1(E) & v1_funct_1(E) & v1_finseq_1(E) ) => ! [F] : ( ( v1_relat_1(F) & v1_funct_1(F) & v1_finseq_1(F) ) => ( ( E = k1_funct_1(A,D) & F = k1_funct_1(B,D) ) => k1_funct_1(C,D) = k7_finseq_1(E,F) ) ) ) ) ) ) ) ) ) ), file(matrlin,d2_matrlin), [interesting(0.00)]). fof(t68_finseq_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : k4_finseq_1(k2_finseq_2(A,B)) = k2_finseq_1(A) ) ), file(finseq_2,t68_finseq_2), [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(t70_finseq_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B,C] : ( r2_hidden(B,k2_finseq_1(A)) => k1_funct_1(k2_finseq_2(A,C),B) = C ) ) ), file(finseq_2,t70_finseq_2), [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(s4_funct_2,theorem,( ? [A] : ( v1_funct_1(A) & v1_funct_2(A,f1_s4_funct_2,f2_s4_funct_2) & m2_relset_1(A,f1_s4_funct_2,f2_s4_funct_2) & ! [B] : ( m1_subset_1(B,f1_s4_funct_2) => k8_funct_2(f1_s4_funct_2,f2_s4_funct_2,A,B) = f3_s4_funct_2(B) ) ) ), file(funct_2,s4_funct_2), [interesting(0.00)]). fof(t36_finseq_2,theorem,( ! [A,B,C] : ( m2_finseq_1(C,A) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => m2_finseq_1(k1_partfun1(k5_numbers,A,A,B,C,D),B) ) ) ), file(finseq_2,t36_finseq_2), [interesting(0.00)]). fof(d24_pboole,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_funcop_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_funcop_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_funcop_1(C) ) => ( C = k13_pboole(A,B) <=> ( k1_relat_1(C) = k3_xboole_0(k1_relat_1(A),k1_relat_1(B)) & ! [D] : ( r2_hidden(D,k1_relat_1(C)) => k1_funct_1(C,D) = k5_relat_1(k1_funct_1(A,D),k1_funct_1(B,D)) ) ) ) ) ) ) ), file(pboole,d24_pboole), [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(t13_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B,C] : ( m2_finseq_1(C,B) => ( r2_hidden(A,k4_finseq_1(C)) => r2_hidden(k1_funct_1(C,A),B) ) ) ) ), file(finseq_2,t13_finseq_2), [interesting(0.00)]). fof(t37_finseq_2,theorem,( ! [A,B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ! [D] : ( m2_finseq_1(D,A) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => ( C = k1_partfun1(k5_numbers,A,A,B,D,E) => k3_finseq_1(C) = k3_finseq_1(D) ) ) ) ) ) ), file(finseq_2,t37_finseq_2), [interesting(0.00)]). fof(d2_card_3,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_card_3(B) ) => ( B = k1_card_3(A) <=> ( k1_relat_1(B) = k1_relat_1(A) & ! [C] : ( r2_hidden(C,k1_relat_1(A)) => k1_funct_1(B,C) = k1_card_1(k1_funct_1(A,C)) ) ) ) ) ) ), file(card_3,d2_card_3), [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(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(t102_rvsum_1,theorem,( k15_rvsum_1(k6_finseq_1(k1_numbers)) = 0 ), file(rvsum_1,t102_rvsum_1), [interesting(0.00)]). fof(t14_scmfsa_7,theorem,( ! [A,B] : ( m2_finseq_1(B,k13_finseq_1(A)) => ! [C] : ( m2_finseq_1(C,k13_finseq_1(A)) => k15_dtconstr(A,k8_finseq_1(k13_finseq_1(A),B,C)) = k8_finseq_1(A,k15_dtconstr(A,B),k15_dtconstr(A,C)) ) ) ), file(scmfsa_7,t14_scmfsa_7), [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(t13_dtconstr,theorem,( ! [A,B] : ( m2_finseq_2(B,A,k3_finseq_2(A)) => k15_dtconstr(A,k3_lang1(k3_finseq_2(A),B)) = B ) ), file(dtconstr,t13_dtconstr), [interesting(0.00)]). fof(t104_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k15_rvsum_1(k8_finseq_1(k1_numbers,B,k12_finseq_1(k1_numbers,A))) = k9_binop_2(k15_rvsum_1(B),A) ) ) ), file(rvsum_1,t104_rvsum_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(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(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(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(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(s2_finseq_2,theorem, ( ( p1_s2_finseq_2(k6_finseq_1(f1_s2_finseq_2)) & ! [A] : ( m2_finseq_1(A,f1_s2_finseq_2) => ! [B] : ( m1_subset_1(B,f1_s2_finseq_2) => ( p1_s2_finseq_2(A) => p1_s2_finseq_2(k8_finseq_1(f1_s2_finseq_2,A,k12_finseq_1(f1_s2_finseq_2,B))) ) ) ) ) => ! [A] : ( m2_finseq_1(A,f1_s2_finseq_2) => p1_s2_finseq_2(A) ) ), file(finseq_2,s2_finseq_2), [interesting(0.00)]). fof(t26_finseq_5,theorem,( ! [A,B] : ( m2_finseq_1(B,A) => ! [C] : ( m2_finseq_1(C,A) => k16_finseq_1(A,k8_finseq_1(A,B,C),k3_finseq_1(B)) = B ) ) ), file(finseq_5,t26_finseq_5), [interesting(0.00)]). fof(t39_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => k5_binarith(k2_xcmplx_0(A,B),B) = A ) ) ), file(binarith,t39_binarith), [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(t6_finseq_5,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( r2_hidden(1,k4_finseq_1(A)) & r2_hidden(k3_finseq_1(A),k4_finseq_1(A)) ) ) ), file(finseq_5,t6_finseq_5), [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(t8_sprect_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(k1_nat_1(A,B),C) => r1_xreal_0(B,k5_binarith(C,A)) ) ) ) ) ), file(sprect_3,t8_sprect_3), [interesting(0.00)]). fof(t6_sprect_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(A,k1_nat_1(B,C)) => r1_xreal_0(k5_binarith(A,C),B) ) ) ) ) ), file(sprect_3,t6_sprect_3), [interesting(0.00)]). fof(t53_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(B,A) => k2_xcmplx_0(k5_binarith(A,B),B) = A ) ) ) ), file(binarith,t53_binarith), [interesting(0.00)]). fof(t39_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) ) => r1_tarski(k4_finseq_1(A),k4_finseq_1(k7_finseq_1(A,B))) ) ) ), file(finseq_1,t39_finseq_1), [interesting(0.00)]). fof(t52_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => r1_xreal_0(k5_binarith(A,B),A) ) ) ), file(binarith,t52_binarith), [interesting(0.00)]). fof(t25_finseq_5,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B,C] : ( m2_finseq_1(C,B) => ! [D] : ( m2_finseq_1(D,B) => ( r1_xreal_0(A,k3_finseq_1(C)) => k16_finseq_1(B,k8_finseq_1(B,C,D),A) = k16_finseq_1(B,C,A) ) ) ) ) ), file(finseq_5,t25_finseq_5), [interesting(0.00)]). fof(d15_finseq_1,definition,( ! [A,B] : ( m2_finseq_1(B,A) => ! [C] : ( v4_ordinal2(C) => k16_finseq_1(A,B,C) = k7_relat_1(B,k2_finseq_1(C)) ) ) ), file(finseq_1,d15_finseq_1), [interesting(0.00)]). fof(t90_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => k1_relat_1(k7_relat_1(B,A)) = k3_xboole_0(k1_relat_1(B),A) ) ), file(relat_1,t90_relat_1), [interesting(0.00)]). fof(t89_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => r1_tarski(k1_relat_1(k7_relat_1(B,A)),k1_relat_1(B)) ) ), file(relat_1,t89_relat_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(t1_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,A) ) => A = B ) ) ) ), file(xreal_1,t1_xreal_1), [interesting(0.00)]). fof(t41_finseq_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [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) ) => ( r2_hidden(A,k4_finseq_1(B)) => r2_hidden(k1_nat_1(k3_finseq_1(C),A),k4_finseq_1(k7_finseq_1(C,B))) ) ) ) ) ), file(finseq_1,t41_finseq_1), [interesting(0.00)]). fof(t22_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(A,k1_relat_1(k5_relat_1(C,B))) => k1_funct_1(k5_relat_1(C,B),A) = k1_funct_1(B,k1_funct_1(C,A)) ) ) ) ), file(funct_1,t22_funct_1), [interesting(0.00)]). fof(t17_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( ( k4_finseq_1(A) = k4_finseq_1(B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r2_hidden(C,k4_finseq_1(A)) => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) ) => A = B ) ) ) ), file(finseq_1,t17_finseq_1), [interesting(0.00)]). fof(d8_matrlin,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_1(B,k3_finseq_2(u1_struct_0(A))) => ! [C] : ( m2_finseq_1(C,u1_struct_0(A)) => ( C = k8_matrlin(A,B) <=> ( k3_finseq_1(C) = k3_finseq_1(B) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k1_relat_1(C)) => k4_finseq_4(k5_numbers,u1_struct_0(A),C,D) = k9_rlvect_1(A,k1_matrlin(u1_struct_0(A),k5_numbers,k3_finseq_2(u1_struct_0(A)),B,D)) ) ) ) ) ) ) ) ), file(matrlin,d8_matrlin), [interesting(0.00)]). fof(t26_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( A = k1_xboole_0 <=> k4_finseq_1(A) = k1_xboole_0 ) ) ), file(finseq_1,t26_finseq_1), [interesting(0.00)]). fof(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)) ) ) ) ), file(rlvect_1,t58_rlvect_1), [interesting(0.00)]). 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 ) ) ), file(rlvect_1,t61_rlvect_1), [interesting(0.00)]). fof(t25_finseq_4,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => k4_finseq_4(k5_numbers,A,k12_finseq_1(A,B),1) = B ) ) ), file(finseq_4,t25_finseq_4), [interesting(0.00)]). fof(t83_finseq_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_1(C,B) => ! [D] : ( m2_finseq_1(D,B) => ( r2_hidden(A,k4_finseq_1(C)) => k4_finseq_4(k5_numbers,B,k8_finseq_1(B,C,D),A) = k4_finseq_4(k5_numbers,B,C,A) ) ) ) ) ) ), file(finseq_4,t83_finseq_4), [interesting(0.00)]). fof(t84_finseq_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_1(C,B) => ! [D] : ( m2_finseq_1(D,B) => ( r2_hidden(A,k4_finseq_1(D)) => k4_finseq_4(k5_numbers,B,k8_finseq_1(B,C,D),k1_nat_1(k3_finseq_1(C),A)) = k4_finseq_4(k5_numbers,B,D,A) ) ) ) ) ) ), file(finseq_4,t84_finseq_4), [interesting(0.00)]). fof(t18_polynom1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m2_finseq_1(B,k3_finseq_2(u1_struct_0(A))) => ! [C] : ( m2_finseq_1(C,k3_finseq_2(u1_struct_0(A))) => k8_matrlin(A,k8_finseq_1(k3_finseq_2(u1_struct_0(A)),B,C)) = k8_finseq_1(u1_struct_0(A),k8_matrlin(A,B),k8_matrlin(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t15_polynom1,t15_polynom1,t31_finseq_3,t35_finseq_1,t31_finseq_3,t31_finseq_3,t35_finseq_1,t31_finseq_3,d4_finseq_4,d7_finseq_1,d4_finseq_4,d8_matrlin,t83_finseq_4,d4_finseq_4,d7_finseq_1,d4_finseq_4,d8_matrlin,t84_finseq_4,t38_finseq_1,d8_matrlin]), [file(polynom1,t18_polynom1),interesting(0.00)]). 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) ) ), file(rlvect_1,t60_rlvect_1), [interesting(0.00)]). fof(d3_polynom1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m2_finseq_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m2_finseq_1(D,u1_struct_0(A)) => ( D = k7_polynom1(A,B,C) <=> ( k4_finseq_1(D) = k4_finseq_1(B) & ! [E] : ( r2_hidden(E,k4_finseq_1(B)) => k4_finseq_4(k5_numbers,u1_struct_0(A),D,E) = k1_group_1(A,k4_finseq_4(k5_numbers,u1_struct_0(A),B,E),C) ) ) ) ) ) ) ) ), file(polynom1,d3_polynom1), [interesting(0.00)]). fof(t39_vectsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v5_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k1_group_1(A,k1_rlvect_1(A),B) = k1_rlvect_1(A) ) ) ), file(vectsp_1,t39_vectsp_1), [interesting(0.00)]). fof(t13_finseq_5,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,A) => ! [C] : ( m2_finseq_1(C,A) => ( ( k4_finseq_1(B) = k4_finseq_1(C) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(B)) => k4_finseq_4(k5_numbers,A,B,D) = k4_finseq_4(k5_numbers,A,C,D) ) ) ) => B = C ) ) ) ) ), file(finseq_5,t13_finseq_5), [interesting(0.00)]). fof(t24_polynom1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m2_finseq_1(C,u1_struct_0(A)) => ! [D] : ( m2_finseq_1(D,u1_struct_0(A)) => k7_polynom1(A,k8_finseq_1(u1_struct_0(A),C,D),B) = k8_finseq_1(u1_struct_0(A),k7_polynom1(A,C,B),k7_polynom1(A,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_polynom1,t31_finseq_3,d3_polynom1,t31_finseq_3,t35_finseq_1,t35_finseq_1,d3_polynom1,t31_finseq_3,d3_polynom1,t83_finseq_4,d3_polynom1,t83_finseq_4,d3_polynom1,t84_finseq_4,d3_polynom1,t84_finseq_4,t38_finseq_1,t13_finseq_5]), [file(polynom1,t24_polynom1),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(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(t124_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => m2_finseq_2(k11_finseq_1(B,C,D),A,k4_finseq_2(3,A)) ) ) ) ) ), file(finseq_2,t124_finseq_2), [interesting(0.00)]). fof(t27_finseq_4,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => ( k4_finseq_4(k5_numbers,A,k3_finseq_4(A,B,C,D),1) = B & k4_finseq_4(k5_numbers,A,k3_finseq_4(A,B,C,D),2) = C & k4_finseq_4(k5_numbers,A,k3_finseq_4(A,B,C,D),3) = D ) ) ) ) ) ), file(finseq_4,t27_finseq_4), [interesting(0.00)]). fof(t18_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(A) = k3_finseq_1(B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r1_xreal_0(1,C) & r1_xreal_0(C,k3_finseq_1(A)) ) => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) ) => A = B ) ) ) ), file(finseq_1,t18_finseq_1), [interesting(0.00)]). fof(d2_polynom1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m2_finseq_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m2_finseq_1(D,u1_struct_0(A)) => ( D = k6_polynom1(A,B,C) <=> ( k4_finseq_1(D) = k4_finseq_1(B) & ! [E] : ( r2_hidden(E,k4_finseq_1(B)) => k4_finseq_4(k5_numbers,u1_struct_0(A),D,E) = k1_group_1(A,C,k4_finseq_4(k5_numbers,u1_struct_0(A),B,E)) ) ) ) ) ) ) ) ), file(polynom1,d2_polynom1), [interesting(0.00)]). fof(t23_polynom1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m2_finseq_1(C,u1_struct_0(A)) => ! [D] : ( m2_finseq_1(D,u1_struct_0(A)) => k6_polynom1(A,k8_finseq_1(u1_struct_0(A),C,D),B) = k8_finseq_1(u1_struct_0(A),k6_polynom1(A,C,B),k6_polynom1(A,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_polynom1,t31_finseq_3,d2_polynom1,t31_finseq_3,t35_finseq_1,t35_finseq_1,d2_polynom1,t31_finseq_3,d2_polynom1,t83_finseq_4,d2_polynom1,t83_finseq_4,d2_polynom1,t84_finseq_4,d2_polynom1,t84_finseq_4,t38_finseq_1,t13_finseq_5]), [file(polynom1,t23_polynom1),interesting(0.00)]). fof(d4_group_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ( v4_group_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)) => k1_group_1(A,k1_group_1(A,B,C),D) = k1_group_1(A,B,k1_group_1(A,C,D)) ) ) ) ) ) ), file(group_1,d4_group_1), [interesting(0.00)]). fof(d18_polynom1,definition,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( m1_trees_4(C,k13_polynom1(A),k14_polynom1(A)) => ( C = k20_polynom1(A,B) <=> ? [D] : ( ~ v1_xboole_0(D) & v1_finset_1(D) & m1_subset_1(D,k1_zfmisc_1(k14_polynom1(A))) & C = k2_triang_1(k14_polynom1(A),D,k17_polynom1(A)) & ! [E] : ( ( v7_seqm_3(E) & v1_polynom1(E) & m1_pboole(E,A) ) => ( r2_hidden(E,D) <=> r3_polynom1(A,E,B) ) ) ) ) ) ) ) ), file(polynom1,d18_polynom1), [interesting(0.00)]). fof(d1_relat_2,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r1_relat_2(A,B) <=> ! [C] : ( r2_hidden(C,B) => r2_hidden(k4_tarski(C,C),A) ) ) ) ), file(relat_2,d1_relat_2), [interesting(0.00)]). fof(d16_polynom1,definition,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v1_partfun1(B,k14_polynom1(A),k14_polynom1(A)) & v1_relat_2(B) & v4_relat_2(B) & v8_relat_2(B) & m2_relset_1(B,k14_polynom1(A),k14_polynom1(A)) ) => ( B = k17_polynom1(A) <=> ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ! [D] : ( ( v7_seqm_3(D) & v1_polynom1(D) & m1_pboole(D,A) ) => ( r2_hidden(k4_tarski(C,D),B) <=> r2_polynom1(A,C,D) ) ) ) ) ) ) ), file(polynom1,d16_polynom1), [interesting(0.00)]). fof(d4_relat_2,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r4_relat_2(A,B) <=> ! [C,D] : ( ( r2_hidden(C,B) & r2_hidden(D,B) & r2_hidden(k4_tarski(C,D),A) & r2_hidden(k4_tarski(D,C),A) ) => C = D ) ) ) ), file(relat_2,d4_relat_2), [interesting(0.00)]). fof(d8_relat_2,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r8_relat_2(A,B) <=> ! [C,D,E] : ( ( r2_hidden(C,B) & r2_hidden(D,B) & r2_hidden(E,B) & r2_hidden(k4_tarski(C,D),A) & r2_hidden(k4_tarski(D,E),A) ) => r2_hidden(k4_tarski(C,E),A) ) ) ) ), file(relat_2,d8_relat_2), [interesting(0.00)]). fof(d6_relat_2,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r6_relat_2(A,B) <=> ! [C,D] : ~ ( r2_hidden(C,B) & r2_hidden(D,B) & C != D & ~ r2_hidden(k4_tarski(C,D),A) & ~ r2_hidden(k4_tarski(D,C),A) ) ) ) ), file(relat_2,d6_relat_2), [interesting(0.00)]). fof(t23_ordinal1,theorem,( ! [A,B] : ( v3_ordinal1(B) => ( r2_hidden(A,B) => v3_ordinal1(A) ) ) ), file(ordinal1,t23_ordinal1), [interesting(0.00)]). fof(s1_ordinal1,theorem, ( ? [A] : ( v3_ordinal1(A) & p1_s1_ordinal1(A) ) => ? [A] : ( v3_ordinal1(A) & p1_s1_ordinal1(A) & ! [B] : ( v3_ordinal1(B) => ( p1_s1_ordinal1(B) => r1_ordinal1(A,B) ) ) ) ), file(ordinal1,s1_ordinal1), [interesting(0.00)]). fof(t7_ordinal1,theorem,( ! [A,B] : ~ ( r2_hidden(A,B) & r1_tarski(B,A) ) ), file(ordinal1,t7_ordinal1), [interesting(0.00)]). fof(d8_orders_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r3_orders_1(A,B) <=> ( r1_relat_2(A,B) & r8_relat_2(A,B) & r4_relat_2(A,B) & r6_relat_2(A,B) ) ) ) ), file(orders_1,d8_orders_1), [interesting(0.00)]). fof(t134_orders_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B,C] : ( ( r3_orders_1(A,B) & r1_tarski(C,B) ) => r3_orders_1(A,C) ) ) ), file(orders_1,t134_orders_1), [interesting(0.00)]). fof(d2_triang_1,definition,( ! [A,B] : ( ( v1_finset_1(B) & m1_subset_1(B,k1_zfmisc_1(A)) ) => ! [C] : ( ( v1_relat_2(C) & v4_relat_2(C) & v8_relat_2(C) & v1_partfun1(C,A,A) & m2_relset_1(C,A,A) ) => ( r3_orders_1(C,B) => ! [D] : ( m2_finseq_1(D,A) => ( D = k2_triang_1(A,B,C) <=> ( k2_relat_1(D) = B & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ( ( r2_hidden(E,k4_finseq_1(D)) & r2_hidden(F,k4_finseq_1(D)) ) => ( r1_xreal_0(F,E) | ( k4_finseq_4(k5_numbers,A,D,E) != k4_finseq_4(k5_numbers,A,D,F) & r2_hidden(k4_tarski(k4_finseq_4(k5_numbers,A,D,E),k4_finseq_4(k5_numbers,A,D,F)),C) ) ) ) ) ) ) ) ) ) ) ) ), file(triang_1,d2_triang_1), [interesting(0.00)]). fof(d13_polynom1,definition,( ! [A,B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ( r3_polynom1(A,B,C) <=> ! [D] : r1_xreal_0(k8_polynom1(B,D),k8_polynom1(C,D)) ) ) ) ), file(polynom1,d13_polynom1), [interesting(0.00)]). fof(t3_jordan4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(A,B) => k5_binarith(k1_nat_1(B,C),A) = k1_nat_1(k5_binarith(B,A),C) ) ) ) ) ), file(jordan4,t3_jordan4), [interesting(0.00)]). fof(t26_finseq_4,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ( k4_finseq_4(k5_numbers,A,k2_finseq_4(A,B,C),1) = B & k4_finseq_4(k5_numbers,A,k2_finseq_4(A,B,C),2) = C ) ) ) ) ), file(finseq_4,t26_finseq_4), [interesting(0.00)]). fof(t4_partfun2,theorem,( ! [A,B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( ( v1_funct_1(D) & m2_relset_1(D,C,B) ) => ( r2_hidden(A,k2_relat_1(D)) <=> ? [E] : ( m1_subset_1(E,C) & r2_hidden(E,k4_relset_1(C,B,D)) & A = k4_finseq_4(C,B,D,E) ) ) ) ) ) ), file(partfun2,t4_partfun2), [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(t3_group_7,theorem,( ! [A,B,C,D,E,F] : ( k11_finseq_1(A,B,C) = k11_finseq_1(D,E,F) => ( A = D & B = E & C = F ) ) ), file(group_7,t3_group_7), [interesting(0.00)]). fof(t4_vectsp_9,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( ( k2_relat_1(A) = k2_relat_1(B) & v2_funct_1(A) & v2_funct_1(B) ) => r1_rfinseq(A,B) ) ) ) ), file(vectsp_9,t4_vectsp_9), [interesting(0.00)]). fof(t17_rfinseq,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) ) => ( r1_rfinseq(A,B) <=> ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k4_finseq_1(B),k4_finseq_1(B)) & v3_funct_2(C,k4_finseq_1(B),k4_finseq_1(B)) & m2_relset_1(C,k4_finseq_1(B),k4_finseq_1(B)) & A = k5_relat_1(C,B) ) ) ) ) ), file(rfinseq,t17_rfinseq), [interesting(0.00)]). fof(t78_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( m2_finseq_1(C,k3_finseq_2(k4_finseq_2(3,k14_polynom1(A)))) => ! [D] : ( m2_finseq_1(D,k3_finseq_2(k4_finseq_2(3,k14_polynom1(A)))) => ~ ( k4_finseq_1(C) = k4_finseq_1(k21_polynom1(A,B)) & k4_finseq_1(D) = k4_finseq_1(k21_polynom1(A,B)) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r2_hidden(E,k4_finseq_1(C)) => k1_funct_1(C,E) = k4_polynom1(k21_polynom1(A,k4_finseq_4(k5_numbers,k14_polynom1(A),k3_polynom1(k14_polynom1(A),k5_numbers,k4_finseq_2(2,k14_polynom1(A)),k21_polynom1(A,B),E),1)),k2_finseq_2(k3_finseq_1(k21_polynom1(A,k4_finseq_4(k5_numbers,k14_polynom1(A),k3_polynom1(k14_polynom1(A),k5_numbers,k4_finseq_2(2,k14_polynom1(A)),k21_polynom1(A,B),E),1))),k13_binarith(k14_polynom1(A),k4_finseq_4(k5_numbers,k14_polynom1(A),k3_polynom1(k14_polynom1(A),k5_numbers,k4_finseq_2(2,k14_polynom1(A)),k21_polynom1(A,B),E),2)))) ) ) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r2_hidden(E,k4_finseq_1(D)) => k1_funct_1(D,E) = k4_polynom1(k2_finseq_2(k3_finseq_1(k21_polynom1(A,k4_finseq_4(k5_numbers,k14_polynom1(A),k3_polynom1(k14_polynom1(A),k5_numbers,k4_finseq_2(2,k14_polynom1(A)),k21_polynom1(A,B),E),2))),k13_binarith(k14_polynom1(A),k4_finseq_4(k5_numbers,k14_polynom1(A),k3_polynom1(k14_polynom1(A),k5_numbers,k4_finseq_2(2,k14_polynom1(A)),k21_polynom1(A,B),E),1))),k21_polynom1(A,k4_finseq_4(k5_numbers,k14_polynom1(A),k3_polynom1(k14_polynom1(A),k5_numbers,k4_finseq_2(2,k14_polynom1(A)),k21_polynom1(A,B),E),2))) ) ) & ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k4_finseq_1(k15_dtconstr(k4_finseq_2(3,k14_polynom1(A)),C)),k4_finseq_1(k15_dtconstr(k4_finseq_2(3,k14_polynom1(A)),C))) & v3_funct_2(E,k4_finseq_1(k15_dtconstr(k4_finseq_2(3,k14_polynom1(A)),C)),k4_finseq_1(k15_dtconstr(k4_finseq_2(3,k14_polynom1(A)),C))) & m2_relset_1(E,k4_finseq_1(k15_dtconstr(k4_finseq_2(3,k14_polynom1(A)),C)),k4_finseq_1(k15_dtconstr(k4_finseq_2(3,k14_polynom1(A)),C))) ) => k15_dtconstr(k4_finseq_2(3,k14_polynom1(A)),D) != k1_partfun1(k4_finseq_1(k15_dtconstr(k4_finseq_2(3,k14_polynom1(A)),C)),k4_finseq_1(k15_dtconstr(k4_finseq_2(3,k14_polynom1(A)),C)),k5_numbers,k4_finseq_2(3,k14_polynom1(A)),E,k15_dtconstr(k4_finseq_2(3,k14_polynom1(A)),C)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_funct_1,t32_polynom1,t72_polynom1,d14_polynom1,t26_finseq_4,t26_finseq_4,d2_matrlin,t68_finseq_2,d3_finseq_1,t72_polynom1,d3_finseq_1,d4_finseq_4,t70_finseq_2,d2_matrlin,t60_finseq_1,t39_polynom1,t73_polynom1,t73_polynom1,d14_polynom1,t26_finseq_4,t26_finseq_4,d2_matrlin,t68_finseq_2,d3_finseq_1,t26_finseq_4,d3_finseq_1,d4_finseq_4,d2_matrlin,t70_finseq_2,t60_finseq_1,t33_polynom1,t33_polynom1,d5_funct_1,d5_funct_1,t32_polynom1,t72_polynom1,d14_polynom1,t26_finseq_4,t26_finseq_4,d2_matrlin,t68_finseq_2,d3_finseq_1,t72_polynom1,d4_finseq_4,d3_finseq_1,t70_finseq_2,d2_matrlin,t60_finseq_1,t39_polynom1,t73_polynom1,t73_polynom1,d14_polynom1,t26_finseq_4,t26_finseq_4,d2_matrlin,t68_finseq_2,d3_finseq_1,d3_finseq_1,d4_finseq_4,d2_matrlin,t70_finseq_2,t60_finseq_1,t33_polynom1,t33_polynom1,d5_funct_1,t2_tarski,d8_funct_1,t32_polynom1,t32_polynom1,d4_finseq_4,t72_polynom1,d14_polynom1,t26_finseq_4,t26_finseq_4,d2_matrlin,t68_finseq_2,d3_finseq_1,t72_polynom1,d4_finseq_4,d3_finseq_1,t70_finseq_2,d2_matrlin,t60_finseq_1,d4_finseq_4,t72_polynom1,d14_polynom1,t26_finseq_4,t26_finseq_4,d2_matrlin,t68_finseq_2,d3_finseq_1,t72_polynom1,d3_finseq_1,d4_finseq_4,t70_finseq_2,d2_matrlin,t60_finseq_1,t3_group_7,d8_funct_1,d8_funct_1,d8_funct_1,t32_polynom1,t32_polynom1,d4_finseq_4,t72_polynom1,d14_polynom1,t26_finseq_4,t26_finseq_4,d2_matrlin,t68_finseq_2,d3_finseq_1,t72_polynom1,d3_finseq_1,d4_finseq_4,t70_finseq_2,d2_matrlin,t60_finseq_1,d4_finseq_4,t72_polynom1,d14_polynom1,t26_finseq_4,t26_finseq_4,d2_matrlin,t68_finseq_2,d3_finseq_1,t72_polynom1,d4_finseq_4,d3_finseq_1,t70_finseq_2,d2_matrlin,t60_finseq_1,t3_group_7,d8_funct_1,d8_funct_1,t4_vectsp_9,t17_rfinseq]), [file(polynom1,t78_polynom1),interesting(0.00)]). fof(t55_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ! [C] : ( v1_relat_1(C) => k5_relat_1(k5_relat_1(A,B),C) = k5_relat_1(A,k5_relat_1(B,C)) ) ) ) ), file(relat_1,t55_relat_1), [interesting(0.00)]). fof(t9_rlvect_2,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)) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k1_relat_1(B),k1_relat_1(B)) & v3_funct_2(D,k1_relat_1(B),k1_relat_1(B)) & m2_relset_1(D,k1_relat_1(B),k1_relat_1(B)) ) => ( C = k5_relat_1(D,B) => k9_rlvect_1(A,B) = k9_rlvect_1(A,C) ) ) ) ) ) ), file(rlvect_2,t9_rlvect_2), [interesting(0.00)]). fof(t15_matrlin,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] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r2_hidden(C,k1_relat_1(B)) => k4_finseq_4(k5_numbers,u1_struct_0(A),B,C) = k1_rlvect_1(A) ) ) => k9_rlvect_1(A,B) = k1_rlvect_1(A) ) ) ) ), file(matrlin,t15_matrlin), [interesting(0.00)]). fof(d27_polynom1,definition,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( ~ v3_struct_0(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v2_group_1(B) & v7_vectsp_1(B) & ~ v3_realset2(B) & l3_vectsp_1(B) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_vectsp_1(C) & l3_vectsp_1(C) ) => ( C = k30_polynom1(A,B) <=> ( ! [D] : ( r2_hidden(D,u1_struct_0(C)) <=> ( v1_funct_1(D) & v1_funct_2(D,k14_polynom1(A),u1_struct_0(B)) & v2_polynom1(D,k14_polynom1(A),B) & m2_relset_1(D,k14_polynom1(A),u1_struct_0(B)) ) ) & ! [D] : ( m1_subset_1(D,u1_struct_0(C)) => ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k14_polynom1(A),u1_struct_0(B)) & v2_polynom1(F,k14_polynom1(A),B) & m2_relset_1(F,k14_polynom1(A),u1_struct_0(B)) ) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k14_polynom1(A),u1_struct_0(B)) & v2_polynom1(G,k14_polynom1(A),B) & m2_relset_1(G,k14_polynom1(A),u1_struct_0(B)) ) => ( ( D = F & E = G ) => k2_rlvect_1(C,D,E) = k22_polynom1(A,B,F,G) ) ) ) ) ) & ! [D] : ( m1_subset_1(D,u1_struct_0(C)) => ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k14_polynom1(A),u1_struct_0(B)) & v2_polynom1(F,k14_polynom1(A),B) & m2_relset_1(F,k14_polynom1(A),u1_struct_0(B)) ) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k14_polynom1(A),u1_struct_0(B)) & v2_polynom1(G,k14_polynom1(A),B) & m2_relset_1(G,k14_polynom1(A),u1_struct_0(B)) ) => ( ( D = F & E = G ) => k1_group_1(C,D,E) = k28_polynom1(A,B,F,G) ) ) ) ) ) & k1_rlvect_1(C) = k26_polynom1(A,B) & k2_vectsp_1(C) = k27_polynom1(A,B) ) ) ) ) ) ), file(polynom1,d27_polynom1), [interesting(0.00)]). fof(t22_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,A) => ~ ( k3_finseq_1(B) != 0 & ! [C] : ( m2_finseq_1(C,A) => ! [D] : ( m1_subset_1(D,A) => B != k8_finseq_1(A,C,k12_finseq_1(A,D)) ) ) ) ) ) ), file(finseq_2,t22_finseq_2), [interesting(0.00)]). fof(t97_orders_1,theorem,( ! [A,B] : ( ( v1_partfun1(B,A,A) & m2_relset_1(B,A,A) ) => k3_relat_1(B) = A ) ), file(orders_1,t97_orders_1), [interesting(0.00)]). fof(d12_relat_2,definition,( ! [A] : ( v1_relat_1(A) => ( v4_relat_2(A) <=> r4_relat_2(A,k3_relat_1(A)) ) ) ), file(relat_2,d12_relat_2), [interesting(0.00)]). fof(t8_polynom1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( ~ v1_xboole_0(B) & v1_finset_1(B) & m1_subset_1(B,k1_zfmisc_1(A)) ) => ! [C] : ( ( v1_partfun1(C,A,A) & v1_relat_2(C) & v4_relat_2(C) & v8_relat_2(C) & m2_relset_1(C,A,A) ) => ! [D] : ( m1_subset_1(D,A) => ( ( r2_hidden(D,B) & r3_orders_1(C,B) & ! [E] : ( m1_subset_1(E,A) => ( r2_hidden(E,B) => r2_hidden(k4_tarski(D,E),C) ) ) ) => k4_finseq_4(k5_numbers,A,k2_triang_1(A,B,C),1) = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_triang_1,t4_partfun2,t27_finseq_3,t1_xreal_1,t60_relat_1,d2_triang_1,t6_finseq_5,d2_triang_1,t4_partfun2,t97_orders_1,d12_relat_2,d4_relat_2]), [file(polynom1,t8_polynom1),interesting(0.00)]). fof(t9_polynom1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( ~ v1_xboole_0(B) & v1_finset_1(B) & m1_subset_1(B,k1_zfmisc_1(A)) ) => ! [C] : ( ( v1_partfun1(C,A,A) & v1_relat_2(C) & v4_relat_2(C) & v8_relat_2(C) & m2_relset_1(C,A,A) ) => ! [D] : ( m1_subset_1(D,A) => ( ( r2_hidden(D,B) & r3_orders_1(C,B) & ! [E] : ( m1_subset_1(E,A) => ( r2_hidden(E,B) => r2_hidden(k4_tarski(E,D),C) ) ) ) => k4_finseq_4(k5_numbers,A,k2_triang_1(A,B,C),k3_finseq_1(k2_triang_1(A,B,C))) = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_triang_1,t4_partfun2,t27_finseq_3,t1_xreal_1,t60_relat_1,d2_triang_1,t6_finseq_5,d2_triang_1,t4_partfun2,t97_orders_1,d12_relat_2,d4_relat_2]), [file(polynom1,t9_polynom1),interesting(0.00)]). fof(t69_polynom1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ( k4_finseq_4(k5_numbers,k13_polynom1(A),k20_polynom1(A,B),1) = k16_polynom1(A) & k4_finseq_4(k5_numbers,k13_polynom1(A),k20_polynom1(A,B),k3_finseq_1(k20_polynom1(A,B))) = B ) ) ) ), inference(mizar_proof,[status(thm)],[d18_polynom1,t63_polynom1,l85_polynom1,t134_orders_1,t64_polynom1,d16_polynom1,t8_polynom1,t53_polynom1,d16_polynom1,t9_polynom1]), [file(polynom1,t69_polynom1),interesting(0.00)]). fof(t2_jordan3,theorem,( ! [A] : ( v4_ordinal2(A) => k5_binarith(A,0) = A ) ), file(jordan3,t2_jordan3), [interesting(0.00)]). fof(t19_finseq_2,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k3_finseq_1(k7_finseq_1(B,k9_finseq_1(A))) = k1_nat_1(k3_finseq_1(B),1) ) ), file(finseq_2,t19_finseq_2), [interesting(0.00)]). fof(t59_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k1_funct_1(k7_finseq_1(B,k9_finseq_1(A)),k1_nat_1(k3_finseq_1(B),1)) = A ) ), file(finseq_1,t59_finseq_1), [interesting(0.00)]). fof(t84_polynom1,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v2_group_1(B) & l2_vectsp_1(B) ) => ( k15_polynom1(A,B,k27_polynom1(A,B),k16_polynom1(A)) = k2_group_1(B) & ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ( C != k16_polynom1(A) => k15_polynom1(A,B,k27_polynom1(A,B),C) = k1_rlvect_1(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_funcop_1,t33_funct_7,d14_polynom1,t34_funct_7,t13_funcop_1]), [file(polynom1,t84_polynom1),interesting(0.00)]). fof(t17_partfun2,theorem,( ! [A,B,C] : ( ~ v1_xboole_0(C) => ! [D] : ( ~ v1_xboole_0(D) => ! [E] : ( ( v1_funct_1(E) & m2_relset_1(E,C,D) ) => ( ( v2_funct_1(E) & r2_hidden(A,k4_relset_1(C,D,E)) & r2_hidden(B,k4_relset_1(C,D,E)) & k4_finseq_4(C,D,E,A) = k4_finseq_4(C,D,E,B) ) => A = B ) ) ) ) ), file(partfun2,t17_partfun2), [interesting(0.00)]). fof(t1_jordan4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( k5_binarith(A,B) = 0 => r1_xreal_0(A,B) ) ) ) ), file(jordan4,t1_jordan4), [interesting(0.00)]). fof(t80_card_2,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => r1_ordinal1(k1_card_1(k2_relat_1(A)),k1_card_1(k1_relat_1(A))) ) ), file(card_2,t80_card_2), [interesting(0.00)]). fof(t55_funct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v2_funct_1(A) => ( k2_relat_1(A) = k1_relat_1(k2_funct_1(A)) & k1_relat_1(A) = k2_relat_1(k2_funct_1(A)) ) ) ) ), file(funct_1,t55_funct_1), [interesting(0.00)]). fof(t21_pre_circ,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => k1_card_1(A) = k1_card_1(k1_relat_1(A)) ) ), file(pre_circ,t21_pre_circ), [interesting(0.00)]). fof(t79_card_1,theorem,( ! [A] : k4_card_1(k1_tarski(A)) = 1 ), file(card_1,t79_card_1), [interesting(0.00)]). 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 ) ) ) ), file(rlvect_1,t10_rlvect_1), [interesting(0.00)]). fof(t111_finseq_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,A) => ~ ( ~ v1_xboole_0(B) & ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m2_finseq_1(D,A) => ~ ( C = k1_funct_1(B,1) & B = k8_finseq_1(A,k12_finseq_1(A,C),D) ) ) ) ) ) ) ), file(finseq_3,t111_finseq_3), [interesting(0.00)]). fof(t112_finseq_3,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( r2_hidden(A,k4_finseq_1(B)) => k1_funct_1(k7_finseq_1(k9_finseq_1(C),B),k2_xcmplx_0(A,1)) = k1_funct_1(B,A) ) ) ) ), file(finseq_3,t112_finseq_3), [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)]).