fof(t75_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( k2_relat_1(A) = k4_finseq_1(A) => v2_funct_1(A) ) ) ), inference(mizar_proof,[status(thm)],[t25_finseq_1,d3_finseq_1,t6_finseq_1,t29_finseq_4,t30_finseq_4,d1_tarski,d13_funct_1,t38_zfmisc_1,t76_card_2,t80_card_1,t66_finseq_3,t8_xreal_1,t8_xreal_1,d3_finseq_1,t21_xreal_1,t72_finseq_3,t12_finseq_1,t78_finseq_1,t28_card_1,t78_finseq_1,d11_card_1,t72_card_1,t2_xreal_1,t21_xreal_1,t8_xreal_1,t37_finseq_4,t40_finseq_4,t69_finseq_4,t72_finseq_3,t12_finseq_1,d3_finseq_1,t71_finseq_4,s1_nat_1]), [file(finseq_4,t75_finseq_4),interesting(1.00)]). fof(t77_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( v2_funct_1(A) <=> k4_card_1(k2_relat_1(A)) = k3_finseq_1(A) ) ) ), inference(mizar_proof,[status(thm)],[t60_card_1,t146_relat_1,d3_finseq_1,t81_card_1,t78_finseq_1,t3_funct_2,t78_finseq_1,d3_finseq_1,l84_finseq_4]), [file(finseq_4,t77_finseq_4),interesting(0.99)]). fof(l84_finseq_4,theorem,( ! [A] : ( v1_finset_1(A) => ! [B] : ( v1_finset_1(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ( ( k4_card_1(A) = k4_card_1(B) & k2_relat_1(C) = B ) => v2_funct_1(C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t73_finseq_4,t73_finseq_4,t60_card_1,t21_card_1,t146_relat_1,t22_wellord2,d3_finseq_1,t22_wellord2,t81_card_1,t78_finseq_1,d3_finseq_1,t78_finseq_1,t64_relat_1,t55_funct_1,t12_relset_1,t46_relat_1,d1_funct_2,t46_relat_1,d3_finseq_1,d2_finseq_1,t55_relat_1,d1_funct_2,t47_relat_1,t55_funct_1,t47_relat_1,t55_funct_1,d3_finseq_1,t75_finseq_4,t55_relat_1,t55_relat_1,t61_funct_1,t55_relat_1,t42_funct_1,t55_relat_1,t61_funct_1,d1_funct_2,t42_funct_1,t46_funct_1,t62_funct_1,t46_funct_1]), [file(finseq_4,l84_finseq_4),interesting(0.92)]). fof(t79_finseq_4,theorem,( ! [A] : ( v1_finset_1(A) => ! [B] : ( v1_finset_1(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ( ( k4_card_1(A) = k4_card_1(B) & k2_relat_1(C) = B ) => v2_funct_1(C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l84_finseq_4]), [file(finseq_4,t79_finseq_4),interesting(0.89)]). fof(t76_finseq_4,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) ) => ( ( k2_relat_1(A) = k2_relat_1(B) & k3_finseq_1(A) = k3_finseq_1(B) & v2_funct_1(B) ) => v2_funct_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t55_funct_1,t46_relat_1,d3_finseq_1,d2_finseq_1,t47_relat_1,t55_funct_1,d3_finseq_1,t75_finseq_4,t48_funct_1]), [file(finseq_4,t76_finseq_4),interesting(0.84)]). fof(t10_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v2_funct_1(A) <=> ! [B] : ( r2_hidden(B,k2_relat_1(A)) => r2_finseq_4(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_funct_1,d8_funct_1,t9_finseq_4,d8_funct_1,d5_funct_1,t8_finseq_4,d1_tarski,d13_funct_1,d1_tarski]), [file(finseq_4,t10_finseq_4),interesting(0.72)]). fof(t49_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ~ ( r2_hidden(B,k2_relat_1(A)) & r2_hidden(B,k2_relat_1(k6_finseq_4(A,B))) ) ) ), inference(mizar_proof,[status(thm)],[t32_finseq_4,t45_finseq_4,d5_funct_1,t47_finseq_4,t76_funct_1,t3_finseq_1,t31_xreal_1,t21_xreal_1,t2_xreal_1,t34_finseq_4,t70_funct_1]), [file(finseq_4,t49_finseq_4),interesting(0.72)]). fof(t60_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_finseq_4(A,B) <=> ( r2_hidden(B,k2_relat_1(A)) & ~ r2_hidden(B,k2_relat_1(k7_finseq_4(A,B))) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_finseq_4,d5_funct_1,d7_finseq_4,t58_finseq_4,t36_finseq_4,t26_finseq_3,t38_nat_1,t21_xreal_1,t46_finseq_4,t27_finseq_3,t27_finseq_3,t48_finseq_4,d5_funct_1,t49_finseq_4,t28_nat_1,t8_xreal_1,t38_nat_1,t27_finseq_3,t21_xreal_1,d7_finseq_4,t27_finseq_3,d7_finseq_4,d5_funct_1,t1_xreal_1,t37_finseq_4]), [file(finseq_4,t60_finseq_4),interesting(0.72)]). fof(t73_finseq_4,theorem,( ! [A] : ~ ( v1_finset_1(A) & ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ~ ( k2_relat_1(B) = A & v2_funct_1(B) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_finseq_1,t46_zfmisc_1,t44_finseq_1,t55_finseq_1,d8_funct_1,d3_finseq_1,d7_finseq_1,d8_funct_1,t4_finseq_1,t55_finseq_1,d1_tarski,d7_finseq_1,d7_finseq_1,d8_finseq_1,d5_funct_1,t4_finseq_1,t55_finseq_1,d1_tarski,d7_finseq_1,d7_finseq_1,d8_finseq_1,d5_funct_1,t4_finseq_1,d8_finseq_1,d1_tarski,t38_finseq_1,s2_finset_1]), [file(finseq_4,t73_finseq_4),interesting(0.72)]). fof(t7_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( r2_finseq_4(A,B) => r2_hidden(B,k2_relat_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d2_finseq_4,t78_card_1,t173_relat_1,t4_xboole_0,d3_xboole_0,d1_tarski,d3_xboole_0]), [file(finseq_4,t7_finseq_4),interesting(0.71)]). fof(t2_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( r1_finseq_4(A,B) => r2_hidden(B,k1_relat_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d1_finseq_4,d1_tarski,d13_funct_1]), [file(finseq_4,t2_finseq_4),interesting(0.71)]). fof(t71_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( r2_hidden(B,k2_relat_1(A)) & v2_funct_1(k1_finseq_3(A,k1_tarski(B))) & k1_finseq_3(A,k1_tarski(B)) = k7_finseq_1(k6_finseq_4(A,B),k7_finseq_4(A,B)) ) => v2_funct_1(A) ) ) ), inference(mizar_proof,[status(thm)],[d8_funct_1,t69_finseq_4,t29_finseq_4,t36_finseq_4,t29_finseq_4,t36_finseq_4,t29_finseq_4,t36_finseq_4,t18_nat_1,t22_nat_1,d3_finseq_1,t3_finseq_1,t31_finseq_4,t2_xreal_1,t38_nat_1,t21_xreal_1,t40_finseq_4,t3_finseq_1,d3_finseq_1,t38_nat_1,t31_finseq_4,t2_xreal_1,d3_finseq_1,t3_finseq_1,t21_xreal_1,t40_finseq_4,t3_finseq_1,d3_finseq_1,t41_finseq_4,d8_funct_1,d3_finseq_1,t3_finseq_1,t31_finseq_4,t2_xreal_1,t38_nat_1,t21_xreal_1,t40_finseq_4,t3_finseq_1,d3_finseq_1,t41_finseq_4,d8_funct_1,t18_nat_1,t22_nat_1,t22_nat_1,t38_nat_1,t31_finseq_4,t2_xreal_1,d3_finseq_1,t3_finseq_1,t21_xreal_1,t40_finseq_4,t3_finseq_1,d3_finseq_1,t41_finseq_4,d8_funct_1,t29_finseq_4,t36_finseq_4,t18_nat_1,t22_nat_1,d3_finseq_1,t3_finseq_1,t31_finseq_4,t2_xreal_1,t38_nat_1,t21_xreal_1,t40_finseq_4,t3_finseq_1,d3_finseq_1,t38_nat_1,t31_finseq_4,t2_xreal_1,d3_finseq_1,t3_finseq_1,t21_xreal_1,t40_finseq_4,t3_finseq_1,d3_finseq_1,t41_finseq_4,d8_funct_1,t1_xreal_1]), [file(finseq_4,t71_finseq_4),interesting(0.70)]). fof(t8_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( r2_finseq_4(A,B) <=> ? [C] : k1_tarski(C) = k10_relat_1(A,k1_tarski(B)) ) ) ), inference(mizar_proof,[status(thm)],[t7_finseq_4,d5_funct_1,d2_finseq_4,t60_card_2,d1_tarski,d13_funct_1,d1_tarski,d2_finseq_4,t79_card_1]), [file(finseq_4,t8_finseq_4),interesting(0.69)]). fof(t11_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( r1_finseq_4(A,B) <=> ( r2_hidden(B,k1_relat_1(A)) & r2_finseq_4(A,k1_funct_1(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t2_finseq_4,t3_finseq_4,t8_finseq_4,t8_finseq_4,d1_tarski,d13_funct_1,d1_tarski,t3_finseq_4]), [file(finseq_4,t11_finseq_4),interesting(0.69)]). fof(t35_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_finseq_4(A,B) => k1_finseq_4(A,B) = k5_finseq_4(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_4,t7_finseq_4,d3_finseq_4,t29_finseq_4,t30_finseq_4,d3_finseq_4]), [file(finseq_4,t35_finseq_4),interesting(0.69)]). fof(t61_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ~ ( r2_hidden(B,k2_relat_1(A)) & v2_funct_1(A) & r2_hidden(B,k2_relat_1(k7_finseq_4(A,B))) ) ) ), inference(mizar_proof,[status(thm)],[d5_funct_1,d7_finseq_4,t29_finseq_4,t30_finseq_4,t31_finseq_4,t37_nat_1,t2_xreal_1,d3_finseq_1,d7_finseq_4,t3_finseq_1,t21_xreal_1,t3_finseq_1,d3_finseq_1,d8_funct_1,t3_finseq_1]), [file(finseq_4,t61_finseq_4),interesting(0.68)]). fof(t67_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( r2_hidden(B,k2_relat_1(A)) & v2_funct_1(A) ) => v2_funct_1(k6_finseq_4(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t66_finseq_4,t45_finseq_1,t98_finseq_3]), [file(finseq_4,t67_finseq_4),interesting(0.68)]). fof(t68_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( r2_hidden(B,k2_relat_1(A)) & v2_funct_1(A) ) => v2_funct_1(k7_finseq_4(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t66_finseq_4,t98_finseq_3]), [file(finseq_4,t68_finseq_4),interesting(0.68)]). fof(t17_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( r2_finseq_4(A,B) => k10_relat_1(A,k1_tarski(B)) = k1_tarski(k1_finseq_4(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t8_finseq_4,t37_zfmisc_1,d13_funct_1,d1_tarski,d3_finseq_4]), [file(finseq_4,t17_finseq_4),interesting(0.67)]). fof(t74_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( ( r1_tarski(k2_relat_1(A),k4_finseq_1(A)) & v2_funct_1(A) ) => k2_relat_1(A) = k4_finseq_1(A) ) ) ), inference(mizar_proof,[status(thm)],[t25_finseq_1,t26_finseq_1,t27_finseq_1,d3_finseq_1,d3_tarski,t94_finseq_3,t97_finseq_3,t72_finseq_3,d3_finseq_1,t33_xboole_1,t12_finseq_1,d1_tarski,d4_xboole_0,t12_finseq_1,d4_xboole_0,t19_finseq_1,t59_finseq_3,d3_finseq_1,t76_funct_1,d3_tarski,d1_tarski,d4_xboole_0,t12_finseq_1,t1_xboole_1,t84_funct_1,t6_finseq_1,d5_funct_1,d5_funct_1,t76_funct_1,t72_funct_1,t3_finseq_1,t31_xreal_1,d8_funct_1,d10_xboole_0,s1_nat_1]), [file(finseq_4,t74_finseq_4),interesting(0.67)]). fof(t21_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( r2_finseq_4(A,B) => r1_finseq_4(A,k1_finseq_4(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_4,d3_finseq_4,d3_finseq_4,t4_finseq_4]), [file(finseq_4,t21_finseq_4),interesting(0.66)]). fof(t30_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => r2_hidden(k5_finseq_4(A,B),k4_finseq_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_1,t142_funct_1,t167_relat_1,d13_finseq_1,t34_finseq_3,d5_funct_1,d13_finseq_1,d13_funct_1]), [file(finseq_4,t30_finseq_4),interesting(0.66)]). fof(t66_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => A = k7_finseq_1(k7_finseq_1(k6_finseq_4(A,B),k9_finseq_1(B)),k7_finseq_4(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[d7_finseq_4,t46_finseq_4,t57_finseq_1,t35_finseq_1,d7_finseq_1,t48_finseq_4,t4_finseq_1,d8_finseq_1,d1_tarski,d7_finseq_1,d8_finseq_1,t29_finseq_4,t46_finseq_4,t38_finseq_1,d7_finseq_4,t46_finseq_4,t57_finseq_1,t35_finseq_1,t43_finseq_3]), [file(finseq_4,t66_finseq_4),interesting(0.66)]). fof(t20_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( r1_finseq_4(A,B) => k1_finseq_4(A,k1_funct_1(A,B)) = B ) ) ), inference(mizar_proof,[status(thm)],[t11_finseq_4,d3_finseq_4]), [file(finseq_4,t20_finseq_4),interesting(0.65)]). fof(t29_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => k1_funct_1(A,k5_finseq_4(A,B)) = B ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_1,t142_funct_1,t167_relat_1,d13_finseq_1,t34_finseq_3,d13_finseq_1,d5_funct_1,d13_funct_1,d1_tarski]), [file(finseq_4,t29_finseq_4),interesting(0.65)]). fof(t5_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( ! [B] : ( r2_hidden(B,k1_relat_1(A)) => r1_finseq_4(A,B) ) <=> v2_funct_1(A) ) ) ), inference(mizar_proof,[status(thm)],[d8_funct_1,t4_finseq_4,d8_funct_1,t4_finseq_4]), [file(finseq_4,t5_finseq_4),interesting(0.65)]). fof(t69_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_finseq_4(A,B) <=> ( r2_hidden(B,k2_relat_1(A)) & k1_finseq_3(A,k1_tarski(B)) = k7_finseq_1(k6_finseq_4(A,B),k7_finseq_4(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_finseq_4,t46_finseq_4,d7_finseq_4,t40_finseq_4,d3_finseq_1,t48_finseq_4,t31_finseq_4,t11_xreal_1,t46_finseq_4,t40_finseq_4,t7_finseq_1,d3_finseq_1,d3_finseq_1,t3_finseq_1,t46_finseq_4,t31_xreal_1,t21_xreal_1,t2_xreal_1,t41_finseq_4,d7_finseq_4,t32_finseq_4,d3_finseq_1,t31_finseq_4,t3_finseq_1,t9_xreal_1,t21_xreal_1,t3_finseq_1,d7_finseq_4,t21_xreal_1,t11_xreal_1,t40_finseq_4,d3_finseq_1,t3_finseq_1,t9_xreal_1,t21_xreal_1,t41_finseq_4,t46_finseq_4,d7_finseq_1,t66_finseq_3,t35_finseq_1,t46_finseq_4,d7_finseq_4,d3_tarski,t29_finseq_4,t30_finseq_4,d1_tarski,d13_funct_1,d2_tarski,t80_card_1,t76_card_2,t37_finseq_4]), [file(finseq_4,t69_finseq_4),interesting(0.65)]). fof(t4_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( r1_finseq_4(A,B) <=> ( r2_hidden(B,k1_relat_1(A)) & ! [C] : ~ ( r2_hidden(C,k1_relat_1(A)) & B != C & k1_funct_1(A,B) = k1_funct_1(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t2_finseq_4,d1_tarski,d13_funct_1,t3_finseq_4,d1_tarski,t3_finseq_4,t2_tarski,d1_tarski,d13_funct_1,d13_funct_1,d1_tarski,d1_tarski,d1_tarski]), [file(finseq_4,t4_finseq_4),interesting(0.64)]). fof(t9_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( r2_finseq_4(A,B) <=> ? [C] : ( r2_hidden(C,k1_relat_1(A)) & B = k1_funct_1(A,C) & ! [D] : ~ ( r2_hidden(D,k1_relat_1(A)) & D != C & k1_funct_1(A,D) = B ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_finseq_4,t7_finseq_4,d5_funct_1,d1_tarski,d13_funct_1,t38_zfmisc_1,t80_card_1,t76_card_2,d3_tarski,d1_tarski,d13_funct_1,d10_xboole_0,d3_tarski,d13_funct_1,d1_tarski,d1_tarski,t79_card_1,d2_finseq_4]), [file(finseq_4,t9_finseq_4),interesting(0.63)]). fof(t33_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => r2_hidden(k5_finseq_4(A,B),k10_relat_1(A,k1_tarski(B))) ) ) ), inference(mizar_proof,[status(thm)],[t29_finseq_4,t30_finseq_4,d1_tarski,d13_funct_1]), [file(finseq_4,t33_finseq_4),interesting(0.63)]). fof(t62_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_finseq_4(A,B) <=> ( r2_hidden(B,k2_relat_1(A)) & r1_xboole_0(k2_relat_1(k7_finseq_4(A,B)),k1_tarski(B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t60_finseq_4,t60_finseq_4,t3_xboole_0,d1_tarski,d1_tarski,t3_xboole_0,t60_finseq_4]), [file(finseq_4,t62_finseq_4),interesting(0.62)]). fof(t78_finseq_4,theorem,( ! [A] : ( v1_finset_1(A) => ! [B] : ( v1_finset_1(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ( ( k4_card_1(A) = k4_card_1(B) & v2_funct_1(C) ) => k2_relat_1(C) = B ) ) ) ) ), inference(mizar_proof,[status(thm)],[t73_finseq_4,t73_finseq_4,t60_card_1,t21_card_1,t146_relat_1,t22_wellord2,d3_finseq_1,t22_wellord2,t81_card_1,t78_finseq_1,d3_finseq_1,t78_finseq_1,t37_zfmisc_1,t80_card_1,t78_card_1,t79_card_1,t10_partfun1,t57_partfun1,t55_funct_1,t12_relset_1,t46_relat_1,d1_funct_2,t46_relat_1,d3_finseq_1,d2_finseq_1,t55_relat_1,t45_relat_1,t55_funct_1,d3_finseq_1,t62_funct_1,t46_funct_1,t46_funct_1,t74_finseq_4,t12_relset_1,t55_relat_1,t55_relat_1,t61_funct_1,t55_relat_1,t79_relat_1,d3_finseq_1,t47_relat_1,d1_funct_2,t47_relat_1]), [file(finseq_4,t78_finseq_4),interesting(0.62)]). fof(t3_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( r1_finseq_4(A,B) <=> ( r2_hidden(B,k1_relat_1(A)) & k10_relat_1(A,k1_tarski(k1_funct_1(A,B))) = k1_tarski(B) ) ) ) ), inference(mizar_proof,[status(thm)],[t2_finseq_4,d1_finseq_4,t117_funct_1,t117_funct_1,d1_finseq_4]), [file(finseq_4,t3_finseq_4),interesting(0.60)]). fof(t40_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_finseq_4(A,B) <=> k3_finseq_1(k1_finseq_3(A,k1_tarski(B))) = k6_xcmplx_0(k3_finseq_1(A),1) ) ) ), inference(mizar_proof,[status(thm)],[t66_finseq_3,t38_finseq_4,t79_card_1,t66_finseq_3,d2_finseq_4]), [file(finseq_4,t40_finseq_4),interesting(0.60)]). fof(t31_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => ( r1_xreal_0(1,k5_finseq_4(A,B)) & r1_xreal_0(k5_finseq_4(A,B),k3_finseq_1(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t30_finseq_4,t27_finseq_3]), [file(finseq_4,t31_finseq_4),interesting(0.60)]). fof(t50_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => r1_xboole_0(k2_relat_1(k6_finseq_4(A,B)),k1_tarski(B)) ) ) ), inference(mizar_proof,[status(thm)],[t49_finseq_4,d1_tarski,t3_xboole_0]), [file(finseq_4,t50_finseq_4),interesting(0.60)]). fof(t25_finseq_4,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => k4_finseq_4(k5_numbers,A,k12_finseq_1(A,B),1) = B ) ) ), inference(mizar_proof,[status(thm)],[t4_finseq_1,d8_finseq_1,d1_tarski,d4_finseq_4]), [file(finseq_4,t25_finseq_4),interesting(0.59)]). fof(t38_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_finseq_4(A,B) <=> ( r2_hidden(B,k2_relat_1(A)) & k1_tarski(k5_finseq_4(A,B)) = k10_relat_1(A,k1_tarski(B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t35_finseq_4,t7_finseq_4,t17_finseq_4,t29_finseq_4,t30_finseq_4,d1_tarski,d13_funct_1,d1_tarski,t9_finseq_4]), [file(finseq_4,t38_finseq_4),interesting(0.59)]). fof(t59_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => r1_tarski(k2_relat_1(k7_finseq_4(A,B)),k2_relat_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d5_funct_1,d7_finseq_4,t58_finseq_4,d5_funct_1]), [file(finseq_4,t59_finseq_4),interesting(0.59)]). fof(t72_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( r2_hidden(B,k2_relat_1(A)) & v2_funct_1(A) ) => r1_xboole_0(k2_relat_1(k6_finseq_4(A,B)),k2_relat_1(k7_finseq_4(A,B))) ) ) ), inference(mizar_proof,[status(thm)],[t66_finseq_4,t42_finseq_1,t98_finseq_3,t63_xboole_1]), [file(finseq_4,t72_finseq_4),interesting(0.59)]). fof(t46_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => k3_finseq_1(k6_finseq_4(A,B)) = k6_xcmplx_0(k5_finseq_4(A,B),1) ) ) ), inference(mizar_proof,[status(thm)],[d6_finseq_4,t31_finseq_4,t37_nat_1,t2_xreal_1,t21_finseq_1]), [file(finseq_4,t46_finseq_4),interesting(0.57)]). fof(t65_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B,C] : ( ~ v1_xboole_0(C) => ( ( r2_hidden(B,k2_relat_1(A)) & m2_finseq_1(A,C) ) => m2_finseq_1(k7_finseq_4(A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d5_funct_1,d3_finseq_1,d7_finseq_4,t31_finseq_4,t37_nat_1,t2_xreal_1,d7_finseq_4,t3_finseq_1,t21_xreal_1,t3_finseq_1,d3_finseq_1,d4_finseq_1,d5_funct_1,d4_finseq_1]), [file(finseq_4,t65_finseq_4),interesting(0.57)]). fof(t18_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v2_funct_1(A) & r2_hidden(B,k2_relat_1(A)) ) => k1_funct_1(k2_funct_1(A),B) = k1_finseq_4(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d5_funct_1,t10_finseq_4,d3_finseq_4,t54_funct_1]), [file(finseq_4,t18_finseq_4),interesting(0.56)]). fof(t70_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( r2_hidden(B,k2_relat_1(A)) & v2_funct_1(A) ) => k1_finseq_3(A,k1_tarski(B)) = k7_finseq_1(k6_finseq_4(A,B),k7_finseq_4(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t10_finseq_4,t69_finseq_4]), [file(finseq_4,t70_finseq_4),interesting(0.56)]). fof(t81_finseq_4,theorem,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ~ ( r2_hidden(k1_card_1(A),k1_card_1(B)) & ! [D] : ~ ( r2_hidden(D,B) & ! [E] : ~ ( r2_hidden(E,A) & k1_funct_1(C,E) = D ) ) ) ) ), inference(mizar_proof,[status(thm)],[t47_card_1,d1_funct_2,t12_relset_1,d10_xboole_0,d3_tarski,d5_funct_1,t28_card_1,t14_card_1]), [file(finseq_4,t81_finseq_4),interesting(0.56)]). fof(t16_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( r2_finseq_4(A,B) => k9_relat_1(A,k1_tarski(k1_finseq_4(A,B))) = k1_tarski(B) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_4,t117_funct_1,d3_finseq_4]), [file(finseq_4,t16_finseq_4),interesting(0.55)]). fof(t51_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => r1_tarski(k2_relat_1(k6_finseq_4(A,B)),k2_relat_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d6_finseq_4,t76_funct_1]), [file(finseq_4,t51_finseq_4),interesting(0.54)]). fof(t63_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( r2_hidden(B,k2_relat_1(A)) & v2_funct_1(A) ) => r1_xboole_0(k2_relat_1(k7_finseq_4(A,B)),k1_tarski(B)) ) ) ), inference(mizar_proof,[status(thm)],[t61_finseq_4,d1_tarski,t3_xboole_0]), [file(finseq_4,t63_finseq_4),interesting(0.54)]). fof(t22_finseq_4,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] : ( m1_subset_1(D,A) => k4_finseq_4(A,B,C,D) = k8_funct_2(A,B,C,D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,d4_finseq_4]), [file(finseq_4,t22_finseq_4),interesting(0.53)]). fof(t36_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_finseq_4(A,B) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ ( r2_hidden(C,k4_finseq_1(A)) & C != k5_finseq_4(A,B) & k1_funct_1(A,C) = B ) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_finseq_4,t29_finseq_4,t35_finseq_4,d3_finseq_4]), [file(finseq_4,t36_finseq_4),interesting(0.52)]). fof(t34_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B,C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ ( r2_hidden(C,k4_finseq_1(A)) & ~ r1_xreal_0(k5_finseq_4(A,B),C) & k1_funct_1(A,C) = B ) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_1,t167_relat_1,d13_finseq_1,d1_tarski,d13_funct_1,d5_funct_1,d3_finseq_1,d5_real_1,t39_nat_1,t26_finseq_3,t3_finseq_1,d13_finseq_1]), [file(finseq_4,t34_finseq_4),interesting(0.52)]). fof(t26_finseq_4,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ( k4_finseq_4(k5_numbers,A,k2_finseq_4(A,B,C),1) = B & k4_finseq_4(k5_numbers,A,k2_finseq_4(A,B,C),2) = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[t4_finseq_1,t61_finseq_1,t29_finseq_3,d2_tarski,d4_finseq_4]), [file(finseq_4,t26_finseq_4),interesting(0.51)]). fof(t53_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B,C] : ( ~ v1_xboole_0(C) => ( ( r2_hidden(B,k2_relat_1(A)) & m2_finseq_1(A,C) ) => m2_finseq_1(k6_finseq_4(A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_finseq_4,t23_finseq_1]), [file(finseq_4,t53_finseq_4),interesting(0.51)]). fof(t58_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B,C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r2_hidden(B,k2_relat_1(A)) & r2_hidden(C,k4_finseq_1(k7_finseq_4(A,B))) ) => r2_hidden(k1_nat_1(C,k5_finseq_4(A,B)),k4_finseq_1(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_finseq_3,t37_nat_1,t2_xreal_1,t32_finseq_4,t57_finseq_4,t3_finseq_1,t21_xreal_1,t27_finseq_3]), [file(finseq_4,t58_finseq_4),interesting(0.51)]). fof(t52_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => ( k5_finseq_4(A,B) = 1 <=> k6_finseq_4(A,B) = k1_xboole_0 ) ) ) ), inference(mizar_proof,[status(thm)],[t46_finseq_4,t25_finseq_1,t46_finseq_4,t25_finseq_1]), [file(finseq_4,t52_finseq_4),interesting(0.50)]). fof(t80_finseq_4,theorem,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,B,A) & m2_relset_1(C,B,A) ) => ~ ( r2_hidden(k1_card_1(A),k1_card_1(B)) & A != k1_xboole_0 & ! [D,E] : ~ ( r2_hidden(D,B) & r2_hidden(E,B) & D != E & k1_funct_1(C,D) = k1_funct_1(C,E) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,d8_funct_1,t60_card_1,t146_relat_1,t21_card_1,t12_relset_1,t27_card_1,t14_card_1]), [file(finseq_4,t80_finseq_4),interesting(0.49)]). fof(t39_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v2_funct_1(A) & r2_hidden(B,k2_relat_1(A)) ) => k1_tarski(k5_finseq_4(A,B)) = k10_relat_1(A,k1_tarski(B)) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d1_tarski,t33_finseq_4,d10_xboole_0,d3_tarski,d13_funct_1,t29_finseq_4,t30_finseq_4,d1_tarski,d8_funct_1,d1_tarski]), [file(finseq_4,t39_finseq_4),interesting(0.48)]). fof(t32_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => ( m2_subset_1(k6_xcmplx_0(k5_finseq_4(A,B),1),k1_numbers,k5_numbers) & m2_subset_1(k6_xcmplx_0(k3_finseq_1(A),k5_finseq_4(A,B)),k1_numbers,k5_numbers) ) ) ) ), inference(mizar_proof,[status(thm)],[t31_finseq_4,t18_int_1]), [file(finseq_4,t32_finseq_4),interesting(0.48)]). fof(t37_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( r2_hidden(B,k2_relat_1(A)) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ ( r2_hidden(C,k4_finseq_1(A)) & C != k5_finseq_4(A,B) & k1_funct_1(A,C) = B ) ) ) => r2_finseq_4(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t29_finseq_4,t30_finseq_4,t9_finseq_4]), [file(finseq_4,t37_finseq_4),interesting(0.48)]). fof(t48_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B,C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r2_hidden(B,k2_relat_1(A)) & r2_hidden(C,k4_finseq_1(k6_finseq_4(A,B))) ) => k1_funct_1(A,C) = k1_funct_1(k6_finseq_4(A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_finseq_4,t70_funct_1]), [file(finseq_4,t48_finseq_4),interesting(0.47)]). fof(t82_finseq_4,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,A) => ! [C] : ( m1_subset_1(C,A) => k4_finseq_4(k5_numbers,A,k8_finseq_1(A,B,k12_finseq_1(A,C)),k1_nat_1(k3_finseq_1(B),1)) = C ) ) ) ), inference(mizar_proof,[status(thm)],[t35_finseq_1,t56_finseq_1,t29_nat_1,t27_finseq_3,d4_finseq_4,t59_finseq_1]), [file(finseq_4,t82_finseq_4),interesting(0.46)]). fof(t64_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => ( k5_finseq_4(A,B) = k3_finseq_1(A) <=> k7_finseq_4(A,B) = k1_xboole_0 ) ) ) ), inference(mizar_proof,[status(thm)],[d7_finseq_4,t25_finseq_1,d7_finseq_4,t25_finseq_1]), [file(finseq_4,t64_finseq_4),interesting(0.44)]). fof(t83_finseq_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_1(C,B) => ! [D] : ( m2_finseq_1(D,B) => ( r2_hidden(A,k4_finseq_1(C)) => k4_finseq_4(k5_numbers,B,k8_finseq_1(B,C,D),A) = k4_finseq_4(k5_numbers,B,C,A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t24_finseq_3,d4_finseq_4,d7_finseq_1,d4_finseq_4]), [file(finseq_4,t83_finseq_4),interesting(0.44)]). fof(t24_finseq_4,theorem,( ! [A,B] : ( m2_finseq_1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r1_xreal_0(1,C) & r1_xreal_0(C,k3_finseq_1(B)) ) => k4_finseq_4(k5_numbers,A,B,C) = k1_funct_1(B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_finseq_3,d4_finseq_4]), [file(finseq_4,t24_finseq_4),interesting(0.42)]). fof(t85_finseq_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v4_ordinal2(B) => ! [C,D] : ( m2_finseq_1(D,C) => ( r2_hidden(B,k4_finseq_1(k16_finseq_1(C,D,A))) => k4_finseq_4(k5_numbers,C,k16_finseq_1(C,D,A),B) = k4_finseq_4(k5_numbers,C,D,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_finseq_1,t90_relat_1,d3_xboole_0,d4_finseq_4,d15_finseq_1,t70_funct_1,d4_finseq_4]), [file(finseq_4,t85_finseq_4),interesting(0.42)]). fof(t47_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B,C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r2_hidden(B,k2_relat_1(A)) & C = k6_xcmplx_0(k5_finseq_4(A,B),1) ) => k4_finseq_1(k6_finseq_4(A,B)) = k2_finseq_1(C) ) ) ) ), inference(mizar_proof,[status(thm)],[t46_finseq_4,d3_finseq_1]), [file(finseq_4,t47_finseq_4),interesting(0.41)]). fof(t86_finseq_4,theorem,( ! [A,B] : ( m2_finseq_1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( ( r2_hidden(C,k4_finseq_1(B)) & r2_hidden(D,k2_finseq_1(C)) ) => ( r2_hidden(D,k4_finseq_1(B)) & k4_finseq_4(k5_numbers,A,k16_finseq_1(A,B,C),D) = k4_finseq_4(k5_numbers,A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_1,d15_finseq_1,t27_finseq_3,t7_finseq_1,t28_xboole_1,t68_funct_1,d4_finseq_4,t68_funct_1,d4_finseq_4]), [file(finseq_4,t86_finseq_4),interesting(0.39)]). fof(t84_finseq_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_1(C,B) => ! [D] : ( m2_finseq_1(D,B) => ( r2_hidden(A,k4_finseq_1(D)) => k4_finseq_4(k5_numbers,B,k8_finseq_1(B,C,D),k1_nat_1(k3_finseq_1(C),A)) = k4_finseq_4(k5_numbers,B,D,A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t41_finseq_1,d4_finseq_4,d7_finseq_1,d4_finseq_4]), [file(finseq_4,t84_finseq_4),interesting(0.37)]). fof(t41_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_finseq_4(A,B) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r2_hidden(C,k4_finseq_1(k1_finseq_3(A,k1_tarski(B)))) => ( ( ~ r1_xreal_0(k5_finseq_4(A,B),C) => k1_funct_1(k1_finseq_3(A,k1_tarski(B)),C) = k1_funct_1(A,C) ) & ( r1_xreal_0(k5_finseq_4(A,B),C) => k1_funct_1(k1_finseq_3(A,k1_tarski(B)),C) = k1_funct_1(A,k1_nat_1(C,1)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_finseq_4,t70_finseq_3,d3_tarski,t36_finseq_4,d1_tarski,d10_xboole_0,t2_xboole_1,t36_finseq_4,d1_tarski,t78_card_1,t92_finseq_3,d3_tarski,d1_tarski,t36_finseq_4,d1_tarski,d10_xboole_0,d3_tarski,d1_tarski,t30_finseq_4,t37_nat_1,t29_finseq_4,d1_tarski,t40_finseq_4,d3_finseq_1,t3_finseq_1,t37_nat_1,t2_xreal_1,t21_xreal_1,t3_finseq_1,d3_finseq_1,t31_xreal_1,t36_finseq_4,d1_tarski,t92_finseq_3,t79_card_1]), [file(finseq_4,t41_finseq_4),interesting(0.28)]). fof(t12_finseq_4,theorem,( $true ), file(finseq_4,t12_finseq_4), [interesting(0.00)]). fof(t13_finseq_4,theorem,( $true ), file(finseq_4,t13_finseq_4), [interesting(0.00)]). fof(t14_finseq_4,theorem,( $true ), file(finseq_4,t14_finseq_4), [interesting(0.00)]). fof(t15_finseq_4,theorem,( $true ), file(finseq_4,t15_finseq_4), [interesting(0.00)]). fof(d3_finseq_4,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( r2_finseq_4(A,B) => ! [C] : ( C = k1_finseq_4(A,B) <=> ( r2_hidden(C,k1_relat_1(A)) & k1_funct_1(A,C) = B ) ) ) ) ), file(finseq_4,d3_finseq_4), [interesting(0.00)]). fof(t117_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r2_hidden(A,k1_relat_1(B)) => k9_relat_1(B,k1_tarski(A)) = k1_tarski(k1_funct_1(B,A)) ) ) ), file(funct_1,t117_funct_1), [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(d8_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v2_funct_1(A) <=> ! [B,C] : ( ( r2_hidden(B,k1_relat_1(A)) & r2_hidden(C,k1_relat_1(A)) & k1_funct_1(A,B) = k1_funct_1(A,C) ) => B = C ) ) ) ), file(funct_1,d8_funct_1), [interesting(0.00)]). fof(d2_finseq_4,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( r2_finseq_4(A,B) <=> ? [C] : ( v1_finset_1(C) & C = k10_relat_1(A,k1_tarski(B)) & k4_card_1(C) = 1 ) ) ) ), file(finseq_4,d2_finseq_4), [interesting(0.00)]). fof(t78_card_1,theorem,( k4_card_1(k1_xboole_0) = 0 ), file(card_1,t78_card_1), [interesting(0.00)]). fof(t173_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( k10_relat_1(B,A) = k1_xboole_0 <=> r1_xboole_0(k2_relat_1(B),A) ) ) ), file(relat_1,t173_relat_1), [interesting(0.00)]). fof(t4_xboole_0,theorem,( ! [A,B] : ( ~ ( ~ r1_xboole_0(A,B) & ! [C] : ~ r2_hidden(C,k3_xboole_0(A,B)) ) & ~ ( ? [C] : r2_hidden(C,k3_xboole_0(A,B)) & r1_xboole_0(A,B) ) ) ), file(xboole_0,t4_xboole_0), [interesting(0.00)]). fof(d3_xboole_0,definition,( ! [A,B,C] : ( C = k3_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & r2_hidden(D,B) ) ) ) ), file(xboole_0,d3_xboole_0), [interesting(0.00)]). fof(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [interesting(0.00)]). fof(d13_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C] : ( C = k10_relat_1(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,k1_relat_1(A)) & r2_hidden(k1_funct_1(A,D),B) ) ) ) ) ), file(funct_1,d13_funct_1), [interesting(0.00)]). fof(t38_zfmisc_1,theorem,( ! [A,B,C] : ( r1_tarski(k2_tarski(A,B),C) <=> ( r2_hidden(A,C) & r2_hidden(B,C) ) ) ), file(zfmisc_1,t38_zfmisc_1), [interesting(0.00)]). fof(t80_card_1,theorem,( ! [A] : ( v1_finset_1(A) => ! [B] : ( v1_finset_1(B) => ( r1_tarski(A,B) => r1_xreal_0(k4_card_1(A),k4_card_1(B)) ) ) ) ), file(card_1,t80_card_1), [interesting(0.00)]). fof(t76_card_2,theorem,( ! [A,B] : ( A != B => k4_card_1(k2_tarski(A,B)) = 2 ) ), file(card_2,t76_card_2), [interesting(0.00)]). fof(d3_tarski,definition,( ! [A,B] : ( r1_tarski(A,B) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(C,B) ) ) ), file(tarski,d3_tarski), [interesting(0.00)]). fof(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(t79_card_1,theorem,( ! [A] : k4_card_1(k1_tarski(A)) = 1 ), file(card_1,t79_card_1), [interesting(0.00)]). fof(t60_card_2,theorem,( ! [A] : ( k1_card_1(A) = 1 <=> ? [B] : A = k1_tarski(B) ) ), file(card_2,t60_card_2), [interesting(0.00)]). fof(t54_funct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v2_funct_1(A) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( B = k2_funct_1(A) <=> ( k1_relat_1(B) = k2_relat_1(A) & ! [C,D] : ( ( ( r2_hidden(C,k2_relat_1(A)) & D = k1_funct_1(B,C) ) => ( r2_hidden(D,k1_relat_1(A)) & C = k1_funct_1(A,D) ) ) & ( ( r2_hidden(D,k1_relat_1(A)) & C = k1_funct_1(A,D) ) => ( r2_hidden(C,k2_relat_1(A)) & D = k1_funct_1(B,C) ) ) ) ) ) ) ) ) ), file(funct_1,t54_funct_1), [interesting(0.00)]). fof(t19_finseq_4,theorem,( $true ), file(finseq_4,t19_finseq_4), [interesting(0.00)]). fof(t1_finseq_4,theorem,( $true ), file(finseq_4,t1_finseq_4), [interesting(0.00)]). fof(d1_finseq_4,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( r1_finseq_4(A,B) <=> k10_relat_1(A,k9_relat_1(A,k1_tarski(B))) = k1_tarski(B) ) ) ), file(finseq_4,d1_finseq_4), [interesting(0.00)]). fof(t2_tarski,theorem,( ! [A,B] : ( ! [C] : ( r2_hidden(C,A) <=> r2_hidden(C,B) ) => A = B ) ), file(tarski,t2_tarski), [interesting(0.00)]). fof(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_4,definition,( ! [A,B,C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,B) ) => ! [D] : ( r2_hidden(D,k1_relat_1(C)) => k4_finseq_4(A,B,C,D) = k1_funct_1(C,D) ) ) ), file(finseq_4,d4_finseq_4), [interesting(0.00)]). fof(t23_finseq_4,theorem,( $true ), file(finseq_4,t23_finseq_4), [interesting(0.00)]). fof(t27_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( v4_ordinal2(B) => ( r2_hidden(B,k4_finseq_1(A)) <=> ( r1_xreal_0(1,B) & r1_xreal_0(B,k3_finseq_1(A)) ) ) ) ) ), file(finseq_3,t27_finseq_3), [interesting(0.00)]). fof(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(d8_finseq_1,definition,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( B = k9_finseq_1(A) <=> ( k1_relat_1(B) = k2_finseq_1(1) & k1_funct_1(B,1) = A ) ) ) ), file(finseq_1,d8_finseq_1), [interesting(0.00)]). fof(t61_finseq_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( C = k10_finseq_1(A,B) <=> ( k3_finseq_1(C) = 2 & k1_funct_1(C,1) = A & k1_funct_1(C,2) = B ) ) ) ), file(finseq_1,t61_finseq_1), [interesting(0.00)]). fof(t29_finseq_3,theorem,( ! [A,B] : k4_finseq_1(k10_finseq_1(A,B)) = k2_finseq_1(2) ), file(finseq_3,t29_finseq_3), [interesting(0.00)]). fof(d2_tarski,definition,( ! [A,B,C] : ( C = k2_tarski(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( D = A | D = B ) ) ) ), file(tarski,d2_tarski), [interesting(0.00)]). fof(d1_enumset1,definition,( ! [A,B,C,D] : ( D = k1_enumset1(A,B,C) <=> ! [E] : ( r2_hidden(E,D) <=> ~ ( E != A & E != B & E != C ) ) ) ), file(enumset1,d1_enumset1), [interesting(0.00)]). fof(t62_finseq_1,theorem,( ! [A,B,C,D] : ( ( v1_relat_1(D) & v1_funct_1(D) & v1_finseq_1(D) ) => ( D = k11_finseq_1(A,B,C) <=> ( k3_finseq_1(D) = 3 & k1_funct_1(D,1) = A & k1_funct_1(D,2) = B & k1_funct_1(D,3) = C ) ) ) ), file(finseq_1,t62_finseq_1), [interesting(0.00)]). fof(t1_finseq_3,theorem,( k2_finseq_1(3) = k1_enumset1(1,2,3) ), file(finseq_3,t1_finseq_3), [interesting(0.00)]). fof(t30_finseq_3,theorem,( ! [A,B,C] : k4_finseq_1(k11_finseq_1(A,B,C)) = k2_finseq_1(3) ), file(finseq_3,t30_finseq_3), [interesting(0.00)]). fof(t27_finseq_4,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => ( k4_finseq_4(k5_numbers,A,k3_finseq_4(A,B,C,D),1) = B & k4_finseq_4(k5_numbers,A,k3_finseq_4(A,B,C,D),2) = C & k4_finseq_4(k5_numbers,A,k3_finseq_4(A,B,C,D),3) = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_enumset1,t62_finseq_1,t1_finseq_3,t30_finseq_3,d4_finseq_4]), [file(finseq_4,t27_finseq_4),interesting(0.00)]). fof(t28_finseq_4,theorem,( $true ), file(finseq_4,t28_finseq_4), [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(t142_funct_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r2_hidden(A,k2_relat_1(B)) <=> k10_relat_1(B,k1_tarski(A)) != k1_xboole_0 ) ) ), file(funct_1,t142_funct_1), [interesting(0.00)]). fof(t167_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => r1_tarski(k10_relat_1(B,A),k1_relat_1(B)) ) ), file(relat_1,t167_relat_1), [interesting(0.00)]). fof(d13_finseq_1,definition,( ! [A] : ( ? [B] : ( v4_ordinal2(B) & r1_tarski(A,k2_finseq_1(B)) ) => ! [B] : ( m2_finseq_1(B,k5_numbers) => ( B = k14_finseq_1(A) <=> ( k2_relat_1(B) = A & ! [C] : ( v4_ordinal2(C) => ! [D] : ( v4_ordinal2(D) => ! [E] : ( v4_ordinal2(E) => ! [F] : ( v4_ordinal2(F) => ~ ( r1_xreal_0(1,C) & ~ r1_xreal_0(D,C) & r1_xreal_0(D,k3_finseq_1(B)) & E = k1_funct_1(B,C) & F = k1_funct_1(B,D) & r1_xreal_0(F,E) ) ) ) ) ) ) ) ) ) ), file(finseq_1,d13_finseq_1), [interesting(0.00)]). fof(t34_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( k2_relat_1(A) != k1_xboole_0 => r2_hidden(1,k4_finseq_1(A)) ) ) ), file(finseq_3,t34_finseq_3), [interesting(0.00)]). fof(t70_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : r1_tarski(k4_finseq_1(k1_finseq_3(A,B)),k4_finseq_1(A)) ) ), file(finseq_3,t70_finseq_3), [interesting(0.00)]). fof(t66_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : k3_finseq_1(k1_finseq_3(A,B)) = k6_xcmplx_0(k3_finseq_1(A),k4_card_1(k10_relat_1(A,B))) ) ), file(finseq_3,t66_finseq_3), [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(t3_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r2_hidden(A,k2_finseq_1(B)) <=> ( r1_xreal_0(1,A) & r1_xreal_0(A,B) ) ) ) ) ), file(finseq_1,t3_finseq_1), [interesting(0.00)]). fof(t37_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v4_ordinal2(C) => ( r1_xreal_0(A,B) => r1_xreal_0(A,k2_xcmplx_0(B,C)) ) ) ) ) ), file(nat_1,t37_nat_1), [interesting(0.00)]). fof(t2_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,C) ) => r1_xreal_0(A,C) ) ) ) ) ), file(xreal_1,t2_xreal_1), [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(t2_xboole_1,theorem,( ! [A] : r1_tarski(k1_xboole_0,A) ), file(xboole_1,t2_xboole_1), [interesting(0.00)]). fof(t92_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B,C] : ( v4_ordinal2(C) => ( r2_hidden(C,k4_finseq_1(A)) => ! [D] : ( v1_finset_1(D) => ~ ( D = a_3_0_finseq_3(A,B,C) & ~ r2_hidden(k1_funct_1(A,C),B) & k1_funct_1(k1_finseq_3(A,B),k6_xcmplx_0(C,k4_card_1(D))) != k1_funct_1(A,C) ) ) ) ) ) ), file(finseq_3,t92_finseq_3), [interesting(0.00)]). fof(t31_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k2_xcmplx_0(B,A),B) ) ) ) ), file(xreal_1,t31_xreal_1), [interesting(0.00)]). fof(t42_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v2_funct_1(A) & r2_hidden(B,k2_relat_1(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r2_hidden(C,k4_finseq_1(k1_finseq_3(A,k1_tarski(B)))) => ( ~ ( k1_funct_1(k1_finseq_3(A,k1_tarski(B)),C) = k1_funct_1(A,C) & r1_xreal_0(k5_finseq_4(A,B),C) ) & ( ~ r1_xreal_0(k5_finseq_4(A,B),C) => k1_funct_1(k1_finseq_3(A,k1_tarski(B)),C) = k1_funct_1(A,C) ) & ( k1_funct_1(k1_finseq_3(A,k1_tarski(B)),C) = k1_funct_1(A,k1_nat_1(C,1)) => r1_xreal_0(k5_finseq_4(A,B),C) ) & ( r1_xreal_0(k5_finseq_4(A,B),C) => k1_funct_1(k1_finseq_3(A,k1_tarski(B)),C) = k1_funct_1(A,k1_nat_1(C,1)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_finseq_4,t70_finseq_3,t40_finseq_4,d3_finseq_1,t3_finseq_1,t37_nat_1,t2_xreal_1,t21_xreal_1,t3_finseq_1,d3_finseq_1,t41_finseq_4,d8_funct_1,t41_finseq_4,t41_finseq_4,d8_funct_1,t41_finseq_4]), [file(finseq_4,t42_finseq_4),interesting(0.00)]). fof(t43_finseq_4,theorem,( $true ), file(finseq_4,t43_finseq_4), [interesting(0.00)]). fof(t44_finseq_4,theorem,( $true ), file(finseq_4,t44_finseq_4), [interesting(0.00)]). fof(t18_int_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( r1_xreal_0(A,B) => r2_hidden(k6_xcmplx_0(B,A),k5_numbers) ) ) ) ), file(int_1,t18_int_1), [interesting(0.00)]). fof(d6_finseq_4,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( C = k6_finseq_4(A,B) <=> ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & D = k6_xcmplx_0(k5_finseq_4(A,B),1) & C = k7_relat_1(A,k2_finseq_1(D)) ) ) ) ) ) ), file(finseq_4,d6_finseq_4), [interesting(0.00)]). fof(t45_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B,C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r2_hidden(B,k2_relat_1(A)) & C = k6_xcmplx_0(k5_finseq_4(A,B),1) ) => k7_relat_1(A,k2_finseq_1(C)) = k6_finseq_4(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_finseq_4]), [file(finseq_4,t45_finseq_4),interesting(0.00)]). fof(t21_finseq_1,theorem,( ! [A] : ( v4_ordinal2(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) ) => ( ( r1_xreal_0(A,k3_finseq_1(B)) & C = k7_relat_1(B,k2_finseq_1(A)) ) => ( k3_finseq_1(C) = A & k4_finseq_1(C) = k2_finseq_1(A) ) ) ) ) ) ), file(finseq_1,t21_finseq_1), [interesting(0.00)]). fof(t76_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r1_tarski(k1_relat_1(k7_relat_1(B,A)),k1_relat_1(B)) & r1_tarski(k2_relat_1(k7_relat_1(B,A)),k2_relat_1(B)) ) ) ), file(funct_1,t76_funct_1), [interesting(0.00)]). fof(d5_real_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) <=> ~ ( r1_xreal_0(B,A) & B != A ) ) ) ) ), file(real_1,d5_real_1), [interesting(0.00)]). fof(t39_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ( ~ r1_xreal_0(1,A) => A = 0 ) ) ), file(nat_1,t39_nat_1), [interesting(0.00)]). fof(t26_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ~ ( r2_hidden(B,k4_finseq_1(A)) & B = 0 ) ) ), file(finseq_3,t26_finseq_3), [interesting(0.00)]). fof(t70_funct_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(B,k1_relat_1(k7_relat_1(C,A))) => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ), file(funct_1,t70_funct_1), [interesting(0.00)]). fof(t3_xboole_0,theorem,( ! [A,B] : ( ~ ( ~ r1_xboole_0(A,B) & ! [C] : ~ ( r2_hidden(C,A) & r2_hidden(C,B) ) ) & ~ ( ? [C] : ( r2_hidden(C,A) & r2_hidden(C,B) ) & r1_xboole_0(A,B) ) ) ), file(xboole_0,t3_xboole_0), [interesting(0.00)]). fof(t25_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( k3_finseq_1(A) = 0 <=> A = k1_xboole_0 ) ) ), file(finseq_1,t25_finseq_1), [interesting(0.00)]). fof(t23_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B,C] : ( m2_finseq_1(C,B) => m2_finseq_1(k7_relat_1(C,k2_finseq_1(A)),B) ) ) ), file(finseq_1,t23_finseq_1), [interesting(0.00)]). fof(t54_finseq_4,theorem,( $true ), file(finseq_4,t54_finseq_4), [interesting(0.00)]). fof(t55_finseq_4,theorem,( $true ), file(finseq_4,t55_finseq_4), [interesting(0.00)]). fof(t56_finseq_4,theorem,( $true ), file(finseq_4,t56_finseq_4), [interesting(0.00)]). fof(d7_finseq_4,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( C = k7_finseq_4(A,B) <=> ( k3_finseq_1(C) = k6_xcmplx_0(k3_finseq_1(A),k5_finseq_4(A,B)) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(C)) => k1_funct_1(C,D) = k1_funct_1(A,k1_nat_1(D,k5_finseq_4(A,B))) ) ) ) ) ) ) ) ), file(finseq_4,d7_finseq_4), [interesting(0.00)]). fof(t57_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B,C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r2_hidden(B,k2_relat_1(A)) & C = k6_xcmplx_0(k3_finseq_1(A),k5_finseq_4(A,B)) ) => k4_finseq_1(k7_finseq_4(A,B)) = k2_finseq_1(C) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_finseq_4,d3_finseq_1]), [file(finseq_4,t57_finseq_4),interesting(0.00)]). fof(t38_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ~ r1_xreal_0(k2_xcmplx_0(B,1),A) <=> r1_xreal_0(A,B) ) ) ) ), file(nat_1,t38_nat_1), [interesting(0.00)]). fof(t28_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ~ ( r1_xreal_0(A,B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => B != k2_xcmplx_0(A,C) ) ) ) ) ), file(nat_1,t28_nat_1), [interesting(0.00)]). fof(t8_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,B) <=> r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t8_xreal_1), [interesting(0.00)]). fof(t1_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,A) ) => A = B ) ) ) ), file(xreal_1,t1_xreal_1), [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(t57_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( B = k9_finseq_1(A) <=> ( k3_finseq_1(B) = 1 & k1_funct_1(B,1) = A ) ) ) ), file(finseq_1,t57_finseq_1), [interesting(0.00)]). fof(t35_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k3_finseq_1(k7_finseq_1(A,B)) = k1_nat_1(k3_finseq_1(A),k3_finseq_1(B)) ) ) ), file(finseq_1,t35_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(t38_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] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ ( r2_hidden(C,k4_finseq_1(k7_finseq_1(A,B))) & ~ r2_hidden(C,k4_finseq_1(A)) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ~ ( r2_hidden(D,k4_finseq_1(B)) & C = k1_nat_1(k3_finseq_1(A),D) ) ) ) ) ) ) ), file(finseq_1,t38_finseq_1), [interesting(0.00)]). fof(t43_finseq_3,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) ) => ( ( k3_finseq_1(A) = k1_nat_1(k3_finseq_1(B),k3_finseq_1(C)) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(B)) => k1_funct_1(A,D) = k1_funct_1(B,D) ) ) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(C)) => k1_funct_1(A,k1_nat_1(k3_finseq_1(B),D)) = k1_funct_1(C,D) ) ) ) => A = k7_finseq_1(B,C) ) ) ) ) ), file(finseq_3,t43_finseq_3), [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(t98_finseq_3,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) ) => ( ( r1_xboole_0(k2_relat_1(A),k2_relat_1(B)) & v2_funct_1(A) & v2_funct_1(B) ) <=> v2_funct_1(k7_finseq_1(A,B)) ) ) ) ), file(finseq_3,t98_finseq_3), [interesting(0.00)]). fof(t6_finseq_4,theorem,( $true ), file(finseq_4,t6_finseq_4), [interesting(0.00)]). fof(t11_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,B) <=> r1_xreal_0(k6_xcmplx_0(A,C),k6_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t11_xreal_1), [interesting(0.00)]). fof(t7_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(A,B) <=> r1_tarski(k2_finseq_1(A),k2_finseq_1(B)) ) ) ) ), file(finseq_1,t7_finseq_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(t42_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) ) => r1_tarski(k2_relat_1(A),k2_relat_1(k7_finseq_1(A,B))) ) ) ), file(finseq_1,t42_finseq_1), [interesting(0.00)]). fof(t63_xboole_1,theorem,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_xboole_0(B,C) ) => r1_xboole_0(A,C) ) ), file(xboole_1,t63_xboole_1), [interesting(0.00)]). fof(t55_funct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v2_funct_1(A) => ( k2_relat_1(A) = k1_relat_1(k2_funct_1(A)) & k1_relat_1(A) = k2_relat_1(k2_funct_1(A)) ) ) ) ), file(funct_1,t55_funct_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(d2_finseq_1,definition,( ! [A] : ( v1_relat_1(A) => ( v1_finseq_1(A) <=> ? [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) & k1_relat_1(A) = k2_finseq_1(B) ) ) ) ), file(finseq_1,d2_finseq_1), [interesting(0.00)]). fof(t47_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ( r1_tarski(k1_relat_1(A),k2_relat_1(B)) => k2_relat_1(k5_relat_1(B,A)) = k2_relat_1(A) ) ) ) ), file(relat_1,t47_relat_1), [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(t72_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : k2_relat_1(k1_finseq_3(A,B)) = k4_xboole_0(k2_relat_1(A),B) ) ), file(finseq_3,t72_finseq_3), [interesting(0.00)]). fof(t12_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => k2_finseq_1(A) = k4_xboole_0(k2_finseq_1(k2_xcmplx_0(A,1)),k1_tarski(k2_xcmplx_0(A,1))) ) ), file(finseq_1,t12_finseq_1), [interesting(0.00)]). fof(t78_finseq_1,theorem, ( ! [A] : ( v4_ordinal2(A) => k4_card_1(k2_finseq_1(A)) = A ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( k4_card_1(A) = A & k4_card_1(k1_card_1(A)) = A ) ) ), file(finseq_1,t78_finseq_1), [interesting(0.00)]). fof(t28_card_1,theorem,( ! [A,B] : ( r1_tarski(k1_card_1(A),k1_card_1(B)) <=> ? [C] : ( v1_relat_1(C) & v1_funct_1(C) & k1_relat_1(C) = B & r1_tarski(A,k2_relat_1(C)) ) ) ), file(card_1,t28_card_1), [interesting(0.00)]). fof(d11_card_1,definition,( ! [A] : ( v1_finset_1(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( B = k4_card_1(A) <=> k1_card_1(B) = k1_card_1(A) ) ) ) ), file(card_1,d11_card_1), [interesting(0.00)]). fof(t72_card_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r1_tarski(k1_card_1(A),k1_card_1(B)) <=> r1_xreal_0(A,B) ) ) ) ), file(card_1,t72_card_1), [interesting(0.00)]). fof(t18_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => r1_xreal_0(0,A) ) ), file(nat_1,t18_nat_1), [interesting(0.00)]). fof(t22_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ~ ( A != 0 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => A != k1_nat_1(B,1) ) ) ) ), file(nat_1,t22_nat_1), [interesting(0.00)]). fof(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(t48_funct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( ( v2_funct_1(k5_relat_1(B,A)) & k2_relat_1(B) = k1_relat_1(A) ) => ( v2_funct_1(B) & v2_funct_1(A) ) ) ) ) ), file(funct_1,t48_funct_1), [interesting(0.00)]). fof(t60_card_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( ( r1_tarski(A,k1_relat_1(B)) & v2_funct_1(B) ) => r2_wellord2(A,k9_relat_1(B,A)) ) ) ), file(card_1,t60_card_1), [interesting(0.00)]). fof(t146_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => k9_relat_1(A,k1_relat_1(A)) = k2_relat_1(A) ) ), file(relat_1,t146_relat_1), [interesting(0.00)]). fof(t81_card_1,theorem,( ! [A] : ( v1_finset_1(A) => ! [B] : ( v1_finset_1(B) => ( r2_wellord2(A,B) => k4_card_1(A) = k4_card_1(B) ) ) ) ), file(card_1,t81_card_1), [interesting(0.00)]). fof(t3_funct_2,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v1_funct_1(A) & v1_funct_2(A,k1_relat_1(A),k2_relat_1(A)) & m2_relset_1(A,k1_relat_1(A),k2_relat_1(A)) ) ) ), file(funct_2,t3_funct_2), [interesting(0.00)]). fof(t27_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( A = k1_xboole_0 <=> k2_relat_1(A) = k1_xboole_0 ) ) ), file(finseq_1,t27_finseq_1), [interesting(0.00)]). fof(t46_zfmisc_1,theorem,( ! [A,B] : ( r2_hidden(A,B) => k2_xboole_0(k1_tarski(A),B) = B ) ), file(zfmisc_1,t46_zfmisc_1), [interesting(0.00)]). fof(t44_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) ) => k2_relat_1(k7_finseq_1(A,B)) = k2_xboole_0(k2_relat_1(A),k2_relat_1(B)) ) ) ), file(finseq_1,t44_finseq_1), [interesting(0.00)]). fof(t55_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( B = k9_finseq_1(A) <=> ( k4_finseq_1(B) = k2_finseq_1(1) & k2_relat_1(B) = k1_tarski(A) ) ) ) ), file(finseq_1,t55_finseq_1), [interesting(0.00)]). fof(s2_finset_1,theorem, ( ( v1_finset_1(f1_s2_finset_1) & p1_s2_finset_1(k1_xboole_0) & ! [A,B] : ( ( r2_hidden(A,f1_s2_finset_1) & r1_tarski(B,f1_s2_finset_1) & p1_s2_finset_1(B) ) => p1_s2_finset_1(k2_xboole_0(B,k1_tarski(A))) ) ) => p1_s2_finset_1(f1_s2_finset_1) ), file(finset_1,s2_finset_1), [interesting(0.00)]). fof(t21_card_1,theorem,( ! [A,B] : ( r2_wellord2(A,B) <=> k1_card_1(A) = k1_card_1(B) ) ), file(card_1,t21_card_1), [interesting(0.00)]). fof(t22_wellord2,theorem,( ! [A,B,C] : ( ( r2_wellord2(A,B) & r2_wellord2(B,C) ) => r2_wellord2(A,C) ) ), file(wellord2,t22_wellord2), [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(t12_relset_1,theorem,( ! [A,B,C] : ( m2_relset_1(C,A,B) => ( r1_tarski(k1_relat_1(C),A) & r1_tarski(k2_relat_1(C),B) ) ) ), file(relset_1,t12_relset_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(t61_funct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v2_funct_1(A) => ( k5_relat_1(A,k2_funct_1(A)) = k6_relat_1(k1_relat_1(A)) & k5_relat_1(k2_funct_1(A),A) = k6_relat_1(k2_relat_1(A)) ) ) ) ), file(funct_1,t61_funct_1), [interesting(0.00)]). fof(t42_funct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( k5_relat_1(k6_relat_1(k1_relat_1(A)),A) = A & k5_relat_1(A,k6_relat_1(k2_relat_1(A))) = A ) ) ), file(funct_1,t42_funct_1), [interesting(0.00)]). fof(t46_funct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( ( v2_funct_1(A) & v2_funct_1(B) ) => v2_funct_1(k5_relat_1(A,B)) ) ) ) ), file(funct_1,t46_funct_1), [interesting(0.00)]). fof(t62_funct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v2_funct_1(A) => v2_funct_1(k2_funct_1(A)) ) ) ), file(funct_1,t62_funct_1), [interesting(0.00)]). fof(t10_partfun1,theorem,( k2_relat_1(k1_xboole_0) = k1_xboole_0 ), file(partfun1,t10_partfun1), [interesting(0.00)]). fof(t57_partfun1,theorem,( ! [A,B] : ( ( v1_funct_1(B) & m2_relset_1(B,k1_xboole_0,A) ) => B = k1_xboole_0 ) ), file(partfun1,t57_partfun1), [interesting(0.00)]). fof(t45_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => r1_tarski(k2_relat_1(k5_relat_1(A,B)),k2_relat_1(B)) ) ) ), file(relat_1,t45_relat_1), [interesting(0.00)]). fof(t26_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( A = k1_xboole_0 <=> k4_finseq_1(A) = k1_xboole_0 ) ) ), file(finseq_1,t26_finseq_1), [interesting(0.00)]). fof(t94_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( v2_funct_1(A) => v2_funct_1(k1_finseq_3(A,B)) ) ) ), file(finseq_3,t94_finseq_3), [interesting(0.00)]). fof(t97_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v2_funct_1(A) & r2_hidden(B,k2_relat_1(A)) ) => k3_finseq_1(k1_finseq_3(A,k1_tarski(B))) = k6_xcmplx_0(k3_finseq_1(A),1) ) ) ), file(finseq_3,t97_finseq_3), [interesting(0.00)]). fof(t33_xboole_1,theorem,( ! [A,B,C] : ( r1_tarski(A,B) => r1_tarski(k4_xboole_0(A,C),k4_xboole_0(B,C)) ) ), file(xboole_1,t33_xboole_1), [interesting(0.00)]). fof(d4_xboole_0,definition,( ! [A,B,C] : ( C = k4_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & ~ r2_hidden(D,B) ) ) ) ), file(xboole_0,d4_xboole_0), [interesting(0.00)]). fof(t19_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( v1_relat_1(k7_relat_1(B,k2_finseq_1(A))) & v1_funct_1(k7_relat_1(B,k2_finseq_1(A))) & v1_finseq_1(k7_relat_1(B,k2_finseq_1(A))) ) ) ) ), file(finseq_1,t19_finseq_1), [interesting(0.00)]). fof(t59_finseq_3,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] : ( v4_ordinal2(C) => ! [D] : ( v4_ordinal2(D) => ( ( k3_finseq_1(A) = k2_xcmplx_0(C,D) & B = k7_relat_1(A,k2_finseq_1(C)) ) => k3_finseq_1(B) = C ) ) ) ) ) ), file(finseq_3,t59_finseq_3), [interesting(0.00)]). fof(t1_xboole_1,theorem,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_tarski(B,C) ) => r1_tarski(A,C) ) ), file(xboole_1,t1_xboole_1), [interesting(0.00)]). fof(t84_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( v2_funct_1(B) => v2_funct_1(k7_relat_1(B,A)) ) ) ), file(funct_1,t84_funct_1), [interesting(0.00)]). fof(t72_funct_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(B,A) => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ), file(funct_1,t72_funct_1), [interesting(0.00)]). fof(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(t27_card_1,theorem,( ! [A,B] : ( r1_tarski(A,B) => r1_tarski(k1_card_1(A),k1_card_1(B)) ) ), file(card_1,t27_card_1), [interesting(0.00)]). fof(t14_card_1,theorem,( ! [A] : ( v1_card_1(A) => ! [B] : ( v1_card_1(B) => ( r2_hidden(A,B) <=> ~ r1_tarski(B,A) ) ) ) ), file(card_1,t14_card_1), [interesting(0.00)]). fof(t47_card_1,theorem,( k1_card_1(k1_xboole_0) = k1_xboole_0 ), file(card_1,t47_card_1), [interesting(0.00)]). fof(t56_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( B = k9_finseq_1(A) <=> ( k3_finseq_1(B) = 1 & k2_relat_1(B) = k1_tarski(A) ) ) ) ), file(finseq_1,t56_finseq_1), [interesting(0.00)]). fof(t29_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => r1_xreal_0(A,k2_xcmplx_0(A,B)) ) ) ), file(nat_1,t29_nat_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(t24_finseq_3,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] : ( r2_hidden(C,k4_finseq_1(A)) => r2_hidden(C,k4_finseq_1(k7_finseq_1(A,B))) ) ) ) ), file(finseq_3,t24_finseq_3), [interesting(0.00)]). fof(t41_finseq_1,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) ) => ( r2_hidden(A,k4_finseq_1(B)) => r2_hidden(k1_nat_1(k3_finseq_1(C),A),k4_finseq_1(k7_finseq_1(C,B))) ) ) ) ) ), file(finseq_1,t41_finseq_1), [interesting(0.00)]). fof(d15_finseq_1,definition,( ! [A,B] : ( m2_finseq_1(B,A) => ! [C] : ( v4_ordinal2(C) => k16_finseq_1(A,B,C) = k7_relat_1(B,k2_finseq_1(C)) ) ) ), file(finseq_1,d15_finseq_1), [interesting(0.00)]). fof(t90_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => k1_relat_1(k7_relat_1(B,A)) = k3_xboole_0(k1_relat_1(B),A) ) ), file(relat_1,t90_relat_1), [interesting(0.00)]). fof(t28_xboole_1,theorem,( ! [A,B] : ( r1_tarski(A,B) => k3_xboole_0(A,B) = A ) ), file(xboole_1,t28_xboole_1), [interesting(0.00)]). fof(t68_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( B = k7_relat_1(C,A) <=> ( k1_relat_1(B) = k3_xboole_0(k1_relat_1(C),A) & ! [D] : ( r2_hidden(D,k1_relat_1(B)) => k1_funct_1(B,D) = k1_funct_1(C,D) ) ) ) ) ) ), file(funct_1,t68_funct_1), [interesting(0.00)]).