fof(t12_ami_2,theorem,( ! [A] : ( m2_subset_1(A,k5_numbers,k3_ami_2) => ! [B] : ( m2_subset_1(B,k5_numbers,k2_ami_2) => A != B ) ) ), inference(mizar_proof,[status(thm)],[t10_ami_2,t11_ami_2,t6_ami_2]), [file(ami_2,t12_ami_2),interesting(1.00)]). fof(t13_ami_2,theorem,( k5_card_3(0,k4_card_3(k5_ami_2)) = k3_ami_2 ), inference(mizar_proof,[status(thm)],[d1_funct_2,t22_card_3,t7_ami_2]), [file(ami_2,t13_ami_2),interesting(0.89)]). fof(t14_ami_2,theorem,( ! [A] : ( m2_subset_1(A,k5_numbers,k2_ami_2) => k5_card_3(A,k4_card_3(k5_ami_2)) = k4_numbers ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,t22_card_3,t10_ami_2]), [file(ami_2,t14_ami_2),interesting(0.84)]). fof(t15_ami_2,theorem,( ! [A] : ( m2_subset_1(A,k5_numbers,k3_ami_2) => k5_card_3(A,k4_card_3(k5_ami_2)) = k4_ami_2 ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,t22_card_3,t11_ami_2]), [file(ami_2,t15_ami_2),interesting(0.84)]). fof(t18_ami_2,theorem,( ! [A] : ( m1_subset_1(A,k4_card_3(k5_ami_2)) => ! [B] : ( m2_subset_1(B,k5_numbers,k3_ami_2) => ! [C] : ( m2_subset_1(C,k5_numbers,k3_ami_2) => k1_funct_1(k7_ami_2(A,B),C) = k1_funct_1(A,C) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_ami_2,t11_ami_2,t5_cqc_lang,t6_ami_2,d1_tarski,t12_funct_4]), [file(ami_2,t18_ami_2),interesting(0.75)]). fof(t17_ami_2,theorem,( ! [A] : ( m1_subset_1(A,k4_card_3(k5_ami_2)) => ! [B] : ( m2_subset_1(B,k5_numbers,k3_ami_2) => ! [C] : ( m2_subset_1(C,k5_numbers,k2_ami_2) => k1_funct_1(k7_ami_2(A,B),C) = k1_funct_1(A,C) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_ami_2,t10_ami_2,t5_cqc_lang,t6_ami_2,d1_tarski,t12_funct_4]), [file(ami_2,t17_ami_2),interesting(0.73)]). fof(t19_ami_2,theorem,( ! [A] : ( m1_subset_1(A,k4_card_3(k5_ami_2)) => ! [B] : ( m2_subset_1(B,k5_numbers,k2_ami_2) => ! [C] : ( v1_int_1(C) => k1_funct_1(k8_ami_2(A,B,C),0) = k1_funct_1(A,0) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_ami_2,t10_ami_2,t5_cqc_lang,t6_ami_2,d1_tarski,t12_funct_4]), [file(ami_2,t19_ami_2),interesting(0.71)]). fof(t22_ami_2,theorem,( ! [A] : ( m1_subset_1(A,k4_card_3(k5_ami_2)) => ! [B] : ( m2_subset_1(B,k5_numbers,k2_ami_2) => ! [C] : ( v1_int_1(C) => ! [D] : ( m2_subset_1(D,k5_numbers,k3_ami_2) => k1_funct_1(k8_ami_2(A,B,C),D) = k1_funct_1(A,D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_ami_2,t11_ami_2,t5_cqc_lang,t6_ami_2,d1_tarski,t12_funct_4]), [file(ami_2,t22_ami_2),interesting(0.71)]). fof(t11_ami_2,theorem,( ! [A] : ( m2_subset_1(A,k5_numbers,k3_ami_2) => k8_funct_2(k5_numbers,k2_xboole_0(k1_tarski(k4_numbers),k2_tarski(k4_ami_2,k3_ami_2)),k5_ami_2,A) = k4_ami_2 ) ), inference(mizar_proof,[status(thm)],[t22_nat_1,t9_ami_2]), [file(ami_2,t11_ami_2),interesting(0.69)]). fof(t6_ami_2,theorem, ( k3_ami_2 != k4_numbers & k4_ami_2 != k4_numbers & k3_ami_2 != k4_ami_2 ), inference(mizar_proof,[status(thm)],[t17_numbers,t27_numbers,d10_xboole_0,d2_xboole_0,d2_xboole_0,d2_xboole_0,d1_tarski,t3_ami_1,d2_int_1]), [file(ami_2,t6_ami_2),interesting(0.68)]). fof(t10_ami_2,theorem,( ! [A] : ( m2_subset_1(A,k5_numbers,k2_ami_2) => k8_funct_2(k5_numbers,k2_xboole_0(k1_tarski(k4_numbers),k2_tarski(k4_ami_2,k3_ami_2)),k5_ami_2,A) = k4_numbers ) ), inference(mizar_proof,[status(thm)],[t8_ami_2]), [file(ami_2,t10_ami_2),interesting(0.68)]). fof(t2_ami_2,theorem,( r2_hidden(k4_tarski(0,k1_xboole_0),k4_ami_2) ), inference(mizar_proof,[status(thm)],[d1_tarski,d2_xboole_0,d2_xboole_0,d2_xboole_0]), [file(ami_2,t2_ami_2),interesting(0.68)]). fof(t7_ami_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( k8_funct_2(k5_numbers,k2_xboole_0(k1_tarski(k4_numbers),k2_tarski(k4_ami_2,k3_ami_2)),k5_ami_2,A) = k3_ami_2 <=> A = 0 ) ) ), inference(mizar_proof,[status(thm)],[l10_ami_2,d5_ami_2,t6_ami_2,d5_ami_2]), [file(ami_2,t7_ami_2),interesting(0.58)]). fof(t16_ami_2,theorem,( ! [A] : ( m1_subset_1(A,k4_card_3(k5_ami_2)) => ! [B] : ( m2_subset_1(B,k5_numbers,k3_ami_2) => k1_funct_1(k7_ami_2(A,B),0) = B ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,d1_tarski,t14_funct_4,t6_cqc_lang]), [file(ami_2,t16_ami_2),interesting(0.48)]). fof(t20_ami_2,theorem,( ! [A] : ( m1_subset_1(A,k4_card_3(k5_ami_2)) => ! [B] : ( m2_subset_1(B,k5_numbers,k2_ami_2) => ! [C] : ( v1_int_1(C) => k1_funct_1(k8_ami_2(A,B,C),B) = C ) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,d1_tarski,t14_funct_4,t6_cqc_lang]), [file(ami_2,t20_ami_2),interesting(0.48)]). fof(t9_ami_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( k8_funct_2(k5_numbers,k2_xboole_0(k1_tarski(k4_numbers),k2_tarski(k4_ami_2,k3_ami_2)),k5_ami_2,A) = k4_ami_2 <=> ? [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) & A = k1_nat_1(k2_nat_1(2,B),2) ) ) ) ), inference(mizar_proof,[status(thm)],[l10_ami_2,d5_ami_2,t6_ami_2,d5_ami_2]), [file(ami_2,t9_ami_2),interesting(0.43)]). fof(t8_ami_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( k8_funct_2(k5_numbers,k2_xboole_0(k1_tarski(k4_numbers),k2_tarski(k4_ami_2,k3_ami_2)),k5_ami_2,A) = k4_numbers <=> ? [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) & A = k1_nat_1(k2_nat_1(2,B),1) ) ) ) ), inference(mizar_proof,[status(thm)],[l10_ami_2,d5_ami_2,t6_ami_2,d5_ami_2]), [file(ami_2,t8_ami_2),interesting(0.40)]). fof(t3_ami_2,theorem,( ! [A] : ( m2_subset_1(A,k5_numbers,k3_ami_2) => r2_hidden(k1_domain_1(k5_numbers,k1_zfmisc_1(k2_zfmisc_1(k5_numbers,k3_ami_2)),6,k12_finseq_1(k3_ami_2,A)),k4_ami_2) ) ), inference(mizar_proof,[status(thm)],[t10_gr_cy_1,d2_xboole_0,d2_xboole_0,d2_xboole_0]), [file(ami_2,t3_ami_2),interesting(0.40)]). fof(t21_ami_2,theorem,( ! [A] : ( m1_subset_1(A,k4_card_3(k5_ami_2)) => ! [B] : ( m2_subset_1(B,k5_numbers,k2_ami_2) => ! [C] : ( v1_int_1(C) => ! [D] : ( m2_subset_1(D,k5_numbers,k2_ami_2) => ( D != B => k1_funct_1(k8_ami_2(A,B,C),D) = k1_funct_1(A,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,d1_tarski,t12_funct_4]), [file(ami_2,t21_ami_2),interesting(0.35)]). fof(t4_ami_2,theorem,( ! [A,B] : ( m2_subset_1(B,k5_numbers,k3_ami_2) => ! [C] : ( m2_subset_1(C,k5_numbers,k2_ami_2) => ( r2_hidden(A,k7_domain_1(k5_numbers,7,8)) => r2_hidden(k4_tarski(A,k2_finseq_4(k5_numbers,B,C)),k4_ami_2) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_tarski,t10_gr_cy_1,d2_xboole_0,d2_xboole_0]), [file(ami_2,t4_ami_2),interesting(0.35)]). fof(t5_ami_2,theorem,( ! [A,B] : ( m2_subset_1(B,k5_numbers,k2_ami_2) => ! [C] : ( m2_subset_1(C,k5_numbers,k2_ami_2) => ( r2_hidden(A,k10_domain_1(k5_numbers,1,2,3,4,5)) => r2_hidden(k4_tarski(A,k2_finseq_4(k2_ami_2,B,C)),k4_ami_2) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_enumset1,t10_gr_cy_1,d2_xboole_0]), [file(ami_2,t5_ami_2),interesting(0.28)]). fof(t24_ami_2,theorem,( ! [A] : ( m2_subset_1(A,k2_zfmisc_1(k1_gr_cy_1(9),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),k5_numbers))),k4_ami_2) => ! [B] : ( m2_subset_1(B,k5_numbers,k3_ami_2) => ! [C] : ( m2_subset_1(C,k5_numbers,k1_gr_cy_1(9)) => ( A = k1_domain_1(k1_gr_cy_1(9),k1_zfmisc_1(k2_zfmisc_1(k5_numbers,k3_ami_2)),C,k12_finseq_1(k3_ami_2,B)) => k11_ami_2(A) = B ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_ami_2,t7_mcart_1,t25_finseq_4]), [file(ami_2,t24_ami_2),interesting(0.02)]). fof(t23_ami_2,theorem,( ! [A] : ( m2_subset_1(A,k2_zfmisc_1(k1_gr_cy_1(9),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),k5_numbers))),k4_ami_2) => ! [B] : ( m2_subset_1(B,k5_numbers,k2_ami_2) => ! [C] : ( m2_subset_1(C,k5_numbers,k2_ami_2) => ! [D] : ( m2_subset_1(D,k5_numbers,k1_gr_cy_1(9)) => ( A = k1_domain_1(k1_gr_cy_1(9),k1_zfmisc_1(k2_zfmisc_1(k5_numbers,k2_ami_2)),D,k2_finseq_4(k2_ami_2,B,C)) => ( k9_ami_2(A) = B & k10_ami_2(A) = C ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_ami_2,t7_mcart_1,t26_finseq_4,d10_ami_2,t7_mcart_1,t26_finseq_4]), [file(ami_2,t23_ami_2),interesting(0.01)]). fof(d2_nat_1,definition,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( C = k4_nat_1(A,B) <=> ~ ( ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ~ ( A = k2_xcmplx_0(k3_xcmplx_0(B,D),C) & ~ r1_xreal_0(B,C) ) ) & ~ ( C = 0 & B = 0 ) ) ) ) ) ) ), file(nat_1,d2_nat_1), [interesting(0.00)]). fof(l11_ami_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( ( ? [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) & A = k1_nat_1(k2_nat_1(2,B),1) ) => ( A != 0 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => A != k1_nat_1(k2_nat_1(2,B),2) ) ) ) & ( ? [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) & A = k1_nat_1(k2_nat_1(2,B),k1_nat_1(1,1)) ) => ( A != 0 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => A != k1_nat_1(k2_nat_1(2,B),1) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_nat_1,d2_nat_1,d2_nat_1,d2_nat_1]), [file(ami_2,l11_ami_2),interesting(0.00)]). fof(t1_scheme1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ~ ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( A != k2_nat_1(2,B) & A != k1_nat_1(k2_nat_1(2,B),1) ) ) ) ), file(scheme1,t1_scheme1), [interesting(0.00)]). fof(t22_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ~ ( A != 0 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => A != k1_nat_1(B,1) ) ) ) ), file(nat_1,t22_nat_1), [interesting(0.00)]). fof(l10_ami_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ~ ( A != 0 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => A != k1_nat_1(k2_nat_1(2,B),1) ) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => A != k1_nat_1(k2_nat_1(2,B),2) ) ) ) ), inference(mizar_proof,[status(thm)],[t1_scheme1,t22_nat_1]), [file(ami_2,l10_ami_2),interesting(0.00)]). fof(d5_ami_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k2_xboole_0(k1_tarski(k4_numbers),k2_tarski(k4_ami_2,k3_ami_2))) & m2_relset_1(A,k5_numbers,k2_xboole_0(k1_tarski(k4_numbers),k2_tarski(k4_ami_2,k3_ami_2))) ) => ( A = k5_ami_2 <=> ( k8_funct_2(k5_numbers,k2_xboole_0(k1_tarski(k4_numbers),k2_tarski(k4_ami_2,k3_ami_2)),A,0) = k3_ami_2 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( k8_funct_2(k5_numbers,k2_xboole_0(k1_tarski(k4_numbers),k2_tarski(k4_ami_2,k3_ami_2)),A,k1_nat_1(k2_nat_1(2,B),1)) = k4_numbers & k8_funct_2(k5_numbers,k2_xboole_0(k1_tarski(k4_numbers),k2_tarski(k4_ami_2,k3_ami_2)),A,k1_nat_1(k2_nat_1(2,B),2)) = k4_ami_2 ) ) ) ) ) ), file(ami_2,d5_ami_2), [interesting(0.00)]). fof(t17_numbers,theorem,( r1_tarski(k5_numbers,k4_numbers) ), file(numbers,t17_numbers), [interesting(0.00)]). fof(t27_numbers,theorem,( k5_numbers != k4_numbers ), file(numbers,t27_numbers), [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(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(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [interesting(0.00)]). fof(t3_ami_1,theorem,( ! [A,B] : 2 != k4_tarski(A,B) ), file(ami_1,t3_ami_1), [interesting(0.00)]). fof(d2_int_1,definition,( ! [A] : ( v1_int_1(A) <=> r2_hidden(A,k4_numbers) ) ), file(int_1,d2_int_1), [interesting(0.00)]). fof(d1_funct_2,definition,( ! [A,B,C] : ( m2_relset_1(C,A,B) => ( ( ( B = k1_xboole_0 => A = k1_xboole_0 ) => ( v1_funct_2(C,A,B) <=> A = k4_relset_1(A,B,C) ) ) & ( B = k1_xboole_0 => ( A = k1_xboole_0 | ( v1_funct_2(C,A,B) <=> C = k1_xboole_0 ) ) ) ) ) ), file(funct_2,d1_funct_2), [interesting(0.00)]). fof(t22_card_3,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r2_hidden(A,k1_relat_1(B)) => ( k4_card_3(B) = k1_xboole_0 | k5_card_3(A,k4_card_3(B)) = k1_funct_1(B,A) ) ) ) ), file(card_3,t22_card_3), [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(t14_funct_4,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(k1_funct_4(C,B),A) = k1_funct_1(B,A) ) ) ) ), file(funct_4,t14_funct_4), [interesting(0.00)]). fof(t6_cqc_lang,theorem,( ! [A,B] : k1_funct_1(k3_cqc_lang(A,B),A) = B ), file(cqc_lang,t6_cqc_lang), [interesting(0.00)]). fof(t12_funct_4,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(k1_funct_4(C,B),A) = k1_funct_1(C,A) ) ) ) ), file(funct_4,t12_funct_4), [interesting(0.00)]). fof(t1_ami_2,theorem,( $true ), file(ami_2,t1_ami_2), [interesting(0.00)]). fof(d9_ami_2,definition,( ! [A] : ( m2_subset_1(A,k2_zfmisc_1(k1_gr_cy_1(9),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),k5_numbers))),k4_ami_2) => ( ? [B] : ( m2_subset_1(B,k5_numbers,k2_ami_2) & ? [C] : ( m2_subset_1(C,k5_numbers,k2_ami_2) & ? [D] : ( m2_subset_1(D,k5_numbers,k1_gr_cy_1(9)) & A = k1_domain_1(k1_gr_cy_1(9),k1_zfmisc_1(k2_zfmisc_1(k5_numbers,k2_ami_2)),D,k2_finseq_4(k2_ami_2,B,C)) ) ) ) => ! [B] : ( m2_subset_1(B,k5_numbers,k2_ami_2) => ( B = k9_ami_2(A) <=> ? [C] : ( m2_finseq_1(C,k2_ami_2) & C = k3_domain_1(k1_gr_cy_1(9),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),k5_numbers)),A) & B = k4_finseq_4(k5_numbers,k2_ami_2,C,1) ) ) ) ) ) ), file(ami_2,d9_ami_2), [interesting(0.00)]). fof(t7_mcart_1,theorem,( ! [A,B] : ( k1_mcart_1(k4_tarski(A,B)) = A & k2_mcart_1(k4_tarski(A,B)) = B ) ), file(mcart_1,t7_mcart_1), [interesting(0.00)]). fof(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(d10_ami_2,definition,( ! [A] : ( m2_subset_1(A,k2_zfmisc_1(k1_gr_cy_1(9),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),k5_numbers))),k4_ami_2) => ( ? [B] : ( m2_subset_1(B,k5_numbers,k2_ami_2) & ? [C] : ( m2_subset_1(C,k5_numbers,k2_ami_2) & ? [D] : ( m2_subset_1(D,k5_numbers,k1_gr_cy_1(9)) & A = k1_domain_1(k1_gr_cy_1(9),k1_zfmisc_1(k2_zfmisc_1(k5_numbers,k2_ami_2)),D,k2_finseq_4(k2_ami_2,B,C)) ) ) ) => ! [B] : ( m2_subset_1(B,k5_numbers,k2_ami_2) => ( B = k10_ami_2(A) <=> ? [C] : ( m2_finseq_1(C,k2_ami_2) & C = k3_domain_1(k1_gr_cy_1(9),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),k5_numbers)),A) & B = k4_finseq_4(k5_numbers,k2_ami_2,C,2) ) ) ) ) ) ), file(ami_2,d10_ami_2), [interesting(0.00)]). fof(d11_ami_2,definition,( ! [A] : ( m2_subset_1(A,k2_zfmisc_1(k1_gr_cy_1(9),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),k5_numbers))),k4_ami_2) => ( ? [B] : ( m2_subset_1(B,k5_numbers,k3_ami_2) & ? [C] : ( m2_subset_1(C,k5_numbers,k1_gr_cy_1(9)) & A = k1_domain_1(k1_gr_cy_1(9),k1_zfmisc_1(k2_zfmisc_1(k5_numbers,k3_ami_2)),C,k12_finseq_1(k3_ami_2,B)) ) ) => ! [B] : ( m2_subset_1(B,k5_numbers,k3_ami_2) => ( B = k11_ami_2(A) <=> ? [C] : ( m2_finseq_1(C,k3_ami_2) & C = k3_domain_1(k1_gr_cy_1(9),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),k5_numbers)),A) & B = k4_finseq_4(k5_numbers,k3_ami_2,C,1) ) ) ) ) ) ), file(ami_2,d11_ami_2), [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(d12_ami_2,definition,( ! [A] : ( m2_subset_1(A,k2_zfmisc_1(k1_gr_cy_1(9),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),k5_numbers))),k4_ami_2) => ( ? [B] : ( m2_subset_1(B,k5_numbers,k3_ami_2) & ? [C] : ( m2_subset_1(C,k5_numbers,k2_ami_2) & ? [D] : ( m2_subset_1(D,k5_numbers,k1_gr_cy_1(9)) & A = k1_domain_1(k1_gr_cy_1(9),k1_zfmisc_1(k2_zfmisc_1(k5_numbers,k5_numbers)),D,k2_finseq_4(k5_numbers,B,C)) ) ) ) => ! [B] : ( m2_subset_1(B,k5_numbers,k3_ami_2) => ( B = k12_ami_2(A) <=> ? [C] : ( m2_subset_1(C,k5_numbers,k3_ami_2) & ? [D] : ( m2_subset_1(D,k5_numbers,k2_ami_2) & k2_finseq_4(k5_numbers,C,D) = k3_domain_1(k1_gr_cy_1(9),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),k5_numbers)),A) & B = k4_finseq_4(k5_numbers,k5_numbers,k2_finseq_4(k5_numbers,C,D),1) ) ) ) ) ) ) ), file(ami_2,d12_ami_2), [interesting(0.00)]). fof(d13_ami_2,definition,( ! [A] : ( m2_subset_1(A,k2_zfmisc_1(k1_gr_cy_1(9),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),k5_numbers))),k4_ami_2) => ( ? [B] : ( m2_subset_1(B,k5_numbers,k3_ami_2) & ? [C] : ( m2_subset_1(C,k5_numbers,k2_ami_2) & ? [D] : ( m2_subset_1(D,k5_numbers,k1_gr_cy_1(9)) & A = k1_domain_1(k1_gr_cy_1(9),k1_zfmisc_1(k2_zfmisc_1(k5_numbers,k5_numbers)),D,k2_finseq_4(k5_numbers,B,C)) ) ) ) => ! [B] : ( m2_subset_1(B,k5_numbers,k2_ami_2) => ( B = k13_ami_2(A) <=> ? [C] : ( m2_subset_1(C,k5_numbers,k3_ami_2) & ? [D] : ( m2_subset_1(D,k5_numbers,k2_ami_2) & k2_finseq_4(k5_numbers,C,D) = k3_domain_1(k1_gr_cy_1(9),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),k5_numbers)),A) & B = k4_finseq_4(k5_numbers,k5_numbers,k2_finseq_4(k5_numbers,C,D),2) ) ) ) ) ) ) ), file(ami_2,d13_ami_2), [interesting(0.00)]). fof(t25_ami_2,theorem,( ! [A] : ( m2_subset_1(A,k2_zfmisc_1(k1_gr_cy_1(9),k13_finseq_1(k2_xboole_0(k3_tarski(k1_tarski(k4_numbers)),k5_numbers))),k4_ami_2) => ! [B] : ( m2_subset_1(B,k5_numbers,k3_ami_2) => ! [C] : ( m2_subset_1(C,k5_numbers,k2_ami_2) => ! [D] : ( m2_subset_1(D,k5_numbers,k1_gr_cy_1(9)) => ( A = k1_domain_1(k1_gr_cy_1(9),k1_zfmisc_1(k2_zfmisc_1(k5_numbers,k5_numbers)),D,k2_finseq_4(k5_numbers,B,C)) => ( k12_ami_2(A) = B & k13_ami_2(A) = C ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_ami_2,t7_mcart_1,t26_finseq_4,d13_ami_2,t7_mcart_1,t26_finseq_4]), [file(ami_2,t25_ami_2),interesting(0.00)]). fof(t10_gr_cy_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ~ r1_xreal_0(A,0) => ( r2_hidden(B,k1_gr_cy_1(A)) <=> ~ r1_xreal_0(A,B) ) ) ) ) ), file(gr_cy_1,t10_gr_cy_1), [interesting(0.00)]). fof(d2_tarski,definition,( ! [A,B,C] : ( C = k2_tarski(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( D = A | D = B ) ) ) ), file(tarski,d2_tarski), [interesting(0.00)]). fof(d3_enumset1,definition,( ! [A,B,C,D,E,F] : ( F = k3_enumset1(A,B,C,D,E) <=> ! [G] : ( r2_hidden(G,F) <=> ~ ( G != A & G != B & G != C & G != D & G != E ) ) ) ), file(enumset1,d3_enumset1), [interesting(0.00)]).