% Mizar problem: t85_sublemma,sublemma,2192,44 fof(t85_sublemma,conjecture,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_valuat_1(B,A) => ! [C] : ( m2_subset_1(C,k8_qc_lang1,k7_cqc_lang) => ! [D] : ( m2_fraenkel(D,k2_qc_lang1,A,k2_valuat_1(A)) => ! [E] : ( ( v1_funct_1(E) & m2_relset_1(E,k2_qc_lang1,A) ) => ! [F] : ( ( v1_funct_1(F) & m2_relset_1(F,k2_qc_lang1,A) ) => ! [G] : ( ( v1_funct_1(G) & m2_relset_1(G,k2_qc_lang1,A) ) => ( ( ! [H] : ( m2_subset_1(H,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(H,k4_relset_1(k2_qc_lang1,A,F)) & r2_hidden(H,k24_qc_lang1(C)) ) ) & ! [H] : ( m2_subset_1(H,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(H,k4_relset_1(k2_qc_lang1,A,G)) => k1_funct_1(G,H) = k8_funct_2(k2_qc_lang1,A,D,H) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,A,E),k4_relset_1(k2_qc_lang1,A,G)) ) => ( r1_valuat_1(A,C,B,k1_sublemma(A,D,E)) <=> r1_valuat_1(A,C,B,k1_sublemma(A,D,k15_sublemma(A,k15_sublemma(A,E,F),G))) ) ) ) ) ) ) ) ) ) ), inference(mizar_bg_added,[status(thm)],[antisymmetry_r2_hidden,cc1_fraenkel,cc1_funct_1,cc1_nat_1,cc1_relat_1,cc1_relset_1,cc2_funct_1,cc2_nat_1,cc3_nat_1,d1_sublemma,d4_cqc_lang,dt_k10_cqc_lang,dt_k11_cqc_lang,dt_k11_qc_lang1,dt_k12_qc_lang1,dt_k13_qc_lang1,dt_k14_qc_lang1,dt_k15_cqc_lang,dt_k15_sublemma,dt_k1_funct_1,dt_k1_funct_4,dt_k1_numbers,dt_k1_qc_lang1,dt_k1_relat_1,dt_k1_sublemma,dt_k1_valuat_1,dt_k1_xboole_0,dt_k1_zfmisc_1,dt_k24_qc_lang1,dt_k2_qc_lang1,dt_k2_valuat_1,dt_k2_zfmisc_1,dt_k3_margrel1,dt_k3_qc_lang1,dt_k4_qc_lang1,dt_k4_relset_1,dt_k5_numbers,dt_k5_ordinal2,dt_k5_qc_lang1,dt_k5_qc_lang3,dt_k6_qc_lang3,dt_k7_cqc_lang,dt_k7_qc_lang1,dt_k8_cqc_lang,dt_k8_funct_2,dt_k8_qc_lang1,dt_k9_cqc_lang,dt_k9_qc_lang1,dt_m1_finseq_1,dt_m1_fraenkel,dt_m1_qc_lang1,dt_m1_relset_1,dt_m1_subset_1,dt_m1_valuat_1,dt_m2_finseq_1,dt_m2_fraenkel,dt_m2_relset_1,dt_m2_subset_1,existence_m1_finseq_1,existence_m1_fraenkel,existence_m1_qc_lang1,existence_m1_relset_1,existence_m1_subset_1,existence_m1_valuat_1,existence_m2_finseq_1,existence_m2_fraenkel,existence_m2_relset_1,existence_m2_subset_1,fc12_relat_1,fc1_ordinal2,fc1_qc_lang1,fc1_subset_1,fc2_cqc_lang,fc2_qc_lang1,fc3_qc_lang1,fc4_qc_lang1,fc4_relat_1,fc4_subset_1,fc5_qc_lang1,fc5_relat_1,fc6_qc_lang1,fc7_relat_1,fraenkel_a_0_0_cqc_lang,idempotence_k15_sublemma,idempotence_k1_funct_4,rc1_cqc_lang,rc1_fraenkel,rc1_funct_1,rc1_nat_1,rc1_relat_1,rc1_subset_1,rc2_funct_1,rc2_nat_1,rc2_relat_1,rc2_subset_1,rc3_funct_1,rc3_nat_1,rc3_relat_1,rc4_funct_1,redefinition_k10_cqc_lang,redefinition_k11_cqc_lang,redefinition_k15_cqc_lang,redefinition_k15_sublemma,redefinition_k2_valuat_1,redefinition_k4_relset_1,redefinition_k5_numbers,redefinition_k8_cqc_lang,redefinition_k8_funct_2,redefinition_k9_cqc_lang,redefinition_m2_finseq_1,redefinition_m2_fraenkel,redefinition_m2_relset_1,redefinition_m2_subset_1,reflexivity_r1_tarski,s1_cqc_lang__e2_98__sublemma,symmetry_r1_xboole_0,t1_subset,t2_subset,t2_tarski,t3_subset,t44_valuat_1,t4_subset,t5_subset,t6_boole,t79_sublemma,t7_boole,t80_sublemma,t81_sublemma,t84_sublemma,t8_boole]), [file(sublemma,t85_sublemma)]). fof(antisymmetry_r2_hidden,axiom,( ! [A,B] : ( r2_hidden(A,B) => ~ r2_hidden(B,A) ) ), file(hidden,r2_hidden), []). fof(cc1_fraenkel,axiom,( ! [A] : ( v1_fraenkel(A) => ! [B] : ( m1_subset_1(B,A) => ( v1_relat_1(B) & v1_funct_1(B) ) ) ) ), file(fraenkel,cc1_fraenkel), []). fof(cc1_funct_1,axiom,( ! [A] : ( v1_xboole_0(A) => v1_funct_1(A) ) ), file(funct_1,cc1_funct_1), []). fof(cc1_nat_1,axiom,( ! [A] : ( m1_subset_1(A,k5_numbers) => ( v1_ordinal1(A) & v2_ordinal1(A) & v3_ordinal1(A) & v4_ordinal2(A) & v1_xcmplx_0(A) & v1_xreal_0(A) ) ) ), file(nat_1,cc1_nat_1), []). fof(cc1_relat_1,axiom,( ! [A] : ( v1_xboole_0(A) => v1_relat_1(A) ) ), file(relat_1,cc1_relat_1), []). fof(cc1_relset_1,axiom,( ! [A,B,C] : ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) => v1_relat_1(C) ) ), file(relset_1,cc1_relset_1), []). fof(cc2_funct_1,axiom,( ! [A] : ( ( v1_relat_1(A) & v1_xboole_0(A) & v1_funct_1(A) ) => ( v1_relat_1(A) & v1_funct_1(A) & v2_funct_1(A) ) ) ), file(funct_1,cc2_funct_1), []). fof(cc2_nat_1,axiom,( ! [A] : ( m1_subset_1(A,k5_numbers) => ( v1_ordinal1(A) & v2_ordinal1(A) & v3_ordinal1(A) & v4_ordinal2(A) & v1_xcmplx_0(A) & v1_xreal_0(A) & ~ v3_xreal_0(A) ) ) ), file(nat_1,cc2_nat_1), []). fof(cc3_nat_1,axiom,( ! [A] : ( v4_ordinal2(A) => ( v4_ordinal2(A) & v1_xcmplx_0(A) & v1_xreal_0(A) & ~ v3_xreal_0(A) ) ) ), file(nat_1,cc3_nat_1), []). fof(d1_sublemma,axiom,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,k2_qc_lang1,A,k2_valuat_1(A)) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,k2_qc_lang1,A) ) => k1_sublemma(A,B,C) = k1_funct_4(B,C) ) ) ) ), file(sublemma,d1_sublemma), []). fof(d4_cqc_lang,axiom,( k7_cqc_lang = a_0_0_cqc_lang ), file(cqc_lang,d4_cqc_lang), []). fof(dt_k10_cqc_lang,axiom,( ! [A] : ( m1_subset_1(A,k7_cqc_lang) => m2_subset_1(k10_cqc_lang(A),k8_qc_lang1,k7_cqc_lang) ) ), file(cqc_lang,k10_cqc_lang), []). fof(dt_k11_cqc_lang,axiom,( ! [A,B] : ( ( m1_subset_1(A,k7_cqc_lang) & m1_subset_1(B,k7_cqc_lang) ) => m2_subset_1(k11_cqc_lang(A,B),k8_qc_lang1,k7_cqc_lang) ) ), file(cqc_lang,k11_cqc_lang), []). fof(dt_k11_qc_lang1,axiom,( m1_subset_1(k11_qc_lang1,k8_qc_lang1) ), file(qc_lang1,k11_qc_lang1), []). fof(dt_k12_qc_lang1,axiom,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => m1_subset_1(k12_qc_lang1(A),k8_qc_lang1) ) ), file(qc_lang1,k12_qc_lang1), []). fof(dt_k13_qc_lang1,axiom,( ! [A,B] : ( ( m1_subset_1(A,k8_qc_lang1) & m1_subset_1(B,k8_qc_lang1) ) => m1_subset_1(k13_qc_lang1(A,B),k8_qc_lang1) ) ), file(qc_lang1,k13_qc_lang1), []). fof(dt_k14_qc_lang1,axiom,( ! [A,B] : ( ( m1_subset_1(A,k2_qc_lang1) & m1_subset_1(B,k8_qc_lang1) ) => m1_subset_1(k14_qc_lang1(A,B),k8_qc_lang1) ) ), file(qc_lang1,k14_qc_lang1), []). fof(dt_k15_cqc_lang,axiom,( ! [A,B] : ( ( m1_subset_1(A,k2_qc_lang1) & m1_subset_1(B,k7_cqc_lang) ) => m2_subset_1(k15_cqc_lang(A,B),k8_qc_lang1,k7_cqc_lang) ) ), file(cqc_lang,k15_cqc_lang), []). fof(dt_k15_sublemma,axiom,( ! [A,B,C] : ( ( ~ v1_xboole_0(A) & v1_funct_1(B) & m1_relset_1(B,k2_qc_lang1,A) & v1_funct_1(C) & m1_relset_1(C,k2_qc_lang1,A) ) => ( v1_funct_1(k15_sublemma(A,B,C)) & m2_relset_1(k15_sublemma(A,B,C),k2_qc_lang1,A) ) ) ), file(sublemma,k15_sublemma), []). fof(dt_k1_funct_1,axiom,( $true ), file(funct_1,k1_funct_1), []). fof(dt_k1_funct_4,axiom,( ! [A,B] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_relat_1(B) & v1_funct_1(B) ) => ( v1_relat_1(k1_funct_4(A,B)) & v1_funct_1(k1_funct_4(A,B)) ) ) ), file(funct_4,k1_funct_4), []). fof(dt_k1_numbers,axiom,( $true ), file(numbers,k1_numbers), []). fof(dt_k1_qc_lang1,axiom,( $true ), file(qc_lang1,k1_qc_lang1), []). fof(dt_k1_relat_1,axiom,( $true ), file(relat_1,k1_relat_1), []). fof(dt_k1_sublemma,axiom,( ! [A,B,C] : ( ( ~ v1_xboole_0(A) & m1_subset_1(B,k2_valuat_1(A)) & v1_funct_1(C) & m1_relset_1(C,k2_qc_lang1,A) ) => m2_fraenkel(k1_sublemma(A,B,C),k2_qc_lang1,A,k2_valuat_1(A)) ) ), file(sublemma,k1_sublemma), []). fof(dt_k1_valuat_1,axiom,( $true ), file(valuat_1,k1_valuat_1), []). fof(dt_k1_xboole_0,axiom,( $true ), file(xboole_0,k1_xboole_0), []). fof(dt_k1_zfmisc_1,axiom,( $true ), file(zfmisc_1,k1_zfmisc_1), []). fof(dt_k24_qc_lang1,axiom,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => m1_subset_1(k24_qc_lang1(A),k1_zfmisc_1(k2_qc_lang1)) ) ), file(qc_lang1,k24_qc_lang1), []). fof(dt_k2_qc_lang1,axiom,( m1_subset_1(k2_qc_lang1,k1_zfmisc_1(k1_qc_lang1)) ), file(qc_lang1,k2_qc_lang1), []). fof(dt_k2_valuat_1,axiom,( ! [A] : ( ~ v1_xboole_0(A) => m1_fraenkel(k2_valuat_1(A),k2_qc_lang1,A) ) ), file(valuat_1,k2_valuat_1), []). fof(dt_k2_zfmisc_1,axiom,( $true ), file(zfmisc_1,k2_zfmisc_1), []). fof(dt_k3_margrel1,axiom,( $true ), file(margrel1,k3_margrel1), []). fof(dt_k3_qc_lang1,axiom,( m1_subset_1(k3_qc_lang1,k1_zfmisc_1(k1_qc_lang1)) ), file(qc_lang1,k3_qc_lang1), []). fof(dt_k4_qc_lang1,axiom,( m1_subset_1(k4_qc_lang1,k1_zfmisc_1(k1_qc_lang1)) ), file(qc_lang1,k4_qc_lang1), []). fof(dt_k4_relset_1,axiom,( ! [A,B,C] : ( m1_relset_1(C,A,B) => m1_subset_1(k4_relset_1(A,B,C),k1_zfmisc_1(A)) ) ), file(relset_1,k4_relset_1), []). fof(dt_k5_numbers,axiom,( m1_subset_1(k5_numbers,k1_zfmisc_1(k1_numbers)) ), file(numbers,k5_numbers), []). fof(dt_k5_ordinal2,axiom,( $true ), file(ordinal2,k5_ordinal2), []). fof(dt_k5_qc_lang1,axiom,( $true ), file(qc_lang1,k5_qc_lang1), []). fof(dt_k5_qc_lang3,axiom,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => m1_subset_1(k5_qc_lang3(A),k1_zfmisc_1(k4_qc_lang1)) ) ), file(qc_lang3,k5_qc_lang3), []). fof(dt_k6_qc_lang3,axiom,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => m1_subset_1(k6_qc_lang3(A),k1_zfmisc_1(k3_qc_lang1)) ) ), file(qc_lang3,k6_qc_lang3), []). fof(dt_k7_cqc_lang,axiom,( m1_subset_1(k7_cqc_lang,k1_zfmisc_1(k8_qc_lang1)) ), file(cqc_lang,k7_cqc_lang), []). fof(dt_k7_qc_lang1,axiom,( ! [A] : ( m1_subset_1(A,k5_numbers) => m1_subset_1(k7_qc_lang1(A),k1_zfmisc_1(k5_qc_lang1)) ) ), file(qc_lang1,k7_qc_lang1), []). fof(dt_k8_cqc_lang,axiom,( ! [A,B,C] : ( ( m1_subset_1(A,k5_numbers) & m1_subset_1(B,k7_qc_lang1(A)) & v1_cqc_lang(C,A) & m1_qc_lang1(C,A) ) => m2_subset_1(k8_cqc_lang(A,B,C),k8_qc_lang1,k7_cqc_lang) ) ), file(cqc_lang,k8_cqc_lang), []). fof(dt_k8_funct_2,axiom,( ! [A,B,C,D] : ( ( ~ v1_xboole_0(A) & v1_funct_1(C) & v1_funct_2(C,A,B) & m1_relset_1(C,A,B) & m1_subset_1(D,A) ) => m1_subset_1(k8_funct_2(A,B,C,D),B) ) ), file(funct_2,k8_funct_2), []). fof(dt_k8_qc_lang1,axiom,( ~ v1_xboole_0(k8_qc_lang1) ), file(qc_lang1,k8_qc_lang1), []). fof(dt_k9_cqc_lang,axiom,( m2_subset_1(k9_cqc_lang,k8_qc_lang1,k7_cqc_lang) ), file(cqc_lang,k9_cqc_lang), []). fof(dt_k9_qc_lang1,axiom,( ! [A,B] : ( ( m1_subset_1(A,k5_qc_lang1) & m1_finseq_1(B,k1_qc_lang1) ) => m1_subset_1(k9_qc_lang1(A,B),k8_qc_lang1) ) ), file(qc_lang1,k9_qc_lang1), []). fof(dt_m1_finseq_1,axiom,( ! [A,B] : ( m1_finseq_1(B,A) => ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) ) ), file(finseq_1,m1_finseq_1), []). fof(dt_m1_fraenkel,axiom,( ! [A,B,C] : ( m1_fraenkel(C,A,B) => ( ~ v1_xboole_0(C) & v1_fraenkel(C) ) ) ), file(fraenkel,m1_fraenkel), []). fof(dt_m1_qc_lang1,axiom,( ! [A] : ( m1_subset_1(A,k5_numbers) => ! [B] : ( m1_qc_lang1(B,A) => m2_finseq_1(B,k1_qc_lang1) ) ) ), file(qc_lang1,m1_qc_lang1), []). fof(dt_m1_relset_1,axiom,( $true ), file(relset_1,m1_relset_1), []). fof(dt_m1_subset_1,axiom,( $true ), file(subset_1,m1_subset_1), []). fof(dt_m1_valuat_1,axiom,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_valuat_1(B,A) => ( v1_funct_1(B) & v1_funct_2(B,k5_qc_lang1,k3_margrel1(A)) & m2_relset_1(B,k5_qc_lang1,k3_margrel1(A)) ) ) ) ), file(valuat_1,m1_valuat_1), []). fof(dt_m2_finseq_1,axiom,( ! [A,B] : ( m2_finseq_1(B,A) => ( v1_funct_1(B) & v1_finseq_1(B) & m2_relset_1(B,k5_numbers,A) ) ) ), file(finseq_1,m2_finseq_1), []). fof(dt_m2_fraenkel,axiom,( ! [A,B,C] : ( ( ~ v1_xboole_0(B) & m1_fraenkel(C,A,B) ) => ! [D] : ( m2_fraenkel(D,A,B,C) => ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) ) ) ), file(fraenkel,m2_fraenkel), []). fof(dt_m2_relset_1,axiom,( ! [A,B,C] : ( m2_relset_1(C,A,B) => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ), file(relset_1,m2_relset_1), []). fof(dt_m2_subset_1,axiom,( ! [A,B] : ( ( ~ v1_xboole_0(A) & ~ v1_xboole_0(B) & m1_subset_1(B,k1_zfmisc_1(A)) ) => ! [C] : ( m2_subset_1(C,A,B) => m1_subset_1(C,A) ) ) ), file(subset_1,m2_subset_1), []). fof(existence_m1_finseq_1,axiom,( ! [A] : ? [B] : m1_finseq_1(B,A) ), file(finseq_1,m1_finseq_1), []). fof(existence_m1_fraenkel,axiom,( ! [A,B] : ? [C] : m1_fraenkel(C,A,B) ), file(fraenkel,m1_fraenkel), []). fof(existence_m1_qc_lang1,axiom,( ! [A] : ( m1_subset_1(A,k5_numbers) => ? [B] : m1_qc_lang1(B,A) ) ), file(qc_lang1,m1_qc_lang1), []). fof(existence_m1_relset_1,axiom,( ! [A,B] : ? [C] : m1_relset_1(C,A,B) ), file(relset_1,m1_relset_1), []). fof(existence_m1_subset_1,axiom,( ! [A] : ? [B] : m1_subset_1(B,A) ), file(subset_1,m1_subset_1), []). fof(existence_m1_valuat_1,axiom,( ! [A] : ( ~ v1_xboole_0(A) => ? [B] : m1_valuat_1(B,A) ) ), file(valuat_1,m1_valuat_1), []). fof(existence_m2_finseq_1,axiom,( ! [A] : ? [B] : m2_finseq_1(B,A) ), file(finseq_1,m2_finseq_1), []). fof(existence_m2_fraenkel,axiom,( ! [A,B,C] : ( ( ~ v1_xboole_0(B) & m1_fraenkel(C,A,B) ) => ? [D] : m2_fraenkel(D,A,B,C) ) ), file(fraenkel,m2_fraenkel), []). fof(existence_m2_relset_1,axiom,( ! [A,B] : ? [C] : m2_relset_1(C,A,B) ), file(relset_1,m2_relset_1), []). fof(existence_m2_subset_1,axiom,( ! [A,B] : ( ( ~ v1_xboole_0(A) & ~ v1_xboole_0(B) & m1_subset_1(B,k1_zfmisc_1(A)) ) => ? [C] : m2_subset_1(C,A,B) ) ), file(subset_1,m2_subset_1), []). fof(fc12_relat_1,axiom, ( v1_xboole_0(k1_xboole_0) & v1_relat_1(k1_xboole_0) & v3_relat_1(k1_xboole_0) ), file(relat_1,fc12_relat_1), []). fof(fc1_ordinal2,axiom, ( v1_ordinal1(k5_ordinal2) & v2_ordinal1(k5_ordinal2) & v3_ordinal1(k5_ordinal2) & ~ v1_xboole_0(k5_ordinal2) ), file(ordinal2,fc1_ordinal2), []). fof(fc1_qc_lang1,axiom,( ~ v1_xboole_0(k1_qc_lang1) ), file(qc_lang1,fc1_qc_lang1), []). fof(fc1_subset_1,axiom,( ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ), file(subset_1,fc1_subset_1), []). fof(fc2_cqc_lang,axiom,( ~ v1_xboole_0(k7_cqc_lang) ), file(cqc_lang,fc2_cqc_lang), []). fof(fc2_qc_lang1,axiom,( ~ v1_xboole_0(k2_qc_lang1) ), file(qc_lang1,fc2_qc_lang1), []). fof(fc3_qc_lang1,axiom,( ~ v1_xboole_0(k3_qc_lang1) ), file(qc_lang1,fc3_qc_lang1), []). fof(fc4_qc_lang1,axiom,( ~ v1_xboole_0(k4_qc_lang1) ), file(qc_lang1,fc4_qc_lang1), []). fof(fc4_relat_1,axiom, ( v1_xboole_0(k1_xboole_0) & v1_relat_1(k1_xboole_0) ), file(relat_1,fc4_relat_1), []). fof(fc4_subset_1,axiom,( ! [A,B] : ( ( ~ v1_xboole_0(A) & ~ v1_xboole_0(B) ) => ~ v1_xboole_0(k2_zfmisc_1(A,B)) ) ), file(subset_1,fc4_subset_1), []). fof(fc5_qc_lang1,axiom,( ~ v1_xboole_0(k5_qc_lang1) ), file(qc_lang1,fc5_qc_lang1), []). fof(fc5_relat_1,axiom,( ! [A] : ( ( ~ v1_xboole_0(A) & v1_relat_1(A) ) => ~ v1_xboole_0(k1_relat_1(A)) ) ), file(relat_1,fc5_relat_1), []). fof(fc6_qc_lang1,axiom,( ! [A] : ( m1_subset_1(A,k5_numbers) => ~ v1_xboole_0(k7_qc_lang1(A)) ) ), file(qc_lang1,fc6_qc_lang1), []). fof(fc7_relat_1,axiom,( ! [A] : ( v1_xboole_0(A) => ( v1_xboole_0(k1_relat_1(A)) & v1_relat_1(k1_relat_1(A)) ) ) ), file(relat_1,fc7_relat_1), []). fof(fraenkel_a_0_0_cqc_lang,axiom,( ! [A] : ( r2_hidden(A,a_0_0_cqc_lang) <=> ? [B] : ( m1_subset_1(B,k8_qc_lang1) & A = B & k6_qc_lang3(B) = k1_xboole_0 & k5_qc_lang3(B) = k1_xboole_0 ) ) ), file(cqc_lang,a_0_0_cqc_lang), []). fof(idempotence_k15_sublemma,axiom,( ! [A,B,C] : ( ( ~ v1_xboole_0(A) & v1_funct_1(B) & m1_relset_1(B,k2_qc_lang1,A) & v1_funct_1(C) & m1_relset_1(C,k2_qc_lang1,A) ) => k15_sublemma(A,B,B) = B ) ), file(sublemma,k15_sublemma), []). fof(idempotence_k1_funct_4,axiom,( ! [A,B] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_relat_1(B) & v1_funct_1(B) ) => k1_funct_4(A,A) = A ) ), file(funct_4,k1_funct_4), []). fof(rc1_cqc_lang,axiom,( ! [A] : ( m1_subset_1(A,k5_numbers) => ? [B] : ( m1_qc_lang1(B,A) & v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) & v1_cqc_lang(B,A) ) ) ), file(cqc_lang,rc1_cqc_lang), []). fof(rc1_fraenkel,axiom,( ? [A] : ( ~ v1_xboole_0(A) & v1_fraenkel(A) ) ), file(fraenkel,rc1_fraenkel), []). fof(rc1_funct_1,axiom,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) ) ), file(funct_1,rc1_funct_1), []). fof(rc1_nat_1,axiom,( ? [A] : ( ~ v1_xboole_0(A) & v4_ordinal2(A) & v1_xcmplx_0(A) & v1_xreal_0(A) ) ), file(nat_1,rc1_nat_1), []). fof(rc1_relat_1,axiom,( ? [A] : ( v1_xboole_0(A) & v1_relat_1(A) ) ), file(relat_1,rc1_relat_1), []). fof(rc1_subset_1,axiom,( ! [A] : ( ~ v1_xboole_0(A) => ? [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) & ~ v1_xboole_0(B) ) ) ), file(subset_1,rc1_subset_1), []). fof(rc2_funct_1,axiom,( ? [A] : ( v1_relat_1(A) & v1_xboole_0(A) & v1_funct_1(A) ) ), file(funct_1,rc2_funct_1), []). fof(rc2_nat_1,axiom,( ? [A] : ( m1_subset_1(A,k1_zfmisc_1(k1_numbers)) & ~ v1_xboole_0(A) & v3_ordinal1(A) ) ), file(nat_1,rc2_nat_1), []). fof(rc2_relat_1,axiom,( ? [A] : ( ~ v1_xboole_0(A) & v1_relat_1(A) ) ), file(relat_1,rc2_relat_1), []). fof(rc2_subset_1,axiom,( ! [A] : ? [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) & v1_xboole_0(B) ) ), file(subset_1,rc2_subset_1), []). fof(rc3_funct_1,axiom,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v2_funct_1(A) ) ), file(funct_1,rc3_funct_1), []). fof(rc3_nat_1,axiom,( ? [A] : ( m1_subset_1(A,k5_numbers) & ~ v1_xboole_0(A) & v1_ordinal1(A) & v2_ordinal1(A) & v3_ordinal1(A) & v4_ordinal2(A) & v1_xcmplx_0(A) & v1_xreal_0(A) ) ), file(nat_1,rc3_nat_1), []). fof(rc3_relat_1,axiom,( ? [A] : ( v1_relat_1(A) & v3_relat_1(A) ) ), file(relat_1,rc3_relat_1), []). fof(rc4_funct_1,axiom,( ? [A] : ( v1_relat_1(A) & v3_relat_1(A) & v1_funct_1(A) ) ), file(funct_1,rc4_funct_1), []). fof(redefinition_k10_cqc_lang,axiom,( ! [A] : ( m1_subset_1(A,k7_cqc_lang) => k10_cqc_lang(A) = k12_qc_lang1(A) ) ), file(cqc_lang,k10_cqc_lang), []). fof(redefinition_k11_cqc_lang,axiom,( ! [A,B] : ( ( m1_subset_1(A,k7_cqc_lang) & m1_subset_1(B,k7_cqc_lang) ) => k11_cqc_lang(A,B) = k13_qc_lang1(A,B) ) ), file(cqc_lang,k11_cqc_lang), []). fof(redefinition_k15_cqc_lang,axiom,( ! [A,B] : ( ( m1_subset_1(A,k2_qc_lang1) & m1_subset_1(B,k7_cqc_lang) ) => k15_cqc_lang(A,B) = k14_qc_lang1(A,B) ) ), file(cqc_lang,k15_cqc_lang), []). fof(redefinition_k15_sublemma,axiom,( ! [A,B,C] : ( ( ~ v1_xboole_0(A) & v1_funct_1(B) & m1_relset_1(B,k2_qc_lang1,A) & v1_funct_1(C) & m1_relset_1(C,k2_qc_lang1,A) ) => k15_sublemma(A,B,C) = k1_funct_4(B,C) ) ), file(sublemma,k15_sublemma), []). fof(redefinition_k2_valuat_1,axiom,( ! [A] : ( ~ v1_xboole_0(A) => k2_valuat_1(A) = k1_valuat_1(A) ) ), file(valuat_1,k2_valuat_1), []). fof(redefinition_k4_relset_1,axiom,( ! [A,B,C] : ( m1_relset_1(C,A,B) => k4_relset_1(A,B,C) = k1_relat_1(C) ) ), file(relset_1,k4_relset_1), []). fof(redefinition_k5_numbers,axiom,( k5_numbers = k5_ordinal2 ), file(numbers,k5_numbers), []). fof(redefinition_k8_cqc_lang,axiom,( ! [A,B,C] : ( ( m1_subset_1(A,k5_numbers) & m1_subset_1(B,k7_qc_lang1(A)) & v1_cqc_lang(C,A) & m1_qc_lang1(C,A) ) => k8_cqc_lang(A,B,C) = k9_qc_lang1(B,C) ) ), file(cqc_lang,k8_cqc_lang), []). fof(redefinition_k8_funct_2,axiom,( ! [A,B,C,D] : ( ( ~ v1_xboole_0(A) & v1_funct_1(C) & v1_funct_2(C,A,B) & m1_relset_1(C,A,B) & m1_subset_1(D,A) ) => k8_funct_2(A,B,C,D) = k1_funct_1(C,D) ) ), file(funct_2,k8_funct_2), []). fof(redefinition_k9_cqc_lang,axiom,( k9_cqc_lang = k11_qc_lang1 ), file(cqc_lang,k9_cqc_lang), []). fof(redefinition_m2_finseq_1,axiom,( ! [A,B] : ( m2_finseq_1(B,A) <=> m1_finseq_1(B,A) ) ), file(finseq_1,m2_finseq_1), []). fof(redefinition_m2_fraenkel,axiom,( ! [A,B,C] : ( ( ~ v1_xboole_0(B) & m1_fraenkel(C,A,B) ) => ! [D] : ( m2_fraenkel(D,A,B,C) <=> m1_subset_1(D,C) ) ) ), file(fraenkel,m2_fraenkel), []). fof(redefinition_m2_relset_1,axiom,( ! [A,B,C] : ( m2_relset_1(C,A,B) <=> m1_relset_1(C,A,B) ) ), file(relset_1,m2_relset_1), []). fof(redefinition_m2_subset_1,axiom,( ! [A,B] : ( ( ~ v1_xboole_0(A) & ~ v1_xboole_0(B) & m1_subset_1(B,k1_zfmisc_1(A)) ) => ! [C] : ( m2_subset_1(C,A,B) <=> m1_subset_1(C,B) ) ) ), file(subset_1,m2_subset_1), []). fof(reflexivity_r1_tarski,axiom,( ! [A,B] : r1_tarski(A,A) ), file(tarski,r1_tarski), []). fof(s1_cqc_lang__e2_98__sublemma,axiom,( ! [A,B] : ( ( ~ v1_xboole_0(A) & m1_valuat_1(B,A) ) => ( ! [C] : ( m2_subset_1(C,k8_qc_lang1,k7_cqc_lang) => ! [D] : ( m2_subset_1(D,k8_qc_lang1,k7_cqc_lang) => ! [E] : ( m2_subset_1(E,k1_qc_lang1,k2_qc_lang1) => ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ! [G] : ( ( v1_cqc_lang(G,F) & m1_qc_lang1(G,F) ) => ! [H] : ( m2_subset_1(H,k5_qc_lang1,k7_qc_lang1(F)) => ( ! [I] : ( m2_fraenkel(I,k2_qc_lang1,A,k2_valuat_1(A)) => ! [J] : ( ( v1_funct_1(J) & m2_relset_1(J,k2_qc_lang1,A) ) => ! [K] : ( ( v1_funct_1(K) & m2_relset_1(K,k2_qc_lang1,A) ) => ! [L] : ( ( v1_funct_1(L) & m2_relset_1(L,k2_qc_lang1,A) ) => ( ( ! [M] : ( m2_subset_1(M,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(M,k4_relset_1(k2_qc_lang1,A,K)) & r2_hidden(M,k24_qc_lang1(k9_cqc_lang)) ) ) & ! [M] : ( m2_subset_1(M,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(M,k4_relset_1(k2_qc_lang1,A,L)) => k1_funct_1(L,M) = k8_funct_2(k2_qc_lang1,A,I,M) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,A,J),k4_relset_1(k2_qc_lang1,A,L)) ) => ( r1_valuat_1(A,k9_cqc_lang,B,k1_sublemma(A,I,J)) <=> r1_valuat_1(A,k9_cqc_lang,B,k1_sublemma(A,I,k15_sublemma(A,k15_sublemma(A,J,K),L))) ) ) ) ) ) ) & ! [N] : ( m2_fraenkel(N,k2_qc_lang1,A,k2_valuat_1(A)) => ! [O] : ( ( v1_funct_1(O) & m2_relset_1(O,k2_qc_lang1,A) ) => ! [P] : ( ( v1_funct_1(P) & m2_relset_1(P,k2_qc_lang1,A) ) => ! [Q] : ( ( v1_funct_1(Q) & m2_relset_1(Q,k2_qc_lang1,A) ) => ( ( ! [R] : ( m2_subset_1(R,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(R,k4_relset_1(k2_qc_lang1,A,P)) & r2_hidden(R,k24_qc_lang1(k8_cqc_lang(F,H,G))) ) ) & ! [R] : ( m2_subset_1(R,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(R,k4_relset_1(k2_qc_lang1,A,Q)) => k1_funct_1(Q,R) = k8_funct_2(k2_qc_lang1,A,N,R) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,A,O),k4_relset_1(k2_qc_lang1,A,Q)) ) => ( r1_valuat_1(A,k8_cqc_lang(F,H,G),B,k1_sublemma(A,N,O)) <=> r1_valuat_1(A,k8_cqc_lang(F,H,G),B,k1_sublemma(A,N,k15_sublemma(A,k15_sublemma(A,O,P),Q))) ) ) ) ) ) ) & ( ! [S] : ( m2_fraenkel(S,k2_qc_lang1,A,k2_valuat_1(A)) => ! [T] : ( ( v1_funct_1(T) & m2_relset_1(T,k2_qc_lang1,A) ) => ! [U] : ( ( v1_funct_1(U) & m2_relset_1(U,k2_qc_lang1,A) ) => ! [V] : ( ( v1_funct_1(V) & m2_relset_1(V,k2_qc_lang1,A) ) => ( ( ! [W] : ( m2_subset_1(W,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(W,k4_relset_1(k2_qc_lang1,A,U)) & r2_hidden(W,k24_qc_lang1(C)) ) ) & ! [W] : ( m2_subset_1(W,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(W,k4_relset_1(k2_qc_lang1,A,V)) => k1_funct_1(V,W) = k8_funct_2(k2_qc_lang1,A,S,W) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,A,T),k4_relset_1(k2_qc_lang1,A,V)) ) => ( r1_valuat_1(A,C,B,k1_sublemma(A,S,T)) <=> r1_valuat_1(A,C,B,k1_sublemma(A,S,k15_sublemma(A,k15_sublemma(A,T,U),V))) ) ) ) ) ) ) => ! [X] : ( m2_fraenkel(X,k2_qc_lang1,A,k2_valuat_1(A)) => ! [Y] : ( ( v1_funct_1(Y) & m2_relset_1(Y,k2_qc_lang1,A) ) => ! [Z] : ( ( v1_funct_1(Z) & m2_relset_1(Z,k2_qc_lang1,A) ) => ! [A1] : ( ( v1_funct_1(A1) & m2_relset_1(A1,k2_qc_lang1,A) ) => ( ( ! [B1] : ( m2_subset_1(B1,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(B1,k4_relset_1(k2_qc_lang1,A,Z)) & r2_hidden(B1,k24_qc_lang1(k10_cqc_lang(C))) ) ) & ! [B1] : ( m2_subset_1(B1,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(B1,k4_relset_1(k2_qc_lang1,A,A1)) => k1_funct_1(A1,B1) = k8_funct_2(k2_qc_lang1,A,X,B1) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,A,Y),k4_relset_1(k2_qc_lang1,A,A1)) ) => ( r1_valuat_1(A,k10_cqc_lang(C),B,k1_sublemma(A,X,Y)) <=> r1_valuat_1(A,k10_cqc_lang(C),B,k1_sublemma(A,X,k15_sublemma(A,k15_sublemma(A,Y,Z),A1))) ) ) ) ) ) ) ) & ( ( ! [C1] : ( m2_fraenkel(C1,k2_qc_lang1,A,k2_valuat_1(A)) => ! [D1] : ( ( v1_funct_1(D1) & m2_relset_1(D1,k2_qc_lang1,A) ) => ! [E1] : ( ( v1_funct_1(E1) & m2_relset_1(E1,k2_qc_lang1,A) ) => ! [F1] : ( ( v1_funct_1(F1) & m2_relset_1(F1,k2_qc_lang1,A) ) => ( ( ! [G1] : ( m2_subset_1(G1,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(G1,k4_relset_1(k2_qc_lang1,A,E1)) & r2_hidden(G1,k24_qc_lang1(C)) ) ) & ! [G1] : ( m2_subset_1(G1,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(G1,k4_relset_1(k2_qc_lang1,A,F1)) => k1_funct_1(F1,G1) = k8_funct_2(k2_qc_lang1,A,C1,G1) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,A,D1),k4_relset_1(k2_qc_lang1,A,F1)) ) => ( r1_valuat_1(A,C,B,k1_sublemma(A,C1,D1)) <=> r1_valuat_1(A,C,B,k1_sublemma(A,C1,k15_sublemma(A,k15_sublemma(A,D1,E1),F1))) ) ) ) ) ) ) & ! [H1] : ( m2_fraenkel(H1,k2_qc_lang1,A,k2_valuat_1(A)) => ! [I1] : ( ( v1_funct_1(I1) & m2_relset_1(I1,k2_qc_lang1,A) ) => ! [J1] : ( ( v1_funct_1(J1) & m2_relset_1(J1,k2_qc_lang1,A) ) => ! [K1] : ( ( v1_funct_1(K1) & m2_relset_1(K1,k2_qc_lang1,A) ) => ( ( ! [L1] : ( m2_subset_1(L1,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(L1,k4_relset_1(k2_qc_lang1,A,J1)) & r2_hidden(L1,k24_qc_lang1(D)) ) ) & ! [L1] : ( m2_subset_1(L1,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(L1,k4_relset_1(k2_qc_lang1,A,K1)) => k1_funct_1(K1,L1) = k8_funct_2(k2_qc_lang1,A,H1,L1) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,A,I1),k4_relset_1(k2_qc_lang1,A,K1)) ) => ( r1_valuat_1(A,D,B,k1_sublemma(A,H1,I1)) <=> r1_valuat_1(A,D,B,k1_sublemma(A,H1,k15_sublemma(A,k15_sublemma(A,I1,J1),K1))) ) ) ) ) ) ) ) => ! [M1] : ( m2_fraenkel(M1,k2_qc_lang1,A,k2_valuat_1(A)) => ! [N1] : ( ( v1_funct_1(N1) & m2_relset_1(N1,k2_qc_lang1,A) ) => ! [O1] : ( ( v1_funct_1(O1) & m2_relset_1(O1,k2_qc_lang1,A) ) => ! [P1] : ( ( v1_funct_1(P1) & m2_relset_1(P1,k2_qc_lang1,A) ) => ( ( ! [Q1] : ( m2_subset_1(Q1,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(Q1,k4_relset_1(k2_qc_lang1,A,O1)) & r2_hidden(Q1,k24_qc_lang1(k11_cqc_lang(C,D))) ) ) & ! [Q1] : ( m2_subset_1(Q1,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(Q1,k4_relset_1(k2_qc_lang1,A,P1)) => k1_funct_1(P1,Q1) = k8_funct_2(k2_qc_lang1,A,M1,Q1) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,A,N1),k4_relset_1(k2_qc_lang1,A,P1)) ) => ( r1_valuat_1(A,k11_cqc_lang(C,D),B,k1_sublemma(A,M1,N1)) <=> r1_valuat_1(A,k11_cqc_lang(C,D),B,k1_sublemma(A,M1,k15_sublemma(A,k15_sublemma(A,N1,O1),P1))) ) ) ) ) ) ) ) & ( ! [R1] : ( m2_fraenkel(R1,k2_qc_lang1,A,k2_valuat_1(A)) => ! [S1] : ( ( v1_funct_1(S1) & m2_relset_1(S1,k2_qc_lang1,A) ) => ! [T1] : ( ( v1_funct_1(T1) & m2_relset_1(T1,k2_qc_lang1,A) ) => ! [U1] : ( ( v1_funct_1(U1) & m2_relset_1(U1,k2_qc_lang1,A) ) => ( ( ! [V1] : ( m2_subset_1(V1,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(V1,k4_relset_1(k2_qc_lang1,A,T1)) & r2_hidden(V1,k24_qc_lang1(C)) ) ) & ! [V1] : ( m2_subset_1(V1,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(V1,k4_relset_1(k2_qc_lang1,A,U1)) => k1_funct_1(U1,V1) = k8_funct_2(k2_qc_lang1,A,R1,V1) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,A,S1),k4_relset_1(k2_qc_lang1,A,U1)) ) => ( r1_valuat_1(A,C,B,k1_sublemma(A,R1,S1)) <=> r1_valuat_1(A,C,B,k1_sublemma(A,R1,k15_sublemma(A,k15_sublemma(A,S1,T1),U1))) ) ) ) ) ) ) => ! [W1] : ( m2_fraenkel(W1,k2_qc_lang1,A,k2_valuat_1(A)) => ! [X1] : ( ( v1_funct_1(X1) & m2_relset_1(X1,k2_qc_lang1,A) ) => ! [Y1] : ( ( v1_funct_1(Y1) & m2_relset_1(Y1,k2_qc_lang1,A) ) => ! [Z1] : ( ( v1_funct_1(Z1) & m2_relset_1(Z1,k2_qc_lang1,A) ) => ( ( ! [A2] : ( m2_subset_1(A2,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(A2,k4_relset_1(k2_qc_lang1,A,Y1)) & r2_hidden(A2,k24_qc_lang1(k15_cqc_lang(E,C))) ) ) & ! [A2] : ( m2_subset_1(A2,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(A2,k4_relset_1(k2_qc_lang1,A,Z1)) => k1_funct_1(Z1,A2) = k8_funct_2(k2_qc_lang1,A,W1,A2) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,A,X1),k4_relset_1(k2_qc_lang1,A,Z1)) ) => ( r1_valuat_1(A,k15_cqc_lang(E,C),B,k1_sublemma(A,W1,X1)) <=> r1_valuat_1(A,k15_cqc_lang(E,C),B,k1_sublemma(A,W1,k15_sublemma(A,k15_sublemma(A,X1,Y1),Z1))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => ! [C] : ( m2_subset_1(C,k8_qc_lang1,k7_cqc_lang) => ! [B2] : ( m2_fraenkel(B2,k2_qc_lang1,A,k2_valuat_1(A)) => ! [C2] : ( ( v1_funct_1(C2) & m2_relset_1(C2,k2_qc_lang1,A) ) => ! [D2] : ( ( v1_funct_1(D2) & m2_relset_1(D2,k2_qc_lang1,A) ) => ! [E2] : ( ( v1_funct_1(E2) & m2_relset_1(E2,k2_qc_lang1,A) ) => ( ( ! [F2] : ( m2_subset_1(F2,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(F2,k4_relset_1(k2_qc_lang1,A,D2)) & r2_hidden(F2,k24_qc_lang1(C)) ) ) & ! [F2] : ( m2_subset_1(F2,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(F2,k4_relset_1(k2_qc_lang1,A,E2)) => k1_funct_1(E2,F2) = k8_funct_2(k2_qc_lang1,A,B2,F2) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,A,C2),k4_relset_1(k2_qc_lang1,A,E2)) ) => ( r1_valuat_1(A,C,B,k1_sublemma(A,B2,C2)) <=> r1_valuat_1(A,C,B,k1_sublemma(A,B2,k15_sublemma(A,k15_sublemma(A,C2,D2),E2))) ) ) ) ) ) ) ) ) ) ), file(sublemma,s1_cqc_lang__e2_98__sublemma), []). fof(symmetry_r1_xboole_0,axiom,( ! [A,B] : ( r1_xboole_0(A,B) => r1_xboole_0(B,A) ) ), file(xboole_0,r1_xboole_0), []). fof(t1_subset,axiom,( ! [A,B] : ( r2_hidden(A,B) => m1_subset_1(A,B) ) ), file(subset,t1_subset), []). fof(t2_subset,axiom,( ! [A,B] : ( m1_subset_1(A,B) => ( v1_xboole_0(B) | r2_hidden(A,B) ) ) ), file(subset,t2_subset), []). fof(t2_tarski,axiom,( ! [A,B] : ( ! [C] : ( r2_hidden(C,A) <=> r2_hidden(C,B) ) => A = B ) ), file(tarski,t2_tarski), []). fof(t3_subset,axiom,( ! [A,B] : ( m1_subset_1(A,k1_zfmisc_1(B)) <=> r1_tarski(A,B) ) ), file(subset,t3_subset), []). fof(t44_valuat_1,axiom,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,k2_qc_lang1,A,k2_valuat_1(A)) => ! [C] : ( m1_valuat_1(C,A) => r1_valuat_1(A,k9_cqc_lang,C,B) ) ) ) ), file(valuat_1,t44_valuat_1), []). fof(t4_subset,axiom,( ! [A,B,C] : ( ( r2_hidden(A,B) & m1_subset_1(B,k1_zfmisc_1(C)) ) => m1_subset_1(A,C) ) ), file(subset,t4_subset), []). fof(t5_subset,axiom,( ! [A,B,C] : ~ ( r2_hidden(A,B) & m1_subset_1(B,k1_zfmisc_1(C)) & v1_xboole_0(C) ) ), file(subset,t5_subset), []). fof(t6_boole,axiom,( ! [A] : ( v1_xboole_0(A) => A = k1_xboole_0 ) ), file(boole,t6_boole), []). fof(t79_sublemma,axiom,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_valuat_1(C,B) => ! [D] : ( m2_subset_1(D,k5_qc_lang1,k7_qc_lang1(A)) => ! [E] : ( ( v1_cqc_lang(E,A) & m1_qc_lang1(E,A) ) => ! [F] : ( m2_fraenkel(F,k2_qc_lang1,B,k2_valuat_1(B)) => ! [G] : ( ( v1_funct_1(G) & m2_relset_1(G,k2_qc_lang1,B) ) => ! [H] : ( ( v1_funct_1(H) & m2_relset_1(H,k2_qc_lang1,B) ) => ! [I] : ( ( v1_funct_1(I) & m2_relset_1(I,k2_qc_lang1,B) ) => ( ( ! [J] : ( m2_subset_1(J,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(J,k4_relset_1(k2_qc_lang1,B,H)) & r2_hidden(J,k24_qc_lang1(k8_cqc_lang(A,D,E))) ) ) & ! [J] : ( m2_subset_1(J,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(J,k4_relset_1(k2_qc_lang1,B,I)) => k1_funct_1(I,J) = k8_funct_2(k2_qc_lang1,B,F,J) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,B,G),k4_relset_1(k2_qc_lang1,B,I)) ) => ( r1_valuat_1(B,k8_cqc_lang(A,D,E),C,k1_sublemma(B,F,G)) <=> r1_valuat_1(B,k8_cqc_lang(A,D,E),C,k1_sublemma(B,F,k15_sublemma(B,k15_sublemma(B,G,H),I))) ) ) ) ) ) ) ) ) ) ) ) ), file(sublemma,t79_sublemma), []). fof(t7_boole,axiom,( ! [A,B] : ~ ( r2_hidden(A,B) & v1_xboole_0(B) ) ), file(boole,t7_boole), []). fof(t80_sublemma,axiom,( ! [A] : ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_valuat_1(C,B) => ( ! [D] : ( m2_fraenkel(D,k2_qc_lang1,B,k2_valuat_1(B)) => ! [E] : ( ( v1_funct_1(E) & m2_relset_1(E,k2_qc_lang1,B) ) => ! [F] : ( ( v1_funct_1(F) & m2_relset_1(F,k2_qc_lang1,B) ) => ! [G] : ( ( v1_funct_1(G) & m2_relset_1(G,k2_qc_lang1,B) ) => ( ( ! [H] : ( m2_subset_1(H,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(H,k4_relset_1(k2_qc_lang1,B,F)) & r2_hidden(H,k24_qc_lang1(A)) ) ) & ! [H] : ( m2_subset_1(H,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(H,k4_relset_1(k2_qc_lang1,B,G)) => k1_funct_1(G,H) = k8_funct_2(k2_qc_lang1,B,D,H) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,B,E),k4_relset_1(k2_qc_lang1,B,G)) ) => ( r1_valuat_1(B,A,C,k1_sublemma(B,D,E)) <=> r1_valuat_1(B,A,C,k1_sublemma(B,D,k15_sublemma(B,k15_sublemma(B,E,F),G))) ) ) ) ) ) ) => ! [D] : ( m2_fraenkel(D,k2_qc_lang1,B,k2_valuat_1(B)) => ! [E] : ( ( v1_funct_1(E) & m2_relset_1(E,k2_qc_lang1,B) ) => ! [F] : ( ( v1_funct_1(F) & m2_relset_1(F,k2_qc_lang1,B) ) => ! [G] : ( ( v1_funct_1(G) & m2_relset_1(G,k2_qc_lang1,B) ) => ( ( ! [H] : ( m2_subset_1(H,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(H,k4_relset_1(k2_qc_lang1,B,F)) & r2_hidden(H,k24_qc_lang1(k10_cqc_lang(A))) ) ) & ! [H] : ( m2_subset_1(H,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(H,k4_relset_1(k2_qc_lang1,B,G)) => k1_funct_1(G,H) = k8_funct_2(k2_qc_lang1,B,D,H) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,B,E),k4_relset_1(k2_qc_lang1,B,G)) ) => ( r1_valuat_1(B,k10_cqc_lang(A),C,k1_sublemma(B,D,E)) <=> r1_valuat_1(B,k10_cqc_lang(A),C,k1_sublemma(B,D,k15_sublemma(B,k15_sublemma(B,E,F),G))) ) ) ) ) ) ) ) ) ) ) ), file(sublemma,t80_sublemma), []). fof(t81_sublemma,axiom,( ! [A] : ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) => ! [B] : ( m2_subset_1(B,k8_qc_lang1,k7_cqc_lang) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_valuat_1(D,C) => ( ( ! [E] : ( m2_fraenkel(E,k2_qc_lang1,C,k2_valuat_1(C)) => ! [F] : ( ( v1_funct_1(F) & m2_relset_1(F,k2_qc_lang1,C) ) => ! [G] : ( ( v1_funct_1(G) & m2_relset_1(G,k2_qc_lang1,C) ) => ! [H] : ( ( v1_funct_1(H) & m2_relset_1(H,k2_qc_lang1,C) ) => ( ( ! [I] : ( m2_subset_1(I,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(I,k4_relset_1(k2_qc_lang1,C,G)) & r2_hidden(I,k24_qc_lang1(A)) ) ) & ! [I] : ( m2_subset_1(I,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(I,k4_relset_1(k2_qc_lang1,C,H)) => k1_funct_1(H,I) = k8_funct_2(k2_qc_lang1,C,E,I) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,C,F),k4_relset_1(k2_qc_lang1,C,H)) ) => ( r1_valuat_1(C,A,D,k1_sublemma(C,E,F)) <=> r1_valuat_1(C,A,D,k1_sublemma(C,E,k15_sublemma(C,k15_sublemma(C,F,G),H))) ) ) ) ) ) ) & ! [E] : ( m2_fraenkel(E,k2_qc_lang1,C,k2_valuat_1(C)) => ! [F] : ( ( v1_funct_1(F) & m2_relset_1(F,k2_qc_lang1,C) ) => ! [G] : ( ( v1_funct_1(G) & m2_relset_1(G,k2_qc_lang1,C) ) => ! [H] : ( ( v1_funct_1(H) & m2_relset_1(H,k2_qc_lang1,C) ) => ( ( ! [I] : ( m2_subset_1(I,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(I,k4_relset_1(k2_qc_lang1,C,G)) & r2_hidden(I,k24_qc_lang1(B)) ) ) & ! [I] : ( m2_subset_1(I,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(I,k4_relset_1(k2_qc_lang1,C,H)) => k1_funct_1(H,I) = k8_funct_2(k2_qc_lang1,C,E,I) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,C,F),k4_relset_1(k2_qc_lang1,C,H)) ) => ( r1_valuat_1(C,B,D,k1_sublemma(C,E,F)) <=> r1_valuat_1(C,B,D,k1_sublemma(C,E,k15_sublemma(C,k15_sublemma(C,F,G),H))) ) ) ) ) ) ) ) => ! [E] : ( m2_fraenkel(E,k2_qc_lang1,C,k2_valuat_1(C)) => ! [F] : ( ( v1_funct_1(F) & m2_relset_1(F,k2_qc_lang1,C) ) => ! [G] : ( ( v1_funct_1(G) & m2_relset_1(G,k2_qc_lang1,C) ) => ! [H] : ( ( v1_funct_1(H) & m2_relset_1(H,k2_qc_lang1,C) ) => ( ( ! [I] : ( m2_subset_1(I,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(I,k4_relset_1(k2_qc_lang1,C,G)) & r2_hidden(I,k24_qc_lang1(k11_cqc_lang(A,B))) ) ) & ! [I] : ( m2_subset_1(I,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(I,k4_relset_1(k2_qc_lang1,C,H)) => k1_funct_1(H,I) = k8_funct_2(k2_qc_lang1,C,E,I) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,C,F),k4_relset_1(k2_qc_lang1,C,H)) ) => ( r1_valuat_1(C,k11_cqc_lang(A,B),D,k1_sublemma(C,E,F)) <=> r1_valuat_1(C,k11_cqc_lang(A,B),D,k1_sublemma(C,E,k15_sublemma(C,k15_sublemma(C,F,G),H))) ) ) ) ) ) ) ) ) ) ) ) ), file(sublemma,t81_sublemma), []). fof(t84_sublemma,axiom,( ! [A] : ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) => ! [B] : ( m2_subset_1(B,k1_qc_lang1,k2_qc_lang1) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_valuat_1(D,C) => ( ! [E] : ( m2_fraenkel(E,k2_qc_lang1,C,k2_valuat_1(C)) => ! [F] : ( ( v1_funct_1(F) & m2_relset_1(F,k2_qc_lang1,C) ) => ! [G] : ( ( v1_funct_1(G) & m2_relset_1(G,k2_qc_lang1,C) ) => ! [H] : ( ( v1_funct_1(H) & m2_relset_1(H,k2_qc_lang1,C) ) => ( ( ! [I] : ( m2_subset_1(I,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(I,k4_relset_1(k2_qc_lang1,C,G)) & r2_hidden(I,k24_qc_lang1(A)) ) ) & ! [I] : ( m2_subset_1(I,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(I,k4_relset_1(k2_qc_lang1,C,H)) => k1_funct_1(H,I) = k8_funct_2(k2_qc_lang1,C,E,I) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,C,F),k4_relset_1(k2_qc_lang1,C,H)) ) => ( r1_valuat_1(C,A,D,k1_sublemma(C,E,F)) <=> r1_valuat_1(C,A,D,k1_sublemma(C,E,k15_sublemma(C,k15_sublemma(C,F,G),H))) ) ) ) ) ) ) => ! [E] : ( m2_fraenkel(E,k2_qc_lang1,C,k2_valuat_1(C)) => ! [F] : ( ( v1_funct_1(F) & m2_relset_1(F,k2_qc_lang1,C) ) => ! [G] : ( ( v1_funct_1(G) & m2_relset_1(G,k2_qc_lang1,C) ) => ! [H] : ( ( v1_funct_1(H) & m2_relset_1(H,k2_qc_lang1,C) ) => ( ( ! [I] : ( m2_subset_1(I,k1_qc_lang1,k2_qc_lang1) => ~ ( r2_hidden(I,k4_relset_1(k2_qc_lang1,C,G)) & r2_hidden(I,k24_qc_lang1(k15_cqc_lang(B,A))) ) ) & ! [I] : ( m2_subset_1(I,k1_qc_lang1,k2_qc_lang1) => ( r2_hidden(I,k4_relset_1(k2_qc_lang1,C,H)) => k1_funct_1(H,I) = k8_funct_2(k2_qc_lang1,C,E,I) ) ) & r1_xboole_0(k4_relset_1(k2_qc_lang1,C,F),k4_relset_1(k2_qc_lang1,C,H)) ) => ( r1_valuat_1(C,k15_cqc_lang(B,A),D,k1_sublemma(C,E,F)) <=> r1_valuat_1(C,k15_cqc_lang(B,A),D,k1_sublemma(C,E,k15_sublemma(C,k15_sublemma(C,F,G),H))) ) ) ) ) ) ) ) ) ) ) ) ), file(sublemma,t84_sublemma), []). fof(t8_boole,axiom,( ! [A,B] : ~ ( v1_xboole_0(A) & A != B & v1_xboole_0(B) ) ), file(boole,t8_boole), []).