fof(t22_rvsum_1,theorem,( v1_finseqop(k33_binop_2,k1_numbers) ), inference(mizar_proof,[status(thm)],[t21_rvsum_1,d2_finseqop]), [file(rvsum_1,t22_rvsum_1),interesting(1.00)]). fof(t16_rvsum_1,theorem,( r6_binop_1(k1_numbers,k35_binop_2,k33_binop_2) ), inference(mizar_proof,[status(thm)],[d9_binop_2,d11_binop_2,d9_binop_2,d11_binop_2,d11_binop_2,d9_binop_2,d11_binop_2,d9_binop_2,d11_binop_2,d11_binop_2,t23_binop_1]), [file(rvsum_1,t16_rvsum_1),interesting(0.96)]). fof(t21_rvsum_1,theorem,( r1_finseqop(k1_numbers,k31_binop_2,k33_binop_2) ), inference(mizar_proof,[status(thm)],[d1_finseqop,d9_binop_2,d7_binop_2,t3_rvsum_1,d8_binop_1,d9_binop_2,d7_binop_2,t3_rvsum_1,d8_binop_1]), [file(rvsum_1,t21_rvsum_1),interesting(0.95)]). fof(t116_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => r1_xreal_0(0,k15_rvsum_1(k11_rvsum_1(A))) ) ), inference(mizar_proof,[status(thm)],[t72_square_1,t78_rvsum_1,t114_rvsum_1]), [file(rvsum_1,t116_rvsum_1),interesting(0.94)]). fof(t24_rvsum_1,theorem,( r7_binop_1(k1_numbers,k31_binop_2,k33_binop_2) ), inference(mizar_proof,[status(thm)],[t22_rvsum_1,t23_rvsum_1,t67_finseqop]), [file(rvsum_1,t24_rvsum_1),interesting(0.94)]). fof(t23_rvsum_1,theorem,( k6_finseqop(k1_numbers,k33_binop_2) = k31_binop_2 ), inference(mizar_proof,[status(thm)],[t21_rvsum_1,t22_rvsum_1,d3_finseqop]), [file(rvsum_1,t23_rvsum_1),interesting(0.92)]). fof(t117_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k15_rvsum_1(k9_rvsum_1(A,B)) = k11_binop_2(A,k15_rvsum_1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t16_rvsum_1,t22_rvsum_1,t41_setwop_2,l22_rvsum_1]), [file(rvsum_1,t117_rvsum_1),interesting(0.80)]). fof(t122_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => r1_xreal_0(k7_square_1(k15_rvsum_1(k14_rvsum_1(A,B,C))),k11_binop_2(k15_rvsum_1(k12_rvsum_1(A,B)),k15_rvsum_1(k12_rvsum_1(A,C)))) ) ) ) ), inference(mizar_proof,[status(thm)],[t113_finseq_2,t102_rvsum_1,t137_finseq_2,t137_finseq_2,t21_xreal_1,t117_rvsum_1,t84_rvsum_1,t117_rvsum_1,t84_rvsum_1,t11_finseqop,d11_binop_2,t104_rvsum_1,t117_rvsum_1,t71_rvsum_1,t94_rvsum_1,t94_rvsum_1,t117_rvsum_1,t120_rvsum_1,t119_rvsum_1,t9_finseqop,d2_rvsum_1,t104_rvsum_1,t99_rvsum_1,t116_rvsum_1,t9_xreal_1,t21_xreal_1,s1_nat_1]), [file(rvsum_1,t122_rvsum_1),interesting(0.79)]). fof(t3_rvsum_1,theorem,( r3_binop_1(k1_numbers,0,k33_binop_2) ), inference(mizar_proof,[status(thm)],[t2_binop_2,t22_setwiseo]), [file(rvsum_1,t3_rvsum_1),interesting(0.76)]). fof(t118_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => k15_rvsum_1(k5_rvsum_1(A)) = k7_binop_2(k15_rvsum_1(A)) ) ), inference(mizar_proof,[status(thm)],[t22_rvsum_1,t23_rvsum_1,t42_setwop_2,d7_binop_2]), [file(rvsum_1,t118_rvsum_1),interesting(0.76)]). fof(t17_rvsum_1,theorem,( r7_binop_1(k1_numbers,k1_rvsum_1,k35_binop_2) ), inference(mizar_proof,[status(thm)],[d20_binop_1,d11_binop_2,d2_rvsum_1,d11_binop_2,d2_rvsum_1,d2_rvsum_1]), [file(rvsum_1,t17_rvsum_1),interesting(0.75)]). fof(t77_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => k4_finseq_1(k11_rvsum_1(A)) = k4_finseq_1(A) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,d4_finseq_1,t46_relat_1]), [file(rvsum_1,t77_rvsum_1),interesting(0.74)]). fof(t34_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => k4_finseq_1(A) = k4_finseq_1(k5_rvsum_1(A)) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,d4_finseq_1,t46_relat_1]), [file(rvsum_1,t34_rvsum_1),interesting(0.74)]). fof(t76_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => k10_rvsum_1(A,k7_binop_2(1),B) = k6_rvsum_1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d7_binop_2,t16_rvsum_1,t22_rvsum_1,t23_rvsum_1,t7_binop_2,t72_finseqop]), [file(rvsum_1,t76_rvsum_1),interesting(0.74)]). fof(t20_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => r7_binop_1(k1_numbers,k2_rvsum_1(A),k33_binop_2) ) ), inference(mizar_proof,[status(thm)],[t16_rvsum_1,t55_finseqop]), [file(rvsum_1,t20_rvsum_1),interesting(0.73)]). fof(t124_rvsum_1,theorem,( k16_rvsum_1(k6_finseq_1(k1_numbers)) = 1 ), inference(mizar_proof,[status(thm)],[t7_binop_2,t11_finsop_1]), [file(rvsum_1,t124_rvsum_1),interesting(0.72)]). fof(t97_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => k12_rvsum_1(A,B) = k14_rvsum_1(A,B,B) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,t37_finseq_2,t86_finseq_2,d3_finseq_1,d3_finseq_1,t22_funct_1,d2_rvsum_1,d11_binop_2,t28_funcop_1,t10_finseq_2]), [file(rvsum_1,t97_rvsum_1),interesting(0.71)]). fof(t103_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => k15_rvsum_1(k12_finseq_1(k1_numbers,A)) = A ) ), inference(mizar_proof,[status(thm)],[t12_finsop_1]), [file(rvsum_1,t103_rvsum_1),interesting(0.69)]). fof(t125_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => k16_rvsum_1(k12_finseq_1(k1_numbers,A)) = A ) ), inference(mizar_proof,[status(thm)],[t12_finsop_1]), [file(rvsum_1,t125_rvsum_1),interesting(0.69)]). fof(t102_rvsum_1,theorem,( k15_rvsum_1(k6_finseq_1(k1_numbers)) = 0 ), inference(mizar_proof,[status(thm)],[t2_binop_2,t11_finsop_1]), [file(rvsum_1,t102_rvsum_1),interesting(0.68)]). fof(t58_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => k8_rvsum_1(A,B,B) = k4_finseqop(k1_numbers,A,0) ) ) ), inference(mizar_proof,[status(thm)],[t52_rvsum_1,t40_rvsum_1]), [file(rvsum_1,t58_rvsum_1),interesting(0.68)]). fof(t65_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k4_finseq_1(k9_rvsum_1(A,B)) = k4_finseq_1(B) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,d4_finseq_1,t46_relat_1]), [file(rvsum_1,t65_rvsum_1),interesting(0.67)]). fof(t107_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k15_rvsum_1(k2_finseq_4(k1_numbers,A,B)) = k9_binop_2(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d9_finseq_1,t104_rvsum_1,t103_rvsum_1]), [file(rvsum_1,t107_rvsum_1),interesting(0.66)]). fof(t111_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k15_rvsum_1(k4_finseqop(k1_numbers,A,0)) = 0 ) ), inference(mizar_proof,[status(thm)],[t110_rvsum_1]), [file(rvsum_1,t111_rvsum_1),interesting(0.66)]). fof(t129_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k16_rvsum_1(k2_finseq_4(k1_numbers,A,B)) = k11_binop_2(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d9_finseq_1,t126_rvsum_1,t125_rvsum_1]), [file(rvsum_1,t129_rvsum_1),interesting(0.66)]). fof(t13_rvsum_1,theorem,( r3_binop_1(k1_numbers,1,k35_binop_2) ), inference(mizar_proof,[status(thm)],[t7_binop_2,t22_setwiseo]), [file(rvsum_1,t13_rvsum_1),interesting(0.64)]). fof(t83_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => k12_rvsum_1(A,k6_rvsum_1(A,B)) = k12_rvsum_1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t78_rvsum_1,t35_rvsum_1,t78_rvsum_1,t139_finseq_2]), [file(rvsum_1,t83_rvsum_1),interesting(0.63)]). fof(t56_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k6_rvsum_1(A,k8_rvsum_1(A,B,C)) = k8_rvsum_1(A,C,B) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_rvsum_1,t45_rvsum_1,t52_rvsum_1]), [file(rvsum_1,t56_rvsum_1),interesting(0.63)]). fof(t110_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k15_rvsum_1(k4_finseqop(k1_numbers,A,B)) = k11_binop_2(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t102_rvsum_1,t113_finseq_2,t74_finseq_2,t104_rvsum_1,s1_nat_1]), [file(rvsum_1,t110_rvsum_1),interesting(0.62)]). fof(t105_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k15_rvsum_1(k8_finseq_1(k1_numbers,A,B)) = k9_binop_2(k15_rvsum_1(A),k15_rvsum_1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t6_finsop_1,d9_binop_2]), [file(rvsum_1,t105_rvsum_1),interesting(0.61)]). fof(t127_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k16_rvsum_1(k8_finseq_1(k1_numbers,A,B)) = k11_binop_2(k16_rvsum_1(A),k16_rvsum_1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t6_finsop_1,d11_binop_2]), [file(rvsum_1,t127_rvsum_1),interesting(0.61)]). fof(t99_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k12_rvsum_1(A,k8_rvsum_1(A,B,C)) = k4_rvsum_1(A,k8_rvsum_1(A,k12_rvsum_1(A,B),k10_rvsum_1(A,2,k14_rvsum_1(A,B,C))),k12_rvsum_1(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_rvsum_1,t98_rvsum_1,t83_rvsum_1,t76_rvsum_1,t94_rvsum_1,t71_rvsum_1,t71_rvsum_1,t76_rvsum_1,t52_rvsum_1]), [file(rvsum_1,t99_rvsum_1),interesting(0.59)]). fof(t37_rvsum_1,theorem,( k5_rvsum_1(k6_finseq_1(k1_numbers)) = k6_finseq_1(k1_numbers) ), inference(mizar_proof,[status(thm)],[t38_finseq_2]), [file(rvsum_1,t37_rvsum_1),interesting(0.58)]). fof(t80_rvsum_1,theorem,( k11_rvsum_1(k6_finseq_1(k1_numbers)) = k6_finseq_1(k1_numbers) ), inference(mizar_proof,[status(thm)],[t38_finseq_2]), [file(rvsum_1,t80_rvsum_1),interesting(0.58)]). fof(t57_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k6_rvsum_1(A,k8_rvsum_1(A,B,C)) = k4_rvsum_1(A,k6_rvsum_1(A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_rvsum_1,t45_rvsum_1]), [file(rvsum_1,t57_rvsum_1),interesting(0.57)]). fof(t114_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ( ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r2_hidden(B,k4_finseq_1(A)) => r1_xreal_0(0,k2_seq_1(k5_numbers,k1_numbers,A,B)) ) ) => r1_xreal_0(0,k15_rvsum_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[t110_finseq_2,d3_finseq_1,t70_finseq_2,t112_rvsum_1,t111_rvsum_1]), [file(rvsum_1,t114_rvsum_1),interesting(0.56)]). fof(t63_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => B = k8_rvsum_1(A,k4_rvsum_1(A,B,C),C) ) ) ) ), inference(mizar_proof,[status(thm)],[t33_rvsum_1,t58_rvsum_1,t61_rvsum_1]), [file(rvsum_1,t63_rvsum_1),interesting(0.56)]). fof(t35_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k2_seq_1(k5_numbers,k1_numbers,k5_rvsum_1(B),A) = k7_binop_2(k2_seq_1(k5_numbers,k1_numbers,B,A)) ) ) ), inference(mizar_proof,[status(thm)],[t34_rvsum_1,d4_funct_1,d4_funct_1,t22_funct_1,d7_binop_2]), [file(rvsum_1,t35_rvsum_1),interesting(0.55)]). fof(t64_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => B = k4_rvsum_1(A,k8_rvsum_1(A,B,C),C) ) ) ) ), inference(mizar_proof,[status(thm)],[t33_rvsum_1,t40_rvsum_1,t32_rvsum_1,t52_rvsum_1]), [file(rvsum_1,t64_rvsum_1),interesting(0.55)]). fof(t126_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k16_rvsum_1(k8_finseq_1(k1_numbers,B,k12_finseq_1(k1_numbers,A))) = k11_binop_2(k16_rvsum_1(B),A) ) ) ), inference(mizar_proof,[status(thm)],[t5_finsop_1,d11_binop_2]), [file(rvsum_1,t126_rvsum_1),interesting(0.54)]). fof(t28_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => k3_rvsum_1(k6_finseq_1(k1_numbers),A) = k6_finseq_1(k1_numbers) ) ), inference(mizar_proof,[status(thm)],[t87_finseq_2]), [file(rvsum_1,t28_rvsum_1),interesting(0.54)]). fof(t40_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => k4_rvsum_1(A,B,k6_rvsum_1(A,B)) = k4_finseqop(k1_numbers,A,0) ) ) ), inference(mizar_proof,[status(thm)],[t22_rvsum_1,t23_rvsum_1,t2_binop_2,t77_finseqop]), [file(rvsum_1,t40_rvsum_1),interesting(0.54)]). fof(t39_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k6_rvsum_1(A,k4_finseqop(k1_numbers,A,B)) = k4_finseqop(k1_numbers,A,k7_binop_2(B)) ) ) ), inference(mizar_proof,[status(thm)],[t17_finseqop,d7_binop_2]), [file(rvsum_1,t39_rvsum_1),interesting(0.54)]). fof(t88_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => k13_rvsum_1(k6_finseq_1(k1_numbers),A) = k6_finseq_1(k1_numbers) ) ), inference(mizar_proof,[status(thm)],[t87_finseq_2]), [file(rvsum_1,t88_rvsum_1),interesting(0.54)]). fof(l5_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k2_binop_1(k1_numbers,k1_numbers,k1_numbers,k34_binop_2,A,B) = k10_binop_2(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d10_binop_2]), [file(rvsum_1,l5_rvsum_1),interesting(0.53)]). fof(t78_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k2_seq_1(k5_numbers,k1_numbers,k11_rvsum_1(B),A) = k7_square_1(k2_seq_1(k5_numbers,k1_numbers,B,A)) ) ) ), inference(mizar_proof,[status(thm)],[t77_rvsum_1,d4_funct_1,d4_funct_1,t22_funct_1,d2_rvsum_1]), [file(rvsum_1,t78_rvsum_1),interesting(0.52)]). fof(t19_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k2_seq_1(k1_numbers,k1_numbers,k2_rvsum_1(A),B) = k11_binop_2(A,B) ) ) ), inference(mizar_proof,[status(thm)],[l22_rvsum_1]), [file(rvsum_1,t19_rvsum_1),interesting(0.50)]). fof(t68_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => k9_rvsum_1(A,k6_finseq_1(k1_numbers)) = k6_finseq_1(k1_numbers) ) ), inference(mizar_proof,[status(thm)],[t38_finseq_2]), [file(rvsum_1,t68_rvsum_1),interesting(0.50)]). fof(t104_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k15_rvsum_1(k8_finseq_1(k1_numbers,B,k12_finseq_1(k1_numbers,A))) = k9_binop_2(k15_rvsum_1(B),A) ) ) ), inference(mizar_proof,[status(thm)],[t5_finsop_1,d9_binop_2]), [file(rvsum_1,t104_rvsum_1),interesting(0.49)]). fof(t109_rvsum_1,theorem,( ! [A] : ( m2_finseq_2(A,k1_numbers,k4_finseq_2(0,k1_numbers)) => k15_rvsum_1(A) = 0 ) ), inference(mizar_proof,[status(thm)],[t102_rvsum_1,t113_finseq_2]), [file(rvsum_1,t109_rvsum_1),interesting(0.49)]). fof(t121_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ( k15_rvsum_1(k12_rvsum_1(A,B)) = 0 => B = k4_finseqop(k1_numbers,A,0) ) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,t109_finseq_2,d3_finseq_1,t10_finseq_2,d3_finseq_1,t72_square_1,t78_rvsum_1,t37_finseq_2,t70_finseq_2,t74_square_1,t78_rvsum_1,t115_rvsum_1]), [file(rvsum_1,t121_rvsum_1),interesting(0.49)]). fof(t139_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => k16_rvsum_1(k12_rvsum_1(A,B)) = k7_square_1(k16_rvsum_1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t97_rvsum_1,t137_rvsum_1]), [file(rvsum_1,t139_rvsum_1),interesting(0.49)]). fof(t38_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => k5_rvsum_1(k12_finseq_1(k1_numbers,A)) = k12_finseq_1(k1_numbers,k7_binop_2(A)) ) ), inference(mizar_proof,[status(thm)],[t39_finseq_2,d7_binop_2]), [file(rvsum_1,t38_rvsum_1),interesting(0.49)]). fof(t81_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => k11_rvsum_1(k12_finseq_1(k1_numbers,A)) = k12_finseq_1(k1_numbers,k7_square_1(A)) ) ), inference(mizar_proof,[status(thm)],[t39_finseq_2,d2_rvsum_1]), [file(rvsum_1,t81_rvsum_1),interesting(0.49)]). fof(t69_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k9_rvsum_1(A,k12_finseq_1(k1_numbers,B)) = k12_finseq_1(k1_numbers,k11_binop_2(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t39_finseq_2,l22_rvsum_1]), [file(rvsum_1,t69_rvsum_1),interesting(0.48)]). fof(t75_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => k10_rvsum_1(A,0,B) = k4_finseqop(k1_numbers,A,0) ) ) ), inference(mizar_proof,[status(thm)],[d4_finseq_1,t44_funcop_1,t79_relat_1,t16_rvsum_1,t22_rvsum_1,t2_binop_2,t80_finseqop]), [file(rvsum_1,t75_rvsum_1),interesting(0.47)]). fof(t108_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k15_rvsum_1(k3_finseq_4(k1_numbers,A,B,C)) = k9_binop_2(k9_binop_2(A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[t60_finseq_1,t104_rvsum_1,t107_rvsum_1]), [file(rvsum_1,t108_rvsum_1),interesting(0.46)]). fof(t130_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k16_rvsum_1(k3_finseq_4(k1_numbers,A,B,C)) = k11_binop_2(k11_binop_2(A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[t60_finseq_1,t126_rvsum_1,t129_rvsum_1]), [file(rvsum_1,t130_rvsum_1),interesting(0.46)]). fof(t131_rvsum_1,theorem,( ! [A] : ( m2_finseq_2(A,k1_numbers,k4_finseq_2(0,k1_numbers)) => k16_rvsum_1(A) = 1 ) ), inference(mizar_proof,[status(thm)],[t124_rvsum_1,t113_finseq_2]), [file(rvsum_1,t131_rvsum_1),interesting(0.46)]). fof(t66_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m2_finseq_1(C,k1_numbers) => k2_seq_1(k5_numbers,k1_numbers,k9_rvsum_1(B,C),A) = k11_binop_2(B,k2_seq_1(k5_numbers,k1_numbers,C,A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t65_rvsum_1,d4_funct_1,d4_funct_1,t21_funct_1,t22_funct_1,t42_funcop_1,t35_funct_1,d11_binop_2]), [file(rvsum_1,t66_rvsum_1),interesting(0.44)]). fof(t29_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k3_rvsum_1(k12_finseq_1(k1_numbers,A),k12_finseq_1(k1_numbers,B)) = k12_finseq_1(k1_numbers,k9_binop_2(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t88_finseq_2,d9_binop_2]), [file(rvsum_1,t29_rvsum_1),interesting(0.44)]). fof(t33_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => k4_rvsum_1(A,B,k4_finseqop(k1_numbers,A,0)) = B ) ) ), inference(mizar_proof,[status(thm)],[t2_binop_2,t57_finseqop]), [file(rvsum_1,t33_rvsum_1),interesting(0.44)]). fof(t50_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k7_rvsum_1(k12_finseq_1(k1_numbers,A),k12_finseq_1(k1_numbers,B)) = k12_finseq_1(k1_numbers,k10_binop_2(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t88_finseq_2,l5_rvsum_1]), [file(rvsum_1,t50_rvsum_1),interesting(0.44)]). fof(t89_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k13_rvsum_1(k12_finseq_1(k1_numbers,A),k12_finseq_1(k1_numbers,B)) = k12_finseq_1(k1_numbers,k11_binop_2(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t88_finseq_2,d11_binop_2]), [file(rvsum_1,t89_rvsum_1),interesting(0.44)]). fof(t98_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k12_rvsum_1(A,k4_rvsum_1(A,B,C)) = k4_rvsum_1(A,k4_rvsum_1(A,k12_rvsum_1(A,B),k10_rvsum_1(A,2,k14_rvsum_1(A,B,C))),k12_rvsum_1(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t78_rvsum_1,t27_rvsum_1,t78_rvsum_1,t78_rvsum_1,t87_rvsum_1,t66_rvsum_1,t27_rvsum_1,t27_rvsum_1,t139_finseq_2]), [file(rvsum_1,t98_rvsum_1),interesting(0.43)]). fof(t132_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k16_rvsum_1(k4_finseqop(k1_numbers,A,1)) = 1 ) ), inference(mizar_proof,[status(thm)],[t7_binop_2,t35_setwop_2]), [file(rvsum_1,t132_rvsum_1),interesting(0.43)]). fof(t53_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => k8_rvsum_1(A,B,k4_finseqop(k1_numbers,A,0)) = B ) ) ), inference(mizar_proof,[status(thm)],[t52_rvsum_1,t39_rvsum_1,t33_rvsum_1]), [file(rvsum_1,t53_rvsum_1),interesting(0.42)]). fof(t106_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k15_rvsum_1(k8_finseq_1(k1_numbers,k12_finseq_1(k1_numbers,A),B)) = k9_binop_2(A,k15_rvsum_1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t105_rvsum_1,t103_rvsum_1]), [file(rvsum_1,t106_rvsum_1),interesting(0.41)]). fof(t128_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k16_rvsum_1(k8_finseq_1(k1_numbers,k12_finseq_1(k1_numbers,A),B)) = k11_binop_2(A,k16_rvsum_1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t127_rvsum_1,t125_rvsum_1]), [file(rvsum_1,t128_rvsum_1),interesting(0.41)]). fof(t49_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ( k7_rvsum_1(k6_finseq_1(k1_numbers),A) = k6_finseq_1(k1_numbers) & k7_rvsum_1(A,k6_finseq_1(k1_numbers)) = k6_finseq_1(k1_numbers) ) ) ), inference(mizar_proof,[status(thm)],[t87_finseq_2]), [file(rvsum_1,t49_rvsum_1),interesting(0.41)]). fof(t92_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k14_rvsum_1(A,k4_finseqop(k1_numbers,A,B),C) = k10_rvsum_1(A,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_finseqop,t23_finseqop]), [file(rvsum_1,t92_rvsum_1),interesting(0.40)]). fof(t74_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => k10_rvsum_1(A,1,B) = B ) ) ), inference(mizar_proof,[status(thm)],[d4_finseq_1,t7_binop_2,t45_finseqop,t79_relat_1]), [file(rvsum_1,t74_rvsum_1),interesting(0.40)]). fof(t133_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ( ? [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) & r2_hidden(B,k4_finseq_1(A)) & k2_seq_1(k5_numbers,k1_numbers,A,B) = 0 ) <=> k16_rvsum_1(A) = 0 ) ) ), inference(mizar_proof,[status(thm)],[t124_rvsum_1,t4_finseq_1,t32_finseq_1,t22_finseq_2,t19_finseq_2,t126_rvsum_1,d3_finseq_1,d7_finseq_1,t59_finseq_1,t8_finseq_2,d3_finseq_1,d7_finseq_1,t9_finseq_2,t6_finseq_1,t59_finseq_1,t6_xcmplx_1,d3_finseq_1,s1_nat_1]), [file(rvsum_1,t133_rvsum_1),interesting(0.39)]). fof(t70_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k10_rvsum_1(A,B,k4_finseqop(k1_numbers,A,C)) = k4_finseqop(k1_numbers,A,k11_binop_2(B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t17_finseqop,l22_rvsum_1]), [file(rvsum_1,t70_rvsum_1),interesting(0.38)]). fof(t115_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ~ ( ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r2_hidden(B,k4_finseq_1(A)) => r1_xreal_0(0,k2_seq_1(k5_numbers,k1_numbers,A,B)) ) ) & ? [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) & r2_hidden(B,k4_finseq_1(A)) & ~ r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,B),0) ) & r1_xreal_0(k15_rvsum_1(A),0) ) ) ), inference(mizar_proof,[status(thm)],[t110_finseq_2,d3_finseq_1,t70_finseq_2,t70_finseq_2,t113_rvsum_1,t111_rvsum_1]), [file(rvsum_1,t115_rvsum_1),interesting(0.37)]). fof(t82_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k12_rvsum_1(A,k4_finseqop(k1_numbers,A,B)) = k4_finseqop(k1_numbers,A,k7_square_1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t17_finseqop,d2_rvsum_1]), [file(rvsum_1,t82_rvsum_1),interesting(0.37)]). fof(t41_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ( k4_rvsum_1(A,B,C) = k4_finseqop(k1_numbers,A,0) => B = k6_rvsum_1(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_rvsum_1,t23_rvsum_1,t2_binop_2,t78_finseqop]), [file(rvsum_1,t41_rvsum_1),interesting(0.35)]). fof(t54_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => k8_rvsum_1(A,k4_finseqop(k1_numbers,A,0),B) = k6_rvsum_1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t52_rvsum_1,t33_rvsum_1]), [file(rvsum_1,t54_rvsum_1),interesting(0.32)]). fof(t96_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k10_rvsum_1(A,B,C) = k14_rvsum_1(A,k4_finseqop(k1_numbers,A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[t92_rvsum_1]), [file(rvsum_1,t96_rvsum_1),interesting(0.27)]). fof(t138_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k16_rvsum_1(k10_rvsum_1(A,B,C)) = k11_binop_2(k16_rvsum_1(k4_finseqop(k1_numbers,A,B)),k16_rvsum_1(C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t92_rvsum_1,t137_rvsum_1]), [file(rvsum_1,t138_rvsum_1),interesting(0.23)]). fof(t86_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => ! [C] : ( m2_finseq_1(C,k1_numbers) => ( r2_hidden(A,k4_finseq_1(k13_rvsum_1(B,C))) => k2_seq_1(k5_numbers,k1_numbers,k13_rvsum_1(B,C),A) = k11_binop_2(k2_seq_1(k5_numbers,k1_numbers,B,A),k2_seq_1(k5_numbers,k1_numbers,C,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_funcop_1,d11_binop_2]), [file(rvsum_1,t86_rvsum_1),interesting(0.18)]). fof(t47_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => ! [C] : ( m2_finseq_1(C,k1_numbers) => ( r2_hidden(A,k4_finseq_1(k7_rvsum_1(B,C))) => k2_seq_1(k5_numbers,k1_numbers,k7_rvsum_1(B,C),A) = k10_binop_2(k2_seq_1(k5_numbers,k1_numbers,B,A),k2_seq_1(k5_numbers,k1_numbers,C,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_funcop_1,l5_rvsum_1]), [file(rvsum_1,t47_rvsum_1),interesting(0.18)]). fof(t36_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => ( C = k2_seq_1(k5_numbers,k1_numbers,D,B) => k2_seq_1(k5_numbers,k1_numbers,k6_rvsum_1(A,D),B) = k7_binop_2(C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t35_rvsum_1]), [file(rvsum_1,t36_rvsum_1),interesting(0.16)]). fof(t26_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => ! [C] : ( m2_finseq_1(C,k1_numbers) => ( r2_hidden(A,k4_finseq_1(k3_rvsum_1(B,C))) => k2_seq_1(k5_numbers,k1_numbers,k3_rvsum_1(B,C),A) = k9_binop_2(k2_seq_1(k5_numbers,k1_numbers,B,A),k2_seq_1(k5_numbers,k1_numbers,C,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_funcop_1,d9_binop_2]), [file(rvsum_1,t26_rvsum_1),interesting(0.03)]). 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(d11_binop_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(k1_numbers,k1_numbers),k1_numbers) & m2_relset_1(A,k2_zfmisc_1(k1_numbers,k1_numbers),k1_numbers) ) => ( A = k35_binop_2 <=> ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k2_binop_1(k1_numbers,k1_numbers,k1_numbers,A,B,C) = k11_binop_2(B,C) ) ) ) ) ), file(binop_2,d11_binop_2), [interesting(0.00)]). fof(d2_rvsum_1,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k1_numbers,k1_numbers) & m2_relset_1(A,k1_numbers,k1_numbers) ) => ( A = k1_rvsum_1 <=> ! [B] : ( m1_subset_1(B,k1_numbers) => k2_seq_1(k1_numbers,k1_numbers,A,B) = k7_square_1(B) ) ) ) ), file(rvsum_1,d2_rvsum_1), [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)) ) ) ) ) ) ) ) ), file(finseqop,t52_finseqop), [interesting(0.00)]). fof(t100_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k12_rvsum_1(A,k14_rvsum_1(A,B,C)) = k14_rvsum_1(A,k12_rvsum_1(A,B),k12_rvsum_1(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t17_rvsum_1,t52_finseqop]), [file(rvsum_1,t100_rvsum_1),interesting(0.00)]). fof(t101_rvsum_1,theorem,( $true ), file(rvsum_1,t101_rvsum_1), [interesting(0.00)]). fof(t6_finsop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,A) => ! [C] : ( m2_finseq_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) ) => ( v2_binop_1(D,A) => ( ( ~ v1_setwiseo(D,A) & ~ ( r1_xreal_0(1,k3_finseq_1(B)) & r1_xreal_0(1,k3_finseq_1(C)) ) ) | k2_finsop_1(A,k8_finseq_1(A,B,C),D) = k2_binop_1(A,A,A,D,k2_finsop_1(A,B,D),k2_finsop_1(A,C,D)) ) ) ) ) ) ) ), file(finsop_1,t6_finsop_1), [interesting(0.00)]). fof(d9_binop_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(k1_numbers,k1_numbers),k1_numbers) & m2_relset_1(A,k2_zfmisc_1(k1_numbers,k1_numbers),k1_numbers) ) => ( A = k33_binop_2 <=> ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k2_binop_1(k1_numbers,k1_numbers,k1_numbers,A,B,C) = k9_binop_2(B,C) ) ) ) ) ), file(binop_2,d9_binop_2), [interesting(0.00)]). fof(t12_finsop_1,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) ) => k2_finsop_1(A,k12_finseq_1(A,B),C) = B ) ) ) ), file(finsop_1,t12_finsop_1), [interesting(0.00)]). fof(t60_finseq_1,theorem,( ! [A,B,C] : ( k11_finseq_1(A,B,C) = k7_finseq_1(k9_finseq_1(A),k10_finseq_1(B,C)) & k11_finseq_1(A,B,C) = k7_finseq_1(k10_finseq_1(A,B),k9_finseq_1(C)) ) ), file(finseq_1,t60_finseq_1), [interesting(0.00)]). fof(t5_finsop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m2_finseq_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) | r1_xreal_0(1,k3_finseq_1(C)) ) => k2_finsop_1(A,k8_finseq_1(A,C,k12_finseq_1(A,B)),D) = k2_binop_1(A,A,A,D,k2_finsop_1(A,C,D),B) ) ) ) ) ) ), file(finsop_1,t5_finsop_1), [interesting(0.00)]). fof(d9_finseq_1,definition,( ! [A,B] : k10_finseq_1(A,B) = k7_finseq_1(k9_finseq_1(A),k9_finseq_1(B)) ), file(finseq_1,d9_finseq_1), [interesting(0.00)]). fof(t2_binop_2,theorem,( k3_binop_1(k1_numbers,k33_binop_2) = 0 ), file(binop_2,t2_binop_2), [interesting(0.00)]). fof(t11_finsop_1,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) => k2_finsop_1(A,k6_finseq_1(A),B) = k3_binop_1(A,B) ) ) ) ), file(finsop_1,t11_finsop_1), [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(t10_rvsum_1,theorem,( $true ), file(rvsum_1,t10_rvsum_1), [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(d7_binop_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k1_numbers,k1_numbers) & m2_relset_1(A,k1_numbers,k1_numbers) ) => ( A = k31_binop_2 <=> ! [B] : ( m1_subset_1(B,k1_numbers) => k8_funct_2(k1_numbers,k1_numbers,A,B) = k7_binop_2(B) ) ) ) ), file(binop_2,d7_binop_2), [interesting(0.00)]). fof(t22_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) <=> r3_binop_1(A,k3_binop_1(A,B),B) ) ) ) ), file(setwiseo,t22_setwiseo), [interesting(0.00)]). fof(d8_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) ) => ( ? [C] : ( m1_subset_1(C,A) & r3_binop_1(A,C,B) ) => ! [C] : ( m1_subset_1(C,A) => ( C = k3_binop_1(A,B) <=> r3_binop_1(A,C,B) ) ) ) ) ), file(binop_1,d8_binop_1), [interesting(0.00)]). fof(d2_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_finseqop(B,A) <=> ? [C] : ( v1_funct_1(C) & v1_funct_2(C,A,A) & m2_relset_1(C,A,A) & r1_finseqop(A,C,B) ) ) ) ) ), file(finseqop,d2_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(t42_setwop_2,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] : ( m2_finseq_1(C,A) => ( ( v1_binop_1(B,A) & v2_binop_1(B,A) & v1_setwiseo(B,A) & v1_finseqop(B,A) ) => k8_funct_2(A,A,k6_finseqop(A,B),k2_finsop_1(A,C,B)) = k2_finsop_1(A,k5_finseqop(A,A,C,k6_finseqop(A,B)),B) ) ) ) ) ), file(setwop_2,t42_setwop_2), [interesting(0.00)]). fof(t11_rvsum_1,theorem,( $true ), file(rvsum_1,t11_rvsum_1), [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(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(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(t72_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => r1_xreal_0(0,k5_square_1(A)) ) ), file(square_1,t72_square_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(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(t46_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ( r1_tarski(k2_relat_1(A),k1_relat_1(B)) => k1_relat_1(k5_relat_1(A,B)) = k1_relat_1(A) ) ) ) ), file(relat_1,t46_relat_1), [interesting(0.00)]). fof(d4_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C] : ( ( r2_hidden(B,k1_relat_1(A)) => ( C = k1_funct_1(A,B) <=> r2_hidden(k4_tarski(B,C),A) ) ) & ( ~ r2_hidden(B,k1_relat_1(A)) => ( C = k1_funct_1(A,B) <=> C = k1_xboole_0 ) ) ) ) ), file(funct_1,d4_funct_1), [interesting(0.00)]). fof(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(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(t70_finseq_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B,C] : ( r2_hidden(B,k2_finseq_1(A)) => k1_funct_1(k2_finseq_2(A,C),B) = C ) ) ), file(finseq_2,t70_finseq_2), [interesting(0.00)]). fof(t74_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( 0 != A & r1_xreal_0(k5_square_1(A),0) ) ) ), file(square_1,t74_square_1), [interesting(0.00)]). fof(t110_finseq_2,theorem,( ! [A,B] : ( m2_finseq_1(B,A) => m1_subset_1(B,k4_finseq_2(k3_finseq_1(B),A)) ) ), file(finseq_2,t110_finseq_2), [interesting(0.00)]). fof(t4_finseq_1,theorem, ( k2_finseq_1(0) = k1_xboole_0 & k2_finseq_1(1) = k1_tarski(1) & k2_finseq_1(2) = k2_tarski(1,2) ), file(finseq_1,t4_finseq_1), [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(t6_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => r2_hidden(k2_xcmplx_0(A,1),k2_finseq_1(k2_xcmplx_0(A,1))) ) ), file(finseq_1,t6_finseq_1), [interesting(0.00)]). fof(t136_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)) => ! [D] : ( m1_subset_1(D,B) => k1_funct_1(k8_finseq_1(B,C,k12_finseq_1(B,D)),k1_nat_1(A,1)) = D ) ) ) ) ), file(finseq_2,t136_finseq_2), [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(t9_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r2_hidden(A,k2_finseq_1(B)) => r2_hidden(A,k2_finseq_1(k1_nat_1(B,C))) ) ) ) ) ), file(finseq_2,t9_finseq_2), [interesting(0.00)]). fof(t10_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ~ ( ~ r1_xreal_0(B,A) & r1_xreal_0(C,D) & r1_xreal_0(k2_xcmplx_0(B,D),k2_xcmplx_0(A,C)) ) ) ) ) ) ), file(xreal_1,t10_xreal_1), [interesting(0.00)]). fof(t9_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( ( r1_xreal_0(A,B) & r1_xreal_0(C,D) ) => r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,D)) ) ) ) ) ) ), file(xreal_1,t9_xreal_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(t112_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ( ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k2_finseq_1(A)) => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,B,D),k2_seq_1(k5_numbers,k1_numbers,C,D)) ) ) => r1_xreal_0(k15_rvsum_1(B),k15_rvsum_1(C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t102_rvsum_1,t113_finseq_2,t137_finseq_2,t137_finseq_2,t6_finseq_1,t136_finseq_2,d3_finseq_1,t109_finseq_2,d7_finseq_1,t9_finseq_2,t104_rvsum_1,t9_xreal_1,s1_nat_1]), [file(rvsum_1,t112_rvsum_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(t113_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ~ ( ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k2_finseq_1(A)) => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,B,D),k2_seq_1(k5_numbers,k1_numbers,C,D)) ) ) & ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & r2_hidden(D,k2_finseq_1(A)) & ~ r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,C,D),k2_seq_1(k5_numbers,k1_numbers,B,D)) ) & r1_xreal_0(k15_rvsum_1(C),k15_rvsum_1(B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t4_finseq_1,t137_finseq_2,t137_finseq_2,t6_finseq_1,t136_finseq_2,d3_finseq_1,t109_finseq_2,d7_finseq_1,t9_finseq_2,d3_finseq_1,t109_finseq_2,d7_finseq_1,t104_rvsum_1,t10_xreal_1,t104_rvsum_1,t112_rvsum_1,t10_xreal_1,t8_finseq_2,s1_nat_1]), [file(rvsum_1,t113_rvsum_1),interesting(0.00)]). fof(t74_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : k2_finseq_2(k1_nat_1(A,1),B) = k7_finseq_1(k2_finseq_2(A,B),k9_finseq_1(B)) ) ), file(finseq_2,t74_finseq_2), [interesting(0.00)]). fof(t21_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(k2_xcmplx_0(A,B),C) <=> r1_xreal_0(A,k6_xcmplx_0(C,B)) ) ) ) ) ), file(xreal_1,t21_xreal_1), [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(t41_setwop_2,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] : ( m2_finseq_1(E,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)),k2_finsop_1(A,E,C)) = k2_finsop_1(A,k5_finseqop(A,A,E,k8_funcop_1(A,A,D,B,k6_partfun1(A))),C) ) ) ) ) ) ) ), file(setwop_2,t41_setwop_2), [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(l22_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k2_seq_1(k1_numbers,k1_numbers,k8_funcop_1(k1_numbers,k1_numbers,k35_binop_2,A,k6_partfun1(k1_numbers)),B) = k11_binop_2(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t66_funcop_1,t35_funct_1,d11_binop_2]), [file(rvsum_1,l22_rvsum_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(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(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)) ) ) ) ) ) ) ) ), file(finseqop,t53_finseqop), [interesting(0.00)]). fof(t84_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k12_rvsum_1(A,k10_rvsum_1(A,B,C)) = k10_rvsum_1(A,k7_square_1(B),k12_rvsum_1(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_finseq_1,d4_finseq_1,t44_funcop_1,t79_relat_1,t17_rvsum_1,t53_finseqop,t79_relat_1,t44_funcop_1,d2_rvsum_1]), [file(rvsum_1,t84_rvsum_1),interesting(0.00)]). 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))) ) ) ) ) ) ) ) ) ) ), file(finseqop,t11_finseqop), [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(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(t55_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ! [C] : ( v1_relat_1(C) => k5_relat_1(k5_relat_1(A,B),C) = k5_relat_1(A,k5_relat_1(B,C)) ) ) ) ), file(relat_1,t55_relat_1), [interesting(0.00)]). fof(t71_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => k10_rvsum_1(A,k11_binop_2(B,C),D) = k10_rvsum_1(A,B,k10_rvsum_1(A,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_binop_2,t77_funcop_1,t69_funcop_1,t55_relat_1]), [file(rvsum_1,t71_rvsum_1),interesting(0.00)]). 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) ) ) ) ) ) ) ) ), file(finseqop,t27_finseqop), [interesting(0.00)]). fof(t94_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => k10_rvsum_1(A,B,k14_rvsum_1(A,C,D)) = k14_rvsum_1(A,k10_rvsum_1(A,B,C),D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_finseqop]), [file(rvsum_1,t94_rvsum_1),interesting(0.00)]). fof(d1_rvsum_1,definition,( k34_binop_2 = k8_finseqop(k1_numbers,k33_binop_2,k6_partfun1(k1_numbers),k31_binop_2) ), file(rvsum_1,d1_rvsum_1), [interesting(0.00)]). fof(t48_setwop_2,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] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( m2_finseq_2(E,A,k4_finseq_2(D,A)) => ! [F] : ( m2_finseq_2(F,A,k4_finseq_2(D,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)) ) => k2_binop_1(A,A,A,C,k2_finsop_1(A,E,B),k2_finsop_1(A,F,B)) = k2_finsop_1(A,k1_finseqop(A,A,A,C,E,F),B) ) ) ) ) ) ) ) ), file(setwop_2,t48_setwop_2), [interesting(0.00)]). fof(d10_binop_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(k1_numbers,k1_numbers),k1_numbers) & m2_relset_1(A,k2_zfmisc_1(k1_numbers,k1_numbers),k1_numbers) ) => ( A = k34_binop_2 <=> ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k2_binop_1(k1_numbers,k1_numbers,k1_numbers,A,B,C) = k10_binop_2(B,C) ) ) ) ) ), file(binop_2,d10_binop_2), [interesting(0.00)]). fof(t120_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k15_rvsum_1(k8_rvsum_1(A,B,C)) = k10_binop_2(k15_rvsum_1(B),k15_rvsum_1(C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_rvsum_1,t22_rvsum_1,t23_rvsum_1,t48_setwop_2,l5_rvsum_1]), [file(rvsum_1,t120_rvsum_1),interesting(0.00)]). fof(t46_setwop_2,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] : ( 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)) => ( ( v1_binop_1(B,A) & v2_binop_1(B,A) & v1_setwiseo(B,A) ) => k2_binop_1(A,A,A,B,k2_finsop_1(A,D,B),k2_finsop_1(A,E,B)) = k2_finsop_1(A,k1_finseqop(A,A,A,B,D,E),B) ) ) ) ) ) ) ), file(setwop_2,t46_setwop_2), [interesting(0.00)]). fof(t119_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k15_rvsum_1(k4_rvsum_1(A,B,C)) = k9_binop_2(k15_rvsum_1(B),k15_rvsum_1(C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t46_setwop_2,d9_binop_2]), [file(rvsum_1,t119_rvsum_1),interesting(0.00)]). 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))) ) ) ) ) ) ), file(finseqop,t9_finseqop), [interesting(0.00)]). 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)) ) ) ) ) ) ) ), file(finseqop,t89_finseqop), [interesting(0.00)]). fof(t52_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k8_rvsum_1(A,B,C) = k4_rvsum_1(A,B,k6_rvsum_1(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_rvsum_1,t89_finseqop]), [file(rvsum_1,t52_rvsum_1),interesting(0.00)]). fof(t144_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)) => k4_finseq_1(C) = k2_finseq_1(A) ) ) ) ), file(finseq_2,t144_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(t27_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => k2_seq_1(k5_numbers,k1_numbers,k4_rvsum_1(A,C,D),B) = k9_binop_2(k2_seq_1(k5_numbers,k1_numbers,C,B),k2_seq_1(k5_numbers,k1_numbers,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t144_finseq_2,t144_finseq_2,t144_finseq_2,d4_funct_1,d4_funct_1,d4_funct_1,t144_finseq_2,t26_rvsum_1]), [file(rvsum_1,t27_rvsum_1),interesting(0.00)]). fof(t87_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => k2_seq_1(k5_numbers,k1_numbers,k14_rvsum_1(A,C,D),B) = k11_binop_2(k2_seq_1(k5_numbers,k1_numbers,C,B),k2_seq_1(k5_numbers,k1_numbers,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t144_finseq_2,t144_finseq_2,d4_funct_1,d4_funct_1,t144_finseq_2,t86_rvsum_1]), [file(rvsum_1,t87_rvsum_1),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(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(t139_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)) => ! [D] : ( m2_finseq_2(D,B,k4_finseq_2(A,B)) => ( ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r2_hidden(E,k2_finseq_1(A)) => k1_funct_1(C,E) = k1_funct_1(D,E) ) ) => C = D ) ) ) ) ) ), file(finseq_2,t139_finseq_2), [interesting(0.00)]). fof(t7_binop_2,theorem,( k3_binop_1(k1_numbers,k35_binop_2) = 1 ), file(binop_2,t7_binop_2), [interesting(0.00)]). 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 ) ) ) ) ) ), file(finseqop,t72_finseqop), [interesting(0.00)]). fof(t123_rvsum_1,theorem,( $true ), file(rvsum_1,t123_rvsum_1), [interesting(0.00)]). fof(t12_rvsum_1,theorem,( $true ), file(rvsum_1,t12_rvsum_1), [interesting(0.00)]). fof(t35_setwop_2,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] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( v1_setwiseo(B,A) => k2_finsop_1(A,k1_finsop_1(A,C,k3_binop_1(A,B)),B) = k3_binop_1(A,B) ) ) ) ) ), file(setwop_2,t35_setwop_2), [interesting(0.00)]). fof(t32_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( A = k6_finseq_1(B) <=> k3_finseq_1(A) = 0 ) ) ), file(finseq_1,t32_finseq_1), [interesting(0.00)]). fof(t22_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,A) => ~ ( k3_finseq_1(B) != 0 & ! [C] : ( m2_finseq_1(C,A) => ! [D] : ( m1_subset_1(D,A) => B != k8_finseq_1(A,C,k12_finseq_1(A,D)) ) ) ) ) ) ), file(finseq_2,t22_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(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(t6_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ~ ( k3_xcmplx_0(A,B) = 0 & A != 0 & B != 0 ) ) ) ), file(xcmplx_1,t6_xcmplx_1), [interesting(0.00)]). fof(t37_setwop_2,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] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( v2_binop_1(C,A) => ( ( ~ ( r1_xreal_0(1,D) & r1_xreal_0(1,E) ) & ~ v1_setwiseo(C,A) ) | k2_finsop_1(A,k1_finsop_1(A,k1_nat_1(D,E),B),C) = k2_binop_1(A,A,A,C,k2_finsop_1(A,k1_finsop_1(A,D,B),C),k2_finsop_1(A,k1_finsop_1(A,E,B),C)) ) ) ) ) ) ) ) ), file(setwop_2,t37_setwop_2), [interesting(0.00)]). fof(t134_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k16_rvsum_1(k4_finseqop(k1_numbers,k23_binop_2(A,B),C)) = k11_binop_2(k16_rvsum_1(k4_finseqop(k1_numbers,A,C)),k16_rvsum_1(k4_finseqop(k1_numbers,B,C))) ) ) ) ), inference(mizar_proof,[status(thm)],[t37_setwop_2,d11_binop_2]), [file(rvsum_1,t134_rvsum_1),interesting(0.00)]). fof(t38_setwop_2,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] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( ( v1_binop_1(C,A) & v2_binop_1(C,A) ) => ( ( ~ ( r1_xreal_0(1,D) & r1_xreal_0(1,E) ) & ~ v1_setwiseo(C,A) ) | k2_finsop_1(A,k1_finsop_1(A,k2_nat_1(D,E),B),C) = k2_finsop_1(A,k1_finsop_1(A,E,k2_finsop_1(A,k1_finsop_1(A,D,B),C)),C) ) ) ) ) ) ) ) ), file(setwop_2,t38_setwop_2), [interesting(0.00)]). fof(t135_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k16_rvsum_1(k4_finseqop(k1_numbers,k24_binop_2(A,B),C)) = k16_rvsum_1(k4_finseqop(k1_numbers,B,k16_rvsum_1(k4_finseqop(k1_numbers,A,C)))) ) ) ) ), inference(mizar_proof,[status(thm)],[t38_setwop_2]), [file(rvsum_1,t135_rvsum_1),interesting(0.00)]). fof(t47_setwop_2,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] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( ( v1_binop_1(D,A) & v2_binop_1(D,A) & v1_setwiseo(D,A) ) => k2_finsop_1(A,k1_finsop_1(A,E,k2_binop_1(A,A,A,D,B,C)),D) = k2_binop_1(A,A,A,D,k2_finsop_1(A,k1_finsop_1(A,E,B),D),k2_finsop_1(A,k1_finsop_1(A,E,C),D)) ) ) ) ) ) ) ), file(setwop_2,t47_setwop_2), [interesting(0.00)]). fof(t136_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k16_rvsum_1(k4_finseqop(k1_numbers,A,k11_binop_2(B,C))) = k11_binop_2(k16_rvsum_1(k4_finseqop(k1_numbers,A,B)),k16_rvsum_1(k4_finseqop(k1_numbers,A,C))) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_binop_2,t47_setwop_2,d11_binop_2]), [file(rvsum_1,t136_rvsum_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) ) ) ) ) ) ) ) ), file(finseqop,t21_finseqop), [interesting(0.00)]). 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))) ) ) ) ) ) ) ) ), file(finseqop,t23_finseqop), [interesting(0.00)]). fof(t137_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k16_rvsum_1(k14_rvsum_1(A,B,C)) = k11_binop_2(k16_rvsum_1(B),k16_rvsum_1(C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t46_setwop_2,d11_binop_2]), [file(rvsum_1,t137_rvsum_1),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(t14_rvsum_1,theorem,( $true ), file(rvsum_1,t14_rvsum_1), [interesting(0.00)]). fof(t15_rvsum_1,theorem,( $true ), file(rvsum_1,t15_rvsum_1), [interesting(0.00)]). fof(t18_rvsum_1,theorem,( $true ), file(rvsum_1,t18_rvsum_1), [interesting(0.00)]). fof(t1_rvsum_1,theorem,( $true ), file(rvsum_1,t1_rvsum_1), [interesting(0.00)]). 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) ) ) ) ), file(finseqop,t67_finseqop), [interesting(0.00)]). fof(t25_rvsum_1,theorem,( $true ), file(rvsum_1,t25_rvsum_1), [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(t88_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] : ( m1_subset_1(E,B) => ! [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) => ! [H] : ( m2_finseq_1(H,B) => ( ( G = k12_finseq_1(A,D) & H = k12_finseq_1(B,E) ) => k3_funcop_1(F,G,H) = k12_finseq_1(C,k2_binop_1(A,B,C,F,D,E)) ) ) ) ) ) ) ) ) ) ), file(finseq_2,t88_finseq_2), [interesting(0.00)]). fof(t2_rvsum_1,theorem,( $true ), file(rvsum_1,t2_rvsum_1), [interesting(0.00)]). 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)) ) ) ) ) ) ) ) ), file(finseqop,t18_finseqop), [interesting(0.00)]). fof(t30_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k4_rvsum_1(A,k4_finseqop(k1_numbers,A,B),k4_finseqop(k1_numbers,A,C)) = k4_finseqop(k1_numbers,A,k9_binop_2(B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_finseqop,d9_binop_2]), [file(rvsum_1,t30_rvsum_1),interesting(0.00)]). fof(t31_rvsum_1,theorem,( $true ), file(rvsum_1,t31_rvsum_1), [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(t39_finseq_2,theorem,( ! [A,B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m2_finseq_1(D,B) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,B,C) & m2_relset_1(E,B,C) ) => ( D = k9_finseq_1(A) => k1_partfun1(k5_numbers,B,B,C,D,E) = k9_finseq_1(k1_funct_1(E,A)) ) ) ) ) ) ), file(finseq_2,t39_finseq_2), [interesting(0.00)]). fof(t42_rvsum_1,theorem,( $true ), file(rvsum_1,t42_rvsum_1), [interesting(0.00)]). fof(t43_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ( k6_rvsum_1(A,B) = k6_rvsum_1(A,C) => B = C ) ) ) ) ), file(rvsum_1,t43_rvsum_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)) ) ) ) ) ) ) ) ), file(finseqop,t29_finseqop), [interesting(0.00)]). fof(t32_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => k4_rvsum_1(A,B,k4_rvsum_1(A,C,D)) = k4_rvsum_1(A,k4_rvsum_1(A,B,C),D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_finseqop]), [file(rvsum_1,t32_rvsum_1),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)) ) ) ) ) ) ) ), file(finseqop,t77_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 ) ) ) ) ) ) ), file(finseqop,t57_finseqop), [interesting(0.00)]). fof(t44_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => ( k4_rvsum_1(A,B,C) = k4_rvsum_1(A,D,C) => B = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t32_rvsum_1,t32_rvsum_1,t40_rvsum_1,t33_rvsum_1,t33_rvsum_1]), [file(rvsum_1,t44_rvsum_1),interesting(0.00)]). fof(t46_rvsum_1,theorem,( $true ), file(rvsum_1,t46_rvsum_1), [interesting(0.00)]). fof(t48_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => k2_seq_1(k5_numbers,k1_numbers,k8_rvsum_1(A,C,D),B) = k10_binop_2(k2_seq_1(k5_numbers,k1_numbers,C,B),k2_seq_1(k5_numbers,k1_numbers,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t144_finseq_2,t144_finseq_2,t144_finseq_2,d4_funct_1,d4_funct_1,d4_funct_1,t144_finseq_2,t47_rvsum_1]), [file(rvsum_1,t48_rvsum_1),interesting(0.00)]). fof(t4_rvsum_1,theorem,( $true ), file(rvsum_1,t4_rvsum_1), [interesting(0.00)]). fof(t51_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k8_rvsum_1(A,k4_finseqop(k1_numbers,A,B),k4_finseqop(k1_numbers,A,C)) = k4_finseqop(k1_numbers,A,k10_binop_2(B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_finseqop,l5_rvsum_1]), [file(rvsum_1,t51_rvsum_1),interesting(0.00)]). 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)) ) ) ) ) ) ), file(finseqop,t17_finseqop), [interesting(0.00)]). fof(t55_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k8_rvsum_1(A,B,k6_rvsum_1(A,C)) = k4_rvsum_1(A,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_rvsum_1]), [file(rvsum_1,t55_rvsum_1),interesting(0.00)]). 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 ) ) ) ) ) ) ) ), file(finseqop,t78_finseqop), [interesting(0.00)]). fof(t45_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k6_rvsum_1(A,k4_rvsum_1(A,B,C)) = k4_rvsum_1(A,k6_rvsum_1(A,B),k6_rvsum_1(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t32_rvsum_1,t32_rvsum_1,t40_rvsum_1,t33_rvsum_1,t40_rvsum_1,t41_rvsum_1]), [file(rvsum_1,t45_rvsum_1),interesting(0.00)]). fof(t59_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ( k8_rvsum_1(A,B,C) = k4_finseqop(k1_numbers,A,0) => B = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_rvsum_1,t41_rvsum_1]), [file(rvsum_1,t59_rvsum_1),interesting(0.00)]). fof(t5_rvsum_1,theorem,( $true ), file(rvsum_1,t5_rvsum_1), [interesting(0.00)]). fof(t60_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => k8_rvsum_1(A,k8_rvsum_1(A,B,C),D) = k8_rvsum_1(A,B,k4_rvsum_1(A,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_rvsum_1,t52_rvsum_1,t32_rvsum_1,t45_rvsum_1,t52_rvsum_1]), [file(rvsum_1,t60_rvsum_1),interesting(0.00)]). fof(t62_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => k8_rvsum_1(A,B,k8_rvsum_1(A,C,D)) = k4_rvsum_1(A,k8_rvsum_1(A,B,C),D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_rvsum_1,t57_rvsum_1,t32_rvsum_1,t52_rvsum_1]), [file(rvsum_1,t62_rvsum_1),interesting(0.00)]). fof(t61_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => k4_rvsum_1(A,B,k8_rvsum_1(A,C,D)) = k8_rvsum_1(A,k4_rvsum_1(A,B,C),D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_rvsum_1,t32_rvsum_1,t52_rvsum_1]), [file(rvsum_1,t61_rvsum_1),interesting(0.00)]). fof(t67_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => k2_seq_1(k5_numbers,k1_numbers,k10_rvsum_1(A,C,D),B) = k11_binop_2(C,k2_seq_1(k5_numbers,k1_numbers,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t66_rvsum_1]), [file(rvsum_1,t67_rvsum_1),interesting(0.00)]). fof(t6_rvsum_1,theorem,( $true ), file(rvsum_1,t6_rvsum_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)) ) ) ) ) ) ) ) ) ), file(finseqop,t36_finseqop), [interesting(0.00)]). fof(t31_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] : ( ( v1_relat_1(D) & v1_funct_1(D) ) => k5_relat_1(C,k3_funcop_1(D,A,B)) = k3_funcop_1(D,k5_relat_1(C,A),k5_relat_1(C,B)) ) ) ) ) ), file(funcop_1,t31_funcop_1), [interesting(0.00)]). fof(t72_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => k10_rvsum_1(A,k9_binop_2(B,C),D) = k4_rvsum_1(A,k10_rvsum_1(A,B,D),k10_rvsum_1(A,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_binop_2,t16_rvsum_1,t36_finseqop,t31_funcop_1]), [file(rvsum_1,t72_rvsum_1),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) ) ) ) ) ) ) ), file(finseqop,t55_finseqop), [interesting(0.00)]). fof(t73_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => k10_rvsum_1(A,B,k4_rvsum_1(A,C,D)) = k4_rvsum_1(A,k10_rvsum_1(A,B,C),k10_rvsum_1(A,B,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t20_rvsum_1,t52_finseqop]), [file(rvsum_1,t73_rvsum_1),interesting(0.00)]). 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 ) ) ) ) ) ), file(finseqop,t45_finseqop), [interesting(0.00)]). 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) ) ) ) ) ) ) ) ), file(finseqop,t80_finseqop), [interesting(0.00)]). fof(t79_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k2_seq_1(k5_numbers,k1_numbers,k12_rvsum_1(A,C),B) = k7_square_1(k2_seq_1(k5_numbers,k1_numbers,C,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t78_rvsum_1]), [file(rvsum_1,t79_rvsum_1),interesting(0.00)]). fof(t7_rvsum_1,theorem,( $true ), file(rvsum_1,t7_rvsum_1), [interesting(0.00)]). fof(t85_rvsum_1,theorem,( $true ), file(rvsum_1,t85_rvsum_1), [interesting(0.00)]). fof(t8_rvsum_1,theorem,( $true ), file(rvsum_1,t8_rvsum_1), [interesting(0.00)]). fof(t90_rvsum_1,theorem,( $true ), file(rvsum_1,t90_rvsum_1), [interesting(0.00)]). fof(t91_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [D] : ( m2_finseq_2(D,k1_numbers,k4_finseq_2(A,k1_numbers)) => k14_rvsum_1(A,B,k14_rvsum_1(A,C,D)) = k14_rvsum_1(A,k14_rvsum_1(A,B,C),D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_finseqop]), [file(rvsum_1,t91_rvsum_1),interesting(0.00)]). fof(t93_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k14_rvsum_1(A,k4_finseqop(k1_numbers,A,B),k4_finseqop(k1_numbers,A,C)) = k4_finseqop(k1_numbers,A,k11_binop_2(B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t92_rvsum_1,t70_rvsum_1]), [file(rvsum_1,t93_rvsum_1),interesting(0.00)]). fof(t95_rvsum_1,theorem,( $true ), file(rvsum_1,t95_rvsum_1), [interesting(0.00)]). fof(t9_rvsum_1,theorem,( $true ), file(rvsum_1,t9_rvsum_1), [interesting(0.00)]).