fof(t28_bagorder,theorem,( ! [A] : ( v3_ordinal1(A) => v2_bagorder(k6_bagorder(A),A) ) ), inference(mizar_proof,[status(thm)],[d7_bagorder,d7_bagorder,t27_bagorder]), [file(bagorder,t28_bagorder),interesting(1.00)]). fof(t30_bagorder,theorem,( ! [A] : ( v3_ordinal1(A) => v2_bagorder(k7_bagorder(A),A) ) ), inference(mizar_proof,[status(thm)],[d7_bagorder,d7_bagorder,t27_bagorder]), [file(bagorder,t30_bagorder),interesting(1.00)]). fof(t26_bagorder,theorem,( ! [A] : ( v3_ordinal1(A) => v2_wellord1(k4_bagorder(A)) ) ), inference(mizar_proof,[status(thm)],[d7_bagorder,t92_orders_1,t9_partit_2,t5_wellord1,d2_wellfnd1,t15_wellfnd1,d14_polynom1,d1_wellord2,t7_wellord2,t107_orders_1,t133_orders_1,t134_orders_1,d2_triang_1,t20_bagorder,d14_polynom1,d7_wellfnd1,d7_wellfnd1,d8_bagorder,t56_polynom1,t6_finseq_5,t60_relat_1,t12_funct_1,t23_ordinal1,d14_polynom1,s3_funct_2,d7_polynom1,t11_finseq_2,t27_finseq_3,d2_triang_1,d4_finseq_4,d4_finseq_4,d1_wellord2,t7_ordinal1,d5_real_1,d14_polynom1,d7_wellfnd1,d8_bagorder,t19_ordinal1,t24_ordinal1,s1_nat_1,d15_dickson,d3_bagorder,d15_dickson,d14_polynom1,d7_wellfnd1,d7_wellfnd1,d8_bagorder,t24_ordinal1,d14_dickson,d15_dickson,d7_bagorder,t92_orders_1,t9_partit_2,t11_bagorder,d14_polynom1,t21_bagorder,d14_polynom1,s3_funct_2,d7_wellfnd1,t29_nat_1,d3_pboole,t23_ordinal1,t72_funct_1,t24_ordinal1,t9_funct_1,d7_wellfnd1,d8_bagorder,t24_ordinal1,t21_bagorder,t72_funct_1,t19_ordinal1,t72_funct_1,t72_funct_1,d8_bagorder,d7_wellfnd1,t15_wellfnd1,d2_wellfnd1,d5_wellord1,t8_wellord1,t97_orders_1,d9_relat_2,d16_relat_2,d12_relat_2,t92_orders_1,t5_wellord1,d5_wellord1,t8_wellord1,s2_ordinal1]), [file(bagorder,t26_bagorder),interesting(0.77)]). fof(t31_bagorder,theorem,( ! [A] : ( v3_ordinal1(A) => v2_wellord1(k7_bagorder(A)) ) ), inference(mizar_proof,[status(thm)],[d7_bagorder,t97_orders_1,d9_relat_2,d16_relat_2,d12_relat_2,t92_orders_1,d7_bagorder,d1_xboole_0,t97_orders_1,d3_tarski,d3_tarski,d8_cqc_sim1,t97_orders_1,t26_bagorder,t8_wellord1,d5_wellord1,d3_wellord1,d7_xboole_0,d1_xboole_0,d3_xboole_0,d3_xboole_0,d1_wellord1,t97_orders_1,d8_cqc_sim1,d9_bagorder,d1_wellord1,d3_xboole_0,d9_bagorder,d5_real_1,d7_xboole_0,d3_wellord1,d5_wellord1,t8_wellord1]), [file(bagorder,t31_bagorder),interesting(0.75)]). fof(t29_bagorder,theorem,( ! [A] : ( ( v3_ordinal1(A) & ~ v1_finset_1(A) ) => ~ v2_wellord1(k6_bagorder(A)) ) ), inference(mizar_proof,[status(thm)],[d4_wellord1,t100_orders_1,t5_wellord1,d2_wellfnd1,t19_funcop_1,t8_card_4,d3_funct_7,t18_funct_4,t14_funcop_1,t5_cqc_lang,t1_xboole_1,d8_seqm_3,d1_tarski,t33_funct_7,d1_tarski,t34_funct_7,t13_funcop_1,d4_funct_1,d7_polynom1,d8_polynom1,d14_polynom1,s3_funct_2,d7_wellfnd1,d14_polynom1,d14_polynom1,t8_card_4,t34_funct_7,t13_funcop_1,t19_funcop_1,t33_funct_7,t38_nat_1,t30_axioms,d2_ordinal1,t34_funct_7,t34_funct_7,d11_polynom1,t33_funct_7,d12_polynom1,d16_polynom1,d4_bagorder,d4_bagorder,t8_card_4,d1_wellord2,t7_wellord2,t107_orders_1,t133_orders_1,t134_orders_1,t134_orders_1,t34_funct_7,t13_funcop_1,d7_polynom1,d1_tarski,d1_tarski,t33_funct_7,d7_polynom1,t2_tarski,t12_bagorder,t32_funct_7,t34_funct_7,t13_funcop_1,d7_polynom1,d1_tarski,d1_tarski,t33_funct_7,d7_polynom1,t2_tarski,t12_bagorder,t3_bagorder,t33_funct_7,t33_funct_7,t3_bagorder,d7_bagorder,d9_bagorder,t15_wellfnd1]), [file(bagorder,t29_bagorder),interesting(0.69)]). fof(t25_bagorder,theorem,( ! [A] : ( v3_ordinal1(A) => v2_bagorder(k4_bagorder(A),A) ) ), inference(mizar_proof,[status(thm)],[d14_polynom1,d8_bagorder,d3_pboole,d1_wellord2,t7_wellord2,t107_orders_1,t133_orders_1,t134_orders_1,d2_triang_1,t27_finseq_3,d7_polynom1,d2_xboole_0,t11_finseq_2,d7_polynom1,d2_xboole_0,t11_finseq_2,t9_funct_1,s6_nat_1,t12_funct_1,t23_ordinal1,d7_polynom1,d2_xboole_0,t11_finseq_2,d5_real_1,d2_triang_1,d4_finseq_4,d4_finseq_4,d1_wellord2,t7_ordinal1,d8_bagorder,d5_real_1,d8_bagorder,d7_relat_2,d7_bagorder,d8_bagorder,d1_wellord2,t7_wellord2,t107_orders_1,t133_orders_1,t134_orders_1,d2_triang_1,t20_bagorder,t6_finseq_5,t60_relat_1,t12_funct_1,t23_ordinal1,d7_polynom1,t56_polynom1,d2_ordinal1,t56_polynom1,d7_polynom1,t11_finseq_2,t27_finseq_3,d2_triang_1,d4_finseq_4,d4_finseq_4,d1_wellord2,d10_xboole_0,d5_real_1,d8_bagorder,d14_polynom1,t12_orders_1,d8_bagorder,d5_polynom1,t8_xreal_1,d5_real_1,d5_polynom1,d8_bagorder]), [file(bagorder,t25_bagorder),interesting(0.65)]). fof(t23_bagorder,theorem,( ! [A] : ( v3_ordinal1(A) => v2_bagorder(k17_polynom1(A),A) ) ), inference(mizar_proof,[status(thm)],[d14_polynom1,t49_polynom1,d16_polynom1,d7_relat_2,d7_bagorder,t64_polynom1,d16_polynom1,d16_polynom1,d11_polynom1,t8_xreal_1,d5_polynom1,d5_real_1,d5_polynom1,d11_polynom1,d12_polynom1,d12_polynom1,d16_polynom1]), [file(bagorder,t23_bagorder),interesting(0.63)]). fof(t34_bagorder,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k9_bagorder(A) = k5_yellow_1(A,k2_pre_circ(A,k11_dickson)) ) ), inference(mizar_proof,[status(thm)],[d13_bagorder,t33_bagorder,t20_relat_1,d13_bagorder,t33_bagorder,d4_yellow_1,d14_polynom1,d14_polynom1,t13_funcop_1,t13_funcop_1,d3_pboole,t12_funct_1,d8_seqm_3,d3_pboole,t12_funct_1,d8_seqm_3,d15_dickson,t13_funcop_1,d14_polynom1,d13_bagorder,d13_polynom1,d14_dickson,d15_dickson,d9_orders_2,d4_yellow_1,d9_orders_2,t20_relat_1,t33_bagorder,d14_polynom1,d4_yellow_1,d9_orders_2,d4_yellow_1,t13_funcop_1,d15_dickson,d9_orders_2,d14_dickson,t33_zfmisc_1,t50_polynom1,d13_bagorder,d2_relat_1]), [file(bagorder,t34_bagorder),interesting(0.63)]). fof(t42_bagorder,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & v16_waybel_0(A) & l1_orders_2(A) ) => ( v1_wellfnd1(A) => v1_wellfnd1(k14_bagorder(A)) ) ) ), inference(mizar_proof,[status(thm)],[t15_wellfnd1,d7_wellfnd1,t37_bagorder,s3_funct_2,d5_finsub_1,d5_finsub_1,d1_funct_2,t12_relset_1,d19_bagorder,d11_dickson,d7_wellfnd1,t40_bagorder,d5_funct_1,d26_waybel_4,s1_nat_1,t28_nat_1,t29_nat_1,d20_bagorder,s3_funct_2,t41_bagorder,d7_wellfnd1,t40_bagorder,d20_bagorder,d15_bagorder,t1_bagorder,d7_wellfnd1,d2_zfmisc_1,d2_zfmisc_1,s2_recdef_1,s2_funct_2,d1_mcart_1,d2_mcart_1,d4_xboole_0,d1_tarski,d5_finsub_1,d20_bagorder,t29_nat_1,d15_bagorder,d24_waybel_4,d9_orders_2,d29_waybel_0,d9_orders_2,d1_mcart_1,d2_mcart_1,d4_xboole_0,d1_tarski,d5_finsub_1,d20_bagorder,t29_nat_1,d15_bagorder,d24_waybel_4,d9_orders_2,d29_waybel_0,d9_orders_2,s1_nat_1,t12_relset_1,d19_bagorder,d5_funct_1,d15_bagorder,d1_mcart_1,t12_relset_1,d19_bagorder,d5_funct_1,d15_bagorder,d1_mcart_1,s1_nat_1,s1_nat_1,d7_wellfnd1,t15_wellfnd1]), [file(bagorder,t42_bagorder),interesting(0.63)]). fof(t14_bagorder,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) ) => k3_bagorder(A,k9_polynom1(A,B,C)) = k1_nat_1(k3_bagorder(A,B),k3_bagorder(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_wellord2,t7_wellord2,t107_orders_1,t133_orders_1,d4_bagorder,d4_bagorder,d4_bagorder,t27_finseq_2,t134_orders_1,d2_triang_1,t42_polynom1,d3_pboole,t20_finseq_1,d8_seqm_3,t45_relat_1,t1_xboole_1,t1_xboole_1,d4_finseq_1,d4_finseq_1,d3_pboole,d3_finseq_1,t46_relat_1,t46_relat_1,t46_relat_1,t13_bagorder,t13_bagorder,t31_finseq_3,t2_integra5,t31_finseq_3,d3_pboole,d8_seqm_3,d3_finseq_1,t31_finseq_3,t23_funct_1,d5_polynom1,t23_funct_1,t23_funct_1,t26_rvsum_1,t17_finseq_1,t2_integra5]), [file(bagorder,t14_bagorder),interesting(0.60)]). fof(t24_bagorder,theorem,( ! [A] : ( ( v3_ordinal1(A) & ~ v1_finset_1(A) ) => ~ v2_wellord1(k17_polynom1(A)) ) ), inference(mizar_proof,[status(thm)],[d4_wellord1,t100_orders_1,t5_wellord1,d2_wellfnd1,t19_funcop_1,t8_card_4,d3_funct_7,t18_funct_4,t14_funcop_1,t5_cqc_lang,t1_xboole_1,d8_seqm_3,d1_tarski,t33_funct_7,d1_tarski,t34_funct_7,t13_funcop_1,d4_funct_1,d7_polynom1,d8_polynom1,d14_polynom1,s3_funct_2,d7_wellfnd1,d14_polynom1,d14_polynom1,t8_card_4,t34_funct_7,t13_funcop_1,t19_funcop_1,t33_funct_7,t38_nat_1,t30_axioms,d2_ordinal1,t34_funct_7,t34_funct_7,d11_polynom1,t33_funct_7,d12_polynom1,d16_polynom1,t15_wellfnd1]), [file(bagorder,t24_bagorder),interesting(0.59)]). fof(t16_bagorder,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ( k3_bagorder(A,B) = 0 <=> r6_pboole(A,B,k16_polynom1(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_wellord2,t7_wellord2,t107_orders_1,t133_orders_1,t134_orders_1,d3_pboole,d4_bagorder,t5_bagorder,d2_triang_1,d7_polynom1,d5_funct_1,t46_relat_1,t68_finseq_2,t70_finseq_2,t23_funct_1,t17_funcop_1,d15_polynom1,d15_polynom1,d4_bagorder,d1_xboole_0,t13_funcop_1,d7_polynom1,d2_triang_1,t65_relat_1,t44_relat_1,t3_xboole_1,t64_relat_1,t102_rvsum_1]), [file(bagorder,t16_bagorder),interesting(0.58)]). fof(t1_bagorder,theorem,( ! [A,B,C] : ( ( r2_hidden(C,A) & r2_hidden(C,B) ) => ( k4_xboole_0(A,k1_tarski(C)) = k4_xboole_0(B,k1_tarski(C)) <=> A = B ) ) ), inference(mizar_proof,[status(thm)],[t46_zfmisc_1,t39_xboole_1,t39_xboole_1,t46_zfmisc_1]), [file(bagorder,t1_bagorder),interesting(0.56)]). fof(t33_bagorder,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => u1_struct_0(k5_yellow_1(A,k2_pre_circ(A,k11_dickson))) = k14_polynom1(A) ) ), inference(mizar_proof,[status(thm)],[d4_yellow_1,d5_card_3,d3_pboole,d3_tarski,d5_funct_1,d13_pralg_1,d15_dickson,t13_funcop_1,d8_seqm_3,t41_polynom1,t13_finset_1,d8_polynom1,d3_pboole,d3_pboole,d14_polynom1,d14_polynom1,d3_pboole,d3_pboole,d3_pboole,d13_pralg_1,t13_funcop_1,d15_dickson,d5_card_3,d4_yellow_1,t2_tarski]), [file(bagorder,t33_bagorder),interesting(0.55)]). fof(t20_bagorder,theorem,( ! [A,B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ( k1_polynom2(A,B) = k1_xboole_0 => r6_pboole(A,B,k16_polynom1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d3_pboole,t9_funct_1,t56_polynom1,d7_polynom1]), [file(bagorder,t20_bagorder),interesting(0.54)]). fof(t5_bagorder,theorem,( ! [A] : ( m2_finseq_1(A,k5_numbers) => ( k9_wsierp_1(A) = 0 <=> A = k4_finseqop(k5_numbers,k3_finseq_1(A),0) ) ) ), inference(mizar_proof,[status(thm)],[d4_finseq_1,t1_xboole_1,d4_finseq_1,d3_finseq_1,d2_finseq_2,t19_funcop_1,t115_rvsum_1,t13_funcop_1,t17_finseq_1,t111_rvsum_1]), [file(bagorder,t5_bagorder),interesting(0.54)]). fof(t3_bagorder,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( r2_hidden(B,k1_relat_1(A)) => k5_relat_1(k9_finseq_1(B),A) = k9_finseq_1(k1_funct_1(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[d5_funct_1,d1_funct_2,t11_relset_1,t55_finseq_1,t37_zfmisc_1,d4_finseq_1,t39_finseq_2]), [file(bagorder,t3_bagorder),interesting(0.53)]). fof(t27_bagorder,theorem,( ! [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)) ) => ( ( ! [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(k4_tarski(C,D),B) => r2_hidden(k4_tarski(k9_polynom1(A,C,E),k9_polynom1(A,D,E)),B) ) ) ) ) & r7_relat_2(B,k14_polynom1(A)) ) => v2_bagorder(k5_bagorder(A,B),A) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_polynom1,d9_bagorder,d9_bagorder,d9_bagorder,d7_relat_2,d9_bagorder,d5_real_1,d7_relat_2,d7_bagorder,t16_bagorder,t12_orders_1,t16_bagorder,d9_bagorder,t14_bagorder,t14_bagorder,t10_xreal_1,d9_bagorder,t14_bagorder,t14_bagorder,d9_bagorder,d9_bagorder]), [file(bagorder,t27_bagorder),interesting(0.52)]). fof(t21_bagorder,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( v3_ordinal1(B) => ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => ( r2_hidden(B,A) => ( v7_seqm_3(k7_relat_1(C,B)) & v1_polynom1(k7_relat_1(C,B)) & m1_pboole(k7_relat_1(C,B),B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_ordinal1,d3_pboole,t91_relat_1,d3_pboole]), [file(bagorder,t21_bagorder),interesting(0.52)]). fof(t19_bagorder,theorem,( ! [A] : k1_polynom2(A,k16_polynom1(A)) = k1_xboole_0 ), inference(mizar_proof,[status(thm)],[d1_xboole_0,d7_polynom1,t56_polynom1]), [file(bagorder,t19_bagorder),interesting(0.51)]). fof(t15_bagorder,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,C,B) => k3_bagorder(A,k10_polynom1(A,B,C)) = k5_real_1(k3_bagorder(A,B),k3_bagorder(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t51_polynom1,t14_bagorder]), [file(bagorder,t15_bagorder),interesting(0.50)]). fof(t41_bagorder,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_orders_2(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( v3_wellfnd1(B,A) => v3_wellfnd1(k16_bagorder(A,B,C),A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_bagorder,d20_bagorder,d7_wellfnd1,d7_wellfnd1,d7_wellfnd1]), [file(bagorder,t41_bagorder),interesting(0.45)]). fof(t22_bagorder,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,C,B) => r1_tarski(k1_polynom2(A,C),k1_polynom2(A,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d7_polynom1,d13_polynom1,d7_polynom1]), [file(bagorder,t22_bagorder),interesting(0.41)]). fof(t12_bagorder,theorem,( ! [A,B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_finset_1(C) & m1_subset_1(C,k1_zfmisc_1(A)) ) => ! [D] : ( ( v1_partfun1(D,A,A) & v1_relat_2(D) & v4_relat_2(D) & v8_relat_2(D) & m2_relset_1(D,A,A) ) => ( ( C = k1_tarski(B) & r3_orders_1(D,C) ) => k2_triang_1(A,C,D) = k9_finseq_1(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_triang_1,t50_card_1,t20_card_2,d2_triang_1,t56_finseq_1]), [file(bagorder,t12_bagorder),interesting(0.39)]). fof(t38_bagorder,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & v16_waybel_0(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,k5_finsub_1(u1_struct_0(A))) => m1_subset_1(k4_xboole_0(B,k6_domain_1(u1_struct_0(A),k11_bagorder(A,B))),k5_finsub_1(u1_struct_0(A))) ) ) ), inference(mizar_proof,[status(thm)],[d5_finsub_1,t36_xboole_1,t1_xboole_1,d5_finsub_1]), [file(bagorder,t38_bagorder),interesting(0.38)]). fof(t13_bagorder,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v1_finset_1(C) & m1_subset_1(C,k1_zfmisc_1(A)) ) => ! [D] : ( m2_finseq_1(D,k5_numbers) => ! [E] : ( m2_finseq_1(E,k5_numbers) => ( ( D = k2_polynom2(A,k2_triang_1(A,k1_polynom2(A,B),k1_yellow_1(A)),B) & E = k2_polynom2(A,k2_triang_1(A,k1_finsub_1(k1_zfmisc_1(A),k1_polynom2(A,B),C),k1_yellow_1(A)),B) ) => k9_wsierp_1(D) = k9_wsierp_1(E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_pboole,d1_wellord2,t7_wellord2,t107_orders_1,t133_orders_1,t134_orders_1,t134_orders_1,t134_orders_1,d2_triang_1,d2_triang_1,t44_finseq_1,t20_finseq_1,t64_relat_1,t62_relat_1,d8_seqm_3,t1_xboole_1,t4_funct_2,t45_relat_1,t1_xboole_1,d4_finseq_1,t27_finseq_2,t79_xboole_1,t4_xboole_1,t39_xboole_1,t35_finseq_1,t9_triang_1,t9_triang_1,t53_card_2,t9_triang_1,t31_finseq_3,t8_triang_1,d2_triang_1,t8_triang_1,t8_triang_1,t98_finseq_3,t4_vectsp_9,t4_bagorder,t46_relat_1,d3_finseq_1,t68_finseq_2,t12_funct_1,d4_xboole_0,d7_polynom1,t23_funct_1,t70_finseq_2,t9_funct_1,t10_finseqop,t105_rvsum_1,t111_rvsum_1,t22_rfinseq]), [file(bagorder,t13_bagorder),interesting(0.33)]). fof(t35_bagorder,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [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)) ) => ( v2_bagorder(B,A) => ( r1_tarski(u1_orders_2(k9_bagorder(A)),B) & v2_wellord1(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t20_relat_1,d13_bagorder,d13_bagorder,d5_polynom1,d6_polynom1,d13_polynom1,t11_xreal_1,d3_binarith,t3_pboole,d7_bagorder,d7_bagorder,t57_polynom1,d3_relat_1,d3_dickson,t34_bagorder,t33_bagorder,t50_dickson,d7_bagorder,t92_orders_1,t97_orders_1,d14_relat_2,t17_dickson,d2_wellfnd1,t5_wellord1,d4_wellord1]), [file(bagorder,t35_bagorder),interesting(0.33)]). fof(t37_bagorder,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & v16_waybel_0(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,k5_finsub_1(u1_struct_0(A))) => ~ ( B != k1_xboole_0 & r2_hidden(k4_tarski(B,k1_xboole_0),k3_tarski(k2_relat_1(k12_bagorder(A)))) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_finsub_1,t36_bagorder]), [file(bagorder,t37_bagorder),interesting(0.31)]). fof(t39_bagorder,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & v16_waybel_0(A) & l1_orders_2(A) ) => ( v1_partfun1(k3_tarski(k2_relat_1(k12_bagorder(A))),k5_finsub_1(u1_struct_0(A)),k5_finsub_1(u1_struct_0(A))) & v1_relat_2(k3_tarski(k2_relat_1(k12_bagorder(A)))) & v4_relat_2(k3_tarski(k2_relat_1(k12_bagorder(A)))) & v8_relat_2(k3_tarski(k2_relat_1(k12_bagorder(A)))) & m2_relset_1(k3_tarski(k2_relat_1(k12_bagorder(A))),k5_finsub_1(u1_struct_0(A)),k5_finsub_1(u1_struct_0(A))) ) ) ), inference(mizar_proof,[status(thm)],[d16_bagorder,d4_tarski,t12_relset_1,d3_tarski,d1_relset_1,d5_finsub_1,d16_bagorder,d5_funct_1,t59_card_2,d4_tarski,d4_tarski,t38_bagorder,l55_bagorder,t36_bagorder,s1_nat_1,t74_card_1,d5_card_1,d1_relat_2,d5_finsub_1,t59_card_2,t37_bagorder,t37_bagorder,t13_orders_1,t36_bagorder,t38_bagorder,l55_bagorder,d1_tarski,d15_bagorder,d3_tarski,t45_xboole_1,d1_tarski,d15_bagorder,d3_tarski,t45_xboole_1,t36_bagorder,t36_bagorder,s1_nat_1,t74_card_1,d5_card_1,d4_relat_2,t59_card_2,t36_bagorder,t36_bagorder,t14_orders_1,t36_bagorder,t13_orders_1,t36_bagorder,t36_bagorder,t36_bagorder,t38_bagorder,l55_bagorder,d5_finsub_1,t36_xboole_1,t1_xboole_1,d5_finsub_1,d5_finsub_1,t36_xboole_1,t1_xboole_1,d5_finsub_1,t36_bagorder,t36_bagorder,t36_bagorder,s1_nat_1,d5_finsub_1,t74_card_1,d5_card_1,d8_relat_2,t98_orders_1,d4_partfun1,d9_relat_2,d12_relat_2,d16_relat_2]), [file(bagorder,t39_bagorder),interesting(0.31)]). fof(t11_bagorder,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ~ ( v1_wellfnd1(A) & v1_bagorder(B,A) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & r1_xreal_0(C,D) & k8_funct_2(k5_numbers,u1_struct_0(A),B,C) != k8_funct_2(k5_numbers,u1_struct_0(A),B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_wellfnd1,d1_funct_2,t12_relset_1,d3_wellord1,d7_xboole_0,d5_funct_1,d5_real_1,t10_bagorder,d1_wellord1,t12_funct_1,d3_xboole_0]), [file(bagorder,t11_bagorder),interesting(0.30)]). fof(t7_bagorder,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( ( v1_finset_1(B) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) => ~ ( B != k1_xboole_0 & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ ( r2_hidden(C,B) & r2_waybel_4(B,C,u1_orders_2(A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_orders_2,d6_orders_2,d1_tarski,d1_tarski,d24_waybel_4,d1_tarski,d2_xboole_0,d2_xboole_0,t106_zfmisc_1,d8_relat_2,d4_relat_2,d24_waybel_4,d1_tarski,d2_xboole_0,d24_waybel_4,d2_xboole_0,d2_xboole_0,d24_waybel_4,d1_tarski,t106_zfmisc_1,d4_relat_2,d2_xboole_0,d24_waybel_4,d2_xboole_0,d2_xboole_0,d24_waybel_4,d1_tarski,d2_xboole_0,d24_waybel_4,s2_finset_1]), [file(bagorder,t7_bagorder),interesting(0.28)]). fof(t8_bagorder,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( ( v1_finset_1(B) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) => ~ ( B != k1_xboole_0 & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ ( r2_hidden(C,B) & r4_waybel_4(B,C,u1_orders_2(A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_orders_2,d6_orders_2,d1_tarski,d1_tarski,d26_waybel_4,d1_tarski,d2_xboole_0,d2_xboole_0,t106_zfmisc_1,d8_relat_2,d4_relat_2,d26_waybel_4,d1_tarski,d2_xboole_0,d26_waybel_4,d2_xboole_0,d2_xboole_0,d26_waybel_4,d1_tarski,t106_zfmisc_1,d4_relat_2,d2_xboole_0,d26_waybel_4,d2_xboole_0,d2_xboole_0,d26_waybel_4,d1_tarski,d2_xboole_0,d26_waybel_4,s2_finset_1]), [file(bagorder,t8_bagorder),interesting(0.28)]). fof(t6_bagorder,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m1_pboole(C,A) => ! [D] : ( m1_pboole(D,A) => ( r6_pboole(A,C,D) <=> ( r6_pboole(k5_binarith(k1_nat_1(B,1),0),k1_bagorder(A,0,k1_nat_1(B,1),C),k1_bagorder(A,0,k1_nat_1(B,1),D)) & r6_pboole(k5_binarith(A,k1_nat_1(B,1)),k1_bagorder(A,k1_nat_1(B,1),A,C),k1_bagorder(A,k1_nat_1(B,1),A,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t39_binarith,d1_bagorder,d1_bagorder,t11_xreal_1,d3_binarith,t2_xreal_1,t11_xreal_1,d3_binarith,t92_real_1,t1_euler_1,d1_bagorder,d1_bagorder,d3_binarith,t30_axioms,t1_euler_1,t3_pboole]), [file(bagorder,t6_bagorder),interesting(0.26)]). fof(t32_bagorder,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ( v1_partfun1(C,k14_polynom1(k1_nat_1(A,1)),k14_polynom1(k1_nat_1(A,1))) & v1_relat_2(C) & v4_relat_2(C) & v8_relat_2(C) & m2_relset_1(C,k14_polynom1(k1_nat_1(A,1)),k14_polynom1(k1_nat_1(A,1))) ) => ! [D] : ( ( v1_partfun1(D,k14_polynom1(k5_binarith(B,k1_nat_1(A,1))),k14_polynom1(k5_binarith(B,k1_nat_1(A,1)))) & v1_relat_2(D) & v4_relat_2(D) & v8_relat_2(D) & m2_relset_1(D,k14_polynom1(k5_binarith(B,k1_nat_1(A,1))),k14_polynom1(k5_binarith(B,k1_nat_1(A,1)))) ) => ( ( v2_bagorder(C,k1_nat_1(A,1)) & v2_bagorder(D,k5_binarith(B,k1_nat_1(A,1))) ) => v2_bagorder(k8_bagorder(A,B,C,D),B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t2_jordan3,d7_bagorder,d14_polynom1,d14_polynom1,d14_polynom1,d7_relat_2,d12_bagorder,d12_bagorder,d7_relat_2,d12_bagorder,d7_relat_2,d12_bagorder,d12_bagorder,d12_bagorder,d12_bagorder,d7_relat_2,t17_bagorder,d7_bagorder,d12_bagorder,t17_bagorder,d7_bagorder,d12_bagorder,d7_bagorder,t18_bagorder,t18_bagorder,t52_polynom1,t52_polynom1,t18_bagorder,t18_bagorder,d12_bagorder,d7_bagorder,t18_bagorder,t18_bagorder,t18_bagorder,t18_bagorder,d12_bagorder,d12_bagorder,d7_bagorder]), [file(bagorder,t32_bagorder),interesting(0.16)]). 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) ) ) ) ) ), file(polynom1,t51_polynom1), [interesting(0.00)]). fof(d1_wellord2,definition,( ! [A,B] : ( v1_relat_1(B) => ( B = k1_wellord2(A) <=> ( k3_relat_1(B) = A & ! [C,D] : ( ( r2_hidden(C,A) & r2_hidden(D,A) ) => ( r2_hidden(k4_tarski(C,D),B) <=> r1_tarski(C,D) ) ) ) ) ) ), file(wellord2,d1_wellord2), [interesting(0.00)]). fof(t7_wellord2,theorem,( ! [A] : ( v3_ordinal1(A) => v2_wellord1(k1_wellord2(A)) ) ), file(wellord2,t7_wellord2), [interesting(0.00)]). fof(t107_orders_1,theorem,( ! [A] : ( v1_relat_1(A) => ( v2_wellord1(A) => ( v1_orders_1(A) & v2_orders_1(A) & v3_orders_1(A) ) ) ) ), file(orders_1,t107_orders_1), [interesting(0.00)]). fof(t133_orders_1,theorem,( ! [A] : ( v1_relat_1(A) => ( v3_orders_1(A) => r3_orders_1(A,k3_relat_1(A)) ) ) ), file(orders_1,t133_orders_1), [interesting(0.00)]). fof(d4_bagorder,definition,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( ( v7_seqm_3(B) & v1_polynom1(B) & m1_pboole(B,A) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( C = k3_bagorder(A,B) <=> ? [D] : ( m2_finseq_1(D,k5_numbers) & C = k9_wsierp_1(D) & D = k2_polynom2(A,k2_triang_1(A,k1_polynom2(A,B),k1_yellow_1(A)),B) ) ) ) ) ) ), file(bagorder,d4_bagorder), [interesting(0.00)]). fof(t27_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( ~ v1_xboole_0(B) & m1_subset_1(B,k1_zfmisc_1(A)) ) => ! [C] : ( m2_finseq_1(C,B) => m2_finseq_1(C,A) ) ) ) ), file(finseq_2,t27_finseq_2), [interesting(0.00)]). fof(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(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)) ) ) ), file(polynom1,t42_polynom1), [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(t20_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( r1_tarski(k2_relat_1(B),k1_relat_1(A)) => ( v1_relat_1(k5_relat_1(B,A)) & v1_funct_1(k5_relat_1(B,A)) & v1_finseq_1(k5_relat_1(B,A)) ) ) ) ) ), file(finseq_1,t20_finseq_1), [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(t45_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => r1_tarski(k2_relat_1(k5_relat_1(A,B)),k2_relat_1(B)) ) ) ), file(relat_1,t45_relat_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(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_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(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(t44_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k2_relat_1(k7_finseq_1(A,B)) = k2_xboole_0(k2_relat_1(A),k2_relat_1(B)) ) ) ), file(finseq_1,t44_finseq_1), [interesting(0.00)]). fof(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(t62_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ( k5_relat_1(k1_xboole_0,A) = k1_xboole_0 & k5_relat_1(A,k1_xboole_0) = k1_xboole_0 ) ) ), file(relat_1,t62_relat_1), [interesting(0.00)]). fof(t4_funct_2,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r1_tarski(k2_relat_1(B),A) => ( v1_funct_1(B) & v1_funct_2(B,k1_relat_1(B),A) & m2_relset_1(B,k1_relat_1(B),A) ) ) ) ), file(funct_2,t4_funct_2), [interesting(0.00)]). fof(t79_xboole_1,theorem,( ! [A,B] : r1_xboole_0(k4_xboole_0(A,B),B) ), file(xboole_1,t79_xboole_1), [interesting(0.00)]). fof(t4_xboole_1,theorem,( ! [A,B,C] : k2_xboole_0(k2_xboole_0(A,B),C) = k2_xboole_0(A,k2_xboole_0(B,C)) ), file(xboole_1,t4_xboole_1), [interesting(0.00)]). fof(t39_xboole_1,theorem,( ! [A,B] : k2_xboole_0(A,k4_xboole_0(B,A)) = k2_xboole_0(A,B) ), file(xboole_1,t39_xboole_1), [interesting(0.00)]). fof(t35_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k3_finseq_1(k7_finseq_1(A,B)) = k1_nat_1(k3_finseq_1(A),k3_finseq_1(B)) ) ) ), file(finseq_1,t35_finseq_1), [interesting(0.00)]). fof(t9_triang_1,theorem,( ! [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) => k3_finseq_1(k2_triang_1(A,B,C)) = k1_card_1(B) ) ) ) ), file(triang_1,t9_triang_1), [interesting(0.00)]). fof(t53_card_2,theorem,( ! [A] : ( v1_finset_1(A) => ! [B] : ( v1_finset_1(B) => ( r1_xboole_0(A,B) => k4_card_1(k2_xboole_0(A,B)) = k1_nat_1(k4_card_1(A),k4_card_1(B)) ) ) ) ), file(card_2,t53_card_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(t8_triang_1,theorem,( ! [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) => v2_funct_1(k2_triang_1(A,B,C)) ) ) ) ), file(triang_1,t8_triang_1), [interesting(0.00)]). fof(t98_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) ) => ( ( r1_xboole_0(k2_relat_1(A),k2_relat_1(B)) & v2_funct_1(A) & v2_funct_1(B) ) <=> v2_funct_1(k7_finseq_1(A,B)) ) ) ) ), file(finseq_3,t98_finseq_3), [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(t6_rfinseq,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) => ( r1_rfinseq(A,B) <=> ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k1_relat_1(A),k1_relat_1(A)) & v3_funct_2(C,k1_relat_1(A),k1_relat_1(A)) & m2_relset_1(C,k1_relat_1(A),k1_relat_1(A)) & A = k5_relat_1(C,B) ) ) ) ) ) ), file(rfinseq,t6_rfinseq), [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(t4_bagorder,theorem,( ! [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) ) => ( ( k1_relat_1(A) = k1_relat_1(B) & r1_tarski(k2_relat_1(A),k1_relat_1(C)) & r1_tarski(k2_relat_1(B),k1_relat_1(C)) & r1_rfinseq(A,B) ) => r1_rfinseq(k5_relat_1(A,C),k5_relat_1(B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t6_rfinseq,t46_relat_1,t46_relat_1,t55_relat_1,t6_rfinseq]), [file(bagorder,t4_bagorder),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(t12_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r2_hidden(A,k1_relat_1(B)) => r2_hidden(k1_funct_1(B,A),k2_relat_1(B)) ) ) ), file(funct_1,t12_funct_1), [interesting(0.00)]). fof(d4_xboole_0,definition,( ! [A,B,C] : ( C = k4_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & ~ r2_hidden(D,B) ) ) ) ), file(xboole_0,d4_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_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(B)) => k1_funct_1(k5_relat_1(B,C),A) = k1_funct_1(C,k1_funct_1(B,A)) ) ) ) ), file(funct_1,t23_funct_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(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(t10_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_1(C,A) => ! [D] : ( m2_finseq_1(D,A) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => k5_finseqop(A,B,k8_finseq_1(A,C,D),E) = k8_finseq_1(B,k5_finseqop(A,B,C,E),k5_finseqop(A,B,D,E)) ) ) ) ) ) ), file(finseqop,t10_finseqop), [interesting(0.00)]). fof(t105_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k15_rvsum_1(k8_finseq_1(k1_numbers,A,B)) = k9_binop_2(k15_rvsum_1(A),k15_rvsum_1(B)) ) ) ), file(rvsum_1,t105_rvsum_1), [interesting(0.00)]). fof(t111_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k15_rvsum_1(k4_finseqop(k1_numbers,A,0)) = 0 ) ), file(rvsum_1,t111_rvsum_1), [interesting(0.00)]). fof(t22_rfinseq,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => ( r1_rfinseq(A,B) => k15_rvsum_1(A) = k15_rvsum_1(B) ) ) ) ), file(rfinseq,t22_rfinseq), [interesting(0.00)]). fof(t2_integra5,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => ( k3_finseq_1(A) = k3_finseq_1(B) => ( k3_finseq_1(k3_rvsum_1(A,B)) = k3_finseq_1(A) & k3_finseq_1(k7_rvsum_1(A,B)) = k3_finseq_1(A) & k15_rvsum_1(k3_rvsum_1(A,B)) = k9_binop_2(k15_rvsum_1(A),k15_rvsum_1(B)) & k15_rvsum_1(k7_rvsum_1(A,B)) = k10_binop_2(k15_rvsum_1(A),k15_rvsum_1(B)) ) ) ) ) ), file(integra5,t2_integra5), [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(t26_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => ! [C] : ( m2_finseq_1(C,k1_numbers) => ( r2_hidden(A,k4_finseq_1(k3_rvsum_1(B,C))) => k2_seq_1(k5_numbers,k1_numbers,k3_rvsum_1(B,C),A) = k9_binop_2(k2_seq_1(k5_numbers,k1_numbers,B,A),k2_seq_1(k5_numbers,k1_numbers,C,A)) ) ) ) ) ), file(rvsum_1,t26_rvsum_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(d1_xboole_0,definition,( ! [A] : ( A = k1_xboole_0 <=> ! [B] : ~ r2_hidden(B,A) ) ), file(xboole_0,d1_xboole_0), [interesting(0.00)]). fof(t56_polynom1,theorem,( ! [A,B] : k8_polynom1(k16_polynom1(A),B) = 0 ), file(polynom1,t56_polynom1), [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(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(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(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) ) ) ) ) ), file(polynom1,t49_polynom1), [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(d7_relat_2,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r7_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) ) ) ) ), file(relat_2,d7_relat_2), [interesting(0.00)]). fof(d7_bagorder,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)) ) => ( v2_bagorder(B,A) <=> ( r7_relat_2(B,k14_polynom1(A)) & ! [C] : ( ( v7_seqm_3(C) & v1_polynom1(C) & m1_pboole(C,A) ) => r2_hidden(k4_tarski(k16_polynom1(A),C),B) ) & ! [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(k4_tarski(C,D),B) => r2_hidden(k4_tarski(k9_polynom1(A,C,E),k9_polynom1(A,D,E)),B) ) ) ) ) ) ) ) ) ), file(bagorder,d7_bagorder), [interesting(0.00)]). 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) ) ) ), file(polynom1,t64_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(t8_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,B) <=> r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t8_xreal_1), [interesting(0.00)]). fof(d5_real_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) <=> ~ ( r1_xreal_0(B,A) & B != A ) ) ) ) ), file(real_1,d5_real_1), [interesting(0.00)]). fof(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(d4_wellord1,definition,( ! [A] : ( v1_relat_1(A) => ( v2_wellord1(A) <=> ( v1_relat_2(A) & v8_relat_2(A) & v4_relat_2(A) & v6_relat_2(A) & v1_wellord1(A) ) ) ) ), file(wellord1,d4_wellord1), [interesting(0.00)]). fof(t100_orders_1,theorem,( ! [A,B] : ( ( v1_relat_2(B) & v4_relat_2(B) & v8_relat_2(B) & v1_partfun1(B,A,A) & m2_relset_1(B,A,A) ) => k3_relat_1(B) = A ) ), file(orders_1,t100_orders_1), [interesting(0.00)]). fof(t5_wellord1,theorem,( ! [A] : ( v1_relat_1(A) => ( v1_wellord1(A) <=> r1_wellord1(A,k3_relat_1(A)) ) ) ), file(wellord1,t5_wellord1), [interesting(0.00)]). fof(d2_wellfnd1,definition,( ! [A] : ( l1_orders_2(A) => ( v1_wellfnd1(A) <=> r1_wellord1(u1_orders_2(A),u1_struct_0(A)) ) ) ), file(wellfnd1,d2_wellfnd1), [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(t8_card_4,theorem,( ! [A] : ( v3_ordinal1(A) => ( ~ v1_finset_1(A) <=> r1_ordinal1(k5_ordinal2,A) ) ) ), file(card_4,t8_card_4), [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(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(t14_funcop_1,theorem,( ! [A,B] : ( A != k1_xboole_0 => k2_relat_1(k2_funcop_1(A,B)) = k1_tarski(B) ) ), file(funcop_1,t14_funcop_1), [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(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [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(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(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(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(s3_funct_2,theorem, ( ! [A] : ( m1_subset_1(A,f1_s3_funct_2) => ? [B] : ( m1_subset_1(B,f2_s3_funct_2) & p1_s3_funct_2(A,B) ) ) => ? [A] : ( v1_funct_1(A) & v1_funct_2(A,f1_s3_funct_2,f2_s3_funct_2) & m2_relset_1(A,f1_s3_funct_2,f2_s3_funct_2) & ! [B] : ( m1_subset_1(B,f1_s3_funct_2) => p1_s3_funct_2(B,k8_funct_2(f1_s3_funct_2,f2_s3_funct_2,A,B)) ) ) ), file(funct_2,s3_funct_2), [interesting(0.00)]). fof(d7_wellfnd1,definition,( ! [A] : ( l1_orders_2(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v3_wellfnd1(B,A) <=> ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( k8_funct_2(k5_numbers,u1_struct_0(A),B,k1_nat_1(C,1)) != k8_funct_2(k5_numbers,u1_struct_0(A),B,C) & r2_hidden(k4_tarski(k8_funct_2(k5_numbers,u1_struct_0(A),B,k1_nat_1(C,1)),k8_funct_2(k5_numbers,u1_struct_0(A),B,C)),u1_orders_2(A)) ) ) ) ) ) ), file(wellfnd1,d7_wellfnd1), [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(t30_axioms,theorem,( ! [A] : ( v4_ordinal2(A) => A = a_1_0_axioms(A) ) ), file(axioms,t30_axioms), [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(t15_wellfnd1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_orders_2(A) ) => ( v1_wellfnd1(A) <=> ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ~ v3_wellfnd1(B,A) ) ) ) ), file(wellfnd1,t15_wellfnd1), [interesting(0.00)]). fof(d8_bagorder,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 = k4_bagorder(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) <=> ~ ( ~ r6_pboole(A,C,D) & ! [E] : ( v3_ordinal1(E) => ~ ( r2_hidden(E,A) & ~ r1_xreal_0(k8_polynom1(D,E),k8_polynom1(C,E)) & ! [F] : ( v3_ordinal1(F) => ( ( r2_hidden(E,F) & r2_hidden(F,A) ) => k8_polynom1(C,F) = k8_polynom1(D,F) ) ) ) ) ) ) ) ) ) ) ) ), file(bagorder,d8_bagorder), [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(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(t11_finseq_2,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ~ ( r2_hidden(A,k2_relat_1(B)) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ ( r2_hidden(C,k4_finseq_1(B)) & k1_funct_1(B,C) = A ) ) ) ) ), file(finseq_2,t11_finseq_2), [interesting(0.00)]). fof(s6_nat_1,theorem, ( ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( p1_s6_nat_1(A) => r1_xreal_0(A,f1_s6_nat_1) ) ) & ? [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) & p1_s6_nat_1(A) ) ) => ? [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) & p1_s6_nat_1(A) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( p1_s6_nat_1(B) => r1_xreal_0(B,A) ) ) ) ), file(nat_1,s6_nat_1), [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(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(t7_ordinal1,theorem,( ! [A,B] : ~ ( r2_hidden(A,B) & r1_tarski(B,A) ) ), file(ordinal1,t7_ordinal1), [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(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(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(t12_orders_1,theorem,( ! [A,B,C] : ( ( v1_relat_2(C) & v4_relat_2(C) & v8_relat_2(C) & v1_partfun1(C,A,A) & m2_relset_1(C,A,A) ) => ( r2_hidden(B,A) => r2_hidden(k4_tarski(B,B),C) ) ) ), file(orders_1,t12_orders_1), [interesting(0.00)]). fof(d9_bagorder,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)) ) => ( ! [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(k4_tarski(C,D),B) => r2_hidden(k4_tarski(k9_polynom1(A,C,E),k9_polynom1(A,D,E)),B) ) ) ) ) => ! [C] : ( ( v1_partfun1(C,k14_polynom1(A),k14_polynom1(A)) & v1_relat_2(C) & v4_relat_2(C) & v8_relat_2(C) & m2_relset_1(C,k14_polynom1(A),k14_polynom1(A)) ) => ( C = k5_bagorder(A,B) <=> ! [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(k4_tarski(D,E),C) <=> ~ ( r1_xreal_0(k3_bagorder(A,E),k3_bagorder(A,D)) & ~ ( k3_bagorder(A,D) = k3_bagorder(A,E) & r2_hidden(k4_tarski(D,E),B) ) ) ) ) ) ) ) ) ) ) ), file(bagorder,d9_bagorder), [interesting(0.00)]). fof(d2_finseq_2,definition,( ! [A] : ( v4_ordinal2(A) => ! [B] : k2_finseq_2(A,B) = k2_funcop_1(k2_finseq_1(A),B) ) ), file(finseq_2,d2_finseq_2), [interesting(0.00)]). fof(t115_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ~ ( ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r2_hidden(B,k4_finseq_1(A)) => r1_xreal_0(0,k2_seq_1(k5_numbers,k1_numbers,A,B)) ) ) & ? [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) & r2_hidden(B,k4_finseq_1(A)) & ~ r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,B),0) ) & r1_xreal_0(k15_rvsum_1(A),0) ) ) ), file(rvsum_1,t115_rvsum_1), [interesting(0.00)]). fof(d5_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( B = k2_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(D,k1_relat_1(A)) & C = k1_funct_1(A,D) ) ) ) ) ), file(funct_1,d5_funct_1), [interesting(0.00)]). fof(t17_funcop_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ! [C] : ( r2_hidden(C,k1_relat_1(A)) => k1_funct_1(A,C) = B ) => A = k2_funcop_1(k1_relat_1(A),B) ) ) ), file(funcop_1,t17_funcop_1), [interesting(0.00)]). fof(d15_polynom1,definition,( ! [A] : k16_polynom1(A) = k2_funcop_1(A,0) ), file(polynom1,d15_polynom1), [interesting(0.00)]). fof(t65_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ( k1_relat_1(A) = k1_xboole_0 <=> k2_relat_1(A) = k1_xboole_0 ) ) ), file(relat_1,t65_relat_1), [interesting(0.00)]). fof(t44_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => r1_tarski(k1_relat_1(k5_relat_1(A,B)),k1_relat_1(A)) ) ) ), file(relat_1,t44_relat_1), [interesting(0.00)]). fof(t3_xboole_1,theorem,( ! [A] : ( r1_tarski(A,k1_xboole_0) => A = k1_xboole_0 ) ), file(xboole_1,t3_xboole_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(t10_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ~ ( ~ r1_xreal_0(B,A) & r1_xreal_0(C,D) & r1_xreal_0(k2_xcmplx_0(B,D),k2_xcmplx_0(A,C)) ) ) ) ) ) ), file(xreal_1,t10_xreal_1), [interesting(0.00)]). fof(t2_tarski,theorem,( ! [A,B] : ( ! [C] : ( r2_hidden(C,A) <=> r2_hidden(C,B) ) => A = B ) ), file(tarski,t2_tarski), [interesting(0.00)]). fof(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(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(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(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(t11_relset_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( ( r1_tarski(k1_relat_1(C),A) & r1_tarski(k2_relat_1(C),B) ) => m2_relset_1(C,A,B) ) ) ), file(relset_1,t11_relset_1), [interesting(0.00)]). fof(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(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(t39_finseq_2,theorem,( ! [A,B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m2_finseq_1(D,B) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,B,C) & m2_relset_1(E,B,C) ) => ( D = k9_finseq_1(A) => k1_partfun1(k5_numbers,B,B,C,D,E) = k9_finseq_1(k1_funct_1(E,A)) ) ) ) ) ) ), file(finseq_2,t39_finseq_2), [interesting(0.00)]). fof(d1_finseq_1,definition,( ! [A] : ( v4_ordinal2(A) => k1_finseq_1(A) = a_1_0_finseq_1(A) ) ), file(finseq_1,d1_finseq_1), [interesting(0.00)]). fof(t60_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ~ r1_xreal_0(B,A) => m2_subset_1(k6_xcmplx_0(B,1),k1_numbers,k5_numbers) ) ) ) ), file(nat_1,t60_nat_1), [interesting(0.00)]). fof(t2_bagorder,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r2_hidden(B,k2_finseq_1(A)) <=> ( m2_subset_1(k5_real_1(B,1),k1_numbers,k5_numbers) & ~ r1_xreal_0(A,k5_real_1(B,1)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_finseq_1,t60_nat_1,t60_nat_1,t8_xreal_1,t38_nat_1,t8_xreal_1,t60_nat_1,t38_nat_1]), [file(bagorder,t2_bagorder),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(d9_relat_2,definition,( ! [A] : ( v1_relat_1(A) => ( v1_relat_2(A) <=> r1_relat_2(A,k3_relat_1(A)) ) ) ), file(relat_2,d9_relat_2), [interesting(0.00)]). fof(d16_relat_2,definition,( ! [A] : ( v1_relat_1(A) => ( v8_relat_2(A) <=> r8_relat_2(A,k3_relat_1(A)) ) ) ), file(relat_2,d16_relat_2), [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(t92_orders_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r7_relat_2(B,A) <=> ( r1_relat_2(B,A) & r6_relat_2(B,A) ) ) ) ), file(orders_1,t92_orders_1), [interesting(0.00)]). fof(d8_cqc_sim1,definition,( ! [A] : ( ( ~ v1_xboole_0(A) & m1_subset_1(A,k1_zfmisc_1(k5_numbers)) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( B = k10_cqc_sim1(A) <=> ( r2_hidden(B,A) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r2_hidden(C,A) => r1_xreal_0(B,C) ) ) ) ) ) ) ), file(cqc_sim1,d8_cqc_sim1), [interesting(0.00)]). fof(t9_partit_2,theorem,( ! [A,B] : ( m2_relset_1(B,A,A) => ( r1_relat_2(B,A) => A = k3_relat_1(B) ) ) ), file(partit_2,t9_partit_2), [interesting(0.00)]). fof(t19_ordinal1,theorem,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( v3_ordinal1(B) => ! [C] : ( v1_ordinal1(C) => ( ( r2_hidden(C,A) & r2_hidden(A,B) ) => r2_hidden(C,B) ) ) ) ) ), file(ordinal1,t19_ordinal1), [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(s1_nat_1,theorem, ( ( p1_s1_nat_1(0) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( p1_s1_nat_1(A) => p1_s1_nat_1(k1_nat_1(A,1)) ) ) ) => ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => p1_s1_nat_1(A) ) ), file(nat_1,s1_nat_1), [interesting(0.00)]). fof(d15_dickson,definition,( k11_dickson = g1_orders_2(k5_numbers,k10_dickson) ), file(dickson,d15_dickson), [interesting(0.00)]). fof(d3_bagorder,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_orders_2(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v1_bagorder(B,A) <=> ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => r2_hidden(k1_domain_1(u1_struct_0(A),u1_struct_0(A),k8_funct_2(k5_numbers,u1_struct_0(A),B,k1_nat_1(C,1)),k8_funct_2(k5_numbers,u1_struct_0(A),B,C)),u1_orders_2(A)) ) ) ) ) ), file(bagorder,d3_bagorder), [interesting(0.00)]). fof(d14_dickson,definition,( k10_dickson = a_0_0_dickson ), file(dickson,d14_dickson), [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(d3_wellord1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r1_wellord1(A,B) <=> ! [C] : ~ ( r1_tarski(C,B) & C != k1_xboole_0 & ! [D] : ~ ( r2_hidden(D,C) & r1_xboole_0(k1_wellord1(A,D),C) ) ) ) ) ), file(wellord1,d3_wellord1), [interesting(0.00)]). fof(d7_xboole_0,definition,( ! [A,B] : ( r1_xboole_0(A,B) <=> k3_xboole_0(A,B) = k1_xboole_0 ) ), file(xboole_0,d7_xboole_0), [interesting(0.00)]). fof(d5_orders_2,definition,( ! [A] : ( l1_orders_2(A) => ( v3_orders_2(A) <=> r8_relat_2(u1_orders_2(A),u1_struct_0(A)) ) ) ), file(orders_2,d5_orders_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(t10_bagorder,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v1_bagorder(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( ~ r1_xreal_0(C,D) => r2_hidden(k1_domain_1(u1_struct_0(A),u1_struct_0(A),k8_funct_2(k5_numbers,u1_struct_0(A),B,C),k8_funct_2(k5_numbers,u1_struct_0(A),B,D)),u1_orders_2(A)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_orders_2,t38_nat_1,d3_bagorder,d3_bagorder,d8_relat_2,d5_real_1,s1_nat_1]), [file(bagorder,t10_bagorder),interesting(0.00)]). fof(d1_wellord1,definition,( ! [A] : ( v1_relat_1(A) => ! [B,C] : ( C = k1_wellord1(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( D != B & r2_hidden(k4_tarski(D,B),A) ) ) ) ) ), file(wellord1,d1_wellord1), [interesting(0.00)]). fof(d3_xboole_0,definition,( ! [A,B,C] : ( C = k3_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & r2_hidden(D,B) ) ) ) ), file(xboole_0,d3_xboole_0), [interesting(0.00)]). fof(t91_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r1_tarski(A,k1_relat_1(B)) => k1_relat_1(k7_relat_1(B,A)) = A ) ) ), file(relat_1,t91_relat_1), [interesting(0.00)]). fof(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(t72_funct_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(B,A) => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ), file(funct_1,t72_funct_1), [interesting(0.00)]). fof(d5_wellord1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r2_wellord1(A,B) <=> ( r1_relat_2(A,B) & r8_relat_2(A,B) & r4_relat_2(A,B) & r6_relat_2(A,B) & r1_wellord1(A,B) ) ) ) ), file(wellord1,d5_wellord1), [interesting(0.00)]). fof(t8_wellord1,theorem,( ! [A] : ( v1_relat_1(A) => ( r2_wellord1(A,k3_relat_1(A)) <=> v2_wellord1(A) ) ) ), file(wellord1,t8_wellord1), [interesting(0.00)]). fof(s2_ordinal1,theorem, ( ! [A] : ( v3_ordinal1(A) => ( ! [B] : ( v3_ordinal1(B) => ( r2_hidden(B,A) => p1_s2_ordinal1(B) ) ) => p1_s2_ordinal1(A) ) ) => ! [A] : ( v3_ordinal1(A) => p1_s2_ordinal1(A) ) ), file(ordinal1,s2_ordinal1), [interesting(0.00)]). fof(t2_jordan3,theorem,( ! [A] : ( v4_ordinal2(A) => k5_binarith(A,0) = A ) ), file(jordan3,t2_jordan3), [interesting(0.00)]). fof(d12_bagorder,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ( v1_partfun1(C,k14_polynom1(k1_nat_1(A,1)),k14_polynom1(k1_nat_1(A,1))) & v1_relat_2(C) & v4_relat_2(C) & v8_relat_2(C) & m2_relset_1(C,k14_polynom1(k1_nat_1(A,1)),k14_polynom1(k1_nat_1(A,1))) ) => ! [D] : ( ( v1_partfun1(D,k14_polynom1(k5_binarith(B,k1_nat_1(A,1))),k14_polynom1(k5_binarith(B,k1_nat_1(A,1)))) & v1_relat_2(D) & v4_relat_2(D) & v8_relat_2(D) & m2_relset_1(D,k14_polynom1(k5_binarith(B,k1_nat_1(A,1))),k14_polynom1(k5_binarith(B,k1_nat_1(A,1)))) ) => ! [E] : ( ( v1_partfun1(E,k14_polynom1(B),k14_polynom1(B)) & v1_relat_2(E) & v4_relat_2(E) & v8_relat_2(E) & m2_relset_1(E,k14_polynom1(B),k14_polynom1(B)) ) => ( E = k8_bagorder(A,B,C,D) <=> ! [F] : ( ( v7_seqm_3(F) & v1_polynom1(F) & m1_pboole(F,B) ) => ! [G] : ( ( v7_seqm_3(G) & v1_polynom1(G) & m1_pboole(G,B) ) => ( r2_hidden(k4_tarski(F,G),E) <=> ( ( k1_bagorder(B,0,k1_nat_1(A,1),F) != k1_bagorder(B,0,k1_nat_1(A,1),G) & r2_hidden(k4_tarski(k1_bagorder(B,0,k1_nat_1(A,1),F),k1_bagorder(B,0,k1_nat_1(A,1),G)),C) ) | ( r6_pboole(k5_binarith(k1_nat_1(A,1),0),k1_bagorder(B,0,k1_nat_1(A,1),F),k1_bagorder(B,0,k1_nat_1(A,1),G)) & r2_hidden(k4_tarski(k1_bagorder(B,k1_nat_1(A,1),B,F),k1_bagorder(B,k1_nat_1(A,1),B,G)),D) ) ) ) ) ) ) ) ) ) ) ) ), file(bagorder,d12_bagorder), [interesting(0.00)]). fof(d1_bagorder,definition,( ! [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) => ! [D] : ( m1_pboole(D,A) => ! [E] : ( m1_pboole(E,k5_binarith(C,B)) => ( E = k1_bagorder(A,B,C,D) <=> ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ( r2_hidden(F,k5_binarith(C,B)) => k1_funct_1(E,F) = k1_funct_1(D,k1_nat_1(B,F)) ) ) ) ) ) ) ) ) ), file(bagorder,d1_bagorder), [interesting(0.00)]). fof(t18_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => r1_xreal_0(0,A) ) ), file(nat_1,t18_nat_1), [interesting(0.00)]). fof(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) ) ) ), file(polynom1,t62_polynom1), [interesting(0.00)]). fof(t17_bagorder,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) => r6_pboole(k5_binarith(B,A),k1_bagorder(C,A,B,k16_polynom1(C)),k16_polynom1(k5_binarith(B,A))) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_pboole,t30_axioms,d1_bagorder,t56_polynom1,d4_funct_1,t18_nat_1,d13_polynom1,t62_polynom1]), [file(bagorder,t17_bagorder),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(t18_bagorder,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) => ! [D] : ( ( v7_seqm_3(D) & v1_polynom1(D) & m1_pboole(D,C) ) => ! [E] : ( ( v7_seqm_3(E) & v1_polynom1(E) & m1_pboole(E,C) ) => r6_pboole(k5_binarith(B,A),k1_bagorder(C,A,B,k9_polynom1(C,D,E)),k9_polynom1(k5_binarith(B,A),k1_bagorder(C,A,B,D),k1_bagorder(C,A,B,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t30_axioms,d1_bagorder,d5_polynom1,d1_bagorder,d5_polynom1,t3_pboole]), [file(bagorder,t18_bagorder),interesting(0.00)]). 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) ) ) ), file(polynom1,t52_polynom1), [interesting(0.00)]). fof(t20_relat_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( r2_hidden(k4_tarski(A,B),C) => ( r2_hidden(A,k1_relat_1(C)) & r2_hidden(B,k2_relat_1(C)) ) ) ) ), file(relat_1,t20_relat_1), [interesting(0.00)]). fof(d13_bagorder,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_orders_2(B) & l1_orders_2(B) ) => ( B = k9_bagorder(A) <=> ( u1_struct_0(B) = k14_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),u1_orders_2(B)) <=> r3_polynom1(A,C,D) ) ) ) ) ) ) ) ), file(bagorder,d13_bagorder), [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(t11_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(k6_xcmplx_0(A,C),k6_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t11_xreal_1), [interesting(0.00)]). fof(d3_binarith,definition,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ( r1_xreal_0(0,k6_xcmplx_0(A,B)) => k5_binarith(A,B) = k6_xcmplx_0(A,B) ) & ( ~ r1_xreal_0(0,k6_xcmplx_0(A,B)) => k5_binarith(A,B) = 0 ) ) ) ) ), file(binarith,d3_binarith), [interesting(0.00)]). 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) ) ), file(polynom1,t57_polynom1), [interesting(0.00)]). fof(d3_relat_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ( r1_tarski(A,B) <=> ! [C,D] : ( r2_hidden(k4_tarski(C,D),A) => r2_hidden(k4_tarski(C,D),B) ) ) ) ) ), file(relat_1,d3_relat_1), [interesting(0.00)]). fof(d3_dickson,definition,( ! [A] : ( l1_orders_2(A) => ( v3_dickson(A) <=> ( v2_orders_2(A) & v3_orders_2(A) ) ) ) ), file(dickson,d3_dickson), [interesting(0.00)]). fof(d4_yellow_1,definition,( ! [A,B] : ( ( v1_yellow_1(B) & m1_pboole(B,A) ) => ! [C] : ( ( v1_orders_2(C) & l1_orders_2(C) ) => ( C = k5_yellow_1(A,B) <=> ( u1_struct_0(C) = k4_card_3(k12_pralg_1(A,B)) & ! [D] : ( m1_subset_1(D,u1_struct_0(C)) => ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => ( r2_hidden(D,k4_card_3(k12_pralg_1(A,B))) => ( r1_orders_2(C,D,E) <=> ? [F] : ( v1_relat_1(F) & v1_funct_1(F) & ? [G] : ( v1_relat_1(G) & v1_funct_1(G) & F = D & G = E & ! [H] : ~ ( r2_hidden(H,A) & ! [I] : ( l1_orders_2(I) => ! [J] : ( m1_subset_1(J,u1_struct_0(I)) => ! [K] : ( m1_subset_1(K,u1_struct_0(I)) => ~ ( I = k1_funct_1(B,H) & J = k1_funct_1(F,H) & K = k1_funct_1(G,H) & r1_orders_2(I,J,K) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(yellow_1,d4_yellow_1), [interesting(0.00)]). fof(d5_card_3,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( B = k4_card_3(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( v1_relat_1(D) & v1_funct_1(D) & C = D & k1_relat_1(D) = k1_relat_1(A) & ! [E] : ( r2_hidden(E,k1_relat_1(A)) => r2_hidden(k1_funct_1(D,E),k1_funct_1(A,E)) ) ) ) ) ) ), file(card_3,d5_card_3), [interesting(0.00)]). fof(d13_pralg_1,definition,( ! [A,B] : ( ( v2_pralg_1(B) & m1_pboole(B,A) ) => ! [C] : ( m1_pboole(C,A) => ( C = k12_pralg_1(A,B) <=> ! [D] : ~ ( r2_hidden(D,A) & ! [E] : ( l1_struct_0(E) => ~ ( E = k1_funct_1(B,D) & k1_funct_1(C,D) = u1_struct_0(E) ) ) ) ) ) ) ), file(pralg_1,d13_pralg_1), [interesting(0.00)]). fof(t41_polynom1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => r1_tarski(k11_polynom1(A),k1_relat_1(A)) ) ), file(polynom1,t41_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(d9_orders_2,definition,( ! [A] : ( l1_orders_2(A) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_orders_2(A,B,C) <=> r2_hidden(k4_tarski(B,C),u1_orders_2(A)) ) ) ) ) ), file(orders_2,d9_orders_2), [interesting(0.00)]). fof(t33_zfmisc_1,theorem,( ! [A,B,C,D] : ( k4_tarski(A,B) = k4_tarski(C,D) => ( A = C & B = D ) ) ), file(zfmisc_1,t33_zfmisc_1), [interesting(0.00)]). 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) ) ) ) ), file(polynom1,t50_polynom1), [interesting(0.00)]). fof(d2_relat_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ( A = B <=> ! [C,D] : ( r2_hidden(k4_tarski(C,D),A) <=> r2_hidden(k4_tarski(C,D),B) ) ) ) ) ), file(relat_1,d2_relat_1), [interesting(0.00)]). fof(t50_dickson,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_orders_2(A) ) => ( v3_dickson(A) => ( v4_dickson(A) <=> ! [B] : ( ( ~ v3_struct_0(B) & l1_orders_2(B) ) => ( ( v3_dickson(B) & r1_tarski(u1_orders_2(A),u1_orders_2(B)) & u1_struct_0(A) = u1_struct_0(B) ) => v1_wellfnd1(k5_dickson(B)) ) ) ) ) ) ), file(dickson,t50_dickson), [interesting(0.00)]). fof(d14_relat_2,definition,( ! [A] : ( v1_relat_1(A) => ( v6_relat_2(A) <=> r6_relat_2(A,k3_relat_1(A)) ) ) ), file(relat_2,d14_relat_2), [interesting(0.00)]). fof(t17_dickson,theorem,( ! [A] : ( l1_orders_2(A) => ( ( v1_wellfnd1(k5_dickson(A)) & v4_orders_2(A) ) => v1_wellfnd1(A) ) ) ), file(dickson,t17_dickson), [interesting(0.00)]). fof(d16_bagorder,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & v16_waybel_0(A) & l1_orders_2(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_zfmisc_1(k2_zfmisc_1(k5_finsub_1(u1_struct_0(A)),k5_finsub_1(u1_struct_0(A))))) & m2_relset_1(B,k5_numbers,k1_zfmisc_1(k2_zfmisc_1(k5_finsub_1(u1_struct_0(A)),k5_finsub_1(u1_struct_0(A))))) ) => ( B = k12_bagorder(A) <=> ( k4_relset_1(k5_numbers,k1_zfmisc_1(k2_zfmisc_1(k5_finsub_1(u1_struct_0(A)),k5_finsub_1(u1_struct_0(A)))),B) = k5_numbers & k8_funct_2(k5_numbers,k1_zfmisc_1(k2_zfmisc_1(k5_finsub_1(u1_struct_0(A)),k5_finsub_1(u1_struct_0(A)))),B,0) = a_1_0_bagorder(A) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k1_zfmisc_1(k2_zfmisc_1(k5_finsub_1(u1_struct_0(A)),k5_finsub_1(u1_struct_0(A)))),B,k1_nat_1(C,1)) = a_3_0_bagorder(A,B,C) ) ) ) ) ) ), file(bagorder,d16_bagorder), [interesting(0.00)]). fof(d4_tarski,definition,( ! [A,B] : ( B = k3_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(C,D) & r2_hidden(D,A) ) ) ) ), file(tarski,d4_tarski), [interesting(0.00)]). fof(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(d5_finsub_1,definition,( ! [A,B] : ( v4_finsub_1(B) => ( B = k5_finsub_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ( r1_tarski(C,A) & v1_finset_1(C) ) ) ) ) ), file(finsub_1,d5_finsub_1), [interesting(0.00)]). fof(t59_card_2,theorem,( ! [A] : ( k1_card_1(A) = 0 => A = k1_xboole_0 ) ), file(card_2,t59_card_2), [interesting(0.00)]). fof(t36_xboole_1,theorem,( ! [A,B] : r1_tarski(k4_xboole_0(A,B),A) ), file(xboole_1,t36_xboole_1), [interesting(0.00)]). fof(t47_card_1,theorem,( k1_card_1(k1_xboole_0) = k1_xboole_0 ), file(card_1,t47_card_1), [interesting(0.00)]). fof(d15_bagorder,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & v16_waybel_0(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,k5_finsub_1(u1_struct_0(A))) => ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( C = k11_bagorder(A,B) <=> ( r2_hidden(C,B) & r2_waybel_4(B,C,u1_orders_2(A)) ) ) ) ) ) ) ), file(bagorder,d15_bagorder), [interesting(0.00)]). fof(t63_card_2,theorem,( ! [A] : ( v1_finset_1(A) => ! [B] : ( v1_finset_1(B) => ( r1_tarski(B,A) => k4_card_1(k4_xboole_0(A,B)) = k5_real_1(k4_card_1(A),k4_card_1(B)) ) ) ) ), file(card_2,t63_card_2), [interesting(0.00)]). fof(l55_bagorder,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & v16_waybel_0(A) & l1_orders_2(A) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m1_subset_1(C,k5_finsub_1(u1_struct_0(A))) => ( k1_card_1(C) = k1_nat_1(B,1) => k1_card_1(k4_xboole_0(C,k6_domain_1(u1_struct_0(A),k11_bagorder(A,C)))) = B ) ) ) ) ), inference(mizar_proof,[status(thm)],[t47_card_1,d1_tarski,d15_bagorder,d3_tarski,t63_card_2,t50_card_1,t20_card_2]), [file(bagorder,l55_bagorder),interesting(0.00)]). fof(t36_bagorder,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & v16_waybel_0(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,k5_finsub_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k5_finsub_1(u1_struct_0(A))) => ( r2_hidden(k1_domain_1(k5_finsub_1(u1_struct_0(A)),k5_finsub_1(u1_struct_0(A)),B,C),k3_tarski(k2_relat_1(k12_bagorder(A)))) <=> ~ ( B != k1_xboole_0 & ~ ( B != k1_xboole_0 & C != k1_xboole_0 & k11_bagorder(A,B) != k11_bagorder(A,C) & r2_hidden(k1_domain_1(u1_struct_0(A),u1_struct_0(A),k11_bagorder(A,B),k11_bagorder(A,C)),u1_orders_2(A)) ) & ~ ( B != k1_xboole_0 & C != k1_xboole_0 & k11_bagorder(A,B) = k11_bagorder(A,C) & r2_hidden(k4_tarski(k4_xboole_0(B,k6_domain_1(u1_struct_0(A),k11_bagorder(A,B))),k4_xboole_0(C,k6_domain_1(u1_struct_0(A),k11_bagorder(A,C)))),k3_tarski(k2_relat_1(k12_bagorder(A)))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d16_bagorder,d16_bagorder,d4_tarski,d5_funct_1,t33_zfmisc_1,t60_nat_1,d16_bagorder,t33_zfmisc_1,d5_funct_1,d4_tarski,d5_funct_1,d4_tarski,d5_funct_1,d4_tarski,d4_tarski,d5_funct_1,d16_bagorder,d5_funct_1,d4_tarski]), [file(bagorder,t36_bagorder),interesting(0.00)]). fof(t74_card_1,theorem,( ! [A] : ~ ( v1_finset_1(A) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ~ r2_wellord2(A,B) ) ) ), file(card_1,t74_card_1), [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(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(t18_finsub_1,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & v4_finsub_1(A) ) => r2_hidden(k1_xboole_0,A) ) ), file(finsub_1,t18_finsub_1), [interesting(0.00)]). fof(t13_orders_1,theorem,( ! [A,B,C,D] : ( ( v1_relat_2(D) & v4_relat_2(D) & v8_relat_2(D) & v1_partfun1(D,A,A) & m2_relset_1(D,A,A) ) => ( ( r2_hidden(B,A) & r2_hidden(C,A) & r2_hidden(k4_tarski(B,C),D) & r2_hidden(k4_tarski(C,B),D) ) => B = C ) ) ), file(orders_1,t13_orders_1), [interesting(0.00)]). fof(t45_xboole_1,theorem,( ! [A,B] : ( r1_tarski(A,B) => B = k2_xboole_0(A,k4_xboole_0(B,A)) ) ), file(xboole_1,t45_xboole_1), [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(t14_orders_1,theorem,( ! [A,B,C,D,E] : ( ( v1_relat_2(E) & v4_relat_2(E) & v8_relat_2(E) & v1_partfun1(E,A,A) & m2_relset_1(E,A,A) ) => ( ( r2_hidden(B,A) & r2_hidden(C,A) & r2_hidden(D,A) & r2_hidden(k4_tarski(B,C),E) & r2_hidden(k4_tarski(C,D),E) ) => r2_hidden(k4_tarski(B,D),E) ) ) ), file(orders_1,t14_orders_1), [interesting(0.00)]). fof(t98_orders_1,theorem,( ! [A,B] : ( m2_relset_1(B,A,A) => ( r1_relat_2(B,A) => ( k4_relset_1(A,A,B) = A & k3_relat_1(B) = A ) ) ) ), file(orders_1,t98_orders_1), [interesting(0.00)]). fof(d4_partfun1,definition,( ! [A,B,C] : ( m2_relset_1(C,A,B) => ( v1_partfun1(C,A,B) <=> k4_relset_1(A,B,C) = A ) ) ), file(partfun1,d4_partfun1), [interesting(0.00)]). fof(d19_bagorder,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v16_waybel_0(A) & l1_orders_2(A) ) => ! [B] : ( ~ v1_xboole_0(B) => ( ( v1_wellfnd1(A) & r1_tarski(B,u1_struct_0(A)) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( C = k15_bagorder(A,B) <=> ( r2_hidden(C,B) & r4_waybel_4(B,C,u1_orders_2(A)) ) ) ) ) ) ) ), file(bagorder,d19_bagorder), [interesting(0.00)]). fof(d11_dickson,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( k1_relat_1(A) = k5_numbers & r2_hidden(B,k2_relat_1(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( C = k7_dickson(A,B) <=> ( k1_funct_1(A,C) = B & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( k1_funct_1(A,D) = B => r1_xreal_0(C,D) ) ) ) ) ) ) ) ), file(dickson,d11_dickson), [interesting(0.00)]). fof(t40_bagorder,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & v16_waybel_0(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k14_bagorder(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k14_bagorder(A))) => ( r2_hidden(k1_domain_1(u1_struct_0(k14_bagorder(A)),u1_struct_0(k14_bagorder(A)),B,C),u1_orders_2(k14_bagorder(A))) <=> ? [D] : ( m1_subset_1(D,k5_finsub_1(u1_struct_0(A))) & ? [E] : ( m1_subset_1(E,k5_finsub_1(u1_struct_0(A))) & B = D & C = E & ~ ( D != k1_xboole_0 & ~ ( D != k1_xboole_0 & E != k1_xboole_0 & k11_bagorder(A,D) != k11_bagorder(A,E) & r2_hidden(k1_domain_1(u1_struct_0(A),u1_struct_0(A),k11_bagorder(A,D),k11_bagorder(A,E)),u1_orders_2(A)) ) & ~ ( D != k1_xboole_0 & E != k1_xboole_0 & k11_bagorder(A,D) = k11_bagorder(A,E) & r2_hidden(k4_tarski(k4_xboole_0(D,k6_domain_1(u1_struct_0(A),k11_bagorder(A,D))),k4_xboole_0(E,k6_domain_1(u1_struct_0(A),k11_bagorder(A,E)))),k13_bagorder(A)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t36_bagorder,t36_bagorder]), [file(bagorder,t40_bagorder),interesting(0.00)]). fof(d26_waybel_4,definition,( ! [A,B,C] : ( v1_relat_1(C) => ( r4_waybel_4(A,B,C) <=> ( r2_hidden(B,A) & ! [D] : ~ ( r2_hidden(D,A) & D != B & r2_hidden(k4_tarski(D,B),C) ) ) ) ) ), file(waybel_4,d26_waybel_4), [interesting(0.00)]). fof(t28_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ~ ( r1_xreal_0(A,B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => B != k2_xcmplx_0(A,C) ) ) ) ) ), file(nat_1,t28_nat_1), [interesting(0.00)]). fof(d20_bagorder,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_orders_2(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => ( D = k16_bagorder(A,B,C) <=> ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,u1_struct_0(A),D,E) = k8_funct_2(k5_numbers,u1_struct_0(A),B,k1_nat_1(E,C)) ) ) ) ) ) ) ), file(bagorder,d20_bagorder), [interesting(0.00)]). fof(t46_zfmisc_1,theorem,( ! [A,B] : ( r2_hidden(A,B) => k2_xboole_0(k1_tarski(A),B) = B ) ), file(zfmisc_1,t46_zfmisc_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(s2_recdef_1,theorem, ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,f1_s2_recdef_1) => ? [C] : ( m1_subset_1(C,f1_s2_recdef_1) & p1_s2_recdef_1(A,B,C) ) ) ) => ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,f1_s2_recdef_1) & m2_relset_1(A,k5_numbers,f1_s2_recdef_1) & k8_funct_2(k5_numbers,f1_s2_recdef_1,A,0) = f2_s2_recdef_1 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => p1_s2_recdef_1(B,k8_funct_2(k5_numbers,f1_s2_recdef_1,A,B),k8_funct_2(k5_numbers,f1_s2_recdef_1,A,k1_nat_1(B,1))) ) ) ), file(recdef_1,s2_recdef_1), [interesting(0.00)]). fof(s2_funct_2,theorem, ( ! [A] : ( r2_hidden(A,f1_s2_funct_2) => r2_hidden(f3_s2_funct_2(A),f2_s2_funct_2) ) => ? [A] : ( v1_funct_1(A) & v1_funct_2(A,f1_s2_funct_2,f2_s2_funct_2) & m2_relset_1(A,f1_s2_funct_2,f2_s2_funct_2) & ! [B] : ( r2_hidden(B,f1_s2_funct_2) => k1_funct_1(A,B) = f3_s2_funct_2(B) ) ) ), file(funct_2,s2_funct_2), [interesting(0.00)]). fof(d1_mcart_1,definition,( ! [A] : ( ? [B,C] : A = k4_tarski(B,C) => ! [B] : ( B = k1_mcart_1(A) <=> ! [C,D] : ( A = k4_tarski(C,D) => B = C ) ) ) ), file(mcart_1,d1_mcart_1), [interesting(0.00)]). fof(d2_mcart_1,definition,( ! [A] : ( ? [B,C] : A = k4_tarski(B,C) => ! [B] : ( B = k2_mcart_1(A) <=> ! [C,D] : ( A = k4_tarski(C,D) => B = D ) ) ) ), file(mcart_1,d2_mcart_1), [interesting(0.00)]). fof(d24_waybel_4,definition,( ! [A,B,C] : ( v1_relat_1(C) => ( r2_waybel_4(A,B,C) <=> ( r2_hidden(B,A) & ! [D] : ~ ( r2_hidden(D,A) & D != B & r2_hidden(k4_tarski(B,D),C) ) ) ) ) ), file(waybel_4,d24_waybel_4), [interesting(0.00)]). fof(d29_waybel_0,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_orders_2(A) ) => ( v16_waybel_0(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_orders_2(A,B,C) | r1_orders_2(A,C,B) ) ) ) ) ) ), file(waybel_0,d29_waybel_0), [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(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(t92_real_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( ( ( r1_xreal_0(A,B) & r1_xreal_0(C,D) ) => r1_xreal_0(k6_xcmplx_0(A,D),k6_xcmplx_0(B,C)) ) & ~ ( ( ( ~ r1_xreal_0(B,A) & r1_xreal_0(C,D) ) | ( r1_xreal_0(A,B) & ~ r1_xreal_0(D,C) ) ) & r1_xreal_0(k6_xcmplx_0(B,C),k6_xcmplx_0(A,D)) ) ) ) ) ) ) ), file(real_1,t92_real_1), [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(d6_orders_2,definition,( ! [A] : ( l1_orders_2(A) => ( v4_orders_2(A) <=> r4_relat_2(u1_orders_2(A),u1_struct_0(A)) ) ) ), file(orders_2,d6_orders_2), [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(s2_finset_1,theorem, ( ( v1_finset_1(f1_s2_finset_1) & p1_s2_finset_1(k1_xboole_0) & ! [A,B] : ( ( r2_hidden(A,f1_s2_finset_1) & r1_tarski(B,f1_s2_finset_1) & p1_s2_finset_1(B) ) => p1_s2_finset_1(k2_xboole_0(B,k1_tarski(A))) ) ) => p1_s2_finset_1(f1_s2_finset_1) ), file(finset_1,s2_finset_1), [interesting(0.00)]). fof(t9_bagorder,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v3_wellfnd1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( ~ r1_xreal_0(C,D) => ( k8_funct_2(k5_numbers,u1_struct_0(A),B,D) != k8_funct_2(k5_numbers,u1_struct_0(A),B,C) & r2_hidden(k1_domain_1(u1_struct_0(A),u1_struct_0(A),k8_funct_2(k5_numbers,u1_struct_0(A),B,C),k8_funct_2(k5_numbers,u1_struct_0(A),B,D)),u1_orders_2(A)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_orders_2,d6_orders_2,t38_nat_1,d7_wellfnd1,d7_wellfnd1,d4_relat_2,d8_relat_2,d5_real_1,s1_nat_1]), [file(bagorder,t9_bagorder),interesting(0.00)]).