fof(t7_finseqop,theorem,( ! [A,B,C] : k13_funct_3(k2_funcop_1(A,B),k2_funcop_1(A,C)) = k2_funcop_1(A,k4_tarski(B,C)) ), inference(mizar_proof,[status(thm)],[t1_finseqop,t19_funcop_1,t70_funct_3,t13_funcop_1,t14_funcop_1,t69_funct_3,d5_funct_1,t71_funct_3,t35_zfmisc_1,t37_zfmisc_1,d10_xboole_0,t15_funcop_1]), [file(finseqop,t7_finseqop),interesting(1.00)]). fof(t8_finseqop,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C,D] : ( r2_hidden(k4_tarski(C,D),k1_relat_1(A)) => k3_funcop_1(A,k2_funcop_1(B,C),k2_funcop_1(B,D)) = k2_funcop_1(B,k1_funct_1(A,k4_tarski(C,D))) ) ) ), inference(mizar_proof,[status(thm)],[d3_funcop_1,t7_finseqop,t23_funcop_1]), [file(finseqop,t8_finseqop),interesting(0.86)]). fof(t5_finseqop,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => k4_funcop_1(B,k1_xboole_0,A) = k1_xboole_0 ) ), inference(mizar_proof,[status(thm)],[t34_funcop_1,t4_finseqop]), [file(finseqop,t5_finseqop),interesting(0.77)]). fof(t6_finseqop,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => k5_funcop_1(B,A,k1_xboole_0) = k1_xboole_0 ) ), inference(mizar_proof,[status(thm)],[t41_funcop_1,t4_finseqop]), [file(finseqop,t6_finseqop),interesting(0.77)]). fof(t67_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ( ( v1_setwiseo(B,A) & v2_binop_1(B,A) & v1_binop_1(B,A) & v1_finseqop(B,A) ) => r7_binop_1(A,k6_finseqop(A,B),B) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_binop_1,d3_binop_1,d3_binop_1,d2_binop_1,d3_binop_1,t63_finseqop,d3_binop_1,t63_finseqop,t23_setwiseo,t64_finseqop]), [file(finseqop,t67_finseqop),interesting(0.76)]). fof(t1_finseqop,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( k13_funct_3(k1_xboole_0,A) = k1_xboole_0 & k13_funct_3(A,k1_xboole_0) = k1_xboole_0 ) ) ), inference(mizar_proof,[status(thm)],[d8_funct_3,t64_relat_1]), [file(finseqop,t1_finseqop),interesting(0.73)]). fof(t4_finseqop,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( k3_funcop_1(A,k1_xboole_0,B) = k1_xboole_0 & k3_funcop_1(A,B,k1_xboole_0) = k1_xboole_0 ) ) ) ), inference(mizar_proof,[status(thm)],[d3_funcop_1,t1_finseqop]), [file(finseqop,t4_finseqop),interesting(0.72)]). fof(t9_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m2_finseq_1(D,A) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => k5_finseqop(A,B,k8_finseq_1(A,D,k12_finseq_1(A,C)),E) = k8_finseq_1(B,k5_finseqop(A,B,D,E),k12_finseq_1(B,k8_funct_2(A,B,E,C))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t37_finseq_2,t19_finseq_2,t19_finseq_2,t37_finseq_2,d3_finseq_1,d3_finseq_1,d3_finseq_1,d7_finseq_1,t22_funct_1,d7_finseq_1,t59_finseq_1,t59_finseq_1,t8_finseq_2,t22_funct_1,t10_finseq_2]), [file(finseqop,t9_finseqop),interesting(0.67)]). fof(t10_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_1(C,A) => ! [D] : ( m2_finseq_1(D,A) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => k5_finseqop(A,B,k8_finseq_1(A,C,D),E) = k8_finseq_1(B,k5_finseqop(A,B,C,E),k5_finseqop(A,B,D,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t47_finseq_1,t47_finseq_1,t45_finseq_1,t9_finseqop,t45_finseq_1,t9_finseqop,s2_finseq_2]), [file(finseqop,t10_finseqop),interesting(0.65)]). fof(t2_finseqop,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( k15_funct_3(k1_xboole_0,A) = k1_xboole_0 & k15_funct_3(A,k1_xboole_0) = k1_xboole_0 ) ) ), inference(mizar_proof,[status(thm)],[d9_funct_3,t113_zfmisc_1,t64_relat_1]), [file(finseqop,t2_finseqop),interesting(0.65)]). fof(t18_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m1_subset_1(E,B) => ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(A,B),C) & m2_relset_1(G,k2_zfmisc_1(A,B),C) ) => k1_finseqop(A,B,C,G,k4_finseqop(A,F,D),k4_finseqop(B,F,E)) = k4_finseqop(C,F,k2_binop_1(A,B,C,G,D,E)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_zfmisc_1,d2_finseq_2,d1_funct_2,t8_finseqop,d2_finseq_2]), [file(finseqop,t18_finseqop),interesting(0.62)]). fof(t65_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ( ( v1_setwiseo(B,A) & v2_binop_1(B,A) & v1_finseqop(B,A) ) => k8_funct_2(A,A,k6_finseqop(A,B),k3_binop_1(A,B)) = k3_binop_1(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_setwiseo,t64_finseqop]), [file(finseqop,t65_finseqop),interesting(0.62)]). fof(l11_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ! [D] : ( m2_finseq_2(D,A,k4_finseq_2(0,A)) => k5_finseqop(A,B,D,C) = k6_finseq_1(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t113_finseq_2,t38_finseq_2]), [file(finseqop,l11_finseqop),interesting(0.57)]). fof(t83_finseqop,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) ) => ! [E] : ( ( v1_relat_1(E) & v1_funct_1(E) ) => ( r2_hidden(k4_tarski(A,B),k1_relat_1(k7_finseqop(C,D,E))) => k1_binop_1(k7_finseqop(C,D,E),A,B) = k1_binop_1(C,k1_funct_1(D,A),k1_funct_1(E,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t82_finseqop]), [file(finseqop,t83_finseqop),interesting(0.56)]). fof(t92_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ( ( v2_binop_1(C,A) & v1_setwiseo(C,A) & v1_finseqop(C,A) ) => k2_binop_1(A,A,A,k8_finseqop(A,C,k6_partfun1(A),k6_finseqop(A,C)),B,k3_binop_1(A,C)) = B ) ) ) ) ), inference(mizar_proof,[status(thm)],[t87_finseqop,t65_finseqop,t23_setwiseo]), [file(finseqop,t92_finseqop),interesting(0.54)]). fof(l29_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_2(C,A,k4_finseq_2(B,A)) => ( v1_funct_1(C) & v1_funct_2(C,k2_finseq_1(B),A) & m2_relset_1(C,k2_finseq_1(B),A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,d3_finseq_1,t30_finseq_2]), [file(finseqop,l29_finseqop),interesting(0.53)]). fof(t19_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m1_subset_1(E,B) => ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(A,B),C) & m2_relset_1(G,k2_zfmisc_1(A,B),C) ) => k3_finseqop(A,B,C,G,D,k4_finseqop(B,F,E)) = k4_finseqop(C,F,k2_binop_1(A,B,C,G,D,E)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t41_funcop_1,t68_finseq_2,d2_finseq_2,t18_finseqop]), [file(finseqop,t19_finseqop),interesting(0.51)]). fof(t20_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m1_subset_1(E,B) => ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(A,B),C) & m2_relset_1(G,k2_zfmisc_1(A,B),C) ) => k2_finseqop(A,B,C,G,k4_finseqop(A,F,D),E) = k4_finseqop(C,F,k2_binop_1(A,B,C,G,D,E)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t34_funcop_1,t68_finseq_2,d2_finseq_2,t18_finseqop]), [file(finseqop,t20_finseqop),interesting(0.51)]). fof(t45_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(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,k2_zfmisc_1(B,B),B) & m2_relset_1(D,k2_zfmisc_1(B,B),B) ) => ( v1_setwiseo(D,B) => k8_funcop_1(B,A,D,k3_binop_1(B,D),C) = C ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t66_funcop_1,t23_setwiseo,t113_funct_2]), [file(finseqop,t45_finseqop),interesting(0.50)]). fof(t46_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(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,k2_zfmisc_1(B,B),B) & m2_relset_1(D,k2_zfmisc_1(B,B),B) ) => ( v1_setwiseo(D,B) => k7_funcop_1(B,A,D,C,k3_binop_1(B,D)) = C ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t60_funcop_1,t23_setwiseo,t113_funct_2]), [file(finseqop,t46_finseqop),interesting(0.50)]). fof(t72_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,A) & m2_relset_1(D,A,A) ) => ( ( v1_setwiseo(B,A) & v2_binop_1(B,A) & v1_finseqop(B,A) & D = k6_finseqop(A,B) & r6_binop_1(A,C,B) & v1_setwiseo(C,A) ) => k8_funcop_1(A,A,C,k8_funct_2(A,A,D,k3_binop_1(A,C)),k6_partfun1(A)) = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t66_funcop_1,t35_funct_1,t71_finseqop,t23_setwiseo,t113_funct_2]), [file(finseqop,t72_finseqop),interesting(0.49)]). fof(t91_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ( ( v2_binop_1(C,A) & v1_setwiseo(C,A) & v1_finseqop(C,A) ) => k2_binop_1(A,A,A,k8_finseqop(A,C,k6_partfun1(A),k6_finseqop(A,C)),B,B) = k3_binop_1(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t87_finseqop,t63_finseqop]), [file(finseqop,t91_finseqop),interesting(0.46)]). fof(t89_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_2(C,A,k4_finseq_2(B,A)) => ! [D] : ( m2_finseq_2(D,A,k4_finseq_2(B,A)) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,A),A) & m2_relset_1(E,k2_zfmisc_1(A,A),A) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,A,A) & m2_relset_1(F,A,A) ) => k1_finseqop(A,A,A,k8_finseqop(A,E,k6_partfun1(A),F),C,D) = k1_finseqop(A,A,A,E,C,k5_finseqop(A,A,D,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l11_finseqop,l12_finseqop,t87_finseq_2,t5_finseq_1,l29_finseqop,t88_finseqop]), [file(finseqop,t89_finseqop),interesting(0.37)]). fof(t17_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => k5_finseqop(A,B,k4_finseqop(A,D,C),E) = k4_finseqop(B,D,k8_funct_2(A,B,E,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,t23_funcop_1,d2_finseq_2,d2_finseq_2]), [file(finseqop,t17_finseqop),interesting(0.35)]). fof(t94_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ( ( v1_binop_1(B,A) & v2_binop_1(B,A) & v1_setwiseo(B,A) & v1_finseqop(B,A) & C = k8_finseqop(A,B,k6_partfun1(A),k6_finseqop(A,B)) ) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m1_subset_1(E,A) => ! [F] : ( m1_subset_1(F,A) => ! [G] : ( m1_subset_1(G,A) => k2_binop_1(A,A,A,B,k2_binop_1(A,A,A,C,D,E),k2_binop_1(A,A,A,C,F,G)) = k2_binop_1(A,A,A,C,k2_binop_1(A,A,A,B,D,F),k2_binop_1(A,A,A,B,E,G)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t67_finseqop,t87_finseqop,t87_finseqop,d3_binop_1,d3_binop_1,d2_binop_1,d3_binop_1,d3_binop_1,d12_binop_1,t87_finseqop]), [file(finseqop,t94_finseqop),interesting(0.33)]). fof(t90_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,A) & m2_relset_1(E,A,A) ) => ( ( v2_binop_1(D,A) & v1_setwiseo(D,A) & v1_binop_1(D,A) & v1_finseqop(D,A) & E = k6_finseqop(A,D) ) => ( k8_funct_2(A,A,E,k2_binop_1(A,A,A,k8_finseqop(A,D,k6_partfun1(A),E),B,C)) = k2_binop_1(A,A,A,k8_finseqop(A,D,E,k6_partfun1(A)),B,C) & k2_binop_1(A,A,A,k8_finseqop(A,D,k6_partfun1(A),E),B,C) = k8_funct_2(A,A,E,k2_binop_1(A,A,A,k8_finseqop(A,D,E,k6_partfun1(A)),B,C)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t67_finseqop,t87_finseqop,d12_binop_1,t66_finseqop,t87_finseqop,t66_finseqop]), [file(finseqop,t90_finseqop),interesting(0.30)]). fof(t93_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,A) & m2_relset_1(D,A,A) ) => ( ( v2_binop_1(C,A) & v1_setwiseo(C,A) & v1_finseqop(C,A) & D = k6_finseqop(A,C) ) => k2_binop_1(A,A,A,k8_finseqop(A,C,k6_partfun1(A),D),k3_binop_1(A,C),B) = k8_funct_2(A,A,D,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t87_finseqop,t23_setwiseo]), [file(finseqop,t93_finseqop),interesting(0.30)]). fof(t73_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ( ( v2_binop_1(C,A) & v1_setwiseo(C,A) & v1_finseqop(C,A) & r6_binop_1(A,D,C) ) => k8_funct_2(A,A,k8_funcop_1(A,A,D,B,k6_partfun1(A)),k3_binop_1(A,C)) = k3_binop_1(A,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_setwiseo,t23_binop_1,t63_finseqop,d3_binop_1,t63_finseqop,t23_setwiseo,t35_funct_1,t66_funcop_1]), [file(finseqop,t73_finseqop),interesting(0.25)]). fof(t74_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ( ( v2_binop_1(C,A) & v1_setwiseo(C,A) & v1_finseqop(C,A) & r6_binop_1(A,D,C) ) => k8_funct_2(A,A,k7_funcop_1(A,A,D,k6_partfun1(A),B),k3_binop_1(A,C)) = k3_binop_1(A,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_setwiseo,t23_binop_1,t63_finseqop,d3_binop_1,t63_finseqop,t23_setwiseo,t35_funct_1,t60_funcop_1]), [file(finseqop,t74_finseqop),interesting(0.25)]). fof(t53_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_finseq_2(D,A,k4_finseq_2(C,A)) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,A),A) & m2_relset_1(E,k2_zfmisc_1(A,A),A) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,A,A) & m2_relset_1(F,A,A) ) => ( r7_binop_1(A,F,E) => k5_finseqop(A,A,k3_finseqop(A,A,A,E,B,D),F) = k3_finseqop(A,A,A,E,k8_funct_2(A,A,F,B),k5_finseqop(A,A,D,F)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_binop_1,t50_finseqop]), [file(finseqop,t53_finseqop),interesting(0.24)]). fof(t54_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_finseq_2(D,A,k4_finseq_2(C,A)) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,A),A) & m2_relset_1(E,k2_zfmisc_1(A,A),A) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,A,A) & m2_relset_1(F,A,A) ) => ( r7_binop_1(A,F,E) => k5_finseqop(A,A,k2_finseqop(A,A,A,E,D,B),F) = k2_finseqop(A,A,A,E,k5_finseqop(A,A,D,F),k8_funct_2(A,A,F,B)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_binop_1,t51_finseqop]), [file(finseqop,t54_finseqop),interesting(0.24)]). fof(t50_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,B) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,B,A) & m2_relset_1(E,B,A) ) => ! [F] : ( m2_finseq_2(F,B,k4_finseq_2(D,B)) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(B,B),B) & m2_relset_1(G,k2_zfmisc_1(B,B),B) ) => ! [H] : ( ( v1_funct_1(H) & v1_funct_2(H,k2_zfmisc_1(A,A),A) & m2_relset_1(H,k2_zfmisc_1(A,A),A) ) => ( ! [I] : ( m1_subset_1(I,B) => ! [J] : ( m1_subset_1(J,B) => k8_funct_2(B,A,E,k2_binop_1(B,B,B,G,I,J)) = k2_binop_1(A,A,A,H,k8_funct_2(B,A,E,I),k8_funct_2(B,A,E,J)) ) ) => k5_finseqop(B,A,k3_finseqop(B,B,B,G,C,F),E) = k3_finseqop(A,A,A,H,k8_funct_2(B,A,E,C),k5_finseqop(B,A,F,E)) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l11_finseqop,l13_finseqop,t38_finseq_2,t93_finseq_2,t5_finseq_1,l29_finseqop,t39_finseqop]), [file(finseqop,t50_finseqop),interesting(0.22)]). fof(t51_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,B) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,B,A) & m2_relset_1(E,B,A) ) => ! [F] : ( m2_finseq_2(F,B,k4_finseq_2(D,B)) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(B,B),B) & m2_relset_1(G,k2_zfmisc_1(B,B),B) ) => ! [H] : ( ( v1_funct_1(H) & v1_funct_2(H,k2_zfmisc_1(A,A),A) & m2_relset_1(H,k2_zfmisc_1(A,A),A) ) => ( ! [I] : ( m1_subset_1(I,B) => ! [J] : ( m1_subset_1(J,B) => k8_funct_2(B,A,E,k2_binop_1(B,B,B,G,I,J)) = k2_binop_1(A,A,A,H,k8_funct_2(B,A,E,I),k8_funct_2(B,A,E,J)) ) ) => k5_finseqop(B,A,k2_finseqop(B,B,B,G,F,C),E) = k2_finseqop(A,A,A,H,k5_finseqop(B,A,F,E),k8_funct_2(B,A,E,C)) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l11_finseqop,l14_finseqop,t38_finseq_2,t99_finseq_2,t5_finseq_1,l29_finseqop,t40_finseqop]), [file(finseqop,t51_finseqop),interesting(0.22)]). fof(t11_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,B) => ! [E] : ( m1_subset_1(E,C) => ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(B,C),A) & m2_relset_1(G,k2_zfmisc_1(B,C),A) ) => ! [H] : ( m2_finseq_2(H,B,k4_finseq_2(F,B)) => ! [I] : ( m2_finseq_2(I,C,k4_finseq_2(F,C)) => k1_finseqop(B,C,A,G,k8_finseq_1(B,H,k12_finseq_1(B,D)),k8_finseq_1(C,I,k12_finseq_1(C,E))) = k8_finseq_1(A,k1_finseqop(B,C,A,G,H,I),k12_finseq_1(A,k2_binop_1(B,C,A,G,D,E))) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,t19_finseq_2,t86_finseq_2,t86_finseq_2,t19_finseq_2,d3_finseq_1,d3_finseq_1,d3_finseq_1,d3_finseq_1,d7_finseq_1,t28_funcop_1,d7_finseq_1,t59_finseq_1,t59_finseq_1,t8_finseq_2,t28_funcop_1,t10_finseq_2]), [file(finseqop,t11_finseqop),interesting(0.21)]). fof(t31_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_finseq_2(D,A,k4_finseq_2(C,A)) => ! [E] : ( m2_finseq_2(E,A,k4_finseq_2(C,A)) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,A),A) & m2_relset_1(F,k2_zfmisc_1(A,A),A) ) => ( v2_binop_1(F,A) => k1_finseqop(A,A,A,F,k2_finseqop(A,A,A,F,D,B),E) = k1_finseqop(A,A,A,F,D,k3_finseqop(A,A,A,F,B,E)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l13_finseqop,l14_finseqop,t87_finseq_2,t5_finseq_1,l29_finseqop,t75_funcop_1]), [file(finseqop,t31_finseqop),interesting(0.20)]). fof(t47_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( m2_finseq_2(E,A,k4_finseq_2(D,A)) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,A),A) & m2_relset_1(F,k2_zfmisc_1(A,A),A) ) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(A,A),A) & m2_relset_1(G,k2_zfmisc_1(A,A),A) ) => ( r6_binop_1(A,F,G) => k3_finseqop(A,A,A,F,k2_binop_1(A,A,A,G,B,C),E) = k1_finseqop(A,A,A,G,k3_finseqop(A,A,A,F,B,E),k3_finseqop(A,A,A,F,C,E)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l13_finseqop,l13_finseqop,t87_finseq_2,t5_finseq_1,l29_finseqop,t36_finseqop]), [file(finseqop,t47_finseqop),interesting(0.16)]). fof(t48_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( m2_finseq_2(E,A,k4_finseq_2(D,A)) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,A),A) & m2_relset_1(F,k2_zfmisc_1(A,A),A) ) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(A,A),A) & m2_relset_1(G,k2_zfmisc_1(A,A),A) ) => ( r6_binop_1(A,F,G) => k2_finseqop(A,A,A,F,E,k2_binop_1(A,A,A,G,B,C)) = k1_finseqop(A,A,A,G,k2_finseqop(A,A,A,F,E,B),k2_finseqop(A,A,A,F,E,C)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l14_finseqop,l14_finseqop,t87_finseq_2,t5_finseq_1,l29_finseqop,t37_finseqop]), [file(finseqop,t48_finseqop),interesting(0.16)]). fof(t23_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,C),B) & m2_relset_1(F,k2_zfmisc_1(A,C),B) ) => ! [G] : ( m2_finseq_2(G,C,k4_finseq_2(E,C)) => k3_finseqop(A,C,B,F,D,G) = k5_relat_1(G,k5_funcop_1(F,D,k6_partfun1(C))) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_finseq_1,t79_relat_1,t44_funcop_1]), [file(finseqop,t23_finseqop),interesting(0.12)]). fof(t27_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_finseq_2(D,A,k4_finseq_2(C,A)) => ! [E] : ( m2_finseq_2(E,A,k4_finseq_2(C,A)) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,A),A) & m2_relset_1(F,k2_zfmisc_1(A,A),A) ) => ( v2_binop_1(F,A) => k5_finseqop(A,A,k1_finseqop(A,A,A,F,D,E),k8_funcop_1(A,A,F,B,k6_partfun1(A))) = k1_finseqop(A,A,A,F,k5_finseqop(A,A,D,k8_funcop_1(A,A,F,B,k6_partfun1(A))),E) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l12_finseqop,t113_finseq_2,t38_finseq_2,t87_finseq_2,t5_finseq_1,l29_finseqop,t25_finseqop]), [file(finseqop,t27_finseqop),interesting(0.12)]). fof(t28_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_finseq_2(D,A,k4_finseq_2(C,A)) => ! [E] : ( m2_finseq_2(E,A,k4_finseq_2(C,A)) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,A),A) & m2_relset_1(F,k2_zfmisc_1(A,A),A) ) => ( v2_binop_1(F,A) => k5_finseqop(A,A,k1_finseqop(A,A,A,F,D,E),k7_funcop_1(A,A,F,k6_partfun1(A),B)) = k1_finseqop(A,A,A,F,D,k5_finseqop(A,A,E,k7_funcop_1(A,A,F,k6_partfun1(A),B))) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l12_finseqop,t113_finseq_2,t38_finseq_2,t87_finseq_2,t5_finseq_1,l29_finseqop,t26_finseqop]), [file(finseqop,t28_finseqop),interesting(0.12)]). fof(t80_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_finseq_2(D,A,k4_finseq_2(C,A)) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,A),A) & m2_relset_1(E,k2_zfmisc_1(A,A),A) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,A),A) & m2_relset_1(F,k2_zfmisc_1(A,A),A) ) => ( ( v2_binop_1(E,A) & v1_setwiseo(E,A) & B = k3_binop_1(A,E) & v1_finseqop(E,A) & r6_binop_1(A,F,E) ) => k3_finseqop(A,A,A,F,B,D) = k4_finseqop(A,C,B) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l13_finseqop,t113_finseq_2,t5_finseq_1,l29_finseqop,d2_finseq_2,t79_finseqop]), [file(finseqop,t80_finseqop),interesting(0.11)]). fof(t49_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,B,A) & m2_relset_1(D,B,A) ) => ! [E] : ( m2_finseq_2(E,B,k4_finseq_2(C,B)) => ! [F] : ( m2_finseq_2(F,B,k4_finseq_2(C,B)) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(B,B),B) & m2_relset_1(G,k2_zfmisc_1(B,B),B) ) => ! [H] : ( ( v1_funct_1(H) & v1_funct_2(H,k2_zfmisc_1(A,A),A) & m2_relset_1(H,k2_zfmisc_1(A,A),A) ) => ( ! [I] : ( m1_subset_1(I,B) => ! [J] : ( m1_subset_1(J,B) => k8_funct_2(B,A,D,k2_binop_1(B,B,B,G,I,J)) = k2_binop_1(A,A,A,H,k8_funct_2(B,A,D,I),k8_funct_2(B,A,D,J)) ) ) => k5_finseqop(B,A,k1_finseqop(B,B,B,G,E,F),D) = k1_finseqop(A,A,A,H,k5_finseqop(B,A,E,D),k5_finseqop(B,A,F,D)) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l11_finseqop,l12_finseqop,t38_finseq_2,t87_finseq_2,t5_finseq_1,l29_finseqop,t38_finseqop]), [file(finseqop,t49_finseqop),interesting(0.05)]). fof(t78_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_2(C,A,k4_finseq_2(B,A)) => ! [D] : ( m2_finseq_2(D,A,k4_finseq_2(B,A)) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,A),A) & m2_relset_1(E,k2_zfmisc_1(A,A),A) ) => ( ( v2_binop_1(E,A) & v1_finseqop(E,A) & v1_setwiseo(E,A) & k1_finseqop(A,A,A,E,C,D) = k4_finseqop(A,B,k3_binop_1(A,E)) ) => ( C = k5_finseqop(A,A,D,k6_finseqop(A,E)) & k5_finseqop(A,A,C,k6_finseqop(A,E)) = D ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l11_finseqop,t113_finseq_2,t5_finseq_1,l29_finseqop,d2_finseq_2,t76_finseqop]), [file(finseqop,t78_finseqop),interesting(0.04)]). fof(t47_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( k7_finseq_1(A,k1_xboole_0) = A & k7_finseq_1(k1_xboole_0,A) = A ) ) ), file(finseq_1,t47_finseq_1), [interesting(0.00)]). fof(t45_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => k7_finseq_1(k7_finseq_1(A,B),C) = k7_finseq_1(A,k7_finseq_1(B,C)) ) ) ) ), file(finseq_1,t45_finseq_1), [interesting(0.00)]). fof(t37_finseq_2,theorem,( ! [A,B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ! [D] : ( m2_finseq_1(D,A) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => ( C = k1_partfun1(k5_numbers,A,A,B,D,E) => k3_finseq_1(C) = k3_finseq_1(D) ) ) ) ) ) ), file(finseq_2,t37_finseq_2), [interesting(0.00)]). fof(t19_finseq_2,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k3_finseq_1(k7_finseq_1(B,k9_finseq_1(A))) = k1_nat_1(k3_finseq_1(B),1) ) ), file(finseq_2,t19_finseq_2), [interesting(0.00)]). fof(d3_finseq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( B = k3_finseq_1(A) <=> k2_finseq_1(B) = k1_relat_1(A) ) ) ) ), file(finseq_1,d3_finseq_1), [interesting(0.00)]). fof(d7_finseq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( C = k7_finseq_1(A,B) <=> ( k4_finseq_1(C) = k2_finseq_1(k1_nat_1(k3_finseq_1(A),k3_finseq_1(B))) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(A)) => k1_funct_1(C,D) = k1_funct_1(A,D) ) ) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(B)) => k1_funct_1(C,k1_nat_1(k3_finseq_1(A),D)) = k1_funct_1(B,D) ) ) ) ) ) ) ) ), file(finseq_1,d7_finseq_1), [interesting(0.00)]). fof(t22_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(A,k1_relat_1(k5_relat_1(C,B))) => k1_funct_1(k5_relat_1(C,B),A) = k1_funct_1(B,k1_funct_1(C,A)) ) ) ) ), file(funct_1,t22_funct_1), [interesting(0.00)]). fof(t59_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k1_funct_1(k7_finseq_1(B,k9_finseq_1(A)),k1_nat_1(k3_finseq_1(B),1)) = A ) ), file(finseq_1,t59_finseq_1), [interesting(0.00)]). fof(t8_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ~ ( r2_hidden(A,k2_finseq_1(k1_nat_1(B,1))) & ~ r2_hidden(A,k2_finseq_1(B)) & A != k1_nat_1(B,1) ) ) ) ), file(finseq_2,t8_finseq_2), [interesting(0.00)]). fof(t10_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( ( k3_finseq_1(B) = A & k3_finseq_1(C) = A & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k2_finseq_1(A)) => k1_funct_1(B,D) = k1_funct_1(C,D) ) ) ) => B = C ) ) ) ) ), file(finseq_2,t10_finseq_2), [interesting(0.00)]). fof(s2_finseq_2,theorem, ( ( p1_s2_finseq_2(k6_finseq_1(f1_s2_finseq_2)) & ! [A] : ( m2_finseq_1(A,f1_s2_finseq_2) => ! [B] : ( m1_subset_1(B,f1_s2_finseq_2) => ( p1_s2_finseq_2(A) => p1_s2_finseq_2(k8_finseq_1(f1_s2_finseq_2,A,k12_finseq_1(f1_s2_finseq_2,B))) ) ) ) ) => ! [A] : ( m2_finseq_1(A,f1_s2_finseq_2) => p1_s2_finseq_2(A) ) ), file(finseq_2,s2_finseq_2), [interesting(0.00)]). fof(t113_finseq_2,theorem,( ! [A,B] : ( m1_subset_1(B,k4_finseq_2(0,A)) => B = k6_finseq_1(A) ) ), file(finseq_2,t113_finseq_2), [interesting(0.00)]). fof(t87_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,B),C) & m2_relset_1(D,k2_zfmisc_1(A,B),C) ) => ! [E] : ( m2_finseq_1(E,A) => ! [F] : ( m2_finseq_1(F,B) => ( k3_funcop_1(D,k6_finseq_1(A),F) = k6_finseq_1(C) & k3_funcop_1(D,E,k6_finseq_1(B)) = k6_finseq_1(C) ) ) ) ) ) ) ) ), file(finseq_2,t87_finseq_2), [interesting(0.00)]). fof(t115_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_2(C,B,k4_finseq_2(0,B)) => ! [D] : ( m2_finseq_2(D,B,k4_finseq_2(A,B)) => ( k8_finseq_1(B,C,D) = D & k8_finseq_1(B,D,C) = D ) ) ) ) ) ), file(finseq_2,t115_finseq_2), [interesting(0.00)]). fof(t137_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_2(C,B,k4_finseq_2(k1_nat_1(A,1),B)) => ? [D] : ( m2_finseq_2(D,B,k4_finseq_2(A,B)) & ? [E] : ( m1_subset_1(E,B) & C = k8_finseq_1(B,D,k12_finseq_1(B,E)) ) ) ) ) ) ), file(finseq_2,t137_finseq_2), [interesting(0.00)]). fof(t127_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m2_finseq_2(D,C,k4_finseq_2(A,C)) => ! [E] : ( m2_finseq_2(E,C,k4_finseq_2(B,C)) => m2_finseq_2(k8_finseq_1(C,D,E),C,k4_finseq_2(k1_nat_1(A,B),C)) ) ) ) ) ) ), file(finseq_2,t127_finseq_2), [interesting(0.00)]). fof(t109_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_2(C,B,k4_finseq_2(A,B)) => k3_finseq_1(C) = A ) ) ) ), file(finseq_2,t109_finseq_2), [interesting(0.00)]). fof(t86_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) & v1_finseq_1(D) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,B),C) & m2_relset_1(E,k2_zfmisc_1(A,B),C) ) => ! [F] : ( m2_finseq_1(F,A) => ! [G] : ( m2_finseq_1(G,B) => ( ( k3_finseq_1(F) = k3_finseq_1(G) & D = k3_funcop_1(E,F,G) ) => ( k3_finseq_1(D) = k3_finseq_1(F) & k3_finseq_1(D) = k3_finseq_1(G) ) ) ) ) ) ) ) ) ) ), file(finseq_2,t86_finseq_2), [interesting(0.00)]). fof(t28_funcop_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ! [D] : ( r2_hidden(D,k1_relat_1(k3_funcop_1(C,A,B))) => k1_funct_1(k3_funcop_1(C,A,B),D) = k1_binop_1(C,k1_funct_1(A,D),k1_funct_1(B,D)) ) ) ) ) ), file(funcop_1,t28_funcop_1), [interesting(0.00)]). fof(s1_nat_1,theorem, ( ( p1_s1_nat_1(0) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( p1_s1_nat_1(A) => p1_s1_nat_1(k1_nat_1(A,1)) ) ) ) => ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => p1_s1_nat_1(A) ) ), file(nat_1,s1_nat_1), [interesting(0.00)]). fof(t12_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(B,C),A) & m2_relset_1(F,k2_zfmisc_1(B,C),A) ) => ! [G] : ( m2_finseq_2(G,B,k4_finseq_2(D,B)) => ! [H] : ( m2_finseq_2(H,C,k4_finseq_2(D,C)) => ! [I] : ( m2_finseq_2(I,B,k4_finseq_2(E,B)) => ! [J] : ( m2_finseq_2(J,C,k4_finseq_2(E,C)) => k1_finseqop(B,C,A,F,k8_finseq_1(B,G,I),k8_finseq_1(C,H,J)) = k8_finseq_1(A,k1_finseqop(B,C,A,F,G,H),k1_finseqop(B,C,A,F,I,J)) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t113_finseq_2,t87_finseq_2,t115_finseq_2,t47_finseq_1,t137_finseq_2,t137_finseq_2,t45_finseq_1,t127_finseq_2,t11_finseqop,t45_finseq_1,t11_finseqop,s1_nat_1]), [file(finseqop,t12_finseqop),interesting(0.00)]). fof(t93_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,B),C) & m2_relset_1(E,k2_zfmisc_1(A,B),C) ) => k5_funcop_1(E,D,k6_finseq_1(B)) = k6_finseq_1(C) ) ) ) ) ) ), file(finseq_2,t93_finseq_2), [interesting(0.00)]). fof(t92_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( ( v1_relat_1(E) & v1_funct_1(E) & v1_finseq_1(E) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,B),C) & m2_relset_1(F,k2_zfmisc_1(A,B),C) ) => ! [G] : ( m2_finseq_1(G,B) => ( E = k5_funcop_1(F,D,G) => k3_finseq_1(E) = k3_finseq_1(G) ) ) ) ) ) ) ) ) ), file(finseq_2,t92_finseq_2), [interesting(0.00)]). fof(t42_funcop_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C,D] : ( r2_hidden(C,k1_relat_1(k5_funcop_1(B,D,A))) => k1_funct_1(k5_funcop_1(B,D,A),C) = k1_binop_1(B,D,k1_funct_1(A,C)) ) ) ) ), file(funcop_1,t42_funcop_1), [interesting(0.00)]). fof(t13_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m1_subset_1(E,C) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,C),B) & m2_relset_1(F,k2_zfmisc_1(A,C),B) ) => ! [G] : ( m2_finseq_1(G,C) => k3_finseqop(A,C,B,F,D,k8_finseq_1(C,G,k12_finseq_1(C,E))) = k8_finseq_1(B,k3_finseqop(A,C,B,F,D,G),k12_finseq_1(B,k2_binop_1(A,C,B,F,D,E))) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_finseq_2,t92_finseq_2,t92_finseq_2,t19_finseq_2,d3_finseq_1,d3_finseq_1,d3_finseq_1,d3_finseq_1,d7_finseq_1,t42_funcop_1,d7_finseq_1,t59_finseq_1,t59_finseq_1,t8_finseq_2,t42_funcop_1,t10_finseq_2]), [file(finseqop,t13_finseqop),interesting(0.00)]). fof(t14_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,C),B) & m2_relset_1(E,k2_zfmisc_1(A,C),B) ) => ! [F] : ( m2_finseq_1(F,C) => ! [G] : ( m2_finseq_1(G,C) => k3_finseqop(A,C,B,E,D,k8_finseq_1(C,F,G)) = k8_finseq_1(B,k3_finseqop(A,C,B,E,D,F),k3_finseqop(A,C,B,E,D,G)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t47_finseq_1,t47_finseq_1,t93_finseq_2,t45_finseq_1,t13_finseqop,t45_finseq_1,t13_finseqop,s2_finseq_2]), [file(finseqop,t14_finseqop),interesting(0.00)]). fof(t99_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,B) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,B),C) & m2_relset_1(E,k2_zfmisc_1(A,B),C) ) => k4_funcop_1(E,k6_finseq_1(A),D) = k6_finseq_1(C) ) ) ) ) ) ), file(finseq_2,t99_finseq_2), [interesting(0.00)]). fof(t98_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,B) => ! [E] : ( ( v1_relat_1(E) & v1_funct_1(E) & v1_finseq_1(E) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,B),C) & m2_relset_1(F,k2_zfmisc_1(A,B),C) ) => ! [G] : ( m2_finseq_1(G,A) => ( E = k4_funcop_1(F,G,D) => k3_finseq_1(E) = k3_finseq_1(G) ) ) ) ) ) ) ) ) ), file(finseq_2,t98_finseq_2), [interesting(0.00)]). fof(t35_funcop_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C,D] : ( r2_hidden(C,k1_relat_1(k4_funcop_1(B,A,D))) => k1_funct_1(k4_funcop_1(B,A,D),C) = k1_binop_1(B,k1_funct_1(A,C),D) ) ) ) ), file(funcop_1,t35_funcop_1), [interesting(0.00)]). fof(t15_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,C) => ! [E] : ( m1_subset_1(E,A) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(C,A),B) & m2_relset_1(F,k2_zfmisc_1(C,A),B) ) => ! [G] : ( m2_finseq_1(G,C) => k2_finseqop(C,A,B,F,k8_finseq_1(C,G,k12_finseq_1(C,D)),E) = k8_finseq_1(B,k2_finseqop(C,A,B,F,G,E),k12_finseq_1(B,k2_binop_1(C,A,B,F,D,E))) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_finseq_2,t98_finseq_2,t98_finseq_2,t19_finseq_2,d3_finseq_1,d3_finseq_1,d3_finseq_1,d7_finseq_1,t35_funcop_1,d7_finseq_1,t59_finseq_1,t59_finseq_1,t8_finseq_2,t35_funcop_1,t10_finseq_2]), [file(finseqop,t15_finseqop),interesting(0.00)]). fof(t16_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(C,A),B) & m2_relset_1(E,k2_zfmisc_1(C,A),B) ) => ! [F] : ( m2_finseq_1(F,C) => ! [G] : ( m2_finseq_1(G,C) => k2_finseqop(C,A,B,E,k8_finseq_1(C,F,G),D) = k8_finseq_1(B,k2_finseqop(C,A,B,E,F,D),k2_finseqop(C,A,B,E,G,D)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t47_finseq_1,t47_finseq_1,t99_finseq_2,t45_finseq_1,t15_finseqop,t45_finseq_1,t15_finseqop,s2_finseq_2]), [file(finseqop,t16_finseqop),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(t23_funcop_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C] : ( r2_hidden(C,k1_relat_1(A)) => k5_relat_1(k2_funcop_1(B,C),A) = k2_funcop_1(B,k1_funct_1(A,C)) ) ) ), file(funcop_1,t23_funcop_1), [interesting(0.00)]). fof(d2_finseq_2,definition,( ! [A] : ( v4_ordinal2(A) => ! [B] : k2_finseq_2(A,B) = k2_funcop_1(k2_finseq_1(A),B) ) ), file(finseq_2,d2_finseq_2), [interesting(0.00)]). fof(t41_funcop_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : k5_funcop_1(B,C,A) = k3_funcop_1(B,k2_funcop_1(k1_relat_1(A),C),A) ) ) ), file(funcop_1,t41_funcop_1), [interesting(0.00)]). fof(t68_finseq_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : k4_finseq_1(k2_finseq_2(A,B)) = k2_finseq_1(A) ) ), file(finseq_2,t68_finseq_2), [interesting(0.00)]). fof(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(d3_funcop_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => k3_funcop_1(A,B,C) = k5_relat_1(k13_funct_3(B,C),A) ) ) ) ), file(funcop_1,d3_funcop_1), [interesting(0.00)]). fof(d8_funct_3,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k13_funct_3(A,B) <=> ( k1_relat_1(C) = k3_xboole_0(k1_relat_1(A),k1_relat_1(B)) & ! [D] : ( r2_hidden(D,k1_relat_1(C)) => k1_funct_1(C,D) = k4_tarski(k1_funct_1(A,D),k1_funct_1(B,D)) ) ) ) ) ) ) ), file(funct_3,d8_funct_3), [interesting(0.00)]). fof(t64_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ( ( k1_relat_1(A) = k1_xboole_0 | k2_relat_1(A) = k1_xboole_0 ) => A = k1_xboole_0 ) ) ), file(relat_1,t64_relat_1), [interesting(0.00)]). fof(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(t70_funct_3,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( ( k1_relat_1(B) = A & k1_relat_1(C) = A ) => k1_relat_1(k13_funct_3(B,C)) = A ) ) ) ), file(funct_3,t70_funct_3), [interesting(0.00)]). fof(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(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(t69_funct_3,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) ) => ( ( k1_relat_1(C) = B & k1_relat_1(D) = B & r2_hidden(A,B) ) => k1_funct_1(k13_funct_3(C,D),A) = k4_tarski(k1_funct_1(C,A),k1_funct_1(D,A)) ) ) ) ), file(funct_3,t69_funct_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(t71_funct_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => r1_tarski(k2_relat_1(k13_funct_3(A,B)),k2_zfmisc_1(k2_relat_1(A),k2_relat_1(B))) ) ) ), file(funct_3,t71_funct_3), [interesting(0.00)]). fof(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(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(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(t15_funcop_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( k2_relat_1(A) = k1_tarski(B) => A = k2_funcop_1(k1_relat_1(A),B) ) ) ), file(funcop_1,t15_funcop_1), [interesting(0.00)]). fof(t34_funcop_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : k4_funcop_1(B,A,C) = k3_funcop_1(B,A,k2_funcop_1(k1_relat_1(A),C)) ) ) ), file(funcop_1,t34_funcop_1), [interesting(0.00)]). fof(t21_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,C),B) & m2_relset_1(F,k2_zfmisc_1(A,C),B) ) => ! [G] : ( m2_finseq_2(G,C,k4_finseq_2(E,C)) => k1_finseqop(A,C,B,F,k4_finseqop(A,E,D),G) = k3_finseqop(A,C,B,F,D,G) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_1,t109_finseq_2,d2_finseq_2,t41_funcop_1]), [file(finseqop,t21_finseqop),interesting(0.00)]). fof(t22_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,C) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(C,A),B) & m2_relset_1(F,k2_zfmisc_1(C,A),B) ) => ! [G] : ( m2_finseq_2(G,C,k4_finseq_2(E,C)) => k3_funcop_1(F,G,k4_finseqop(C,E,D)) = k4_funcop_1(F,G,D) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_1,t109_finseq_2,d2_finseq_2,t34_funcop_1]), [file(finseqop,t22_finseqop),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(t79_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r1_tarski(k2_relat_1(B),A) => k5_relat_1(B,k6_relat_1(A)) = B ) ) ), file(relat_1,t79_relat_1), [interesting(0.00)]). fof(t44_funcop_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ! [D] : k5_relat_1(B,k5_funcop_1(C,D,A)) = k5_funcop_1(C,D,k5_relat_1(B,A)) ) ) ) ), file(funcop_1,t44_funcop_1), [interesting(0.00)]). fof(t37_funcop_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ! [D] : k5_relat_1(B,k4_funcop_1(C,A,D)) = k4_funcop_1(C,k5_relat_1(B,A),D) ) ) ) ), file(funcop_1,t37_funcop_1), [interesting(0.00)]). fof(t24_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,C) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(C,A),B) & m2_relset_1(F,k2_zfmisc_1(C,A),B) ) => ! [G] : ( m2_finseq_2(G,C,k4_finseq_2(E,C)) => k4_funcop_1(F,G,D) = k5_relat_1(G,k4_funcop_1(F,k6_partfun1(C),D)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_finseq_1,t79_relat_1,t37_funcop_1]), [file(finseqop,t24_finseqop),interesting(0.00)]). fof(l12_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(B,A),C) & m2_relset_1(E,k2_zfmisc_1(B,A),C) ) => ! [F] : ( m2_finseq_2(F,A,k4_finseq_2(D,A)) => ! [G] : ( m2_finseq_2(G,B,k4_finseq_2(0,B)) => k1_finseqop(B,A,C,E,G,F) = k6_finseq_1(C) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t113_finseq_2,t87_finseq_2]), [file(finseqop,l12_finseqop),interesting(0.00)]). fof(t38_finseq_2,theorem,( ! [A,B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => k1_partfun1(k5_numbers,A,A,B,k6_finseq_1(A),C) = k6_finseq_1(B) ) ) ), file(finseq_2,t38_finseq_2), [interesting(0.00)]). fof(t5_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => ( A = 0 | r2_hidden(A,k2_finseq_1(A)) ) ) ), file(finseq_1,t5_finseq_1), [interesting(0.00)]). fof(t30_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,A) => ( v1_funct_1(B) & v1_funct_2(B,k4_finseq_1(B),A) & m2_relset_1(B,k4_finseq_1(B),A) ) ) ) ), file(finseq_2,t30_finseq_2), [interesting(0.00)]). fof(t21_funct_2,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( ( v1_relat_1(E) & v1_funct_1(E) ) => ( r2_hidden(C,A) => ( B = k1_xboole_0 | k1_funct_1(k5_relat_1(D,E),C) = k1_funct_1(E,k1_funct_1(D,C)) ) ) ) ) ), file(funct_2,t21_funct_2), [interesting(0.00)]). fof(t48_funcop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,B,A) & m2_relset_1(D,B,A) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,B,A) & m2_relset_1(E,B,A) ) => ! [F] : ( m1_subset_1(F,B) => k8_funct_2(B,A,k6_funcop_1(A,B,C,D,E),F) = k2_binop_1(A,A,A,C,k8_funct_2(B,A,D,F),k8_funct_2(B,A,E,F)) ) ) ) ) ) ) ), file(funcop_1,t48_funcop_1), [interesting(0.00)]). fof(t66_funcop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,B,A) & m2_relset_1(D,B,A) ) => ! [E] : ( m1_subset_1(E,A) => ! [F] : ( m1_subset_1(F,B) => k8_funct_2(B,A,k8_funcop_1(A,B,C,E,D),F) = k2_binop_1(A,A,A,C,E,k8_funct_2(B,A,D,F)) ) ) ) ) ) ) ), file(funcop_1,t66_funcop_1), [interesting(0.00)]). fof(t35_funct_1,theorem,( ! [A,B] : ( r2_hidden(B,A) => k1_funct_1(k6_relat_1(A),B) = B ) ), file(funct_1,t35_funct_1), [interesting(0.00)]). fof(d3_binop_1,definition,( ! [A,B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ( v2_binop_1(B,A) <=> ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m1_subset_1(E,A) => k1_binop_1(B,C,k1_binop_1(B,D,E)) = k1_binop_1(B,k1_binop_1(B,C,D),E) ) ) ) ) ) ), file(binop_1,d3_binop_1), [interesting(0.00)]). fof(t69_funcop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(B,B),B) & m2_relset_1(C,k2_zfmisc_1(B,B),B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( m1_subset_1(E,B) => k7_funct_2(A,B,B,D,k8_funcop_1(B,B,C,E,k6_partfun1(B))) = k8_funcop_1(B,A,C,E,D) ) ) ) ) ) ), file(funcop_1,t69_funcop_1), [interesting(0.00)]). fof(t113_funct_2,theorem,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( ! [E] : ( m1_subset_1(E,A) => k1_funct_1(C,E) = k1_funct_1(D,E) ) => C = D ) ) ) ), file(funct_2,t113_funct_2), [interesting(0.00)]). fof(t25_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,B) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(B,B),B) & m2_relset_1(F,k2_zfmisc_1(B,B),B) ) => ( v2_binop_1(F,B) => k7_funct_2(A,B,B,k6_funcop_1(B,A,F,D,E),k8_funcop_1(B,B,F,C,k6_partfun1(B))) = k6_funcop_1(B,A,F,k7_funct_2(A,B,B,D,k8_funcop_1(B,B,F,C,k6_partfun1(B))),E) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_funct_2,t48_funcop_1,t66_funcop_1,t35_funct_1,d3_binop_1,t66_funcop_1,t69_funcop_1,t48_funcop_1,t113_funct_2]), [file(finseqop,t25_finseqop),interesting(0.00)]). fof(t60_funcop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,B,A) & m2_relset_1(D,B,A) ) => ! [E] : ( m1_subset_1(E,A) => ! [F] : ( m1_subset_1(F,B) => k8_funct_2(B,A,k7_funcop_1(A,B,C,D,E),F) = k2_binop_1(A,A,A,C,k8_funct_2(B,A,D,F),E) ) ) ) ) ) ) ), file(funcop_1,t60_funcop_1), [interesting(0.00)]). fof(t63_funcop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(B,B),B) & m2_relset_1(C,k2_zfmisc_1(B,B),B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( m1_subset_1(E,B) => k7_funct_2(A,B,B,D,k7_funcop_1(B,B,C,k6_partfun1(B),E)) = k7_funcop_1(B,A,C,D,E) ) ) ) ) ) ), file(funcop_1,t63_funcop_1), [interesting(0.00)]). fof(t26_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,B) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(B,B),B) & m2_relset_1(F,k2_zfmisc_1(B,B),B) ) => ( v2_binop_1(F,B) => k7_funct_2(A,B,B,k6_funcop_1(B,A,F,D,E),k7_funcop_1(B,B,F,k6_partfun1(B),C)) = k6_funcop_1(B,A,F,D,k7_funct_2(A,B,B,E,k7_funcop_1(B,B,F,k6_partfun1(B),C))) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_funct_2,t48_funcop_1,t60_funcop_1,t35_funct_1,d3_binop_1,t60_funcop_1,t63_funcop_1,t48_funcop_1,t113_funct_2]), [file(finseqop,t26_finseqop),interesting(0.00)]). fof(t76_funcop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(B,B),B) & m2_relset_1(C,k2_zfmisc_1(B,B),B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,A,B) & m2_relset_1(F,A,B) ) => ( v2_binop_1(C,B) => k6_funcop_1(B,A,C,k6_funcop_1(B,A,C,D,E),F) = k6_funcop_1(B,A,C,D,k6_funcop_1(B,A,C,E,F)) ) ) ) ) ) ) ) ), file(funcop_1,t76_funcop_1), [interesting(0.00)]). fof(t29_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_2(C,A,k4_finseq_2(B,A)) => ! [D] : ( m2_finseq_2(D,A,k4_finseq_2(B,A)) => ! [E] : ( m2_finseq_2(E,A,k4_finseq_2(B,A)) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,A),A) & m2_relset_1(F,k2_zfmisc_1(A,A),A) ) => ( v2_binop_1(F,A) => k1_finseqop(A,A,A,F,k1_finseqop(A,A,A,F,C,D),E) = k1_finseqop(A,A,A,F,C,k1_finseqop(A,A,A,F,D,E)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l12_finseqop,t87_finseq_2,t5_finseq_1,l29_finseqop,t76_funcop_1]), [file(finseqop,t29_finseqop),interesting(0.00)]). fof(d9_funct_3,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k15_funct_3(A,B) <=> ( k1_relat_1(C) = k2_zfmisc_1(k1_relat_1(A),k1_relat_1(B)) & ! [D,E] : ( ( r2_hidden(D,k1_relat_1(A)) & r2_hidden(E,k1_relat_1(B)) ) => k1_funct_1(C,k4_tarski(D,E)) = k4_tarski(k1_funct_1(A,D),k1_funct_1(B,E)) ) ) ) ) ) ) ), file(funct_3,d9_funct_3), [interesting(0.00)]). fof(t113_zfmisc_1,theorem,( ! [A,B] : ( k2_zfmisc_1(A,B) = k1_xboole_0 <=> ( A = k1_xboole_0 | B = k1_xboole_0 ) ) ), file(zfmisc_1,t113_zfmisc_1), [interesting(0.00)]). fof(l13_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,B),C) & m2_relset_1(E,k2_zfmisc_1(A,B),C) ) => ! [F] : ( m2_finseq_2(F,B,k4_finseq_2(0,B)) => k3_finseqop(A,B,C,E,D,F) = k6_finseq_1(C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t113_finseq_2,t93_finseq_2]), [file(finseqop,l13_finseqop),interesting(0.00)]). fof(l14_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(B,A),C) & m2_relset_1(E,k2_zfmisc_1(B,A),C) ) => ! [F] : ( m2_finseq_2(F,B,k4_finseq_2(0,B)) => k2_finseqop(B,A,C,E,F,D) = k6_finseq_1(C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t113_finseq_2,t99_finseq_2]), [file(finseqop,l14_finseqop),interesting(0.00)]). fof(t74_funcop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(B,B),B) & m2_relset_1(C,k2_zfmisc_1(B,B),B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( m1_subset_1(E,B) => ! [F] : ( m1_subset_1(F,B) => ( v2_binop_1(C,B) => k7_funcop_1(B,A,C,k8_funcop_1(B,A,C,E,D),F) = k8_funcop_1(B,A,C,E,k7_funcop_1(B,A,C,D,F)) ) ) ) ) ) ) ) ), file(funcop_1,t74_funcop_1), [interesting(0.00)]). fof(t30_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( m2_finseq_2(E,A,k4_finseq_2(D,A)) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,A),A) & m2_relset_1(F,k2_zfmisc_1(A,A),A) ) => ( v2_binop_1(F,A) => k2_finseqop(A,A,A,F,k3_finseqop(A,A,A,F,B,E),C) = k3_finseqop(A,A,A,F,B,k2_finseqop(A,A,A,F,E,C)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l13_finseqop,l14_finseqop,t93_finseq_2,t99_finseq_2,t5_finseq_1,l29_finseqop,t74_funcop_1]), [file(finseqop,t30_finseqop),interesting(0.00)]). fof(t75_funcop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(B,B),B) & m2_relset_1(C,k2_zfmisc_1(B,B),B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => ! [F] : ( m1_subset_1(F,B) => ( v2_binop_1(C,B) => k6_funcop_1(B,A,C,k7_funcop_1(B,A,C,D,F),E) = k6_funcop_1(B,A,C,D,k8_funcop_1(B,A,C,F,E)) ) ) ) ) ) ) ) ), file(funcop_1,t75_funcop_1), [interesting(0.00)]). fof(t77_funcop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(B,B),B) & m2_relset_1(C,k2_zfmisc_1(B,B),B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( m1_subset_1(E,B) => ! [F] : ( m1_subset_1(F,B) => ( v2_binop_1(C,B) => k8_funcop_1(B,A,C,k2_binop_1(B,B,B,C,E,F),D) = k8_funcop_1(B,A,C,E,k8_funcop_1(B,A,C,F,D)) ) ) ) ) ) ) ) ), file(funcop_1,t77_funcop_1), [interesting(0.00)]). fof(t32_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( m2_finseq_2(E,A,k4_finseq_2(D,A)) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,A),A) & m2_relset_1(F,k2_zfmisc_1(A,A),A) ) => ( v2_binop_1(F,A) => k3_finseqop(A,A,A,F,k2_binop_1(A,A,A,F,B,C),E) = k3_finseqop(A,A,A,F,B,k3_finseqop(A,A,A,F,C,E)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l13_finseqop,t113_finseq_2,t93_finseq_2,t5_finseq_1,l29_finseqop,t77_funcop_1]), [file(finseqop,t32_finseqop),interesting(0.00)]). fof(t78_funcop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(B,B),B) & m2_relset_1(C,k2_zfmisc_1(B,B),B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( m1_subset_1(E,B) => ! [F] : ( m1_subset_1(F,B) => ( v2_binop_1(C,B) => k7_funcop_1(B,A,C,D,k2_binop_1(B,B,B,C,E,F)) = k7_funcop_1(B,A,C,k7_funcop_1(B,A,C,D,E),F) ) ) ) ) ) ) ) ), file(funcop_1,t78_funcop_1), [interesting(0.00)]). fof(t33_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( m2_finseq_2(E,A,k4_finseq_2(D,A)) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,A),A) & m2_relset_1(F,k2_zfmisc_1(A,A),A) ) => ( v2_binop_1(F,A) => k2_finseqop(A,A,A,F,E,k2_binop_1(A,A,A,F,B,C)) = k2_finseqop(A,A,A,F,k2_finseqop(A,A,A,F,E,B),C) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l14_finseqop,t113_finseq_2,t99_finseq_2,t5_finseq_1,l29_finseqop,t78_funcop_1]), [file(finseqop,t33_finseqop),interesting(0.00)]). fof(t80_funcop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(B,B),B) & m2_relset_1(C,k2_zfmisc_1(B,B),B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => ( v1_binop_1(C,B) => k6_funcop_1(B,A,C,D,E) = k6_funcop_1(B,A,C,E,D) ) ) ) ) ) ) ), file(funcop_1,t80_funcop_1), [interesting(0.00)]). fof(t34_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_2(C,A,k4_finseq_2(B,A)) => ! [D] : ( m2_finseq_2(D,A,k4_finseq_2(B,A)) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,A),A) & m2_relset_1(E,k2_zfmisc_1(A,A),A) ) => ( v1_binop_1(E,A) => k1_finseqop(A,A,A,E,C,D) = k1_finseqop(A,A,A,E,D,C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l12_finseqop,t5_finseq_1,l29_finseqop,t80_funcop_1]), [file(finseqop,t34_finseqop),interesting(0.00)]). fof(t79_funcop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(B,B),B) & m2_relset_1(C,k2_zfmisc_1(B,B),B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( m1_subset_1(E,B) => ( v1_binop_1(C,B) => k8_funcop_1(B,A,C,E,D) = k7_funcop_1(B,A,C,D,E) ) ) ) ) ) ) ), file(funcop_1,t79_funcop_1), [interesting(0.00)]). fof(t35_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_finseq_2(D,A,k4_finseq_2(C,A)) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,A),A) & m2_relset_1(E,k2_zfmisc_1(A,A),A) ) => ( v1_binop_1(E,A) => k3_finseqop(A,A,A,E,B,D) = k2_finseqop(A,A,A,E,D,B) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l13_finseqop,l14_finseqop,t5_finseq_1,l29_finseqop,t79_funcop_1]), [file(finseqop,t35_finseqop),interesting(0.00)]). fof(t3_finseqop,theorem,( $true ), file(finseqop,t3_finseqop), [interesting(0.00)]). fof(d20_binop_1,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,A,A) & m2_relset_1(B,A,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ( r7_binop_1(A,B,C) <=> ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m1_subset_1(E,A) => k8_funct_2(A,A,B,k2_binop_1(A,A,A,C,D,E)) = k2_binop_1(A,A,A,C,k8_funct_2(A,A,B,D),k8_funct_2(A,A,B,E)) ) ) ) ) ) ) ), file(binop_1,d20_binop_1), [interesting(0.00)]). fof(t38_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,C) & m2_relset_1(D,A,C) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,C) & m2_relset_1(E,A,C) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,C,B) & m2_relset_1(F,C,B) ) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(C,C),C) & m2_relset_1(G,k2_zfmisc_1(C,C),C) ) => ! [H] : ( ( v1_funct_1(H) & v1_funct_2(H,k2_zfmisc_1(B,B),B) & m2_relset_1(H,k2_zfmisc_1(B,B),B) ) => ( ! [I] : ( m1_subset_1(I,C) => ! [J] : ( m1_subset_1(J,C) => k8_funct_2(C,B,F,k2_binop_1(C,C,C,G,I,J)) = k2_binop_1(B,B,B,H,k8_funct_2(C,B,F,I),k8_funct_2(C,B,F,J)) ) ) => k7_funct_2(A,C,B,k6_funcop_1(C,A,G,D,E),F) = k6_funcop_1(B,A,H,k7_funct_2(A,C,B,D,F),k7_funct_2(A,C,B,E,F)) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_funct_2,t48_funcop_1,t21_funct_2,t21_funct_2,t48_funcop_1,t113_funct_2]), [file(finseqop,t38_finseqop),interesting(0.00)]). fof(t41_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(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] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(B,B),B) & m2_relset_1(E,k2_zfmisc_1(B,B),B) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,B,B) & m2_relset_1(F,B,B) ) => ( r7_binop_1(B,F,E) => k7_funct_2(A,B,B,k6_funcop_1(B,A,E,C,D),F) = k6_funcop_1(B,A,E,k7_funct_2(A,B,B,C,F),k7_funct_2(A,B,B,D,F)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_binop_1,t38_finseqop]), [file(finseqop,t41_finseqop),interesting(0.00)]). fof(t58_funcop_1,theorem,( ! [A,B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,B) => ( v1_funct_1(k2_funcop_1(A,C)) & v1_funct_2(k2_funcop_1(A,C),A,B) & m2_relset_1(k2_funcop_1(A,C),A,B) ) ) ) ), file(funcop_1,t58_funcop_1), [interesting(0.00)]). fof(t39_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,C) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,C) & m2_relset_1(E,A,C) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,C,B) & m2_relset_1(F,C,B) ) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(C,C),C) & m2_relset_1(G,k2_zfmisc_1(C,C),C) ) => ! [H] : ( ( v1_funct_1(H) & v1_funct_2(H,k2_zfmisc_1(B,B),B) & m2_relset_1(H,k2_zfmisc_1(B,B),B) ) => ( ! [I] : ( m1_subset_1(I,C) => ! [J] : ( m1_subset_1(J,C) => k8_funct_2(C,B,F,k2_binop_1(C,C,C,G,I,J)) = k2_binop_1(B,B,B,H,k8_funct_2(C,B,F,I),k8_funct_2(C,B,F,J)) ) ) => k7_funct_2(A,C,B,k8_funcop_1(C,A,G,D,E),F) = k8_funcop_1(B,A,H,k8_funct_2(C,B,F,D),k7_funct_2(A,C,B,E,F)) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,d1_funct_2,d1_funct_2,t58_funcop_1,t41_funcop_1,t38_finseqop,t23_funcop_1,t41_funcop_1]), [file(finseqop,t39_finseqop),interesting(0.00)]). fof(t42_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,B) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(B,B),B) & m2_relset_1(E,k2_zfmisc_1(B,B),B) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,B,B) & m2_relset_1(F,B,B) ) => ( r7_binop_1(B,F,E) => k7_funct_2(A,B,B,k8_funcop_1(B,A,E,C,D),F) = k8_funcop_1(B,A,E,k8_funct_2(B,B,F,C),k7_funct_2(A,B,B,D,F)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_binop_1,t39_finseqop]), [file(finseqop,t42_finseqop),interesting(0.00)]). fof(t40_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,C) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,C) & m2_relset_1(E,A,C) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,C,B) & m2_relset_1(F,C,B) ) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(C,C),C) & m2_relset_1(G,k2_zfmisc_1(C,C),C) ) => ! [H] : ( ( v1_funct_1(H) & v1_funct_2(H,k2_zfmisc_1(B,B),B) & m2_relset_1(H,k2_zfmisc_1(B,B),B) ) => ( ! [I] : ( m1_subset_1(I,C) => ! [J] : ( m1_subset_1(J,C) => k8_funct_2(C,B,F,k2_binop_1(C,C,C,G,I,J)) = k2_binop_1(B,B,B,H,k8_funct_2(C,B,F,I),k8_funct_2(C,B,F,J)) ) ) => k7_funct_2(A,C,B,k7_funcop_1(C,A,G,E,D),F) = k7_funcop_1(B,A,H,k7_funct_2(A,C,B,E,F),k8_funct_2(C,B,F,D)) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,d1_funct_2,d1_funct_2,t58_funcop_1,t34_funcop_1,t38_finseqop,t23_funcop_1,t34_funcop_1]), [file(finseqop,t40_finseqop),interesting(0.00)]). fof(t43_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,B) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(B,B),B) & m2_relset_1(E,k2_zfmisc_1(B,B),B) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,B,B) & m2_relset_1(F,B,B) ) => ( r7_binop_1(B,F,E) => k7_funct_2(A,B,B,k7_funcop_1(B,A,E,D,C),F) = k7_funcop_1(B,A,E,k7_funct_2(A,B,B,D,F),k8_funct_2(B,B,F,C)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_binop_1,t40_finseqop]), [file(finseqop,t43_finseqop),interesting(0.00)]). fof(t23_binop_1,theorem,( ! [A,B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ( r6_binop_1(A,B,C) <=> ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m1_subset_1(E,A) => ! [F] : ( m1_subset_1(F,A) => ( k1_binop_1(B,D,k1_binop_1(C,E,F)) = k1_binop_1(C,k1_binop_1(B,D,E),k1_binop_1(B,D,F)) & k1_binop_1(B,k1_binop_1(C,D,E),F) = k1_binop_1(C,k1_binop_1(B,D,F),k1_binop_1(B,E,F)) ) ) ) ) ) ) ) ), file(binop_1,t23_binop_1), [interesting(0.00)]). fof(t36_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,B) => ! [D] : ( m1_subset_1(D,B) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(B,B),B) & m2_relset_1(F,k2_zfmisc_1(B,B),B) ) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(B,B),B) & m2_relset_1(G,k2_zfmisc_1(B,B),B) ) => ( r6_binop_1(B,F,G) => k8_funcop_1(B,A,F,k2_binop_1(B,B,B,G,C,D),E) = k6_funcop_1(B,A,G,k8_funcop_1(B,A,F,C,E),k8_funcop_1(B,A,F,D,E)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t66_funcop_1,t23_binop_1,t66_funcop_1,t66_funcop_1,t48_funcop_1,t113_funct_2]), [file(finseqop,t36_finseqop),interesting(0.00)]). fof(t37_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,B) => ! [D] : ( m1_subset_1(D,B) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(B,B),B) & m2_relset_1(F,k2_zfmisc_1(B,B),B) ) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(B,B),B) & m2_relset_1(G,k2_zfmisc_1(B,B),B) ) => ( r6_binop_1(B,F,G) => k7_funcop_1(B,A,F,E,k2_binop_1(B,B,B,G,C,D)) = k6_funcop_1(B,A,G,k7_funcop_1(B,A,F,E,C),k7_funcop_1(B,A,F,E,D)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t60_funcop_1,t23_binop_1,t60_funcop_1,t60_funcop_1,t48_funcop_1,t113_funct_2]), [file(finseqop,t37_finseqop),interesting(0.00)]). fof(t52_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_2(C,A,k4_finseq_2(B,A)) => ! [D] : ( m2_finseq_2(D,A,k4_finseq_2(B,A)) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,A),A) & m2_relset_1(E,k2_zfmisc_1(A,A),A) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,A,A) & m2_relset_1(F,A,A) ) => ( r7_binop_1(A,F,E) => k5_finseqop(A,A,k1_finseqop(A,A,A,E,C,D),F) = k1_finseqop(A,A,A,E,k5_finseqop(A,A,C,F),k5_finseqop(A,A,D,F)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_binop_1,t49_finseqop]), [file(finseqop,t52_finseqop),interesting(0.00)]). fof(t55_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,A) & m2_relset_1(E,A,A) ) => ( ( r6_binop_1(A,C,D) & E = k8_funcop_1(A,A,C,B,k6_partfun1(A)) ) => r7_binop_1(A,E,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_binop_1,t66_funcop_1,t35_funct_1,t23_binop_1,t35_funct_1,t35_funct_1,t66_funcop_1,t66_funcop_1]), [file(finseqop,t55_finseqop),interesting(0.00)]). fof(t56_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,A) & m2_relset_1(E,A,A) ) => ( ( r6_binop_1(A,C,D) & E = k7_funcop_1(A,A,C,k6_partfun1(A),B) ) => r7_binop_1(A,E,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_binop_1,t60_funcop_1,t35_funct_1,t23_binop_1,t35_funct_1,t35_funct_1,t60_funcop_1,t60_funcop_1]), [file(finseqop,t56_finseqop),interesting(0.00)]). fof(t23_setwiseo,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ( v1_setwiseo(B,A) => ! [C] : ( m1_subset_1(C,A) => ( k2_binop_1(A,A,A,B,k3_binop_1(A,B),C) = C & k2_binop_1(A,A,A,B,C,k3_binop_1(A,B)) = C ) ) ) ) ) ), file(setwiseo,t23_setwiseo), [interesting(0.00)]). fof(t44_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,B,A) & m2_relset_1(C,B,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ( v1_setwiseo(D,A) => ( k3_funcop_1(D,k2_funcop_1(B,k3_binop_1(A,D)),C) = C & k3_funcop_1(D,C,k2_funcop_1(B,k3_binop_1(A,D))) = C ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t58_funcop_1,t48_funcop_1,t13_funcop_1,t23_setwiseo,t113_funct_2,t48_funcop_1,t13_funcop_1,t23_setwiseo,t113_funct_2]), [file(finseqop,t44_finseqop),interesting(0.00)]). fof(t57_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_2(C,A,k4_finseq_2(B,A)) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ( v1_setwiseo(D,A) => ( k1_finseqop(A,A,A,D,k4_finseqop(A,B,k3_binop_1(A,D)),C) = C & k1_finseqop(A,A,A,D,C,k4_finseqop(A,B,k3_binop_1(A,D))) = C ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l12_finseqop,t113_finseq_2,t5_finseq_1,l29_finseqop,d2_finseq_2,t44_finseqop]), [file(finseqop,t57_finseqop),interesting(0.00)]). fof(t58_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_2(C,A,k4_finseq_2(B,A)) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ( v1_setwiseo(D,A) => k3_finseqop(A,A,A,D,k3_binop_1(A,D),C) = C ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l13_finseqop,t113_finseq_2,t5_finseq_1,l29_finseqop,t45_finseqop]), [file(finseqop,t58_finseqop),interesting(0.00)]). fof(t59_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_2(C,A,k4_finseq_2(B,A)) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ( v1_setwiseo(D,A) => k2_finseqop(A,A,A,D,C,k3_binop_1(A,D)) = C ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l14_finseqop,t113_finseq_2,t5_finseq_1,l29_finseqop,t46_finseqop]), [file(finseqop,t59_finseqop),interesting(0.00)]). fof(t60_finseqop,theorem,( $true ), file(finseqop,t60_finseqop), [interesting(0.00)]). fof(t61_finseqop,theorem,( $true ), file(finseqop,t61_finseqop), [interesting(0.00)]). fof(t62_finseqop,theorem,( $true ), file(finseqop,t62_finseqop), [interesting(0.00)]). fof(d3_finseqop,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ( ( v1_setwiseo(B,A) & v2_binop_1(B,A) & v1_finseqop(B,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,A) & m2_relset_1(C,A,A) ) => ( C = k6_finseqop(A,B) <=> r1_finseqop(A,C,B) ) ) ) ) ) ), file(finseqop,d3_finseqop), [interesting(0.00)]). fof(d1_finseqop,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,A,A) & m2_relset_1(B,A,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ( r1_finseqop(A,B,C) <=> ! [D] : ( m1_subset_1(D,A) => ( k2_binop_1(A,A,A,C,D,k8_funct_2(A,A,B,D)) = k3_binop_1(A,C) & k2_binop_1(A,A,A,C,k8_funct_2(A,A,B,D),D) = k3_binop_1(A,C) ) ) ) ) ) ) ), file(finseqop,d1_finseqop), [interesting(0.00)]). fof(t63_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ( ( v1_setwiseo(C,A) & v2_binop_1(C,A) & v1_finseqop(C,A) ) => ( k2_binop_1(A,A,A,C,k8_funct_2(A,A,k6_finseqop(A,C),B),B) = k3_binop_1(A,C) & k2_binop_1(A,A,A,C,B,k8_funct_2(A,A,k6_finseqop(A,C),B)) = k3_binop_1(A,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseqop,d1_finseqop]), [file(finseqop,t63_finseqop),interesting(0.00)]). fof(t68_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,A),A) & m2_relset_1(E,k2_zfmisc_1(A,A),A) ) => ( ( v1_setwiseo(E,A) & v2_binop_1(E,A) & v1_finseqop(E,A) ) => ( ( k2_binop_1(A,A,A,E,B,C) != k2_binop_1(A,A,A,E,B,D) & k2_binop_1(A,A,A,E,C,B) != k2_binop_1(A,A,A,E,D,B) ) | C = D ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_setwiseo,t63_finseqop,d3_binop_1,d3_binop_1,t63_finseqop,t23_setwiseo,t23_setwiseo,t63_finseqop,d3_binop_1,d3_binop_1,t63_finseqop,t23_setwiseo]), [file(finseqop,t68_finseqop),interesting(0.00)]). fof(t69_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ( ( v1_setwiseo(D,A) & v2_binop_1(D,A) & v1_finseqop(D,A) ) => ( ( k2_binop_1(A,A,A,D,B,C) != C & k2_binop_1(A,A,A,D,C,B) != C ) | B = k3_binop_1(A,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_setwiseo,t68_finseqop]), [file(finseqop,t69_finseqop),interesting(0.00)]). fof(t70_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ( ( v2_binop_1(C,A) & v1_setwiseo(C,A) & v1_finseqop(C,A) & r6_binop_1(A,D,C) & B = k3_binop_1(A,C) ) => ! [E] : ( m1_subset_1(E,A) => ( k2_binop_1(A,A,A,D,B,E) = B & k2_binop_1(A,A,A,D,E,B) = B ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_binop_1,t23_setwiseo,t69_finseqop,t23_binop_1,t23_setwiseo,t69_finseqop]), [file(finseqop,t70_finseqop),interesting(0.00)]). fof(t64_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ( ( v1_setwiseo(D,A) & v2_binop_1(D,A) & v1_finseqop(D,A) & k2_binop_1(A,A,A,D,B,C) = k3_binop_1(A,D) ) => ( B = k8_funct_2(A,A,k6_finseqop(A,D),C) & k8_funct_2(A,A,k6_finseqop(A,D),B) = C ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_setwiseo,d3_binop_1,t63_finseqop,t23_setwiseo,t23_setwiseo,d3_binop_1,t63_finseqop,t23_setwiseo]), [file(finseqop,t64_finseqop),interesting(0.00)]). fof(t71_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,A),A) & m2_relset_1(E,k2_zfmisc_1(A,A),A) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,A,A) & m2_relset_1(F,A,A) ) => ( ( v1_setwiseo(D,A) & v2_binop_1(D,A) & v1_finseqop(D,A) & F = k6_finseqop(A,D) & r6_binop_1(A,E,D) ) => ( k8_funct_2(A,A,F,k2_binop_1(A,A,A,E,B,C)) = k2_binop_1(A,A,A,E,k8_funct_2(A,A,F,B),C) & k8_funct_2(A,A,F,k2_binop_1(A,A,A,E,B,C)) = k2_binop_1(A,A,A,E,B,k8_funct_2(A,A,F,C)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_binop_1,t63_finseqop,t70_finseqop,t64_finseqop,t23_binop_1,t63_finseqop,t70_finseqop,t64_finseqop]), [file(finseqop,t71_finseqop),interesting(0.00)]). fof(t133_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m2_finseq_2(D,B,k4_finseq_2(A,B)) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,B,C) & m2_relset_1(E,B,C) ) => m2_finseq_2(k1_partfun1(k5_numbers,B,B,C,D,E),C,k4_finseq_2(A,C)) ) ) ) ) ) ), file(finseq_2,t133_finseq_2), [interesting(0.00)]). fof(t75_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,B,A) & m2_relset_1(C,B,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ( ( v1_setwiseo(D,A) & v2_binop_1(D,A) & v1_finseqop(D,A) ) => ( k6_funcop_1(A,B,D,C,k7_funct_2(B,A,A,C,k6_finseqop(A,D))) = k2_funcop_1(B,k3_binop_1(A,D)) & k6_funcop_1(A,B,D,k7_funct_2(B,A,A,C,k6_finseqop(A,D)),C) = k2_funcop_1(B,k3_binop_1(A,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t58_funcop_1,t48_funcop_1,t21_funct_2,t63_finseqop,t13_funcop_1,t113_funct_2,t48_funcop_1,t21_funct_2,t63_finseqop,t13_funcop_1,t113_funct_2]), [file(finseqop,t75_finseqop),interesting(0.00)]). fof(t77_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_2(C,A,k4_finseq_2(B,A)) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ( ( v1_setwiseo(D,A) & v2_binop_1(D,A) & v1_finseqop(D,A) ) => ( k1_finseqop(A,A,A,D,C,k5_finseqop(A,A,C,k6_finseqop(A,D))) = k4_finseqop(A,B,k3_binop_1(A,D)) & k1_finseqop(A,A,A,D,k5_finseqop(A,A,C,k6_finseqop(A,D)),C) = k4_finseqop(A,B,k3_binop_1(A,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t133_finseq_2,l12_finseqop,t113_finseq_2,t5_finseq_1,l29_finseqop,d2_finseq_2,t75_finseqop]), [file(finseqop,t77_finseqop),interesting(0.00)]). fof(t76_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,B,A) & m2_relset_1(C,B,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,B,A) & m2_relset_1(D,B,A) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,A),A) & m2_relset_1(E,k2_zfmisc_1(A,A),A) ) => ( ( v2_binop_1(E,A) & v1_finseqop(E,A) & v1_setwiseo(E,A) & k6_funcop_1(A,B,E,C,D) = k2_funcop_1(B,k3_binop_1(A,E)) ) => ( C = k7_funct_2(B,A,A,D,k6_finseqop(A,E)) & k7_funct_2(B,A,A,C,k6_finseqop(A,E)) = D ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t58_funcop_1,t48_funcop_1,t13_funcop_1,t64_finseqop,t21_funct_2,t113_funct_2,t48_funcop_1,t13_funcop_1,t64_finseqop,t21_funct_2,t113_funct_2]), [file(finseqop,t76_finseqop),interesting(0.00)]). fof(t79_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,B,A) & m2_relset_1(D,B,A) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,A),A) & m2_relset_1(E,k2_zfmisc_1(A,A),A) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,A),A) & m2_relset_1(F,k2_zfmisc_1(A,A),A) ) => ( ( v2_binop_1(E,A) & v1_setwiseo(E,A) & C = k3_binop_1(A,E) & v1_finseqop(E,A) & r6_binop_1(A,F,E) ) => k8_funcop_1(A,B,F,C,D) = k2_funcop_1(B,C) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t58_funcop_1,t66_funcop_1,t70_finseqop,t13_funcop_1,t113_funct_2]), [file(finseqop,t79_finseqop),interesting(0.00)]). fof(t81_finseqop,theorem,( $true ), file(finseqop,t81_finseqop), [interesting(0.00)]). fof(t84_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( ~ v1_xboole_0(D) => ! [E] : ( ~ v1_xboole_0(E) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(A,B),C) & m2_relset_1(F,k2_zfmisc_1(A,B),C) ) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,D,A) & m2_relset_1(G,D,A) ) => ! [H] : ( ( v1_funct_1(H) & v1_funct_2(H,E,B) & m2_relset_1(H,E,B) ) => ( v1_funct_1(k7_finseqop(F,G,H)) & v1_funct_2(k7_finseqop(F,G,H),k2_zfmisc_1(D,E),C) & m2_relset_1(k7_finseqop(F,G,H),k2_zfmisc_1(D,E),C) ) ) ) ) ) ) ) ) ) ), file(finseqop,t84_finseqop), [interesting(0.00)]). fof(t85_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,A) & m2_relset_1(C,A,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,A) & m2_relset_1(D,A,A) ) => ( v1_funct_1(k7_finseqop(B,C,D)) & v1_funct_2(k7_finseqop(B,C,D),k2_zfmisc_1(A,A),A) & m2_relset_1(k7_finseqop(B,C,D),k2_zfmisc_1(A,A),A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t84_finseqop]), [file(finseqop,t85_finseqop),interesting(0.00)]). fof(t21_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(A,k1_relat_1(k5_relat_1(C,B))) <=> ( r2_hidden(A,k1_relat_1(C)) & r2_hidden(k1_funct_1(C,A),k1_relat_1(B)) ) ) ) ) ), file(funct_1,t21_funct_1), [interesting(0.00)]). fof(t86_funct_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C,D] : ( r2_hidden(k4_tarski(C,D),k2_zfmisc_1(k1_relat_1(A),k1_relat_1(B))) => k1_funct_1(k15_funct_3(A,B),k4_tarski(C,D)) = k4_tarski(k1_funct_1(A,C),k1_funct_1(B,D)) ) ) ) ), file(funct_3,t86_funct_3), [interesting(0.00)]). fof(t82_finseqop,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) ) => ! [E] : ( ( v1_relat_1(E) & v1_funct_1(E) ) => ( r2_hidden(k4_tarski(A,B),k1_relat_1(k7_finseqop(C,D,E))) => k1_funct_1(k7_finseqop(C,D,E),k4_tarski(A,B)) = k1_funct_1(C,k4_tarski(k1_funct_1(D,A),k1_funct_1(E,B))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_funct_1,d9_funct_3,t86_funct_3,t22_funct_1]), [file(finseqop,t82_finseqop),interesting(0.00)]). fof(t86_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( ~ v1_xboole_0(D) => ! [E] : ( ~ v1_xboole_0(E) => ! [F] : ( m1_subset_1(F,D) => ! [G] : ( m1_subset_1(G,E) => ! [H] : ( ( v1_funct_1(H) & v1_funct_2(H,k2_zfmisc_1(A,B),C) & m2_relset_1(H,k2_zfmisc_1(A,B),C) ) => ! [I] : ( ( v1_funct_1(I) & v1_funct_2(I,D,A) & m2_relset_1(I,D,A) ) => ! [J] : ( ( v1_funct_1(J) & v1_funct_2(J,E,B) & m2_relset_1(J,E,B) ) => k1_binop_1(k7_finseqop(H,I,J),F,G) = k2_binop_1(A,B,C,H,k8_funct_2(D,A,I,F),k8_funct_2(E,B,J,G)) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t84_finseqop,d1_funct_2,d2_zfmisc_1,t83_finseqop]), [file(finseqop,t86_finseqop),interesting(0.00)]). fof(t87_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,A) & m2_relset_1(E,A,A) ) => ( k2_binop_1(A,A,A,k8_finseqop(A,D,k6_partfun1(A),E),B,C) = k2_binop_1(A,A,A,D,B,k8_funct_2(A,A,E,C)) & k2_binop_1(A,A,A,k8_finseqop(A,D,E,k6_partfun1(A)),B,C) = k2_binop_1(A,A,A,D,k8_funct_2(A,A,E,B),C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t35_funct_1,t86_finseqop]), [file(finseqop,t87_finseqop),interesting(0.00)]). fof(t88_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(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] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(B,B),B) & m2_relset_1(E,k2_zfmisc_1(B,B),B) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,B,B) & m2_relset_1(F,B,B) ) => k6_funcop_1(B,A,k8_finseqop(B,E,k6_partfun1(B),F),C,D) = k6_funcop_1(B,A,E,C,k7_funct_2(A,B,B,D,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t48_funcop_1,t87_finseqop,t21_funct_2,t48_funcop_1,t113_funct_2]), [file(finseqop,t88_finseqop),interesting(0.00)]). fof(d2_binop_1,definition,( ! [A,B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ( v1_binop_1(B,A) <=> ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => k1_binop_1(B,C,D) = k1_binop_1(B,D,C) ) ) ) ) ), file(binop_1,d2_binop_1), [interesting(0.00)]). fof(d12_binop_1,definition,( ! [A,B] : ( ( v1_funct_1(B) & v1_funct_2(B,A,A) & m2_relset_1(B,A,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ( r7_binop_1(A,B,C) <=> ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m1_subset_1(E,A) => k1_funct_1(B,k1_binop_1(C,D,E)) = k1_binop_1(C,k1_funct_1(B,D),k1_funct_1(B,E)) ) ) ) ) ) ), file(binop_1,d12_binop_1), [interesting(0.00)]). fof(t66_finseqop,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => ( ( v1_setwiseo(C,A) & v2_binop_1(C,A) & v1_finseqop(C,A) ) => k8_funct_2(A,A,k6_finseqop(A,C),k8_funct_2(A,A,k6_finseqop(A,C),B)) = B ) ) ) ) ), inference(mizar_proof,[status(thm)],[t63_finseqop,t64_finseqop]), [file(finseqop,t66_finseqop),interesting(0.00)]).