fof(t41_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => k6_qc_lang3(k17_cqc_lang(B,A)) = k6_qc_lang3(B) ) ) ), inference(mizar_proof,[status(thm)],[t77_qc_lang3,d3_cqc_lang,t40_qc_lang3,t11_cqc_lang,t11_cqc_lang,l9_cqc_lang,t11_cqc_lang,t2_tarski,t30_cqc_lang,t28_cqc_lang,t32_cqc_lang,t78_qc_lang3,t78_qc_lang3,t34_cqc_lang,t80_qc_lang3,t80_qc_lang3,t38_cqc_lang,t81_qc_lang3,t81_qc_lang3,t37_cqc_lang,s1_qc_lang1]), [file(cqc_lang,t41_cqc_lang),interesting(1.00)]). fof(t40_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m2_subset_1(B,k8_qc_lang1,k7_cqc_lang) => k17_cqc_lang(B,A) = B ) ) ), inference(mizar_proof,[status(thm)],[t13_cqc_lang,t39_cqc_lang]), [file(cqc_lang,t40_cqc_lang),interesting(0.95)]). fof(t39_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( k5_qc_lang3(B) = k1_xboole_0 => k17_cqc_lang(B,A) = B ) ) ) ), inference(mizar_proof,[status(thm)],[d3_cqc_lang,t66_qc_lang3,t11_cqc_lang,t18_finseq_1,t30_cqc_lang,t28_cqc_lang,t32_cqc_lang,t67_qc_lang3,t69_qc_lang3,t34_cqc_lang,t15_xboole_1,t37_cqc_lang,t38_cqc_lang,t70_qc_lang3,s1_qc_lang1]), [file(cqc_lang,t39_cqc_lang),interesting(0.94)]). fof(t37_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => k17_cqc_lang(k14_qc_lang1(A,B),A) = k14_qc_lang1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d20_qc_lang1,d26_qc_lang1,t35_cqc_lang]), [file(cqc_lang,t37_cqc_lang),interesting(0.79)]). fof(t42_cqc_lang,theorem,( ! [A,B,C] : k9_funct_2(A,B,C) = k3_cqc_lang(k4_tarski(A,B),C) ), inference(mizar_proof,[status(thm)],[t35_zfmisc_1,t5_cqc_lang,d1_funct_2,t11_relset_1,d5_funct_2]), [file(cqc_lang,t42_cqc_lang),interesting(0.77)]). fof(t32_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => k17_cqc_lang(k12_qc_lang1(B),A) = k12_qc_lang1(k17_cqc_lang(B,A)) ) ) ), inference(mizar_proof,[status(thm)],[d18_qc_lang1,d23_qc_lang1,t31_cqc_lang]), [file(cqc_lang,t32_cqc_lang),interesting(0.76)]). fof(t35_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( ( v5_qc_lang1(B) & k20_qc_lang1(B) = A ) => k17_cqc_lang(B,A) = B ) ) ) ), inference(mizar_proof,[status(thm)],[l43_cqc_lang,d1_cqc_lang]), [file(cqc_lang,t35_cqc_lang),interesting(0.75)]). fof(t31_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( v3_qc_lang1(B) => k17_cqc_lang(B,A) = k12_qc_lang1(k17_cqc_lang(k17_qc_lang1(B),A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_cqc_lang,d6_cqc_lang,l31_cqc_lang]), [file(cqc_lang,t31_cqc_lang),interesting(0.73)]). fof(t34_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ! [C] : ( m1_subset_1(C,k8_qc_lang1) => k17_cqc_lang(k13_qc_lang1(B,C),A) = k13_qc_lang1(k17_cqc_lang(B,A),k17_cqc_lang(C,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d19_qc_lang1,d24_qc_lang1,d25_qc_lang1,t33_cqc_lang]), [file(cqc_lang,t34_cqc_lang),interesting(0.73)]). fof(t38_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m2_subset_1(B,k1_qc_lang1,k2_qc_lang1) => ! [C] : ( m1_subset_1(C,k8_qc_lang1) => ( A != B => k17_cqc_lang(k14_qc_lang1(A,C),B) = k14_qc_lang1(A,k17_cqc_lang(C,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_qc_lang1,d26_qc_lang1,d27_qc_lang1,t36_cqc_lang]), [file(cqc_lang,t38_cqc_lang),interesting(0.73)]). fof(t43_cqc_lang,theorem,( ! [A,B,C] : k1_binop_1(k9_funct_2(A,B,C),A,B) = C ), inference(mizar_proof,[status(thm)],[t42_cqc_lang,t6_cqc_lang]), [file(cqc_lang,t43_cqc_lang),interesting(0.73)]). fof(l9_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ~ r2_hidden(A,k3_qc_lang1) ) ), inference(mizar_proof,[status(thm)],[d2_qc_lang1,d2_zfmisc_1,d3_qc_lang1,d2_zfmisc_1,d1_tarski,t33_zfmisc_1]), [file(cqc_lang,l9_cqc_lang),interesting(0.72)]). fof(t33_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( v4_qc_lang1(B) => k17_cqc_lang(B,A) = k13_qc_lang1(k17_cqc_lang(k18_qc_lang1(B),A),k17_cqc_lang(k19_qc_lang1(B),A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_cqc_lang,d6_cqc_lang,d6_cqc_lang,l31_cqc_lang]), [file(cqc_lang,t33_cqc_lang),interesting(0.71)]). fof(t36_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( v5_qc_lang1(B) => ( k20_qc_lang1(B) = A | k17_cqc_lang(B,A) = k14_qc_lang1(k20_qc_lang1(B),k17_cqc_lang(k21_qc_lang1(B),A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l43_cqc_lang,d1_cqc_lang]), [file(cqc_lang,t36_cqc_lang),interesting(0.71)]). fof(t6_cqc_lang,theorem,( ! [A,B] : k1_funct_1(k3_cqc_lang(A,B),A) = B ), inference(mizar_proof,[status(thm)],[d1_tarski,t13_funcop_1]), [file(cqc_lang,t6_cqc_lang),interesting(0.70)]). fof(t7_cqc_lang,theorem,( ! [A] : ( r2_hidden(A,k1_qc_lang1) <=> ~ ( ~ r2_hidden(A,k3_qc_lang1) & ~ r2_hidden(A,k4_qc_lang1) & ~ r2_hidden(A,k2_qc_lang1) ) ) ), inference(mizar_proof,[status(thm)],[d1_qc_lang1,d2_zfmisc_1,d1_enumset1,d1_tarski,d2_qc_lang1,d3_qc_lang1,d4_qc_lang1,d2_zfmisc_1]), [file(cqc_lang,t7_cqc_lang),interesting(0.69)]). fof(t28_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => k17_cqc_lang(k9_cqc_lang,A) = k9_cqc_lang ) ), inference(mizar_proof,[status(thm)],[d6_cqc_lang]), [file(cqc_lang,t28_cqc_lang),interesting(0.69)]). fof(l43_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( v5_qc_lang1(B) => k17_cqc_lang(B,A) = k2_cqc_lang(k8_qc_lang1,k20_qc_lang1(B),A,B,k14_qc_lang1(k20_qc_lang1(B),k17_cqc_lang(k21_qc_lang1(B),A))) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_cqc_lang,d6_cqc_lang,l31_cqc_lang]), [file(cqc_lang,l43_cqc_lang),interesting(0.69)]). fof(t15_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_qc_lang1(B,A) => ( ( v1_cqc_lang(B,A) & m1_qc_lang1(B,A) ) <=> ( a_2_0_cqc_lang(A,B) = k1_xboole_0 & a_2_1_cqc_lang(A,B) = k1_xboole_0 ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_cqc_lang,t27_finseq_3,d5_funct_1,t42_qc_lang3,d5_cqc_lang,t27_finseq_3,d5_funct_1,t41_qc_lang3,d3_tarski,d5_cqc_lang,d5_funct_1,d4_finseq_1,d5_funct_1,t27_finseq_3,t7_cqc_lang]), [file(cqc_lang,t15_cqc_lang),interesting(0.67)]). fof(t18_cqc_lang,theorem,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ( m2_subset_1(k12_qc_lang1(A),k8_qc_lang1,k7_cqc_lang) <=> m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) ) ) ), inference(mizar_proof,[status(thm)],[t13_cqc_lang,t67_qc_lang3,t78_qc_lang3,t13_cqc_lang,t13_cqc_lang,t67_qc_lang3,t78_qc_lang3,t13_cqc_lang]), [file(cqc_lang,t18_cqc_lang),interesting(0.67)]). 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) ) ), inference(mizar_proof,[status(thm)],[t14_funcop_1,t19_funcop_1]), [file(cqc_lang,t5_cqc_lang),interesting(0.67)]). fof(t19_cqc_lang,theorem,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( m2_subset_1(k13_qc_lang1(A,B),k8_qc_lang1,k7_cqc_lang) <=> ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) & m2_subset_1(B,k8_qc_lang1,k7_cqc_lang) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_cqc_lang,t69_qc_lang3,t80_qc_lang3,t15_xboole_1,t13_cqc_lang,t13_cqc_lang,t69_qc_lang3,t80_qc_lang3,t13_cqc_lang]), [file(cqc_lang,t19_cqc_lang),interesting(0.66)]). fof(t23_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( m2_subset_1(k14_qc_lang1(A,B),k8_qc_lang1,k7_cqc_lang) <=> m2_subset_1(B,k8_qc_lang1,k7_cqc_lang) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_cqc_lang,t70_qc_lang3,t81_qc_lang3,t13_cqc_lang,t13_cqc_lang,t70_qc_lang3,t81_qc_lang3,t13_cqc_lang]), [file(cqc_lang,t23_cqc_lang),interesting(0.66)]). fof(t16_cqc_lang,theorem,( m2_subset_1(k11_qc_lang1,k8_qc_lang1,k7_cqc_lang) ), inference(mizar_proof,[status(thm)],[t13_cqc_lang,t65_qc_lang3,t76_qc_lang3]), [file(cqc_lang,t16_cqc_lang),interesting(0.64)]). fof(t17_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k5_qc_lang1,k7_qc_lang1(A)) => ! [C] : ( m1_qc_lang1(C,A) => ( m2_subset_1(k9_qc_lang1(B,C),k8_qc_lang1,k7_cqc_lang) <=> ( a_2_0_cqc_lang(A,C) = k1_xboole_0 & a_2_1_cqc_lang(A,C) = k1_xboole_0 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t66_qc_lang3,t77_qc_lang3,t13_cqc_lang]), [file(cqc_lang,t17_cqc_lang),interesting(0.59)]). fof(t22_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) => ! [B] : ( m2_subset_1(B,k8_qc_lang1,k7_cqc_lang) => m2_subset_1(k4_qc_lang2(A,B),k8_qc_lang1,k7_cqc_lang) ) ) ), inference(mizar_proof,[status(thm)],[d4_qc_lang2,d2_qc_lang2,d2_qc_lang2]), [file(cqc_lang,t22_cqc_lang),interesting(0.59)]). fof(t30_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_qc_lang1,k2_qc_lang1) => ! [C] : ( m2_subset_1(C,k5_qc_lang1,k7_qc_lang1(A)) => ! [D] : ( m1_qc_lang1(D,A) => k17_cqc_lang(k9_qc_lang1(C,D),B) = k9_qc_lang1(C,k5_cqc_lang(A,D,k6_cqc_lang(k3_qc_lang3(0),B))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d17_qc_lang1,d21_qc_lang1,d22_qc_lang1,t29_cqc_lang]), [file(cqc_lang,t30_cqc_lang),interesting(0.59)]). fof(s1_cqc_lang,theorem, ( ! [A] : ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) => ! [B] : ( m2_subset_1(B,k8_qc_lang1,k7_cqc_lang) => ! [C] : ( m2_subset_1(C,k1_qc_lang1,k2_qc_lang1) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( ( v1_cqc_lang(E,D) & m1_qc_lang1(E,D) ) => ! [F] : ( m2_subset_1(F,k5_qc_lang1,k7_qc_lang1(D)) => ( p1_s1_cqc_lang(k9_cqc_lang) & p1_s1_cqc_lang(k8_cqc_lang(D,F,E)) & ( p1_s1_cqc_lang(A) => p1_s1_cqc_lang(k10_cqc_lang(A)) ) & ( ( p1_s1_cqc_lang(A) & p1_s1_cqc_lang(B) ) => p1_s1_cqc_lang(k11_cqc_lang(A,B)) ) & ( p1_s1_cqc_lang(A) => p1_s1_cqc_lang(k15_cqc_lang(C,A)) ) ) ) ) ) ) ) ) => ! [A] : ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) => p1_s1_cqc_lang(A) ) ), inference(mizar_proof,[status(thm)],[t17_cqc_lang,t15_cqc_lang,t18_cqc_lang,t19_cqc_lang,t23_cqc_lang,s1_qc_lang1]), [file(cqc_lang,s1_cqc_lang),interesting(0.58)]). fof(t29_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( v2_qc_lang1(B) => k17_cqc_lang(B,A) = k9_qc_lang1(k15_qc_lang1(B),k4_cqc_lang(k16_qc_lang1(B),k6_cqc_lang(k3_qc_lang3(0),A))) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_cqc_lang]), [file(cqc_lang,t29_cqc_lang),interesting(0.58)]). fof(t10_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m2_subset_1(B,k1_qc_lang1,k4_qc_lang1) => ( v1_funct_1(k3_cqc_lang(B,A)) & m2_relset_1(k3_cqc_lang(B,A),k4_qc_lang1,k1_qc_lang1) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,t37_zfmisc_1,t11_relset_1]), [file(cqc_lang,t10_cqc_lang),interesting(0.57)]). fof(t20_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) => ! [B] : ( m2_subset_1(B,k8_qc_lang1,k7_cqc_lang) => m2_subset_1(k2_qc_lang2(A,B),k8_qc_lang1,k7_cqc_lang) ) ) ), inference(mizar_proof,[status(thm)],[d2_qc_lang2]), [file(cqc_lang,t20_cqc_lang),interesting(0.57)]). fof(t21_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) => ! [B] : ( m2_subset_1(B,k8_qc_lang1,k7_cqc_lang) => m2_subset_1(k3_qc_lang2(A,B),k8_qc_lang1,k7_cqc_lang) ) ) ), inference(mizar_proof,[status(thm)],[d3_qc_lang2]), [file(cqc_lang,t21_cqc_lang),interesting(0.57)]). fof(t24_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m2_subset_1(B,k8_qc_lang1,k7_cqc_lang) => m2_subset_1(k5_qc_lang2(A,B),k8_qc_lang1,k7_cqc_lang) ) ) ), inference(mizar_proof,[status(thm)],[d5_qc_lang2]), [file(cqc_lang,t24_cqc_lang),interesting(0.55)]). fof(t11_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_qc_lang1,k2_qc_lang1) => ! [C] : ( m2_subset_1(C,k1_qc_lang1,k4_qc_lang1) => ! [D] : ( m2_finseq_1(D,k1_qc_lang1) => ! [E] : ( m2_finseq_1(E,k1_qc_lang1) => ! [F] : ( ( v1_funct_1(F) & m2_relset_1(F,k4_qc_lang1,k1_qc_lang1) ) => ( ( F = k6_cqc_lang(C,B) & D = k4_cqc_lang(E,F) & r1_xreal_0(1,A) & r1_xreal_0(A,k3_finseq_1(E)) ) => ( ( k1_funct_1(E,A) = C => k1_funct_1(D,A) = B ) & ( k1_funct_1(E,A) != C => k1_funct_1(D,A) = k1_funct_1(E,A) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_tarski,t5_cqc_lang,t6_cqc_lang,d3_cqc_lang,d1_tarski,t5_cqc_lang,d3_cqc_lang]), [file(cqc_lang,t11_cqc_lang),interesting(0.52)]). fof(s2_cqc_lang,theorem,( ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k7_cqc_lang,f1_s2_cqc_lang) & m2_relset_1(A,k7_cqc_lang,f1_s2_cqc_lang) & k8_funct_2(k7_cqc_lang,f1_s2_cqc_lang,A,k9_cqc_lang) = f2_s2_cqc_lang & ! [B] : ( m2_subset_1(B,k8_qc_lang1,k7_cqc_lang) => ! [C] : ( m2_subset_1(C,k8_qc_lang1,k7_cqc_lang) => ! [D] : ( m2_subset_1(D,k1_qc_lang1,k2_qc_lang1) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ! [F] : ( ( v1_cqc_lang(F,E) & m1_qc_lang1(F,E) ) => ! [G] : ( m2_subset_1(G,k5_qc_lang1,k7_qc_lang1(E)) => ( k8_funct_2(k7_cqc_lang,f1_s2_cqc_lang,A,k8_cqc_lang(E,G,F)) = f3_s2_cqc_lang(E,G,F) & k8_funct_2(k7_cqc_lang,f1_s2_cqc_lang,A,k10_cqc_lang(B)) = f4_s2_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s2_cqc_lang,A,B)) & k8_funct_2(k7_cqc_lang,f1_s2_cqc_lang,A,k11_cqc_lang(B,C)) = f5_s2_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s2_cqc_lang,A,B),k8_funct_2(k7_cqc_lang,f1_s2_cqc_lang,A,C)) & k8_funct_2(k7_cqc_lang,f1_s2_cqc_lang,A,k15_cqc_lang(D,B)) = f6_s2_cqc_lang(D,k8_funct_2(k7_cqc_lang,f1_s2_cqc_lang,A,B)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[s3_qc_lang1,t38_funct_2,t72_funct_1,d17_qc_lang1,t35_qc_lang1,d21_qc_lang1,d22_qc_lang1,t72_funct_1,t72_funct_1,d18_qc_lang1,d23_qc_lang1,t72_funct_1,d19_qc_lang1,d24_qc_lang1,d25_qc_lang1,t72_funct_1,d20_qc_lang1,d26_qc_lang1,d27_qc_lang1,t72_funct_1]), [file(cqc_lang,s2_cqc_lang),interesting(0.34)]). fof(s3_cqc_lang,theorem, ( ( k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f2_s3_cqc_lang,k9_cqc_lang) = f4_s3_cqc_lang & ! [A] : ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) => ! [B] : ( m2_subset_1(B,k8_qc_lang1,k7_cqc_lang) => ! [C] : ( m2_subset_1(C,k1_qc_lang1,k2_qc_lang1) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( ( v1_cqc_lang(E,D) & m1_qc_lang1(E,D) ) => ! [F] : ( m2_subset_1(F,k5_qc_lang1,k7_qc_lang1(D)) => ( k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f2_s3_cqc_lang,k8_cqc_lang(D,F,E)) = f5_s3_cqc_lang(D,F,E) & k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f2_s3_cqc_lang,k10_cqc_lang(A)) = f6_s3_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f2_s3_cqc_lang,A)) & k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f2_s3_cqc_lang,k11_cqc_lang(A,B)) = f7_s3_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f2_s3_cqc_lang,A),k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f2_s3_cqc_lang,B)) & k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f2_s3_cqc_lang,k15_cqc_lang(C,A)) = f8_s3_cqc_lang(C,k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f2_s3_cqc_lang,A)) ) ) ) ) ) ) ) & k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f3_s3_cqc_lang,k9_cqc_lang) = f4_s3_cqc_lang & ! [A] : ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) => ! [B] : ( m2_subset_1(B,k8_qc_lang1,k7_cqc_lang) => ! [C] : ( m2_subset_1(C,k1_qc_lang1,k2_qc_lang1) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( ( v1_cqc_lang(E,D) & m1_qc_lang1(E,D) ) => ! [F] : ( m2_subset_1(F,k5_qc_lang1,k7_qc_lang1(D)) => ( k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f3_s3_cqc_lang,k8_cqc_lang(D,F,E)) = f5_s3_cqc_lang(D,F,E) & k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f3_s3_cqc_lang,k10_cqc_lang(A)) = f6_s3_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f3_s3_cqc_lang,A)) & k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f3_s3_cqc_lang,k11_cqc_lang(A,B)) = f7_s3_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f3_s3_cqc_lang,A),k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f3_s3_cqc_lang,B)) & k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f3_s3_cqc_lang,k15_cqc_lang(C,A)) = f8_s3_cqc_lang(C,k8_funct_2(k7_cqc_lang,f1_s3_cqc_lang,f3_s3_cqc_lang,A)) ) ) ) ) ) ) ) ) => f2_s3_cqc_lang = f3_s3_cqc_lang ), inference(mizar_proof,[status(thm)],[s1_cqc_lang,t113_funct_2]), [file(cqc_lang,s3_cqc_lang),interesting(0.33)]). fof(s8_cqc_lang,theorem, ( ! [A] : ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) => ! [B] : ( m1_subset_1(B,f1_s8_cqc_lang) => ( B = f2_s8_cqc_lang(A) <=> ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k7_cqc_lang,f1_s8_cqc_lang) & m2_relset_1(C,k7_cqc_lang,f1_s8_cqc_lang) & B = k8_funct_2(k7_cqc_lang,f1_s8_cqc_lang,C,A) & k8_funct_2(k7_cqc_lang,f1_s8_cqc_lang,C,k9_cqc_lang) = f3_s8_cqc_lang & ! [D] : ( m2_subset_1(D,k8_qc_lang1,k7_cqc_lang) => ! [E] : ( m2_subset_1(E,k8_qc_lang1,k7_cqc_lang) => ! [F] : ( m2_subset_1(F,k1_qc_lang1,k2_qc_lang1) => ! [G] : ( m2_subset_1(G,k1_numbers,k5_numbers) => ! [H] : ( ( v1_cqc_lang(H,G) & m1_qc_lang1(H,G) ) => ! [I] : ( m2_subset_1(I,k5_qc_lang1,k7_qc_lang1(G)) => ( k8_funct_2(k7_cqc_lang,f1_s8_cqc_lang,C,k8_cqc_lang(G,I,H)) = f4_s8_cqc_lang(G,I,H) & k8_funct_2(k7_cqc_lang,f1_s8_cqc_lang,C,k10_cqc_lang(D)) = f5_s8_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s8_cqc_lang,C,D)) & k8_funct_2(k7_cqc_lang,f1_s8_cqc_lang,C,k11_cqc_lang(D,E)) = f6_s8_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s8_cqc_lang,C,D),k8_funct_2(k7_cqc_lang,f1_s8_cqc_lang,C,E)) & k8_funct_2(k7_cqc_lang,f1_s8_cqc_lang,C,k15_cqc_lang(F,D)) = f9_s8_cqc_lang(F,k8_funct_2(k7_cqc_lang,f1_s8_cqc_lang,C,D)) ) ) ) ) ) ) ) ) ) ) ) => f2_s8_cqc_lang(k11_cqc_lang(f7_s8_cqc_lang,f8_s8_cqc_lang)) = f6_s8_cqc_lang(f2_s8_cqc_lang(f7_s8_cqc_lang),f2_s8_cqc_lang(f8_s8_cqc_lang)) ), inference(mizar_proof,[status(thm)],[s2_cqc_lang,s3_cqc_lang,s3_cqc_lang]), [file(cqc_lang,s8_cqc_lang),interesting(0.23)]). fof(s7_cqc_lang,theorem, ( ! [A] : ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) => ! [B] : ( m1_subset_1(B,f1_s7_cqc_lang) => ( B = f2_s7_cqc_lang(A) <=> ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k7_cqc_lang,f1_s7_cqc_lang) & m2_relset_1(C,k7_cqc_lang,f1_s7_cqc_lang) & B = k8_funct_2(k7_cqc_lang,f1_s7_cqc_lang,C,A) & k8_funct_2(k7_cqc_lang,f1_s7_cqc_lang,C,k9_cqc_lang) = f3_s7_cqc_lang & ! [D] : ( m2_subset_1(D,k8_qc_lang1,k7_cqc_lang) => ! [E] : ( m2_subset_1(E,k8_qc_lang1,k7_cqc_lang) => ! [F] : ( m2_subset_1(F,k1_qc_lang1,k2_qc_lang1) => ! [G] : ( m2_subset_1(G,k1_numbers,k5_numbers) => ! [H] : ( ( v1_cqc_lang(H,G) & m1_qc_lang1(H,G) ) => ! [I] : ( m2_subset_1(I,k5_qc_lang1,k7_qc_lang1(G)) => ( k8_funct_2(k7_cqc_lang,f1_s7_cqc_lang,C,k8_cqc_lang(G,I,H)) = f4_s7_cqc_lang(G,I,H) & k8_funct_2(k7_cqc_lang,f1_s7_cqc_lang,C,k10_cqc_lang(D)) = f5_s7_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s7_cqc_lang,C,D)) & k8_funct_2(k7_cqc_lang,f1_s7_cqc_lang,C,k11_cqc_lang(D,E)) = f7_s7_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s7_cqc_lang,C,D),k8_funct_2(k7_cqc_lang,f1_s7_cqc_lang,C,E)) & k8_funct_2(k7_cqc_lang,f1_s7_cqc_lang,C,k15_cqc_lang(F,D)) = f8_s7_cqc_lang(F,k8_funct_2(k7_cqc_lang,f1_s7_cqc_lang,C,D)) ) ) ) ) ) ) ) ) ) ) ) => f2_s7_cqc_lang(k10_cqc_lang(f6_s7_cqc_lang)) = f5_s7_cqc_lang(f2_s7_cqc_lang(f6_s7_cqc_lang)) ), inference(mizar_proof,[status(thm)],[s2_cqc_lang,s3_cqc_lang]), [file(cqc_lang,s7_cqc_lang),interesting(0.19)]). fof(s9_cqc_lang,theorem, ( ! [A] : ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) => ! [B] : ( m1_subset_1(B,f1_s9_cqc_lang) => ( B = f2_s9_cqc_lang(A) <=> ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k7_cqc_lang,f1_s9_cqc_lang) & m2_relset_1(C,k7_cqc_lang,f1_s9_cqc_lang) & B = k8_funct_2(k7_cqc_lang,f1_s9_cqc_lang,C,A) & k8_funct_2(k7_cqc_lang,f1_s9_cqc_lang,C,k9_cqc_lang) = f3_s9_cqc_lang & ! [D] : ( m2_subset_1(D,k8_qc_lang1,k7_cqc_lang) => ! [E] : ( m2_subset_1(E,k8_qc_lang1,k7_cqc_lang) => ! [F] : ( m2_subset_1(F,k1_qc_lang1,k2_qc_lang1) => ! [G] : ( m2_subset_1(G,k1_numbers,k5_numbers) => ! [H] : ( ( v1_cqc_lang(H,G) & m1_qc_lang1(H,G) ) => ! [I] : ( m2_subset_1(I,k5_qc_lang1,k7_qc_lang1(G)) => ( k8_funct_2(k7_cqc_lang,f1_s9_cqc_lang,C,k8_cqc_lang(G,I,H)) = f4_s9_cqc_lang(G,I,H) & k8_funct_2(k7_cqc_lang,f1_s9_cqc_lang,C,k10_cqc_lang(D)) = f5_s9_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s9_cqc_lang,C,D)) & k8_funct_2(k7_cqc_lang,f1_s9_cqc_lang,C,k11_cqc_lang(D,E)) = f6_s9_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s9_cqc_lang,C,D),k8_funct_2(k7_cqc_lang,f1_s9_cqc_lang,C,E)) & k8_funct_2(k7_cqc_lang,f1_s9_cqc_lang,C,k15_cqc_lang(F,D)) = f7_s9_cqc_lang(F,k8_funct_2(k7_cqc_lang,f1_s9_cqc_lang,C,D)) ) ) ) ) ) ) ) ) ) ) ) => f2_s9_cqc_lang(k15_cqc_lang(f8_s9_cqc_lang,f9_s9_cqc_lang)) = f7_s9_cqc_lang(f8_s9_cqc_lang,f2_s9_cqc_lang(f9_s9_cqc_lang)) ), inference(mizar_proof,[status(thm)],[s2_cqc_lang,s3_cqc_lang]), [file(cqc_lang,s9_cqc_lang),interesting(0.17)]). fof(s5_cqc_lang,theorem, ( ! [A] : ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) => ! [B] : ( m1_subset_1(B,f1_s5_cqc_lang) => ( B = f2_s5_cqc_lang(A) <=> ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k7_cqc_lang,f1_s5_cqc_lang) & m2_relset_1(C,k7_cqc_lang,f1_s5_cqc_lang) & B = k8_funct_2(k7_cqc_lang,f1_s5_cqc_lang,C,A) & k8_funct_2(k7_cqc_lang,f1_s5_cqc_lang,C,k9_cqc_lang) = f3_s5_cqc_lang & ! [D] : ( m2_subset_1(D,k8_qc_lang1,k7_cqc_lang) => ! [E] : ( m2_subset_1(E,k8_qc_lang1,k7_cqc_lang) => ! [F] : ( m2_subset_1(F,k1_qc_lang1,k2_qc_lang1) => ! [G] : ( m2_subset_1(G,k1_numbers,k5_numbers) => ! [H] : ( ( v1_cqc_lang(H,G) & m1_qc_lang1(H,G) ) => ! [I] : ( m2_subset_1(I,k5_qc_lang1,k7_qc_lang1(G)) => ( k8_funct_2(k7_cqc_lang,f1_s5_cqc_lang,C,k8_cqc_lang(G,I,H)) = f4_s5_cqc_lang(G,I,H) & k8_funct_2(k7_cqc_lang,f1_s5_cqc_lang,C,k10_cqc_lang(D)) = f5_s5_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s5_cqc_lang,C,D)) & k8_funct_2(k7_cqc_lang,f1_s5_cqc_lang,C,k11_cqc_lang(D,E)) = f6_s5_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s5_cqc_lang,C,D),k8_funct_2(k7_cqc_lang,f1_s5_cqc_lang,C,E)) & k8_funct_2(k7_cqc_lang,f1_s5_cqc_lang,C,k15_cqc_lang(F,D)) = f7_s5_cqc_lang(F,k8_funct_2(k7_cqc_lang,f1_s5_cqc_lang,C,D)) ) ) ) ) ) ) ) ) ) ) ) => f2_s5_cqc_lang(k9_cqc_lang) = f3_s5_cqc_lang ), inference(mizar_proof,[status(thm)],[s2_cqc_lang]), [file(cqc_lang,s5_cqc_lang),interesting(0.12)]). fof(s6_cqc_lang,theorem, ( ! [A] : ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) => ! [B] : ( m1_subset_1(B,f1_s6_cqc_lang) => ( B = f3_s6_cqc_lang(A) <=> ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k7_cqc_lang,f1_s6_cqc_lang) & m2_relset_1(C,k7_cqc_lang,f1_s6_cqc_lang) & B = k8_funct_2(k7_cqc_lang,f1_s6_cqc_lang,C,A) & k8_funct_2(k7_cqc_lang,f1_s6_cqc_lang,C,k9_cqc_lang) = f2_s6_cqc_lang & ! [D] : ( m2_subset_1(D,k8_qc_lang1,k7_cqc_lang) => ! [E] : ( m2_subset_1(E,k8_qc_lang1,k7_cqc_lang) => ! [F] : ( m2_subset_1(F,k1_qc_lang1,k2_qc_lang1) => ! [G] : ( m2_subset_1(G,k1_numbers,k5_numbers) => ! [H] : ( ( v1_cqc_lang(H,G) & m1_qc_lang1(H,G) ) => ! [I] : ( m2_subset_1(I,k5_qc_lang1,k7_qc_lang1(G)) => ( k8_funct_2(k7_cqc_lang,f1_s6_cqc_lang,C,k8_cqc_lang(G,I,H)) = f4_s6_cqc_lang(G,I,H) & k8_funct_2(k7_cqc_lang,f1_s6_cqc_lang,C,k10_cqc_lang(D)) = f8_s6_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s6_cqc_lang,C,D)) & k8_funct_2(k7_cqc_lang,f1_s6_cqc_lang,C,k11_cqc_lang(D,E)) = f9_s6_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s6_cqc_lang,C,D),k8_funct_2(k7_cqc_lang,f1_s6_cqc_lang,C,E)) & k8_funct_2(k7_cqc_lang,f1_s6_cqc_lang,C,k15_cqc_lang(F,D)) = f10_s6_cqc_lang(F,k8_funct_2(k7_cqc_lang,f1_s6_cqc_lang,C,D)) ) ) ) ) ) ) ) ) ) ) ) => f3_s6_cqc_lang(k8_cqc_lang(f5_s6_cqc_lang,f6_s6_cqc_lang,f7_s6_cqc_lang)) = f4_s6_cqc_lang(f5_s6_cqc_lang,f6_s6_cqc_lang,f7_s6_cqc_lang) ), inference(mizar_proof,[status(thm)],[s2_cqc_lang]), [file(cqc_lang,s6_cqc_lang),interesting(0.07)]). fof(s3_qc_lang1,theorem,( ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k8_qc_lang1,f1_s3_qc_lang1) & m2_relset_1(A,k8_qc_lang1,f1_s3_qc_lang1) & k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,k11_qc_lang1) = f2_s3_qc_lang1 & ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( ( v2_qc_lang1(B) => k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,B) = f3_s3_qc_lang1(B) ) & ( v3_qc_lang1(B) => k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,B) = f4_s3_qc_lang1(k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,k17_qc_lang1(B))) ) & ( v4_qc_lang1(B) => k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,B) = f5_s3_qc_lang1(k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,k18_qc_lang1(B)),k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,k19_qc_lang1(B))) ) & ( v5_qc_lang1(B) => k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,B) = f6_s3_qc_lang1(B,k8_funct_2(k8_qc_lang1,f1_s3_qc_lang1,A,k21_qc_lang1(B))) ) ) ) ) ), file(qc_lang1,s3_qc_lang1), [interesting(0.00)]). fof(t38_funct_2,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( r1_tarski(C,A) => ( ( B = k1_xboole_0 & A != k1_xboole_0 ) | ( v1_funct_1(k2_partfun1(A,B,D,C)) & v1_funct_2(k2_partfun1(A,B,D,C),C,B) & m2_relset_1(k2_partfun1(A,B,D,C),C,B) ) ) ) ) ), file(funct_2,t38_funct_2), [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(d17_qc_lang1,definition,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ( v2_qc_lang1(A) <=> ? [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) & ? [C] : ( m2_subset_1(C,k5_qc_lang1,k7_qc_lang1(B)) & ? [D] : ( m1_qc_lang1(D,B) & A = k9_qc_lang1(C,D) ) ) ) ) ) ), file(qc_lang1,d17_qc_lang1), [interesting(0.00)]). fof(t35_qc_lang1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k5_qc_lang1,k7_qc_lang1(A)) => k6_qc_lang1(B) = A ) ) ), file(qc_lang1,t35_qc_lang1), [interesting(0.00)]). fof(d21_qc_lang1,definition,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ( v2_qc_lang1(A) => ! [B] : ( m1_subset_1(B,k5_qc_lang1) => ( B = k15_qc_lang1(A) <=> ? [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) & ? [D] : ( m1_qc_lang1(D,C) & ? [E] : ( m2_subset_1(E,k5_qc_lang1,k7_qc_lang1(C)) & B = E & A = k9_qc_lang1(E,D) ) ) ) ) ) ) ) ), file(qc_lang1,d21_qc_lang1), [interesting(0.00)]). fof(d22_qc_lang1,definition,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ( v2_qc_lang1(A) => ! [B] : ( m2_finseq_1(B,k1_qc_lang1) => ( B = k16_qc_lang1(A) <=> ? [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) & ? [D] : ( m2_subset_1(D,k5_qc_lang1,k7_qc_lang1(C)) & ? [E] : ( m1_qc_lang1(E,C) & B = E & A = k9_qc_lang1(D,E) ) ) ) ) ) ) ) ), file(qc_lang1,d22_qc_lang1), [interesting(0.00)]). fof(d18_qc_lang1,definition,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ( v3_qc_lang1(A) <=> ? [B] : ( m1_subset_1(B,k8_qc_lang1) & A = k12_qc_lang1(B) ) ) ) ), file(qc_lang1,d18_qc_lang1), [interesting(0.00)]). fof(d23_qc_lang1,definition,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ( v3_qc_lang1(A) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( B = k17_qc_lang1(A) <=> A = k12_qc_lang1(B) ) ) ) ) ), file(qc_lang1,d23_qc_lang1), [interesting(0.00)]). fof(d19_qc_lang1,definition,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ( v4_qc_lang1(A) <=> ? [B] : ( m1_subset_1(B,k8_qc_lang1) & ? [C] : ( m1_subset_1(C,k8_qc_lang1) & A = k13_qc_lang1(B,C) ) ) ) ) ), file(qc_lang1,d19_qc_lang1), [interesting(0.00)]). fof(d24_qc_lang1,definition,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ( v4_qc_lang1(A) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( B = k18_qc_lang1(A) <=> ? [C] : ( m1_subset_1(C,k8_qc_lang1) & A = k13_qc_lang1(B,C) ) ) ) ) ) ), file(qc_lang1,d24_qc_lang1), [interesting(0.00)]). fof(d25_qc_lang1,definition,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ( v4_qc_lang1(A) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( B = k19_qc_lang1(A) <=> ? [C] : ( m1_subset_1(C,k8_qc_lang1) & A = k13_qc_lang1(C,B) ) ) ) ) ) ), file(qc_lang1,d25_qc_lang1), [interesting(0.00)]). fof(d20_qc_lang1,definition,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ( v5_qc_lang1(A) <=> ? [B] : ( m2_subset_1(B,k1_qc_lang1,k2_qc_lang1) & ? [C] : ( m1_subset_1(C,k8_qc_lang1) & A = k14_qc_lang1(B,C) ) ) ) ) ), file(qc_lang1,d20_qc_lang1), [interesting(0.00)]). fof(d26_qc_lang1,definition,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ( v5_qc_lang1(A) => ! [B] : ( m2_subset_1(B,k1_qc_lang1,k2_qc_lang1) => ( B = k20_qc_lang1(A) <=> ? [C] : ( m1_subset_1(C,k8_qc_lang1) & A = k14_qc_lang1(B,C) ) ) ) ) ) ), file(qc_lang1,d26_qc_lang1), [interesting(0.00)]). fof(d27_qc_lang1,definition,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ( v5_qc_lang1(A) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( B = k21_qc_lang1(A) <=> ? [C] : ( m2_subset_1(C,k1_qc_lang1,k2_qc_lang1) & A = k14_qc_lang1(C,B) ) ) ) ) ) ), file(qc_lang1,d27_qc_lang1), [interesting(0.00)]). fof(t66_qc_lang3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k5_qc_lang1,k7_qc_lang1(A)) => ! [C] : ( m1_qc_lang1(C,A) => k5_qc_lang3(k9_qc_lang1(B,C)) = a_2_2_qc_lang3(A,C) ) ) ) ), file(qc_lang3,t66_qc_lang3), [interesting(0.00)]). fof(t77_qc_lang3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k5_qc_lang1,k7_qc_lang1(A)) => ! [C] : ( m1_qc_lang1(C,A) => k6_qc_lang3(k9_qc_lang1(B,C)) = a_2_3_qc_lang3(A,C) ) ) ) ), file(qc_lang3,t77_qc_lang3), [interesting(0.00)]). fof(t13_cqc_lang,theorem,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ( m2_subset_1(A,k8_qc_lang1,k7_cqc_lang) <=> ( k6_qc_lang3(A) = k1_xboole_0 & k5_qc_lang3(A) = k1_xboole_0 ) ) ) ), file(cqc_lang,t13_cqc_lang), [interesting(0.00)]). fof(d5_cqc_lang,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_qc_lang1(B,A) => ( v1_cqc_lang(B,A) <=> r1_tarski(k2_relat_1(B),k2_qc_lang1) ) ) ) ), file(cqc_lang,d5_cqc_lang), [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(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(t42_qc_lang3,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k4_qc_lang1) => ! [B] : ( m2_subset_1(B,k1_qc_lang1,k2_qc_lang1) => A != B ) ) ), file(qc_lang3,t42_qc_lang3), [interesting(0.00)]). fof(t41_qc_lang3,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k3_qc_lang1) => ! [B] : ( m2_subset_1(B,k1_qc_lang1,k2_qc_lang1) => A != B ) ) ), file(qc_lang3,t41_qc_lang3), [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(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(d1_qc_lang1,definition,( k1_qc_lang1 = k2_zfmisc_1(k1_enumset1(4,5,6),k5_numbers) ), file(qc_lang1,d1_qc_lang1), [interesting(0.00)]). fof(d2_zfmisc_1,definition,( ! [A,B,C] : ( C = k2_zfmisc_1(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ? [E,F] : ( r2_hidden(E,A) & r2_hidden(F,B) & D = k4_tarski(E,F) ) ) ) ), file(zfmisc_1,d2_zfmisc_1), [interesting(0.00)]). fof(d1_enumset1,definition,( ! [A,B,C,D] : ( D = k1_enumset1(A,B,C) <=> ! [E] : ( r2_hidden(E,D) <=> ~ ( E != A & E != B & E != C ) ) ) ), file(enumset1,d1_enumset1), [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(d2_qc_lang1,definition,( k2_qc_lang1 = k2_zfmisc_1(k1_tarski(4),k5_numbers) ), file(qc_lang1,d2_qc_lang1), [interesting(0.00)]). fof(d3_qc_lang1,definition,( k3_qc_lang1 = k2_zfmisc_1(k1_tarski(5),k5_numbers) ), file(qc_lang1,d3_qc_lang1), [interesting(0.00)]). fof(d4_qc_lang1,definition,( k4_qc_lang1 = k2_zfmisc_1(k1_tarski(6),k5_numbers) ), file(qc_lang1,d4_qc_lang1), [interesting(0.00)]). fof(t67_qc_lang3,theorem,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => k5_qc_lang3(k12_qc_lang1(A)) = k5_qc_lang3(A) ) ), file(qc_lang3,t67_qc_lang3), [interesting(0.00)]). fof(t78_qc_lang3,theorem,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => k6_qc_lang3(k12_qc_lang1(A)) = k6_qc_lang3(A) ) ), file(qc_lang3,t78_qc_lang3), [interesting(0.00)]). fof(t69_qc_lang3,theorem,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => k5_qc_lang3(k13_qc_lang1(A,B)) = k4_subset_1(k4_qc_lang1,k5_qc_lang3(A),k5_qc_lang3(B)) ) ) ), file(qc_lang3,t69_qc_lang3), [interesting(0.00)]). fof(t80_qc_lang3,theorem,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => k6_qc_lang3(k13_qc_lang1(A,B)) = k4_subset_1(k3_qc_lang1,k6_qc_lang3(A),k6_qc_lang3(B)) ) ) ), file(qc_lang3,t80_qc_lang3), [interesting(0.00)]). fof(t15_xboole_1,theorem,( ! [A,B] : ( k2_xboole_0(A,B) = k1_xboole_0 => A = k1_xboole_0 ) ), file(xboole_1,t15_xboole_1), [interesting(0.00)]). fof(t70_qc_lang3,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => k5_qc_lang3(k14_qc_lang1(A,B)) = k5_qc_lang3(B) ) ) ), file(qc_lang3,t70_qc_lang3), [interesting(0.00)]). fof(t81_qc_lang3,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => k6_qc_lang3(k14_qc_lang1(A,B)) = k6_qc_lang3(B) ) ) ), file(qc_lang3,t81_qc_lang3), [interesting(0.00)]). fof(s1_qc_lang1,theorem, ( ( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k5_qc_lang1,k7_qc_lang1(A)) => ! [C] : ( m1_qc_lang1(C,A) => p1_s1_qc_lang1(k9_qc_lang1(B,C)) ) ) ) & p1_s1_qc_lang1(k11_qc_lang1) & ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ( p1_s1_qc_lang1(A) => p1_s1_qc_lang1(k12_qc_lang1(A)) ) ) & ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( ( p1_s1_qc_lang1(A) & p1_s1_qc_lang1(B) ) => p1_s1_qc_lang1(k13_qc_lang1(A,B)) ) ) ) & ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => ( p1_s1_qc_lang1(B) => p1_s1_qc_lang1(k14_qc_lang1(A,B)) ) ) ) ) => ! [A] : ( m1_subset_1(A,k8_qc_lang1) => p1_s1_qc_lang1(A) ) ), file(qc_lang1,s1_qc_lang1), [interesting(0.00)]). fof(t113_funct_2,theorem,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( ! [E] : ( m1_subset_1(E,A) => k1_funct_1(C,E) = k1_funct_1(D,E) ) => C = D ) ) ) ), file(funct_2,t113_funct_2), [interesting(0.00)]). fof(s4_cqc_lang,theorem, ( ? [A] : ( m1_subset_1(A,f1_s4_cqc_lang) & ? [B] : ( v1_funct_1(B) & v1_funct_2(B,k7_cqc_lang,f1_s4_cqc_lang) & m2_relset_1(B,k7_cqc_lang,f1_s4_cqc_lang) & A = k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,B,f2_s4_cqc_lang) & k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,B,k9_cqc_lang) = f3_s4_cqc_lang & ! [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)) => ( k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,B,k8_cqc_lang(F,H,G)) = f4_s4_cqc_lang(F,H,G) & k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,B,k10_cqc_lang(C)) = f5_s4_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,B,C)) & k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,B,k11_cqc_lang(C,D)) = f6_s4_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,B,C),k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,B,D)) & k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,B,k15_cqc_lang(E,C)) = f7_s4_cqc_lang(E,k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,B,C)) ) ) ) ) ) ) ) ) ) & ! [A] : ( m1_subset_1(A,f1_s4_cqc_lang) => ! [B] : ( m1_subset_1(B,f1_s4_cqc_lang) => ~ ( ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k7_cqc_lang,f1_s4_cqc_lang) & m2_relset_1(C,k7_cqc_lang,f1_s4_cqc_lang) & A = k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,f2_s4_cqc_lang) & k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,k9_cqc_lang) = f3_s4_cqc_lang & ! [D] : ( m2_subset_1(D,k8_qc_lang1,k7_cqc_lang) => ! [E] : ( m2_subset_1(E,k8_qc_lang1,k7_cqc_lang) => ! [F] : ( m2_subset_1(F,k1_qc_lang1,k2_qc_lang1) => ! [G] : ( m2_subset_1(G,k1_numbers,k5_numbers) => ! [H] : ( ( v1_cqc_lang(H,G) & m1_qc_lang1(H,G) ) => ! [I] : ( m2_subset_1(I,k5_qc_lang1,k7_qc_lang1(G)) => ( k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,k8_cqc_lang(G,I,H)) = f4_s4_cqc_lang(G,I,H) & k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,k10_cqc_lang(D)) = f5_s4_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,D)) & k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,k11_cqc_lang(D,E)) = f6_s4_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,D),k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,E)) & k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,k15_cqc_lang(F,D)) = f7_s4_cqc_lang(F,k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,D)) ) ) ) ) ) ) ) ) & ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k7_cqc_lang,f1_s4_cqc_lang) & m2_relset_1(C,k7_cqc_lang,f1_s4_cqc_lang) & B = k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,f2_s4_cqc_lang) & k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,k9_cqc_lang) = f3_s4_cqc_lang & ! [D] : ( m2_subset_1(D,k8_qc_lang1,k7_cqc_lang) => ! [E] : ( m2_subset_1(E,k8_qc_lang1,k7_cqc_lang) => ! [F] : ( m2_subset_1(F,k1_qc_lang1,k2_qc_lang1) => ! [G] : ( m2_subset_1(G,k1_numbers,k5_numbers) => ! [H] : ( ( v1_cqc_lang(H,G) & m1_qc_lang1(H,G) ) => ! [I] : ( m2_subset_1(I,k5_qc_lang1,k7_qc_lang1(G)) => ( k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,k8_cqc_lang(G,I,H)) = f4_s4_cqc_lang(G,I,H) & k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,k10_cqc_lang(D)) = f5_s4_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,D)) & k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,k11_cqc_lang(D,E)) = f6_s4_cqc_lang(k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,D),k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,E)) & k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,k15_cqc_lang(F,D)) = f7_s4_cqc_lang(F,k8_funct_2(k7_cqc_lang,f1_s4_cqc_lang,C,D)) ) ) ) ) ) ) ) ) & A != B ) ) ) ), inference(mizar_proof,[status(thm)],[s2_cqc_lang,s3_cqc_lang]), [file(cqc_lang,s4_cqc_lang),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(t19_funcop_1,theorem,( ! [A,B] : ( k1_relat_1(k2_funcop_1(A,B)) = A & r1_tarski(k2_relat_1(k2_funcop_1(A,B)),k1_tarski(B)) ) ), file(funcop_1,t19_funcop_1), [interesting(0.00)]). fof(t37_zfmisc_1,theorem,( ! [A,B] : ( r1_tarski(k1_tarski(A),B) <=> r2_hidden(A,B) ) ), file(zfmisc_1,t37_zfmisc_1), [interesting(0.00)]). fof(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(t12_cqc_lang,theorem,( $true ), file(cqc_lang,t12_cqc_lang), [interesting(0.00)]). fof(t14_cqc_lang,theorem,( $true ), file(cqc_lang,t14_cqc_lang), [interesting(0.00)]). fof(t65_qc_lang3,theorem,( k5_qc_lang3(k11_qc_lang1) = k1_xboole_0 ), file(qc_lang3,t65_qc_lang3), [interesting(0.00)]). fof(t76_qc_lang3,theorem,( k6_qc_lang3(k11_qc_lang1) = k1_xboole_0 ), file(qc_lang3,t76_qc_lang3), [interesting(0.00)]). fof(t1_cqc_lang,theorem,( $true ), file(cqc_lang,t1_cqc_lang), [interesting(0.00)]). fof(d2_qc_lang2,definition,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => k2_qc_lang2(A,B) = k12_qc_lang1(k13_qc_lang1(A,k12_qc_lang1(B))) ) ) ), file(qc_lang2,d2_qc_lang2), [interesting(0.00)]). fof(d3_qc_lang2,definition,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => k3_qc_lang2(A,B) = k12_qc_lang1(k13_qc_lang1(k12_qc_lang1(A),k12_qc_lang1(B))) ) ) ), file(qc_lang2,d3_qc_lang2), [interesting(0.00)]). fof(d4_qc_lang2,definition,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => k4_qc_lang2(A,B) = k13_qc_lang1(k2_qc_lang2(A,B),k2_qc_lang2(B,A)) ) ) ), file(qc_lang2,d4_qc_lang2), [interesting(0.00)]). fof(d5_qc_lang2,definition,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( m1_subset_1(B,k8_qc_lang1) => k5_qc_lang2(A,B) = k12_qc_lang1(k14_qc_lang1(A,k12_qc_lang1(B))) ) ) ), file(qc_lang2,d5_qc_lang2), [interesting(0.00)]). fof(t25_cqc_lang,theorem,( $true ), file(cqc_lang,t25_cqc_lang), [interesting(0.00)]). fof(t26_cqc_lang,theorem,( $true ), file(cqc_lang,t26_cqc_lang), [interesting(0.00)]). fof(t27_cqc_lang,theorem,( $true ), file(cqc_lang,t27_cqc_lang), [interesting(0.00)]). fof(t2_cqc_lang,theorem,( $true ), file(cqc_lang,t2_cqc_lang), [interesting(0.00)]). fof(t3_cqc_lang,theorem,( $true ), file(cqc_lang,t3_cqc_lang), [interesting(0.00)]). fof(d3_cqc_lang,definition,( ! [A] : ( m2_finseq_1(A,k1_qc_lang1) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,k4_qc_lang1,k1_qc_lang1) ) => ! [C] : ( m2_finseq_1(C,k1_qc_lang1) => ( C = k4_cqc_lang(A,B) <=> ( k3_finseq_1(C) = k3_finseq_1(A) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( ( r1_xreal_0(1,D) & r1_xreal_0(D,k3_finseq_1(A)) ) => ( ( r2_hidden(k1_funct_1(A,D),k1_relat_1(B)) => k1_funct_1(C,D) = k1_funct_1(B,k1_funct_1(A,D)) ) & ( ~ r2_hidden(k1_funct_1(A,D),k1_relat_1(B)) => k1_funct_1(C,D) = k1_funct_1(A,D) ) ) ) ) ) ) ) ) ) ), file(cqc_lang,d3_cqc_lang), [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(t18_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( ( k3_finseq_1(A) = k3_finseq_1(B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r1_xreal_0(1,C) & r1_xreal_0(C,k3_finseq_1(A)) ) => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) ) => A = B ) ) ) ), file(finseq_1,t18_finseq_1), [interesting(0.00)]). fof(d6_cqc_lang,definition,( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ! [B] : ( m2_subset_1(B,k1_qc_lang1,k2_qc_lang1) => ! [C] : ( m1_subset_1(C,k8_qc_lang1) => ( C = k17_cqc_lang(A,B) <=> ? [D] : ( v1_funct_1(D) & v1_funct_2(D,k8_qc_lang1,k8_qc_lang1) & m2_relset_1(D,k8_qc_lang1,k8_qc_lang1) & C = k8_funct_2(k8_qc_lang1,k8_qc_lang1,D,A) & ! [E] : ( m1_subset_1(E,k8_qc_lang1) => ( k8_funct_2(k8_qc_lang1,k8_qc_lang1,D,k9_cqc_lang) = k9_cqc_lang & ( v2_qc_lang1(E) => k8_funct_2(k8_qc_lang1,k8_qc_lang1,D,E) = k9_qc_lang1(k15_qc_lang1(E),k4_cqc_lang(k16_qc_lang1(E),k6_cqc_lang(k3_qc_lang3(0),B))) ) & ( v3_qc_lang1(E) => k8_funct_2(k8_qc_lang1,k8_qc_lang1,D,E) = k12_qc_lang1(k8_funct_2(k8_qc_lang1,k8_qc_lang1,D,k17_qc_lang1(E))) ) & ( v4_qc_lang1(E) => k8_funct_2(k8_qc_lang1,k8_qc_lang1,D,E) = k13_qc_lang1(k8_funct_2(k8_qc_lang1,k8_qc_lang1,D,k18_qc_lang1(E)),k8_funct_2(k8_qc_lang1,k8_qc_lang1,D,k19_qc_lang1(E))) ) & ( v5_qc_lang1(E) => k8_funct_2(k8_qc_lang1,k8_qc_lang1,D,E) = k2_cqc_lang(k8_qc_lang1,k20_qc_lang1(E),B,E,k14_qc_lang1(k20_qc_lang1(E),k8_funct_2(k8_qc_lang1,k8_qc_lang1,D,k21_qc_lang1(E)))) ) ) ) ) ) ) ) ) ), file(cqc_lang,d6_cqc_lang), [interesting(0.00)]). fof(s1_qc_lang3,theorem, ( ( ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ! [B] : ( m1_subset_1(B,f1_s1_qc_lang3) => ! [C] : ( m1_subset_1(C,f1_s1_qc_lang3) => ( ( A = k11_qc_lang1 => k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f2_s1_qc_lang3,A) = f4_s1_qc_lang3 ) & ( v2_qc_lang1(A) => k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f2_s1_qc_lang3,A) = f5_s1_qc_lang3(A) ) & ( ( v3_qc_lang1(A) & B = k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f2_s1_qc_lang3,k17_qc_lang1(A)) ) => k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f2_s1_qc_lang3,A) = f6_s1_qc_lang3(B) ) & ( ( v4_qc_lang1(A) & B = k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f2_s1_qc_lang3,k18_qc_lang1(A)) & C = k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f2_s1_qc_lang3,k19_qc_lang1(A)) ) => k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f2_s1_qc_lang3,A) = f7_s1_qc_lang3(B,C) ) & ( ( v5_qc_lang1(A) & B = k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f2_s1_qc_lang3,k21_qc_lang1(A)) ) => k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f2_s1_qc_lang3,A) = f8_s1_qc_lang3(A,B) ) ) ) ) ) & ! [A] : ( m1_subset_1(A,k8_qc_lang1) => ! [B] : ( m1_subset_1(B,f1_s1_qc_lang3) => ! [C] : ( m1_subset_1(C,f1_s1_qc_lang3) => ( ( A = k11_qc_lang1 => k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f3_s1_qc_lang3,A) = f4_s1_qc_lang3 ) & ( v2_qc_lang1(A) => k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f3_s1_qc_lang3,A) = f5_s1_qc_lang3(A) ) & ( ( v3_qc_lang1(A) & B = k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f3_s1_qc_lang3,k17_qc_lang1(A)) ) => k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f3_s1_qc_lang3,A) = f6_s1_qc_lang3(B) ) & ( ( v4_qc_lang1(A) & B = k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f3_s1_qc_lang3,k18_qc_lang1(A)) & C = k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f3_s1_qc_lang3,k19_qc_lang1(A)) ) => k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f3_s1_qc_lang3,A) = f7_s1_qc_lang3(B,C) ) & ( ( v5_qc_lang1(A) & B = k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f3_s1_qc_lang3,k21_qc_lang1(A)) ) => k8_funct_2(k8_qc_lang1,f1_s1_qc_lang3,f3_s1_qc_lang3,A) = f8_s1_qc_lang3(A,B) ) ) ) ) ) ) => f2_s1_qc_lang3 = f3_s1_qc_lang3 ), file(qc_lang3,s1_qc_lang3), [interesting(0.00)]). fof(l31_cqc_lang,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k2_qc_lang1) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k8_qc_lang1,k8_qc_lang1) & m2_relset_1(B,k8_qc_lang1,k8_qc_lang1) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k8_qc_lang1,k8_qc_lang1) & m2_relset_1(C,k8_qc_lang1,k8_qc_lang1) ) => ( ( ! [D] : ( m1_subset_1(D,k8_qc_lang1) => ( k8_funct_2(k8_qc_lang1,k8_qc_lang1,B,k9_cqc_lang) = k9_cqc_lang & ( v2_qc_lang1(D) => k8_funct_2(k8_qc_lang1,k8_qc_lang1,B,D) = k9_qc_lang1(k15_qc_lang1(D),k4_cqc_lang(k16_qc_lang1(D),k6_cqc_lang(k3_qc_lang3(0),A))) ) & ( v3_qc_lang1(D) => k8_funct_2(k8_qc_lang1,k8_qc_lang1,B,D) = k12_qc_lang1(k8_funct_2(k8_qc_lang1,k8_qc_lang1,B,k17_qc_lang1(D))) ) & ( v4_qc_lang1(D) => k8_funct_2(k8_qc_lang1,k8_qc_lang1,B,D) = k13_qc_lang1(k8_funct_2(k8_qc_lang1,k8_qc_lang1,B,k18_qc_lang1(D)),k8_funct_2(k8_qc_lang1,k8_qc_lang1,B,k19_qc_lang1(D))) ) & ( v5_qc_lang1(D) => k8_funct_2(k8_qc_lang1,k8_qc_lang1,B,D) = k2_cqc_lang(k8_qc_lang1,k20_qc_lang1(D),A,D,k14_qc_lang1(k20_qc_lang1(D),k8_funct_2(k8_qc_lang1,k8_qc_lang1,B,k21_qc_lang1(D)))) ) ) ) & ! [D] : ( m1_subset_1(D,k8_qc_lang1) => ( k8_funct_2(k8_qc_lang1,k8_qc_lang1,C,k9_cqc_lang) = k9_cqc_lang & ( v2_qc_lang1(D) => k8_funct_2(k8_qc_lang1,k8_qc_lang1,C,D) = k9_qc_lang1(k15_qc_lang1(D),k4_cqc_lang(k16_qc_lang1(D),k6_cqc_lang(k3_qc_lang3(0),A))) ) & ( v3_qc_lang1(D) => k8_funct_2(k8_qc_lang1,k8_qc_lang1,C,D) = k12_qc_lang1(k8_funct_2(k8_qc_lang1,k8_qc_lang1,C,k17_qc_lang1(D))) ) & ( v4_qc_lang1(D) => k8_funct_2(k8_qc_lang1,k8_qc_lang1,C,D) = k13_qc_lang1(k8_funct_2(k8_qc_lang1,k8_qc_lang1,C,k18_qc_lang1(D)),k8_funct_2(k8_qc_lang1,k8_qc_lang1,C,k19_qc_lang1(D))) ) & ( v5_qc_lang1(D) => k8_funct_2(k8_qc_lang1,k8_qc_lang1,C,D) = k2_cqc_lang(k8_qc_lang1,k20_qc_lang1(D),A,D,k14_qc_lang1(k20_qc_lang1(D),k8_funct_2(k8_qc_lang1,k8_qc_lang1,C,k21_qc_lang1(D)))) ) ) ) ) => B = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[s1_qc_lang3]), [file(cqc_lang,l31_cqc_lang),interesting(0.00)]). fof(d1_cqc_lang,definition,( ! [A,B,C,D] : ( ( A = B => k1_cqc_lang(A,B,C,D) = C ) & ( A != B => k1_cqc_lang(A,B,C,D) = D ) ) ), file(cqc_lang,d1_cqc_lang), [interesting(0.00)]). fof(t40_qc_lang3,theorem,( ! [A] : ( m2_subset_1(A,k1_qc_lang1,k3_qc_lang1) => ! [B] : ( m2_subset_1(B,k1_qc_lang1,k4_qc_lang1) => A != B ) ) ), file(qc_lang3,t40_qc_lang3), [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(t2_tarski,theorem,( ! [A,B] : ( ! [C] : ( r2_hidden(C,A) <=> r2_hidden(C,B) ) => A = B ) ), file(tarski,t2_tarski), [interesting(0.00)]). fof(t35_zfmisc_1,theorem,( ! [A,B] : k2_zfmisc_1(k1_tarski(A),k1_tarski(B)) = k1_tarski(k4_tarski(A,B)) ), file(zfmisc_1,t35_zfmisc_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(d5_funct_2,definition,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(k1_tarski(A),k1_tarski(B)),k1_tarski(C)) & m2_relset_1(D,k2_zfmisc_1(k1_tarski(A),k1_tarski(B)),k1_tarski(C)) ) => D = k9_funct_2(A,B,C) ) ), file(funct_2,d5_funct_2), [interesting(0.00)]). fof(t4_cqc_lang,theorem,( $true ), file(cqc_lang,t4_cqc_lang), [interesting(0.00)]). fof(t8_cqc_lang,theorem,( $true ), file(cqc_lang,t8_cqc_lang), [interesting(0.00)]). fof(t9_cqc_lang,theorem,( $true ), file(cqc_lang,t9_cqc_lang), [interesting(0.00)]).