fof(t6_asympt_1,theorem,
    ( r2_hidden(k3_asympt_1(k6_real_1(1,2)),k6_asympt_0(k2_asympt_1))
    & ~ r2_hidden(k2_asympt_1,k6_asympt_0(k3_asympt_1(k6_real_1(1,2)))) ),
    inference(mizar_proof,[status(thm)],[t4_asympt_1,t5_asympt_1,t19_asympt_0]),
    [file(asympt_1,t6_asympt_1),interesting(1.00)]).

fof(l76_asympt_1,theorem,(
    ? [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
      & ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ~ ( r1_xreal_0(A,B)
              & r1_xreal_0(k5_real_1(B,k4_real_1(k9_square_1(B),k6_power(2,B))),k6_real_1(B,2)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l23_asympt_1,d7_seq_2,t46_square_1,t2_xreal_1,l10_asympt_1,d2_asympt_1,d3_asympt_1,l75_asympt_1,t93_square_1,d1_absvalue,t93_square_1,t70_xreal_1,t88_xcmplx_1,t70_xreal_1,d4_square_1,t8_xreal_1,t22_xreal_1]),
    [file(asympt_1,l76_asympt_1),interesting(0.98)]).

fof(t5_asympt_1,theorem,
    ( r1_tarski(k5_asympt_0(k2_asympt_1),k5_asympt_0(k3_asympt_1(k6_real_1(1,2))))
    & k5_asympt_0(k2_asympt_1) != k5_asympt_0(k3_asympt_1(k6_real_1(1,2))) ),
    inference(mizar_proof,[status(thm)],[l23_asympt_1,t16_asympt_0,t19_asympt_0,t4_asympt_1]),
    [file(asympt_1,t5_asympt_1),interesting(0.98)]).

fof(l68_asympt_1,theorem,(
    ? [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
      & ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ~ ( r1_xreal_0(A,B)
              & r1_xreal_0(k5_real_1(k9_square_1(B),k6_power(2,B)),1) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_xreal_1,t73_real_1,l66_asympt_1,t39_power,t65_power,t63_power,t60_power,t63_power,t178_real_2,t39_power,t39_power,t44_power,t2_xreal_1,t65_power,t63_power,t60_power,t70_xreal_1,t70_xreal_1,l67_asympt_1,t65_power,t63_power,t60_power,t53_power,t63_power,t63_power,t53_power,t44_power,t2_xreal_1,t30_power,t70_xreal_1,t70_xreal_1,t2_xreal_1,t65_power,t53_power,t63_power,t60_power,t44_power,d3_power,t63_power,t53_power,t74_square_1,d3_power,t53_power,t63_power,t44_power,t2_xreal_1,t29_power,t65_power,t59_power,t70_xreal_1,t70_xreal_1,t2_xreal_1,t178_real_2,t46_square_1,t46_square_1,t46_square_1,t2_xreal_1,t2_xreal_1,t10_xreal_1,t10_xreal_1,t12_pre_ff,t60_power,t9_xreal_1,t72_square_1,t95_square_1,t89_square_1,t22_xreal_1]),
    [file(asympt_1,l68_asympt_1),interesting(0.97)]).

fof(l23_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ( ~ r1_xreal_0(A,0)
       => ( v4_seq_2(k19_seq_1(k2_asympt_1,k3_asympt_1(A)))
          & k2_seq_2(k19_seq_1(k2_asympt_1,k3_asympt_1(A))) = 0 ) ) ) ),
    inference(mizar_proof,[status(thm)],[t60_xcmplx_1,t100_xcmplx_1,s3_funct_2,l22_asympt_1,l10_asympt_1,l10_asympt_1,d2_asympt_1,t39_power,d2_asympt_1,t30_power,t38_power,t63_power,d9_xcmplx_0,d9_xcmplx_0,t13_seq_1,t13_seq_1,t22_seq_2,t21_seq_2]),
    [file(asympt_1,l23_asympt_1),interesting(0.96)]).

fof(t90_asympt_1,theorem,(
    ? [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
      & ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ~ ( r1_xreal_0(A,B)
              & r1_xreal_0(k5_real_1(B,k4_real_1(k9_square_1(B),k6_power(2,B))),k6_real_1(B,2)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l76_asympt_1]),
    [file(asympt_1,t90_asympt_1),interesting(0.95)]).

fof(l21_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ~ ( ~ r1_xreal_0(A,6)
          & r1_xreal_0(k4_power(2,A),k7_square_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[t59_int_1,t16_int_1,l20_asympt_1,t10_xreal_1,t78_square_1,t2_xreal_1,t66_int_1,d5_int_1,t16_int_1,t2_xreal_1,t11_xreal_1,t16_int_1,t20_int_1,l20_asympt_1,d5_int_1,t77_square_1,t2_xreal_1,d4_int_1,t10_pre_ff,t2_xreal_1]),
    [file(asympt_1,l21_asympt_1),interesting(0.94)]).

fof(t75_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ( ~ r1_xreal_0(A,0)
       => ( v4_seq_2(k19_seq_1(k2_asympt_1,k3_asympt_1(A)))
          & k2_seq_2(k19_seq_1(k2_asympt_1,k3_asympt_1(A))) = 0 ) ) ) ),
    inference(mizar_proof,[status(thm)],[l23_asympt_1]),
    [file(asympt_1,t75_asympt_1),interesting(0.94)]).

fof(t55_asympt_1,theorem,(
    ? [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
      & ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ~ ( r1_xreal_0(A,B)
              & r1_xreal_0(k5_real_1(k9_square_1(B),k6_power(2,B)),1) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l68_asympt_1]),
    [file(asympt_1,t55_asympt_1),interesting(0.93)]).

fof(t36_asympt_1,theorem,(
    ! [A] : 
      ( ( v2_xreal_0(A)
        & m1_subset_1(A,k1_numbers) )
     => ! [B] : 
          ( ( v2_xreal_0(B)
            & m1_subset_1(B,k1_numbers) )
         => v6_asympt_0(k8_asympt_1(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_asympt_1,l96_asympt_1,t54_int_1,l96_asympt_1,d7_asympt_1,l96_asympt_1,t70_xreal_1,t10_xreal_1,t10_xreal_1,t70_xreal_1,d9_xcmplx_0,d5_int_1,d5_int_1,t16_int_1,d5_int_1,t16_int_1,t101_newton,d8_int_1,d9_int_1,t9_wsierp_1,t22_wsierp_1,d5_int_1,d5_int_1,t20_int_1,t10_xreal_1,t70_xreal_1,d9_xcmplx_0,d9_xcmplx_0,t2_xreal_1,t20_int_1,t21_xreal_1,t10_xreal_1,t70_xreal_1,d9_xcmplx_0,d9_xcmplx_0,t2_xreal_1,d5_real_1,t54_int_1,t38_nat_1,t8_xreal_1,l95_asympt_1,t101_newton,d5_int_1,t22_wsierp_1,d8_int_1,d9_int_1,t9_wsierp_1,t20_int_1,t10_xreal_1,t70_xreal_1,d9_xcmplx_0,d9_xcmplx_0,t2_xreal_1,t20_int_1,t21_xreal_1,t10_xreal_1,t70_xreal_1,d9_xcmplx_0,d9_xcmplx_0,t2_xreal_1,d5_real_1,t54_int_1,t62_nat_1,t66_xreal_1,t70_xreal_1,t8_xreal_1,l96_asympt_1,d7_asympt_1,d7_asympt_1,t2_xreal_1,l96_asympt_1,d7_asympt_1,d7_asympt_1,t10_xreal_1,s1_int_2,s2_int_2,d8_asympt_0]),
    [file(asympt_1,t36_asympt_1),interesting(0.90)]).

fof(t73_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ~ ( ~ r1_xreal_0(A,6)
          & r1_xreal_0(k4_power(2,A),k7_square_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[l21_asympt_1]),
    [file(asympt_1,t73_asympt_1),interesting(0.90)]).

fof(l66_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(30,A)
          & r1_xreal_0(k3_series_1(2,A),k3_series_1(A,6)) ) ) ),
    inference(mizar_proof,[status(thm)],[l17_asympt_1,t38_power,t42_power,t32_power,t30_power,t70_xreal_1,t2_xreal_1,l65_asympt_1,t2_xreal_1,s1_int_2]),
    [file(asympt_1,l66_asympt_1),interesting(0.88)]).

fof(l67_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ~ ( ~ r1_xreal_0(A,9)
          & r1_xreal_0(k4_power(2,A),k7_square_1(k4_real_1(2,A))) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_int_1,t16_int_1,d4_int_1,t10_pre_ff,t59_int_1,t59_int_1,t66_int_1,t22_xreal_1,t22_xreal_1,t10_pre_ff,t2_xreal_1,t2_xreal_1,t38_nat_1,l64_asympt_1,t2_xreal_1,t66_xreal_1,t66_xreal_1,l45_asympt_1,t2_xreal_1]),
    [file(asympt_1,l67_asympt_1),interesting(0.84)]).

fof(l111_asympt_1,theorem,(
    v4_asympt_0(k10_seq_1(k3_asympt_1(1),k4_asympt_1(1))) ),
    inference(mizar_proof,[status(thm)],[d6_asympt_0,t2_xreal_1,d3_asympt_1,t30_power,t13_funcop_1,t15_seq_1,t11_seq_1,t14_seq_1,t22_xreal_1]),
    [file(asympt_1,l111_asympt_1),interesting(0.84)]).

fof(t53_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(30,A)
          & r1_xreal_0(k3_series_1(2,A),k3_series_1(A,6)) ) ) ),
    inference(mizar_proof,[status(thm)],[l66_asympt_1]),
    [file(asympt_1,t53_asympt_1),interesting(0.83)]).

fof(l17_asympt_1,theorem,(
    k3_series_1(2,5) = 32 ),
    inference(mizar_proof,[status(thm)],[t32_power,l14_asympt_1,l15_asympt_1]),
    [file(asympt_1,l17_asympt_1),interesting(0.81)]).

fof(l18_asympt_1,theorem,(
    k3_series_1(2,6) = 64 ),
    inference(mizar_proof,[status(thm)],[t32_power,l15_asympt_1]),
    [file(asympt_1,l18_asympt_1),interesting(0.80)]).

fof(l16_asympt_1,theorem,(
    k3_series_1(2,4) = 16 ),
    inference(mizar_proof,[status(thm)],[t32_power,l14_asympt_1]),
    [file(asympt_1,l16_asympt_1),interesting(0.79)]).

fof(t25_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ~ ( ~ r1_xreal_0(A,0)
          & ~ r1_xreal_0(1,A)
          & ! [B] : 
              ( ( v1_funct_1(B)
                & v1_funct_2(B,k5_numbers,k1_numbers)
                & v4_asympt_0(B)
                & m2_relset_1(B,k5_numbers,k1_numbers) )
             => ~ ( B = k1_asympt_1(k3_real_1(1,A),1,0)
                  & r1_tarski(k5_asympt_0(k3_asympt_1(8)),k5_asympt_0(B))
                  & k5_asympt_0(k3_asympt_1(8)) != k5_asympt_0(B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_xreal_1,l41_asympt_1,l56_asympt_1,d1_xreal_0,t46_square_1,t46_square_1,t2_xreal_1,t49_square_1,t49_square_1,t16_int_1,t124_xreal_1,t217_xcmplx_1,d5_int_1,t2_xreal_1,t39_power,t2_xreal_1,l10_asympt_1,d1_asympt_1,d3_asympt_1,l6_asympt_1,l6_asympt_1,t34_power,t2_xreal_1,l13_asympt_1,t38_power,t30_power,t152_real_2,t217_xcmplx_1,t218_xcmplx_1,l6_asympt_1,t33_power,t44_power,t39_power,t151_real_2,t33_power,t33_power,t2_xreal_1,t39_power,d1_absvalue,d6_seq_2,d7_seq_2,t16_asympt_0,t19_asympt_0,t4_asympt_1]),
    [file(asympt_1,t25_asympt_1),interesting(0.79)]).

fof(l65_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(9,A)
          & r1_xreal_0(k2_nat_1(2,k3_series_1(A,6)),k3_series_1(k1_nat_1(A,1),6)) ) ) ),
    inference(mizar_proof,[status(thm)],[t32_power,t30_power,t30_power,t32_power,t32_power,t30_power,t32_power,t30_power,t30_power,t32_power,t30_power,t32_power,t4_xcmplx_1,t30_power,t32_power,t39_power,t39_power,t124_xreal_1,t70_xreal_1,d9_xcmplx_0,t66_xreal_1,t88_xcmplx_1,t66_xreal_1,t88_xcmplx_1,t21_xreal_1,t14_xcmplx_1,t42_power,t178_real_2,t36_power,t2_xreal_1,t36_power,t70_xreal_1,t88_xcmplx_1,s1_int_2]),
    [file(asympt_1,l65_asympt_1),interesting(0.79)]).

fof(l75_asympt_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( r1_xreal_0(0,A)
       => k8_square_1(A) = k3_power(A,k6_real_1(1,2)) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_power,t82_square_1,t53_power,t38_power,t30_power,t39_power,t89_square_1]),
    [file(asympt_1,l75_asympt_1),interesting(0.79)]).

fof(l73_asympt_1,theorem,(
    k3_series_1(4,4) = 256 ),
    inference(mizar_proof,[status(thm)],[t32_power,t30_power,t32_power,t30_power,t32_power,t30_power,t30_power]),
    [file(asympt_1,l73_asympt_1),interesting(0.79)]).

fof(l72_asympt_1,theorem,(
    k3_series_1(5,5) = 3125 ),
    inference(mizar_proof,[status(thm)],[t32_power,t30_power,t32_power,t30_power,t32_power,t30_power,t32_power,t30_power,t30_power]),
    [file(asympt_1,l72_asympt_1),interesting(0.79)]).

fof(l31_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => r1_xreal_0(k2_int_1(k6_real_1(A,2)),A) ) ),
    inference(mizar_proof,[status(thm)],[t54_int_1,t38_nat_1,t20_int_1,d5_int_1,t2_xreal_1,t38_nat_1,d5_int_1,t70_xreal_1,t21_xreal_1,t2_xreal_1,d5_real_1]),
    [file(asympt_1,l31_asympt_1),interesting(0.78)]).

fof(t54_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ~ ( ~ r1_xreal_0(A,9)
          & r1_xreal_0(k4_power(2,A),k7_square_1(k4_real_1(2,A))) ) ) ),
    inference(mizar_proof,[status(thm)],[l67_asympt_1]),
    [file(asympt_1,t54_asympt_1),interesting(0.78)]).

fof(t66_asympt_1,theorem,(
    v4_asympt_0(k10_seq_1(k3_asympt_1(1),k4_asympt_1(1))) ),
    inference(mizar_proof,[status(thm)],[l111_asympt_1]),
    [file(asympt_1,t66_asympt_1),interesting(0.78)]).

fof(t12_asympt_1,theorem,(
    ~ r2_hidden(k3_asympt_1(2),k6_asympt_0(k3_asympt_1(3))) ),
    inference(mizar_proof,[status(thm)],[t10_xreal_1,t46_square_1,t124_xreal_1,t70_xreal_1,d5_int_1,d9_xcmplx_0,t49_square_1,t16_int_1,d3_asympt_1,t32_power,t30_power,d3_asympt_1,t32_power,t29_power,t66_xreal_1,t66_xreal_1,t2_xreal_1,t88_xcmplx_1,t2_xreal_1,t39_power,t66_xreal_1,t46_square_1]),
    [file(asympt_1,t12_asympt_1),interesting(0.77)]).

fof(l14_asympt_1,theorem,(
    k3_series_1(2,2) = 4 ),
    inference(mizar_proof,[status(thm)],[t53_power]),
    [file(asympt_1,l14_asympt_1),interesting(0.77)]).

fof(l15_asympt_1,theorem,(
    k3_series_1(2,3) = 8 ),
    inference(mizar_proof,[status(thm)],[t32_power,l14_asympt_1,t30_power]),
    [file(asympt_1,l15_asympt_1),interesting(0.77)]).

fof(l20_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(6,A)
          & r1_xreal_0(k3_series_1(2,A),k7_square_1(k1_nat_1(A,1))) ) ) ),
    inference(mizar_proof,[status(thm)],[l18_asympt_1,t2_xreal_1,l19_asympt_1,t8_xreal_1,t8_xreal_1,t2_xreal_1,t30_power,t32_power,s1_int_2]),
    [file(asympt_1,l20_asympt_1),interesting(0.77)]).

fof(l101_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(2,A)
          & r2_hidden(k5_real_1(k3_series_1(2,A),1),k9_asympt_1) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_pre_ff,t8_xreal_1,t21_xreal_1,t11_xreal_1,t16_int_1,l100_asympt_1,t22_xreal_1,t22_xreal_1,t44_power,t20_int_1,t21_xreal_1,t1_xreal_1]),
    [file(asympt_1,l101_asympt_1),interesting(0.77)]).

fof(l109_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(3,A)
          & r1_xreal_0(k11_newton(A),A) ) ) ),
    inference(mizar_proof,[status(thm)],[t11_xreal_1,t16_int_1,l106_asympt_1,t20_newton,t2_xreal_1,t70_xreal_1,t21_newton]),
    [file(asympt_1,l109_asympt_1),interesting(0.77)]).

fof(t65_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(3,A)
          & r1_xreal_0(k11_newton(A),A) ) ) ),
    inference(mizar_proof,[status(thm)],[l109_asympt_1]),
    [file(asympt_1,t65_asympt_1),interesting(0.76)]).

fof(l64_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(10,A)
          & r1_xreal_0(k4_power(2,k5_real_1(A,1)),k7_square_1(k2_nat_1(2,A))) ) ) ),
    inference(mizar_proof,[status(thm)],[l18_asympt_1,t32_power,t32_power,t30_power,t32_power,t30_power,t30_power,t32_power,t30_power,t70_xreal_1,t22_xreal_1,t66_xreal_1,t2_xreal_1,l63_asympt_1,t2_xreal_1,s1_int_2]),
    [file(asympt_1,l64_asympt_1),interesting(0.75)]).

fof(l62_asympt_1,theorem,(
    k3_series_1(2,12) = 4096 ),
    inference(mizar_proof,[status(thm)],[l18_asympt_1,t32_power]),
    [file(asympt_1,l62_asympt_1),interesting(0.75)]).

fof(t31_asympt_1,theorem,
    ( r1_tarski(k5_asympt_0(k5_asympt_1(0)),k5_asympt_0(k5_asympt_1(1)))
    & k5_asympt_0(k5_asympt_1(0)) != k5_asympt_0(k5_asympt_1(1)) ),
    inference(mizar_proof,[status(thm)],[t23_newton,l10_asympt_1,d5_asympt_1,d5_asympt_1,t21_newton,t77_xcmplx_1,t60_xcmplx_1,t124_xreal_1,t217_xcmplx_1,t46_square_1,t49_square_1,t16_int_1,t38_nat_1,t26_xreal_1,t124_xreal_1,t217_xcmplx_1,d5_int_1,t2_xreal_1,t2_xreal_1,t151_real_2,t56_xcmplx_1,d1_absvalue,d1_absvalue,t71_xreal_1,d6_seq_2,d7_seq_2,t16_asympt_0,t19_asympt_0,t4_asympt_1]),
    [file(asympt_1,t31_asympt_1),interesting(0.75)]).

fof(l89_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ( r1_xreal_0(4,A)
       => r1_xreal_0(k2_nat_1(2,A),k4_real_1(A,k6_power(2,A))) ) ) ),
    inference(mizar_proof,[status(thm)],[t12_pre_ff,t53_power,t63_power,t60_power,t66_xreal_1]),
    [file(asympt_1,l89_asympt_1),interesting(0.75)]).

fof(t81_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => r1_xreal_0(k2_int_1(k6_real_1(A,2)),A) ) ),
    inference(mizar_proof,[status(thm)],[l31_asympt_1]),
    [file(asympt_1,t81_asympt_1),interesting(0.75)]).

fof(t14_asympt_1,theorem,(
    ~ r2_hidden(k5_asympt_1(0),k7_asympt_0(k5_asympt_1(1))) ),
    inference(mizar_proof,[status(thm)],[t27_asympt_0,t46_square_1,t49_square_1,t16_int_1,t23_newton,d5_asympt_1,t21_newton,d7_xcmplx_0,d5_int_1,t8_xreal_1,t66_xreal_1,t8_xreal_1,t66_xreal_1,t2_xreal_1,t88_xcmplx_1,t8_xreal_1,t10_xreal_1,t2_xreal_1,d5_asympt_1,d7_xcmplx_0,t66_xreal_1,t46_square_1]),
    [file(asympt_1,t14_asympt_1),interesting(0.74)]).

fof(l54_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ( r1_xreal_0(1,A)
       => r1_xreal_0(k3_real_1(k5_real_1(k7_square_1(A),A),1),k7_square_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_xreal_1,t21_xreal_1]),
    [file(asympt_1,l54_asympt_1),interesting(0.74)]).

fof(t47_asympt_1,theorem,(
    k3_series_1(2,5) = 32 ),
    inference(mizar_proof,[status(thm)],[l17_asympt_1]),
    [file(asympt_1,t47_asympt_1),interesting(0.74)]).

fof(t49_asympt_1,theorem,(
    k3_series_1(2,12) = 4096 ),
    inference(mizar_proof,[status(thm)],[l62_asympt_1]),
    [file(asympt_1,t49_asympt_1),interesting(0.74)]).

fof(l36_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k1_numbers)
             => ( ( r1_xreal_0(A,B)
                  & r1_xreal_0(1,C) )
               => ( r1_xreal_0(A,1)
                  | r1_xreal_0(k6_power(B,C),k6_power(A,C)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_xreal_1,t12_pre_ff,t59_power,t12_pre_ff,t60_power,t66_xreal_1,t64_power]),
    [file(asympt_1,l36_asympt_1),interesting(0.73)]).

fof(l13_asympt_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(0,C) )
               => ( r1_xreal_0(A,0)
                  | r1_xreal_0(k3_power(A,C),k3_power(B,C)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t29_power,t42_power,d5_real_1]),
    [file(asympt_1,l13_asympt_1),interesting(0.73)]).

fof(l19_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(4,A)
          & r1_xreal_0(k3_series_1(2,A),k1_nat_1(k2_nat_1(2,A),3)) ) ) ),
    inference(mizar_proof,[status(thm)],[l16_asympt_1,t8_xreal_1,t2_xreal_1,t44_power,t30_power,t8_xreal_1,t2_xreal_1,t30_power,t32_power,s1_int_2]),
    [file(asympt_1,l19_asympt_1),interesting(0.73)]).

fof(l63_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(3,A)
          & r1_xreal_0(k7_square_1(A),k1_nat_1(k2_nat_1(2,A),1)) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_xreal_1,t2_xreal_1,t10_xreal_1,t8_xreal_1,t2_xreal_1,s1_int_2]),
    [file(asympt_1,l63_asympt_1),interesting(0.73)]).

fof(l69_asympt_1,theorem,(
    k11_newton(k1_nat_1(4,1)) = 120 ),
    inference(mizar_proof,[status(thm)],[t21_newton,t21_newton,t21_newton,t20_newton]),
    [file(asympt_1,l69_asympt_1),interesting(0.73)]).

fof(t30_asympt_1,theorem,(
    ? [A] : 
      ( v1_funct_1(A)
      & v1_funct_2(A,k5_numbers,k1_numbers)
      & v4_asympt_0(A)
      & m2_relset_1(A,k5_numbers,k1_numbers)
      & A = k1_asympt_1(2,2,0)
      & r1_tarski(k5_asympt_0(A),k5_asympt_0(k5_asympt_1(0)))
      & k5_asympt_0(A) != k5_asympt_0(k5_asympt_1(0)) ) ),
    inference(mizar_proof,[status(thm)],[t124_xreal_1,t217_xcmplx_1,t46_square_1,t49_square_1,t16_int_1,t2_xreal_1,l10_asympt_1,d1_asympt_1,d5_asympt_1,l70_asympt_1,d5_int_1,t2_xreal_1,t21_xreal_1,t10_pre_ff,d3_power,t152_real_2,t56_xcmplx_1,t2_xreal_1,d1_absvalue,d6_seq_2,d7_seq_2,t16_asympt_0,t19_asympt_0,t4_asympt_1]),
    [file(asympt_1,t30_asympt_1),interesting(0.73)]).

fof(t48_asympt_1,theorem,(
    k3_series_1(2,6) = 64 ),
    inference(mizar_proof,[status(thm)],[l18_asympt_1]),
    [file(asympt_1,t48_asympt_1),interesting(0.73)]).

fof(t99_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(2,A)
          & r2_hidden(k5_real_1(k3_series_1(2,A),1),k9_asympt_1) ) ) ),
    inference(mizar_proof,[status(thm)],[l101_asympt_1]),
    [file(asympt_1,t99_asympt_1),interesting(0.73)]).

fof(l52_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ r1_xreal_0(k3_real_1(k5_real_1(k7_square_1(A),A),1),0) ) ),
    inference(mizar_proof,[status(thm)],[t10_xreal_1,s1_nat_1]),
    [file(asympt_1,l52_asympt_1),interesting(0.72)]).

fof(l95_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(2,A)
          & r1_xreal_0(A,k2_int_1(k6_real_1(A,2))) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_int_1,t70_xreal_1,t21_xreal_1,t2_xreal_1]),
    [file(asympt_1,l95_asympt_1),interesting(0.72)]).

fof(l106_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( r1_xreal_0(B,A)
           => r1_xreal_0(k11_newton(B),k11_newton(A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_xreal_1,t8_xreal_1,t66_xreal_1,t21_newton,t2_xreal_1,t26_nat_1,s1_nat_1]),
    [file(asympt_1,l106_asympt_1),interesting(0.72)]).

fof(t45_asympt_1,theorem,(
    k3_series_1(2,3) = 8 ),
    inference(mizar_proof,[status(thm)],[l15_asympt_1]),
    [file(asympt_1,t45_asympt_1),interesting(0.72)]).

fof(t52_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(9,A)
          & r1_xreal_0(k2_nat_1(2,k3_series_1(A,6)),k3_series_1(k1_nat_1(A,1),6)) ) ) ),
    inference(mizar_proof,[status(thm)],[l65_asympt_1]),
    [file(asympt_1,t52_asympt_1),interesting(0.72)]).

fof(l105_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(2,A)
          & r1_xreal_0(k11_newton(A),1) ) ) ),
    inference(mizar_proof,[status(thm)],[t20_newton,t70_xreal_1,t8_xreal_1,t2_xreal_1,t21_newton,s1_int_2]),
    [file(asympt_1,l105_asympt_1),interesting(0.72)]).

fof(t101_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k1_numbers)
             => ( ( r1_xreal_0(A,B)
                  & r1_xreal_0(1,C) )
               => ( r1_xreal_0(A,1)
                  | r1_xreal_0(k6_power(B,C),k6_power(A,C)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l36_asympt_1]),
    [file(asympt_1,t101_asympt_1),interesting(0.71)]).

fof(t11_asympt_1,theorem,(
    r2_hidden(k3_asympt_1(2),k5_asympt_0(k3_asympt_1(3))) ),
    inference(mizar_proof,[status(thm)],[t11_funct_2,t2_xreal_1,d3_asympt_1,d3_asympt_1,t44_power]),
    [file(asympt_1,t11_asympt_1),interesting(0.71)]).

fof(l1_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(2,A)
          & r1_xreal_0(k3_series_1(2,A),k1_nat_1(A,1)) ) ) ),
    inference(mizar_proof,[status(thm)],[t53_power,t32_power,t30_power,t8_xreal_1,t39_power,t20_int_1,t8_xreal_1,t2_xreal_1,s1_int_2]),
    [file(asympt_1,l1_asympt_1),interesting(0.71)]).

fof(t46_asympt_1,theorem,(
    k3_series_1(2,4) = 16 ),
    inference(mizar_proof,[status(thm)],[l16_asympt_1]),
    [file(asympt_1,t46_asympt_1),interesting(0.71)]).

fof(t58_asympt_1,theorem,(
    k3_series_1(5,5) = 3125 ),
    inference(mizar_proof,[status(thm)],[l72_asympt_1]),
    [file(asympt_1,t58_asympt_1),interesting(0.71)]).

fof(t59_asympt_1,theorem,(
    k3_series_1(4,4) = 256 ),
    inference(mizar_proof,[status(thm)],[l73_asympt_1]),
    [file(asympt_1,t59_asympt_1),interesting(0.71)]).

fof(t89_asympt_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( r1_xreal_0(0,A)
       => k3_power(A,k6_real_1(1,2)) = k8_square_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[l75_asympt_1]),
    [file(asympt_1,t89_asympt_1),interesting(0.71)]).

fof(l71_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ( r1_xreal_0(3,A)
       => r1_xreal_0(k5_real_1(A,1),k4_real_1(2,k5_real_1(A,2))) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_xreal_1,s1_int_2]),
    [file(asympt_1,l71_asympt_1),interesting(0.70)]).

fof(l99_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(2,A)
          & r1_xreal_0(k7_square_1(A),k1_nat_1(A,1)) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_xreal_1,t70_xreal_1,t8_xreal_1,t8_xreal_1,t2_xreal_1,s1_int_2]),
    [file(asympt_1,l99_asympt_1),interesting(0.70)]).

fof(t62_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( r1_xreal_0(B,A)
           => r1_xreal_0(k11_newton(B),k11_newton(A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l106_asympt_1]),
    [file(asympt_1,t62_asympt_1),interesting(0.70)]).

fof(l55_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ( r1_xreal_0(1,A)
       => r1_xreal_0(k7_square_1(A),k4_real_1(2,k3_real_1(k5_real_1(k7_square_1(A),A),1))) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_xreal_1,t66_xreal_1,t8_xreal_1,t8_xreal_1,t8_xreal_1,t2_xreal_1,t2_xreal_1,s1_int_2]),
    [file(asympt_1,l55_asympt_1),interesting(0.69)]).

fof(t44_asympt_1,theorem,(
    k3_series_1(2,2) = 4 ),
    inference(mizar_proof,[status(thm)],[l14_asympt_1]),
    [file(asympt_1,t44_asympt_1),interesting(0.69)]).

fof(t57_asympt_1,theorem,(
    k11_newton(k1_nat_1(4,1)) = 120 ),
    inference(mizar_proof,[status(thm)],[l69_asympt_1]),
    [file(asympt_1,t57_asympt_1),interesting(0.69)]).

fof(t61_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(2,A)
          & r1_xreal_0(k11_newton(A),1) ) ) ),
    inference(mizar_proof,[status(thm)],[l105_asympt_1]),
    [file(asympt_1,t61_asympt_1),interesting(0.69)]).

fof(t72_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(6,A)
          & r1_xreal_0(k3_series_1(2,A),k7_square_1(k1_nat_1(A,1))) ) ) ),
    inference(mizar_proof,[status(thm)],[l20_asympt_1]),
    [file(asympt_1,t72_asympt_1),interesting(0.69)]).

fof(l100_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(1,A)
          & r1_xreal_0(k5_real_1(k3_series_1(2,k1_nat_1(A,1)),k3_series_1(2,A)),1) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_pre_ff,t30_power,t2_xreal_1,t30_power,t32_power]),
    [file(asympt_1,l100_asympt_1),interesting(0.67)]).

fof(t51_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(10,A)
          & r1_xreal_0(k4_power(2,k5_real_1(A,1)),k7_square_1(k2_nat_1(2,A))) ) ) ),
    inference(mizar_proof,[status(thm)],[l64_asympt_1]),
    [file(asympt_1,t51_asympt_1),interesting(0.67)]).

fof(t64_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(2,A)
          & r1_xreal_0(A,k2_int_1(k6_real_1(A,2))) ) ) ),
    inference(mizar_proof,[status(thm)],[l95_asympt_1]),
    [file(asympt_1,t64_asympt_1),interesting(0.67)]).

fof(t67_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(2,A)
          & r1_xreal_0(k3_series_1(2,A),k1_nat_1(A,1)) ) ) ),
    inference(mizar_proof,[status(thm)],[l1_asympt_1]),
    [file(asympt_1,t67_asympt_1),interesting(0.67)]).

fof(t95_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ( r1_xreal_0(4,A)
       => r1_xreal_0(k2_nat_1(2,A),k4_real_1(A,k6_power(2,A))) ) ) ),
    inference(mizar_proof,[status(thm)],[l89_asympt_1]),
    [file(asympt_1,t95_asympt_1),interesting(0.67)]).

fof(t97_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(2,A)
          & r1_xreal_0(k7_square_1(A),k1_nat_1(A,1)) ) ) ),
    inference(mizar_proof,[status(thm)],[l99_asympt_1]),
    [file(asympt_1,t97_asympt_1),interesting(0.67)]).

fof(t37_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => ( ( r2_hidden(B,k9_asympt_1)
               => k2_seq_1(k5_numbers,k1_numbers,A,B) = B )
              & ( ~ r2_hidden(B,k9_asympt_1)
               => k2_seq_1(k5_numbers,k1_numbers,A,B) = k3_series_1(2,B) ) ) )
       => ( r2_hidden(A,k10_asympt_0(k3_asympt_1(1),k9_asympt_1))
          & ~ r2_hidden(A,k7_asympt_0(k3_asympt_1(1)))
          & v7_asympt_0(k3_asympt_1(1))
          & ~ v6_asympt_0(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t27_asympt_0,t11_funct_2,d3_asympt_1,t30_power,l23_asympt_1,d7_seq_2,t46_square_1,t46_square_1,t2_xreal_1,t46_square_1,t2_xreal_1,t49_square_1,t49_square_1,t16_int_1,t39_power,t38_nat_1,t21_xreal_1,t16_int_1,l1_asympt_1,t22_xreal_1,t2_xreal_1,l101_asympt_1,d3_asympt_1,t30_power,t39_power,t12_pre_ff,t63_power,t60_power,t61_power,t2_xreal_1,d5_int_1,t2_xreal_1,t12_pre_ff,t8_xreal_1,t2_xreal_1,t177_real_2,t66_xreal_1,d7_xcmplx_0,d9_xcmplx_0,t2_xreal_1,l10_asympt_1,d2_asympt_1,d3_asympt_1,t30_power,d1_absvalue,d3_asympt_1,d3_asympt_1,t30_power,d3_asympt_1,t30_power,t8_xreal_1,d8_asympt_0,t11_funct_2,t70_xreal_1,d18_asympt_0,d3_asympt_1,t30_power,d3_asympt_1,t30_power,d19_asympt_0,t37_asympt_0,d8_asympt_0,t8_xreal_1,t10_pre_ff,t53_power,t11_xreal_1,t16_int_1,l101_asympt_1,l1_asympt_1,t22_xreal_1,t44_power,t8_xreal_1,t2_xreal_1]),
    [file(asympt_1,t37_asympt_1),interesting(0.66)]).

fof(t70_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k1_numbers)
             => ( ( r1_xreal_0(A,B)
                  & r1_xreal_0(0,C) )
               => ( r1_xreal_0(A,0)
                  | r1_xreal_0(k4_power(A,C),k4_power(B,C)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l13_asympt_1]),
    [file(asympt_1,t70_asympt_1),interesting(0.66)]).

fof(l22_asympt_1,theorem,(
    ! [A] : 
      ( ( v2_xreal_0(A)
        & m1_subset_1(A,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( k2_seq_1(k5_numbers,k1_numbers,B,0) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,0)
                   => k2_seq_1(k5_numbers,k1_numbers,B,C) = k6_power(2,k4_power(C,A)) ) ) )
           => ( v4_seq_2(k19_seq_1(B,k3_asympt_1(A)))
              & k2_seq_2(k19_seq_1(B,k3_asympt_1(A))) = 0 ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_xreal_0,t46_square_1,t46_square_1,t2_xreal_1,t49_square_1,t49_square_1,t16_int_1,t124_xreal_1,t70_xreal_1,d9_xcmplx_0,t2_xreal_1,d5_int_1,t2_xreal_1,t39_power,l13_asympt_1,t38_power,t107_xcmplx_1,t30_power,t66_xreal_1,t88_xcmplx_1,t2_xreal_1,l21_asympt_1,t39_power,t124_xreal_1,t70_xreal_1,t178_real_2,t178_real_2,t79_xcmplx_1,t39_power,d5_int_1,t10_xreal_1,t2_xreal_1,t2_xreal_1,t39_power,t42_power,t38_power,t88_xcmplx_1,t70_xreal_1,t32_power,t29_power,t53_power,t151_real_2,t39_power,t70_xreal_1,t100_xcmplx_1,t2_xreal_1,t65_power,t63_power,t60_power,t178_real_2,t2_xreal_1,t44_power,t29_power,t65_power,t59_power,t70_xreal_1,d9_xcmplx_0,l10_asympt_1,d3_asympt_1,d1_absvalue,d6_seq_2,d7_seq_2]),
    [file(asympt_1,l22_asympt_1),interesting(0.65)]).

fof(t50_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(3,A)
          & r1_xreal_0(k7_square_1(A),k1_nat_1(k2_nat_1(2,A),1)) ) ) ),
    inference(mizar_proof,[status(thm)],[l63_asympt_1]),
    [file(asympt_1,t50_asympt_1),interesting(0.65)]).

fof(t71_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(4,A)
          & r1_xreal_0(k3_series_1(2,A),k1_nat_1(k2_nat_1(2,A),3)) ) ) ),
    inference(mizar_proof,[status(thm)],[l19_asympt_1]),
    [file(asympt_1,t71_asympt_1),interesting(0.65)]).

fof(t84_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ( r1_xreal_0(1,A)
       => r1_xreal_0(k3_real_1(k5_real_1(k7_square_1(A),A),1),k7_square_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[l54_asympt_1]),
    [file(asympt_1,t84_asympt_1),interesting(0.65)]).

fof(l77_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => k2_seq_1(k5_numbers,k1_numbers,A,B) = k4_power(k3_real_1(1,k6_real_1(1,k1_nat_1(B,1))),k1_nat_1(B,1)) )
       => v3_seqm_3(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t39_power,t60_xcmplx_1,t77_xcmplx_1,t30_power,t32_power,t75_xcmplx_1,t36_power,t6_xcmplx_1,t6_xcmplx_1,t114_xcmplx_1,t114_xcmplx_1,t85_xcmplx_1,t121_xcmplx_1,t60_xcmplx_1,t8_xreal_1,t137_real_2,t2_square_1,t26_xreal_1,t56_power,t75_xcmplx_1,t84_xcmplx_1,t60_xcmplx_1,t66_xreal_1,t114_xcmplx_1,t128_xcmplx_1,t77_xcmplx_1,t60_xcmplx_1,t118_real_2,d13_seqm_3]),
    [file(asympt_1,l77_asympt_1),interesting(0.63)]).

fof(t60_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ r1_xreal_0(k3_real_1(k5_real_1(k7_square_1(A),A),1),0) ) ),
    inference(mizar_proof,[status(thm)],[l52_asympt_1]),
    [file(asympt_1,t60_asympt_1),interesting(0.63)]).

fof(t88_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ( r1_xreal_0(3,A)
       => r1_xreal_0(k5_real_1(A,1),k4_real_1(2,k5_real_1(A,2))) ) ) ),
    inference(mizar_proof,[status(thm)],[l71_asympt_1]),
    [file(asympt_1,t88_asympt_1),interesting(0.62)]).

fof(t98_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(1,A)
          & r1_xreal_0(k5_real_1(k3_series_1(2,k1_nat_1(A,1)),k3_series_1(2,A)),1) ) ) ),
    inference(mizar_proof,[status(thm)],[l100_asympt_1]),
    [file(asympt_1,t98_asympt_1),interesting(0.62)]).

fof(t32_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ~ ( k2_seq_1(k5_numbers,k1_numbers,A,0) = 0
          & ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ( ~ r1_xreal_0(B,0)
               => k2_seq_1(k5_numbers,k1_numbers,A,B) = k3_series_1(B,B) ) )
          & ! [B] : 
              ( ( v1_funct_1(B)
                & v1_funct_2(B,k5_numbers,k1_numbers)
                & v4_asympt_0(B)
                & m2_relset_1(B,k5_numbers,k1_numbers) )
             => ~ ( B = A
                  & r1_tarski(k5_asympt_0(k5_asympt_1(1)),k5_asympt_0(B))
                  & k5_asympt_0(k5_asympt_1(1)) != k5_asympt_0(B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_asympt_0,t39_power,l10_asympt_1,d5_asympt_1,t39_power,t124_xreal_1,t217_xcmplx_1,t23_newton,t70_xreal_1,t100_xcmplx_1,s1_seq_1,t23_newton,l10_asympt_1,d5_asympt_1,l10_asympt_1,d5_asympt_1,l74_asympt_1,t21_newton,t104_xcmplx_1,t60_xcmplx_1,t32_power,t30_power,d9_xcmplx_0,d9_xcmplx_0,t36_power,t100_xcmplx_1,l73_asympt_1,t36_power,t77_xcmplx_1,t30_power,t32_power,l72_asympt_1,t8_xreal_1,t124_xreal_1,t70_xreal_1,d9_xcmplx_0,t39_power,t124_xreal_1,t70_xreal_1,d9_xcmplx_0,t70_xreal_1,t2_xreal_1,t124_xreal_1,t70_xreal_1,d9_xcmplx_0,t39_power,t124_xreal_1,t70_xreal_1,d9_xcmplx_0,t70_xreal_1,t124_xreal_1,t70_xreal_1,d9_xcmplx_0,t77_xcmplx_1,t85_xcmplx_1,t178_real_2,l78_asympt_1,t177_real_2,t199_real_2,t70_xreal_1,t88_xcmplx_1,t2_xreal_1,s1_int_2,l10_asympt_1,d5_asympt_1,l69_asympt_1,l73_asympt_1,t29_nat_1,t70_xreal_1,t88_xcmplx_1,t178_real_2,t70_xreal_1,t103_xcmplx_1,t2_xreal_1,l71_asympt_1,t11_xreal_1,t152_real_2,t2_xreal_1,t2_xreal_1,s1_int_2,t124_xreal_1,t217_xcmplx_1,d5_int_1,t31_xreal_1,t2_xreal_1,t16_int_1,t2_xreal_1,t2_xreal_1,t21_xreal_1,t31_xreal_1,t2_xreal_1,t151_real_2,t101_xcmplx_1,t2_xreal_1,t2_xreal_1,d1_absvalue,d6_seq_2,d7_seq_2,t16_asympt_0,t19_asympt_0,t4_asympt_1]),
    [file(asympt_1,t32_asympt_1),interesting(0.60)]).

fof(t85_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ( r1_xreal_0(1,A)
       => r1_xreal_0(k7_square_1(A),k4_real_1(2,k3_real_1(k5_real_1(k7_square_1(A),A),1))) ) ) ),
    inference(mizar_proof,[status(thm)],[l55_asympt_1]),
    [file(asympt_1,t85_asympt_1),interesting(0.60)]).

fof(t27_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ~ ( k2_seq_1(k5_numbers,k1_numbers,A,0) = 0
          & ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ( ~ r1_xreal_0(B,0)
               => k2_seq_1(k5_numbers,k1_numbers,A,B) = k4_power(B,k9_square_1(B)) ) )
          & ! [B] : 
              ( ( v1_funct_1(B)
                & v1_funct_2(B,k5_numbers,k1_numbers)
                & v4_asympt_0(B)
                & m2_relset_1(B,k5_numbers,k1_numbers) )
             => ! [C] : 
                  ( ( v1_funct_1(C)
                    & v1_funct_2(C,k5_numbers,k1_numbers)
                    & v4_asympt_0(C)
                    & m2_relset_1(C,k5_numbers,k1_numbers) )
                 => ~ ( B = A
                      & C = k1_asympt_1(2,1,0)
                      & r1_tarski(k5_asympt_0(B),k5_asympt_0(C))
                      & k5_asympt_0(B) != k5_asympt_0(C) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_asympt_0,t39_power,l76_asympt_1,t124_xreal_1,t217_xcmplx_1,t46_square_1,t46_square_1,t2_xreal_1,t49_square_1,t49_square_1,t16_int_1,l10_asympt_1,l6_asympt_1,d1_asympt_1,t34_power,t2_xreal_1,t26_xreal_1,t44_power,d5_int_1,t2_xreal_1,t177_real_2,t2_xreal_1,t26_xreal_1,t10_pre_ff,t33_power,d3_power,t56_xcmplx_1,t2_xreal_1,t39_power,d1_absvalue,d6_seq_2,d7_seq_2,t16_asympt_0,t19_asympt_0,t4_asympt_1]),
    [file(asympt_1,t27_asympt_1),interesting(0.59)]).

fof(t91_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => k2_seq_1(k5_numbers,k1_numbers,A,B) = k4_power(k3_real_1(1,k6_real_1(1,k1_nat_1(B,1))),k1_nat_1(B,1)) )
       => v3_seqm_3(A) ) ) ),
    inference(mizar_proof,[status(thm)],[l77_asympt_1]),
    [file(asympt_1,t91_asympt_1),interesting(0.59)]).

fof(t74_asympt_1,theorem,(
    ! [A] : 
      ( ( v2_xreal_0(A)
        & m1_subset_1(A,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( k2_seq_1(k5_numbers,k1_numbers,B,0) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,0)
                   => k2_seq_1(k5_numbers,k1_numbers,B,C) = k6_power(2,k4_power(C,A)) ) ) )
           => ( v4_seq_2(k19_seq_1(B,k3_asympt_1(A)))
              & k2_seq_2(k19_seq_1(B,k3_asympt_1(A))) = 0 ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l22_asympt_1]),
    [file(asympt_1,t74_asympt_1),interesting(0.55)]).

fof(t21_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ~ ( ~ r1_xreal_0(A,0)
              & k2_seq_1(k5_numbers,k1_numbers,B,0) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,0)
                   => k2_seq_1(k5_numbers,k1_numbers,B,C) = k4_real_1(C,k6_power(2,C)) ) )
              & ! [C] : 
                  ( ( v1_funct_1(C)
                    & v1_funct_2(C,k5_numbers,k1_numbers)
                    & v4_asympt_0(C)
                    & m2_relset_1(C,k5_numbers,k1_numbers) )
                 => ~ ( C = B
                      & r1_tarski(k5_asympt_0(C),k5_asympt_0(k3_asympt_1(k3_real_1(1,A))))
                      & k5_asympt_0(C) != k5_asympt_0(k3_asympt_1(k3_real_1(1,A))) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_asympt_0,t12_pre_ff,t60_power,t70_xreal_1,l23_asympt_1,l10_asympt_1,d3_asympt_1,t30_power,d9_xcmplx_0,d9_xcmplx_0,t34_power,t33_power,t100_xcmplx_1,d2_asympt_1,d3_asympt_1,l10_asympt_1,l53_asympt_1,t16_asympt_0,t19_asympt_0,t4_asympt_1]),
    [file(asympt_1,t21_asympt_1),interesting(0.53)]).

fof(t16_asympt_1,theorem,(
    ? [A] : 
      ( v1_funct_1(A)
      & v1_funct_2(A,k5_numbers,k1_numbers)
      & v4_asympt_0(A)
      & m2_relset_1(A,k5_numbers,k1_numbers)
      & A = k1_asympt_1(2,1,0)
      & r2_hidden(k3_asympt_0(k3_asympt_1(1),2),k5_asympt_0(k3_asympt_1(1)))
      & ~ r2_hidden(k1_asympt_1(2,2,0),k5_asympt_0(A)) ) ),
    inference(mizar_proof,[status(thm)],[t11_funct_2,t13_seq_1,d3_asympt_1,d3_asympt_1,t30_power,t13_seq_1,t46_square_1,t49_square_1,t16_int_1,d1_asympt_1,t4_xcmplx_1,t32_power,t29_power,d1_asympt_1,t32_power,t10_pre_ff,d5_int_1,t10_pre_ff,t32_power,d3_power,t30_power,t70_xreal_1,t2_xreal_1,t2_xreal_1,t39_power,t66_xreal_1,t46_square_1]),
    [file(asympt_1,t16_asympt_1),interesting(0.47)]).

fof(t24_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ~ ( ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => k2_seq_1(k5_numbers,k1_numbers,A,B) = k4_power(k3_real_1(k5_real_1(k7_square_1(B),B),1),4) )
          & ! [B] : 
              ( ( v1_funct_1(B)
                & v1_funct_2(B,k5_numbers,k1_numbers)
                & v4_asympt_0(B)
                & m2_relset_1(B,k5_numbers,k1_numbers) )
             => ~ ( B = A
                  & k5_asympt_0(k3_asympt_1(8)) = k5_asympt_0(B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_asympt_0,l52_asympt_1,t39_power,t11_funct_2,t11_funct_2,d3_asympt_1,t38_power,t53_power,l54_asympt_1,l52_asympt_1,l13_asympt_1,t39_power,d3_asympt_1,t38_power,t53_power,l55_asympt_1,l52_asympt_1,t70_xreal_1,l13_asympt_1,l16_asympt_1,t35_power,t39_power,l11_asympt_1]),
    [file(asympt_1,t24_asympt_1),interesting(0.46)]).

fof(t22_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ~ ( ~ r1_xreal_0(A,0)
              & ~ r1_xreal_0(1,A)
              & k2_seq_1(k5_numbers,k1_numbers,B,0) = 0
              & k2_seq_1(k5_numbers,k1_numbers,B,1) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,1)
                   => k2_seq_1(k5_numbers,k1_numbers,B,C) = k6_real_1(k3_series_1(C,2),k6_power(2,C)) ) )
              & ! [C] : 
                  ( ( v1_funct_1(C)
                    & v1_funct_2(C,k5_numbers,k1_numbers)
                    & v4_asympt_0(C)
                    & m2_relset_1(C,k5_numbers,k1_numbers) )
                 => ~ ( C = B
                      & r1_tarski(k5_asympt_0(k3_asympt_1(k3_real_1(1,A))),k5_asympt_0(C))
                      & k5_asympt_0(k3_asympt_1(k3_real_1(1,A))) != k5_asympt_0(C) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_asympt_0,t2_xreal_1,d9_xcmplx_0,t39_power,t12_pre_ff,t60_power,t124_xreal_1,t70_xreal_1,t22_xreal_1,l23_asympt_1,t2_xreal_1,l10_asympt_1,d3_asympt_1,d9_xcmplx_0,t215_xcmplx_1,d9_xcmplx_0,d9_xcmplx_0,t34_power,t33_power,t100_xcmplx_1,d2_asympt_1,d3_asympt_1,l10_asympt_1,l53_asympt_1,t16_asympt_0,t19_asympt_0,t4_asympt_1]),
    [file(asympt_1,t22_asympt_1),interesting(0.45)]).

fof(t26_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ~ ( k2_seq_1(k5_numbers,k1_numbers,A,0) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,0)
                   => k2_seq_1(k5_numbers,k1_numbers,A,C) = k4_power(C,k6_power(2,C)) ) )
              & k2_seq_1(k5_numbers,k1_numbers,B,0) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,0)
                   => k2_seq_1(k5_numbers,k1_numbers,B,C) = k4_power(C,k9_square_1(C)) ) )
              & ! [C] : 
                  ( ( v1_funct_1(C)
                    & v1_funct_2(C,k5_numbers,k1_numbers)
                    & v4_asympt_0(C)
                    & m2_relset_1(C,k5_numbers,k1_numbers) )
                 => ! [D] : 
                      ( ( v1_funct_1(D)
                        & v1_funct_2(D,k5_numbers,k1_numbers)
                        & v4_asympt_0(D)
                        & m2_relset_1(D,k5_numbers,k1_numbers) )
                     => ~ ( C = A
                          & D = B
                          & r1_tarski(k5_asympt_0(C),k5_asympt_0(D))
                          & k5_asympt_0(C) != k5_asympt_0(D) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_asympt_0,t39_power,d6_asympt_0,t39_power,l68_asympt_1,t46_square_1,t46_square_1,t2_xreal_1,t2_xreal_1,t49_square_1,t49_square_1,t16_int_1,t124_xreal_1,t217_xcmplx_1,d5_int_1,t2_xreal_1,t2_xreal_1,l10_asympt_1,t34_power,t2_xreal_1,t71_xreal_1,t44_power,t33_power,t30_power,t2_xreal_1,t152_real_2,t56_xcmplx_1,t2_xreal_1,t39_power,d1_absvalue,d6_seq_2,d7_seq_2,t16_asympt_0,t19_asympt_0,t4_asympt_1]),
    [file(asympt_1,t26_asympt_1),interesting(0.41)]).

fof(t34_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ~ ( k2_seq_1(k5_numbers,k1_numbers,B,0) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,0)
                   => k2_seq_1(k5_numbers,k1_numbers,B,C) = k4_real_1(C,k6_power(2,C)) ) )
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => k2_seq_1(k5_numbers,k1_numbers,A,C) = k6_power(2,k11_newton(C)) )
              & ! [C] : 
                  ( ( v1_funct_1(C)
                    & v1_funct_2(C,k5_numbers,k1_numbers)
                    & v2_asympt_0(C)
                    & m2_relset_1(C,k5_numbers,k1_numbers) )
                 => ~ ( C = B
                      & r2_hidden(A,k7_asympt_0(C)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_asympt_0,t12_pre_ff,t60_power,t70_xreal_1,t27_asympt_0,t11_funct_2,s3_funct_2,s3_funct_2,t70_xreal_1,d9_xcmplx_0,d5_int_1,t16_int_1,t21_int_1,t8_xreal_1,d9_xcmplx_0,t16_int_1,d2_asympt_1,t38_nat_1,t12_pre_ff,t59_power,d2_asympt_1,l26_asympt_1,t8_xreal_1,t22_xreal_1,d7_bhsp_4,l31_asympt_1,t8_xreal_1,t21_xreal_1,t2_xreal_1,t12_pre_ff,d2_asympt_1,l30_asympt_1,d5_int_1,t21_xreal_1,t8_xreal_1,t21_xreal_1,l32_asympt_1,t177_real_2,t12_pre_ff,t60_power,t66_xreal_1,t62_power,t60_power,d9_xcmplx_0,d9_xcmplx_0,l89_asympt_1,t66_xreal_1,d9_xcmplx_0,t92_xcmplx_1,d9_xcmplx_0,t21_xreal_1,t21_xreal_1,t2_xreal_1,t2_xreal_1,t2_xreal_1,l88_asympt_1,l88_asympt_1,d2_asympt_1,t12_pre_ff,d2_asympt_1,l27_asympt_1,l28_asympt_1]),
    [file(asympt_1,t34_asympt_1),interesting(0.41)]).

fof(t23_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ~ ( k2_seq_1(k5_numbers,k1_numbers,A,0) = 0
          & k2_seq_1(k5_numbers,k1_numbers,A,1) = 0
          & ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ( ~ r1_xreal_0(B,1)
               => k2_seq_1(k5_numbers,k1_numbers,A,B) = k6_real_1(k3_series_1(B,2),k6_power(2,B)) ) )
          & ! [B] : 
              ( ( v1_funct_1(B)
                & v1_funct_2(B,k5_numbers,k1_numbers)
                & v4_asympt_0(B)
                & m2_relset_1(B,k5_numbers,k1_numbers) )
             => ~ ( B = A
                  & r1_tarski(k5_asympt_0(B),k5_asympt_0(k3_asympt_1(8)))
                  & k5_asympt_0(B) != k5_asympt_0(k3_asympt_1(8)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_asympt_0,t2_xreal_1,d9_xcmplx_0,t39_power,t12_pre_ff,t60_power,t124_xreal_1,t70_xreal_1,d1_xreal_0,t46_square_1,t49_square_1,t16_int_1,t2_xreal_1,t12_pre_ff,t65_power,t2_xreal_1,t60_power,t2_xreal_1,t39_power,l10_asympt_1,d3_asympt_1,d9_xcmplx_0,d9_xcmplx_0,d9_xcmplx_0,t34_power,t33_power,t217_xcmplx_1,t103_xcmplx_1,t70_xreal_1,t151_real_2,t39_power,d5_int_1,t2_xreal_1,l13_asympt_1,t38_power,t39_power,t152_real_2,t33_power,t30_power,t56_xcmplx_1,t2_xreal_1,t70_xreal_1,t124_xreal_1,t217_xcmplx_1,d1_absvalue,d6_seq_2,d7_seq_2,t16_asympt_0,t19_asympt_0,t4_asympt_1]),
    [file(asympt_1,t23_asympt_1),interesting(0.32)]).

fof(t18_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ~ ( ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => k2_seq_1(k5_numbers,k1_numbers,A,C) = k4_nat_1(C,2) )
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => k2_seq_1(k5_numbers,k1_numbers,B,C) = k4_nat_1(k1_nat_1(C,1),2) )
              & ! [C] : 
                  ( ( v1_funct_1(C)
                    & v1_funct_2(C,k5_numbers,k1_numbers)
                    & v2_asympt_0(C)
                    & m2_relset_1(C,k5_numbers,k1_numbers) )
                 => ! [D] : 
                      ( ( v1_funct_1(D)
                        & v1_funct_2(D,k5_numbers,k1_numbers)
                        & v2_asympt_0(D)
                        & m2_relset_1(D,k5_numbers,k1_numbers) )
                     => ~ ( C = A
                          & D = B
                          & ~ r2_hidden(C,k5_asympt_0(D))
                          & ~ r2_hidden(D,k5_asympt_0(C)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_asympt_0,t62_nat_1,d4_asympt_0,t62_nat_1,t38_nat_1,t8_euler_2,t64_nat_1,t64_nat_1,t8_euler_2,t77_nat_1,t78_nat_1,t8_euler_2,t64_nat_1,t77_nat_1,t62_nat_1,t8_euler_2,t64_nat_1,t64_nat_1,t38_nat_1,t8_euler_2,t77_nat_1,t64_nat_1,t8_euler_2,t64_nat_1,t77_nat_1,t62_nat_1]),
    [file(asympt_1,t18_asympt_1),interesting(0.31)]).

fof(t10_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => k2_seq_1(k5_numbers,k1_numbers,A,B) = k3_real_1(k5_real_1(k2_nat_1(3,k3_series_1(10,6)),k2_nat_1(k2_nat_1(18,k3_series_1(10,3)),B)),k4_real_1(27,k7_square_1(B))) )
       => r2_hidden(A,k5_asympt_0(k3_asympt_1(2))) ) ) ),
    inference(mizar_proof,[status(thm)],[t11_funct_2,t53_power,t30_power,t32_power,t32_power,t32_power,t30_power,t53_power,d8_xcmplx_0,t21_xreal_1,t22_xreal_1,t66_xreal_1,t2_xreal_1,t32_power,t8_xreal_1,t66_xreal_1,t2_xreal_1,t9_xreal_1,t2_xreal_1,t8_xreal_1,t2_xreal_1,s1_int_2,t53_power,d3_asympt_1,t22_xreal_1]),
    [file(asympt_1,t10_asympt_1),interesting(0.24)]).

fof(d9_asympt_1,definition,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( ( A != 0
             => ( B = k10_asympt_1(A)
              <=> ? [C] : 
                    ( m2_subset_1(C,k1_numbers,k5_numbers)
                    & r1_xreal_0(k11_newton(C),A)
                    & ~ r1_xreal_0(k11_newton(k1_nat_1(C,1)),A)
                    & B = k11_newton(C) ) ) )
            & ( A = 0
             => ( B = k10_asympt_1(A)
              <=> B = 0 ) ) ) ) ) ),
    file(asympt_1,d9_asympt_1),
    [interesting(0.00)]).

fof(t100_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( ( r1_xreal_0(1,B)
              & r1_xreal_0(k11_newton(A),B) )
           => ( r1_xreal_0(k11_newton(k1_nat_1(A,1)),B)
              | k10_asympt_1(B) = k11_newton(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_asympt_1]),
    [file(asympt_1,t100_asympt_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(t12_pre_ff,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( r1_xreal_0(B,C)
               => ( r1_xreal_0(A,1)
                  | r1_xreal_0(B,0)
                  | r1_xreal_0(k5_power(A,B),k5_power(A,C)) ) ) ) ) ) ),
    file(pre_ff,t12_pre_ff),
    [interesting(0.00)]).

fof(t59_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ~ ( ~ r1_xreal_0(A,0)
          & A != 1
          & k5_power(A,1) != 0 ) ) ),
    file(power,t59_power),
    [interesting(0.00)]).

fof(t60_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ~ ( ~ r1_xreal_0(A,0)
          & A != 1
          & k5_power(A,A) != 1 ) ) ),
    file(power,t60_power),
    [interesting(0.00)]).

fof(t66_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(0,C) )
               => r1_xreal_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,C)) ) ) ) ) ),
    file(xreal_1,t66_xreal_1),
    [interesting(0.00)]).

fof(t64_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ~ ( ~ r1_xreal_0(A,0)
                  & A != 1
                  & ~ r1_xreal_0(B,0)
                  & B != 1
                  & ~ r1_xreal_0(C,0)
                  & k5_power(A,C) != k3_xcmplx_0(k5_power(A,B),k5_power(B,C)) ) ) ) ) ),
    file(power,t64_power),
    [interesting(0.00)]).

fof(t11_funct_2,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & v1_funct_2(C,A,B)
        & m2_relset_1(C,A,B) )
     => ( ( B = k1_xboole_0
         => A = k1_xboole_0 )
       => r2_hidden(C,k1_funct_2(A,B)) ) ) ),
    file(funct_2,t11_funct_2),
    [interesting(0.00)]).

fof(t53_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => k3_power(A,2) = k5_square_1(A) ) ),
    file(power,t53_power),
    [interesting(0.00)]).

fof(t30_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => k3_power(A,1) = A ) ),
    file(power,t30_power),
    [interesting(0.00)]).

fof(t32_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( ~ r1_xreal_0(A,0)
               => k3_power(A,k2_xcmplx_0(B,C)) = k3_xcmplx_0(k3_power(A,B),k3_power(A,C)) ) ) ) ) ),
    file(power,t32_power),
    [interesting(0.00)]).

fof(d8_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k6_xcmplx_0(A,B) = k2_xcmplx_0(A,k4_xcmplx_0(B)) ) ) ),
    file(xcmplx_0,d8_xcmplx_0),
    [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(t22_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( r1_xreal_0(A,k2_xcmplx_0(B,C))
              <=> r1_xreal_0(k6_xcmplx_0(A,B),C) ) ) ) ) ),
    file(xreal_1,t22_xreal_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(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_int_2,theorem,
    ( ( p1_s1_int_2(f1_s1_int_2)
      & ! [A] : 
          ( m2_subset_1(A,k1_numbers,k5_numbers)
         => ( ( r1_xreal_0(f1_s1_int_2,A)
              & p1_s1_int_2(A) )
           => p1_s1_int_2(k1_nat_1(A,1)) ) ) )
   => ! [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
       => ( r1_xreal_0(f1_s1_int_2,A)
         => p1_s1_int_2(A) ) ) ),
    file(int_2,s1_int_2),
    [interesting(0.00)]).

fof(d3_asympt_1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( B = k3_asympt_1(A)
          <=> ( k2_seq_1(k5_numbers,k1_numbers,B,0) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,0)
                   => k2_seq_1(k5_numbers,k1_numbers,B,C) = k4_power(C,A) ) ) ) ) ) ) ),
    file(asympt_1,d3_asympt_1),
    [interesting(0.00)]).

fof(t44_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ~ ( ~ r1_xreal_0(B,A)
                  & ~ r1_xreal_0(C,1)
                  & r1_xreal_0(k3_power(C,B),k3_power(C,A)) ) ) ) ) ),
    file(power,t44_power),
    [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(t46_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => r1_xreal_0(A,k2_square_1(A,B)) ) ) ),
    file(square_1,t46_square_1),
    [interesting(0.00)]).

fof(t124_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( ~ ( ~ r1_xreal_0(A,0)
            & r1_xreal_0(k5_xcmplx_0(A),0) )
        & ~ ( ~ r1_xreal_0(k5_xcmplx_0(A),0)
            & r1_xreal_0(A,0) ) ) ) ),
    file(xreal_1,t124_xreal_1),
    [interesting(0.00)]).

fof(t70_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ~ ( ~ r1_xreal_0(A,0)
                  & ~ r1_xreal_0(C,B)
                  & r1_xreal_0(k3_xcmplx_0(C,A),k3_xcmplx_0(B,A)) ) ) ) ) ),
    file(xreal_1,t70_xreal_1),
    [interesting(0.00)]).

fof(d5_int_1,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_int_1(B)
         => ( B = k2_int_1(A)
          <=> ( r1_xreal_0(A,B)
              & ~ r1_xreal_0(k2_xcmplx_0(A,1),B) ) ) ) ) ),
    file(int_1,d5_int_1),
    [interesting(0.00)]).

fof(d9_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k7_xcmplx_0(A,B) = k3_xcmplx_0(A,k5_xcmplx_0(B)) ) ) ),
    file(xcmplx_0,d9_xcmplx_0),
    [interesting(0.00)]).

fof(t49_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( k2_square_1(A,B) = A
            | k2_square_1(A,B) = B ) ) ) ),
    file(square_1,t49_square_1),
    [interesting(0.00)]).

fof(t16_int_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ( r1_xreal_0(0,A)
       => r2_hidden(A,k5_numbers) ) ) ),
    file(int_1,t16_int_1),
    [interesting(0.00)]).

fof(t29_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => k3_power(A,0) = 1 ) ),
    file(power,t29_power),
    [interesting(0.00)]).

fof(t88_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => k3_xcmplx_0(k7_xcmplx_0(B,A),A) = B ) ) ) ),
    file(xcmplx_1,t88_xcmplx_1),
    [interesting(0.00)]).

fof(t39_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ~ ( ~ r1_xreal_0(A,0)
              & r1_xreal_0(k3_power(A,B),0) ) ) ) ),
    file(power,t39_power),
    [interesting(0.00)]).

fof(t27_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => k7_asympt_0(A) = a_1_2_asympt_0(A) ) ),
    file(asympt_0,t27_asympt_0),
    [interesting(0.00)]).

fof(d1_asympt_1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k1_numbers)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k5_numbers,k1_numbers)
                    & m2_relset_1(D,k5_numbers,k1_numbers) )
                 => ( D = k1_asympt_1(A,B,C)
                  <=> ! [E] : 
                        ( m2_subset_1(E,k1_numbers,k5_numbers)
                       => k2_seq_1(k5_numbers,k1_numbers,D,E) = k4_power(A,k3_real_1(k4_real_1(B,E),C)) ) ) ) ) ) ) ),
    file(asympt_1,d1_asympt_1),
    [interesting(0.00)]).

fof(t10_pre_ff,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( r1_xreal_0(A,B)
               => ( r1_xreal_0(C,1)
                  | r1_xreal_0(k3_power(C,A),k3_power(C,B)) ) ) ) ) ) ),
    file(pre_ff,t10_pre_ff),
    [interesting(0.00)]).

fof(t13_asympt_1,theorem,(
    ? [A] : 
      ( v1_funct_1(A)
      & v1_funct_2(A,k5_numbers,k1_numbers)
      & v4_asympt_0(A)
      & m2_relset_1(A,k5_numbers,k1_numbers)
      & A = k1_asympt_1(2,1,1)
      & r2_hidden(k1_asympt_1(2,1,0),k7_asympt_0(A)) ) ),
    inference(mizar_proof,[status(thm)],[t27_asympt_0,t11_funct_2,t39_power,d1_asympt_1,d1_asympt_1,t32_power,t9_xreal_1,t10_pre_ff]),
    [file(asympt_1,t13_asympt_1),interesting(0.00)]).

fof(t23_newton,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ~ r1_xreal_0(k6_newton(A),0) ) ),
    file(newton,t23_newton),
    [interesting(0.00)]).

fof(d5_asympt_1,definition,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( B = k5_asympt_1(A)
          <=> ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => k2_seq_1(k5_numbers,k1_numbers,B,C) = k11_newton(k1_nat_1(C,A)) ) ) ) ) ),
    file(asympt_1,d5_asympt_1),
    [interesting(0.00)]).

fof(t21_newton,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => k6_newton(k2_xcmplx_0(A,1)) = k3_xcmplx_0(k6_newton(A),k2_xcmplx_0(A,1)) ) ),
    file(newton,t21_newton),
    [interesting(0.00)]).

fof(d7_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( ( A != 0
             => ( B = k5_xcmplx_0(A)
              <=> k3_xcmplx_0(A,B) = 1 ) )
            & ( A = 0
             => ( B = k5_xcmplx_0(A)
              <=> B = 0 ) ) ) ) ) ),
    file(xcmplx_0,d7_xcmplx_0),
    [interesting(0.00)]).

fof(d2_power,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( ( ~ r1_xreal_0(A,0)
                 => ( C = k3_power(A,B)
                  <=> C = k12_prepower(A,B) ) )
                & ( A = 0
                 => ( r1_xreal_0(B,0)
                    | ( C = k3_power(A,B)
                    <=> C = 0 ) ) )
                & ( ( A = 0
                    & B = 0 )
                 => ( C = k3_power(A,B)
                  <=> C = 1 ) )
                & ( v1_int_1(B)
                 => ( r1_xreal_0(0,A)
                    | ( C = k3_power(A,B)
                    <=> ? [D] : 
                          ( v1_int_1(D)
                          & D = B
                          & C = k6_prepower(A,D) ) ) ) ) ) ) ) ) ),
    file(power,d2_power),
    [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(t31_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => k3_power(1,A) = 1 ) ),
    file(power,t31_power),
    [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(l45_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k1_numbers)
             => ! [D] : 
                  ( m1_subset_1(D,k1_numbers)
                 => ( ( r1_xreal_0(0,B)
                      & r1_xreal_0(A,B)
                      & r1_xreal_0(0,C)
                      & r1_xreal_0(C,D) )
                   => r1_xreal_0(k4_real_1(A,C),k4_real_1(B,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t66_xreal_1,t2_xreal_1]),
    [file(asympt_1,l45_asympt_1),interesting(0.00)]).

fof(t12_seq_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( A = k8_seq_1(k5_numbers,k1_numbers,B,C)
              <=> ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k2_seq_1(k5_numbers,k1_numbers,A,D) = k4_real_1(k2_seq_1(k5_numbers,k1_numbers,B,D),k2_seq_1(k5_numbers,k1_numbers,C,D)) ) ) ) ) ) ),
    file(seq_1,t12_seq_1),
    [interesting(0.00)]).

fof(t15_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( r2_hidden(A,k5_asympt_0(k3_asympt_1(1)))
       => r2_hidden(k11_seq_1(A,A),k5_asympt_0(k3_asympt_1(2))) ) ) ),
    inference(mizar_proof,[status(thm)],[t46_square_1,t46_square_1,t11_funct_2,d2_power,d3_asympt_1,d3_asympt_1,t30_power,d3_asympt_1,d3_asympt_1,t38_nat_1,t31_power,d3_asympt_1,d3_asympt_1,t44_power,d3_asympt_1,d3_asympt_1,d5_real_1,l45_asympt_1,d2_power,t32_power,d3_asympt_1,d3_asympt_1,d3_asympt_1,d3_asympt_1,d3_asympt_1,t66_xreal_1,t2_xreal_1,t12_seq_1,t66_xreal_1,t12_seq_1]),
    [file(asympt_1,t15_asympt_1),interesting(0.00)]).

fof(t13_seq_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( B = k14_seq_1(C,A)
              <=> ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k2_seq_1(k5_numbers,k1_numbers,B,D) = k3_xcmplx_0(A,k2_seq_1(k5_numbers,k1_numbers,C,D)) ) ) ) ) ) ),
    file(seq_1,t13_seq_1),
    [interesting(0.00)]).

fof(t4_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k3_xcmplx_0(A,k3_xcmplx_0(B,C)) = k3_xcmplx_0(k3_xcmplx_0(A,B),C) ) ) ) ),
    file(xcmplx_1,t4_xcmplx_1),
    [interesting(0.00)]).

fof(d3_power,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ~ ( ~ r1_xreal_0(A,0)
              & A != 1
              & ~ r1_xreal_0(B,0)
              & ~ ! [C] : 
                    ( v1_xreal_0(C)
                   => ( C = k5_power(A,B)
                    <=> k3_power(A,C) = B ) ) ) ) ) ),
    file(power,d3_power),
    [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(d1_xreal_0,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
    <=> r2_hidden(A,k1_numbers) ) ),
    file(xreal_0,d1_xreal_0),
    [interesting(0.00)]).

fof(t217_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(1,A) = k5_xcmplx_0(A) ) ),
    file(xcmplx_1,t217_xcmplx_1),
    [interesting(0.00)]).

fof(d9_seq_1,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => k19_seq_1(A,B) = k11_seq_1(A,k18_seq_1(B)) ) ) ),
    file(seq_1,d9_seq_1),
    [interesting(0.00)]).

fof(d8_seq_1,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( B = k18_seq_1(A)
          <=> ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => k2_seq_1(k5_numbers,k1_numbers,B,C) = k2_real_1(k2_seq_1(k5_numbers,k1_numbers,A,C)) ) ) ) ) ),
    file(seq_1,d8_seq_1),
    [interesting(0.00)]).

fof(l10_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => k2_seq_1(k5_numbers,k1_numbers,k19_seq_1(A,B),C) = k6_real_1(k2_seq_1(k5_numbers,k1_numbers,A,C),k2_seq_1(k5_numbers,k1_numbers,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_seq_1,t12_seq_1,d8_seq_1,d9_xcmplx_0]),
    [file(asympt_1,l10_asympt_1),interesting(0.00)]).

fof(t34_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( ~ r1_xreal_0(A,0)
               => k3_power(A,k6_xcmplx_0(B,C)) = k7_xcmplx_0(k3_power(A,B),k3_power(A,C)) ) ) ) ) ),
    file(power,t34_power),
    [interesting(0.00)]).

fof(t42_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ~ ( ~ r1_xreal_0(A,0)
                  & ~ r1_xreal_0(B,A)
                  & ~ r1_xreal_0(C,0)
                  & r1_xreal_0(k3_power(B,C),k3_power(A,C)) ) ) ) ) ),
    file(power,t42_power),
    [interesting(0.00)]).

fof(t38_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( ~ r1_xreal_0(A,0)
               => k3_power(k3_power(A,B),C) = k3_power(A,k3_xcmplx_0(B,C)) ) ) ) ) ),
    file(power,t38_power),
    [interesting(0.00)]).

fof(t152_real_2,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( r1_xreal_0(A,B)
           => ( ( r1_xreal_0(A,0)
                & r1_xreal_0(0,B) )
              | r1_xreal_0(k7_xcmplx_0(1,B),k7_xcmplx_0(1,A)) ) ) ) ) ),
    file(real_2,t152_real_2),
    [interesting(0.00)]).

fof(t218_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(1,k5_xcmplx_0(A)) = A ) ),
    file(xcmplx_1,t218_xcmplx_1),
    [interesting(0.00)]).

fof(t33_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ~ r1_xreal_0(A,0)
           => k3_power(A,k4_xcmplx_0(B)) = k7_xcmplx_0(1,k3_power(A,B)) ) ) ) ),
    file(power,t33_power),
    [interesting(0.00)]).

fof(t151_real_2,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ~ ( ~ ( r1_xreal_0(A,0)
                  & r1_xreal_0(0,B) )
              & ~ r1_xreal_0(B,A)
              & r1_xreal_0(k7_xcmplx_0(1,A),k7_xcmplx_0(1,B)) ) ) ) ),
    file(real_2,t151_real_2),
    [interesting(0.00)]).

fof(d1_absvalue,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( ( r1_xreal_0(0,A)
         => k16_complex1(A) = A )
        & ( ~ r1_xreal_0(0,A)
         => k16_complex1(A) = k4_xcmplx_0(A) ) ) ) ),
    file(absvalue,d1_absvalue),
    [interesting(0.00)]).

fof(d6_seq_2,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v4_seq_2(A)
      <=> ? [B] : 
            ( v1_xreal_0(B)
            & ! [C] : 
                ( v1_xreal_0(C)
               => ~ ( ~ r1_xreal_0(C,0)
                    & ! [D] : 
                        ( m2_subset_1(D,k1_numbers,k5_numbers)
                       => ? [E] : 
                            ( m2_subset_1(E,k1_numbers,k5_numbers)
                            & r1_xreal_0(D,E)
                            & r1_xreal_0(C,k18_complex1(k6_xcmplx_0(k2_seq_1(k5_numbers,k1_numbers,A,E),B))) ) ) ) ) ) ) ) ),
    file(seq_2,d6_seq_2),
    [interesting(0.00)]).

fof(d7_seq_2,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v4_seq_2(A)
       => ! [B] : 
            ( v1_xreal_0(B)
           => ( B = k1_seq_2(A)
            <=> ! [C] : 
                  ( v1_xreal_0(C)
                 => ~ ( ~ r1_xreal_0(C,0)
                      & ! [D] : 
                          ( m2_subset_1(D,k1_numbers,k5_numbers)
                         => ? [E] : 
                              ( m2_subset_1(E,k1_numbers,k5_numbers)
                              & r1_xreal_0(D,E)
                              & r1_xreal_0(C,k18_complex1(k6_xcmplx_0(k2_seq_1(k5_numbers,k1_numbers,A,E),B))) ) ) ) ) ) ) ) ) ),
    file(seq_2,d7_seq_2),
    [interesting(0.00)]).

fof(t16_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v4_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v4_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( v4_seq_2(k19_seq_1(A,B))
              & k2_seq_2(k19_seq_1(A,B)) = 0 )
           => ( r2_hidden(A,k5_asympt_0(B))
              & ~ r2_hidden(B,k5_asympt_0(A)) ) ) ) ) ),
    file(asympt_0,t16_asympt_0),
    [interesting(0.00)]).

fof(t19_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( r2_hidden(A,k6_asympt_0(B))
          <=> r2_hidden(B,k5_asympt_0(A)) ) ) ) ),
    file(asympt_0,t19_asympt_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(t17_asympt_1,theorem,
    ( ~ r1_xreal_0(k6_real_1(159,100),k6_power(2,3))
   => ( r2_hidden(k3_asympt_1(k6_power(2,3)),k5_asympt_0(k3_asympt_1(k6_real_1(159,100))))
      & ~ r2_hidden(k3_asympt_1(k6_power(2,3)),k6_asympt_0(k3_asympt_1(k6_real_1(159,100))))
      & ~ r2_hidden(k3_asympt_1(k6_power(2,3)),k7_asympt_0(k3_asympt_1(k6_real_1(159,100)))) ) ),
    inference(mizar_proof,[status(thm)],[t11_xreal_1,t70_xreal_1,d9_xcmplx_0,d1_xreal_0,t46_square_1,t2_xreal_1,t49_square_1,t16_int_1,t124_xreal_1,t217_xcmplx_1,d5_int_1,t2_xreal_1,t39_power,t2_xreal_1,l10_asympt_1,d3_asympt_1,d3_asympt_1,t34_power,t2_xreal_1,l13_asympt_1,t38_power,t88_xcmplx_1,t30_power,t152_real_2,t217_xcmplx_1,t218_xcmplx_1,t33_power,t39_power,t70_xreal_1,t44_power,t151_real_2,t33_power,t33_power,t2_xreal_1,t39_power,d1_absvalue,d6_seq_2,d7_seq_2,t16_asympt_0,t19_asympt_0,t16_asympt_0,t19_asympt_0,d3_xboole_0]),
    [file(asympt_1,t17_asympt_1),interesting(0.00)]).

fof(d4_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v2_asympt_0(A)
      <=> ? [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
            & ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => ( r1_xreal_0(B,C)
                 => r1_xreal_0(0,k2_seq_1(k5_numbers,k1_numbers,A,C)) ) ) ) ) ) ),
    file(asympt_0,d4_asympt_0),
    [interesting(0.00)]).

fof(t62_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ( k4_nat_1(A,2) = 0
        | k4_nat_1(A,2) = 1 ) ) ),
    file(nat_1,t62_nat_1),
    [interesting(0.00)]).

fof(t8_euler_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)
             => k4_nat_1(k1_nat_1(A,B),C) = k4_nat_1(k1_nat_1(k4_nat_1(A,C),k4_nat_1(B,C)),C) ) ) ) ),
    file(euler_2,t8_euler_2),
    [interesting(0.00)]).

fof(t64_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( ~ r1_xreal_0(A,1)
           => k4_nat_1(1,A) = 1 ) ) ) ),
    file(nat_1,t64_nat_1),
    [interesting(0.00)]).

fof(t77_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => k4_nat_1(A,A) = 0 ) ),
    file(nat_1,t77_nat_1),
    [interesting(0.00)]).

fof(t78_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => 0 = k4_nat_1(0,A) ) ),
    file(nat_1,t78_nat_1),
    [interesting(0.00)]).

fof(t10_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => r2_hidden(A,k5_asympt_0(A)) ) ),
    file(asympt_0,t10_asympt_0),
    [interesting(0.00)]).

fof(t12_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & v2_asympt_0(C)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( ( r2_hidden(A,k5_asympt_0(B))
                  & r2_hidden(B,k5_asympt_0(C)) )
               => r2_hidden(A,k5_asympt_0(C)) ) ) ) ) ),
    file(asympt_0,t12_asympt_0),
    [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(t19_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( k5_asympt_0(A) = k5_asympt_0(B)
          <=> r2_hidden(A,k7_asympt_0(B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_asympt_0,t10_asympt_0,t19_asympt_0,d3_xboole_0,d4_asympt_0,d3_xboole_0,t12_asympt_0,d4_asympt_0,d3_xboole_0,t19_asympt_0,t12_asympt_0,t2_tarski]),
    [file(asympt_1,t19_asympt_1),interesting(0.00)]).

fof(d6_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v4_asympt_0(A)
      <=> ? [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
            & ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => ~ ( r1_xreal_0(B,C)
                    & r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,C),0) ) ) ) ) ) ),
    file(asympt_0,d6_asympt_0),
    [interesting(0.00)]).

fof(t65_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ~ ( ~ r1_xreal_0(A,1)
                  & ~ r1_xreal_0(B,0)
                  & ~ r1_xreal_0(C,B)
                  & r1_xreal_0(k5_power(A,C),k5_power(A,B)) ) ) ) ) ),
    file(power,t65_power),
    [interesting(0.00)]).

fof(t199_real_2,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,0)
                          & r1_xreal_0(A,B)
                          & ~ r1_xreal_0(C,0)
                          & ~ r1_xreal_0(D,C) )
                        | ( ~ r1_xreal_0(0,A)
                          & r1_xreal_0(B,A)
                          & ~ r1_xreal_0(0,C)
                          & ~ r1_xreal_0(C,D) ) )
                      & r1_xreal_0(k3_xcmplx_0(B,D),k3_xcmplx_0(A,C)) ) ) ) ) ) ),
    file(real_2,t199_real_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(s3_funct_2,theorem,
    ( ! [A] : 
        ( m1_subset_1(A,f1_s3_funct_2)
       => ? [B] : 
            ( m1_subset_1(B,f2_s3_funct_2)
            & p1_s3_funct_2(A,B) ) )
   => ? [A] : 
        ( v1_funct_1(A)
        & v1_funct_2(A,f1_s3_funct_2,f2_s3_funct_2)
        & m2_relset_1(A,f1_s3_funct_2,f2_s3_funct_2)
        & ! [B] : 
            ( m1_subset_1(B,f1_s3_funct_2)
           => p1_s3_funct_2(B,k8_funct_2(f1_s3_funct_2,f2_s3_funct_2,A,B)) ) ) ),
    file(funct_2,s3_funct_2),
    [interesting(0.00)]).

fof(t11_seq_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( A = k6_seq_1(k5_numbers,k1_numbers,B,C)
              <=> ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k2_seq_1(k5_numbers,k1_numbers,A,D) = k3_real_1(k2_seq_1(k5_numbers,k1_numbers,B,D),k2_seq_1(k5_numbers,k1_numbers,C,D)) ) ) ) ) ) ),
    file(seq_1,t11_seq_1),
    [interesting(0.00)]).

fof(t9_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => k5_asympt_0(k1_asympt_0(A,B)) = k5_asympt_0(k4_asympt_0(A,B)) ) ) ),
    file(asympt_0,t9_asympt_0),
    [interesting(0.00)]).

fof(t63_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ~ ( ~ r1_xreal_0(A,0)
                  & A != 1
                  & ~ r1_xreal_0(B,0)
                  & k5_power(A,k3_power(B,C)) != k3_xcmplx_0(C,k5_power(A,B)) ) ) ) ) ),
    file(power,t63_power),
    [interesting(0.00)]).

fof(t77_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( r1_xreal_0(0,A)
              & r1_xreal_0(A,B) )
           => r1_xreal_0(k5_square_1(A),k5_square_1(B)) ) ) ) ),
    file(square_1,t77_square_1),
    [interesting(0.00)]).

fof(t61_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ~ ( ~ r1_xreal_0(A,0)
                  & A != 1
                  & ~ r1_xreal_0(B,0)
                  & ~ r1_xreal_0(C,0)
                  & k2_xcmplx_0(k5_power(A,B),k5_power(A,C)) != k5_power(A,k3_xcmplx_0(B,C)) ) ) ) ) ),
    file(power,t61_power),
    [interesting(0.00)]).

fof(t20_int_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( v1_int_1(B)
         => ( ~ r1_xreal_0(B,A)
           => r1_xreal_0(k2_xcmplx_0(A,1),B) ) ) ) ),
    file(int_1,t20_int_1),
    [interesting(0.00)]).

fof(d10_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( C = k4_asympt_0(A,B)
              <=> ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k2_seq_1(k5_numbers,k1_numbers,C,D) = k4_square_1(k2_seq_1(k5_numbers,k1_numbers,A,D),k2_seq_1(k5_numbers,k1_numbers,B,D)) ) ) ) ) ) ),
    file(asympt_0,d10_asympt_0),
    [interesting(0.00)]).

fof(d2_square_1,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( r1_xreal_0(B,A)
             => k2_square_1(A,B) = A )
            & ( ~ r1_xreal_0(B,A)
             => k2_square_1(A,B) = B ) ) ) ) ),
    file(square_1,d2_square_1),
    [interesting(0.00)]).

fof(t92_real_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(k6_xcmplx_0(A,D),k6_xcmplx_0(B,C)) )
                    & ~ ( ( ( ~ r1_xreal_0(B,A)
                            & r1_xreal_0(C,D) )
                          | ( r1_xreal_0(A,B)
                            & ~ r1_xreal_0(D,C) ) )
                        & r1_xreal_0(k6_xcmplx_0(B,C),k6_xcmplx_0(A,D)) ) ) ) ) ) ) ),
    file(real_1,t92_real_1),
    [interesting(0.00)]).

fof(t1_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ~ ( k2_seq_1(k5_numbers,k1_numbers,A,0) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,0)
                   => k2_seq_1(k5_numbers,k1_numbers,A,C) = k3_real_1(k3_real_1(k5_real_1(k4_real_1(k2_nat_1(12,k3_series_1(C,3)),k6_power(2,C)),k4_real_1(5,k7_square_1(C))),k7_square_1(k6_power(2,C))),36) ) )
              & k2_seq_1(k5_numbers,k1_numbers,B,0) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,0)
                   => k2_seq_1(k5_numbers,k1_numbers,B,C) = k4_real_1(k3_series_1(C,3),k6_power(2,C)) ) )
              & ! [C] : 
                  ( ( v1_funct_1(C)
                    & v1_funct_2(C,k5_numbers,k1_numbers)
                    & v4_asympt_0(C)
                    & m2_relset_1(C,k5_numbers,k1_numbers) )
                 => ! [D] : 
                      ( ( v1_funct_1(D)
                        & v1_funct_2(D,k5_numbers,k1_numbers)
                        & v4_asympt_0(D)
                        & m2_relset_1(D,k5_numbers,k1_numbers) )
                     => ~ ( C = A
                          & D = B
                          & r2_hidden(C,k5_asympt_0(D)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_asympt_0,t2_xreal_1,t44_power,t39_power,t12_pre_ff,t65_power,t60_power,t2_xreal_1,t199_real_2,t199_real_2,t53_power,t22_xreal_1,t72_square_1,t10_xreal_1,t10_xreal_1,d6_asympt_0,t12_pre_ff,t60_power,t39_power,t70_xreal_1,s3_funct_2,d6_asympt_0,t2_xreal_1,t44_power,t39_power,t12_pre_ff,t65_power,t60_power,t2_xreal_1,t199_real_2,t199_real_2,t53_power,t22_xreal_1,s3_funct_2,d6_asympt_0,t72_square_1,t10_xreal_1,t11_seq_1,t9_asympt_0,t53_power,t63_power,t60_power,t8_xreal_1,t2_xreal_1,t8_xreal_1,t12_pre_ff,t10_xreal_1,t12_pre_ff,t77_square_1,t8_xreal_1,t61_power,t60_power,t2_xreal_1,l1_asympt_1,t12_pre_ff,t10_xreal_1,t2_xreal_1,t65_power,t63_power,t60_power,t199_real_2,t10_xreal_1,t8_xreal_1,t8_xreal_1,t2_xreal_1,t2_xreal_1,s1_int_2,t2_xreal_1,t44_power,t39_power,t12_pre_ff,t2_xreal_1,t199_real_2,t70_xreal_1,t53_power,t11_xreal_1,t2_xreal_1,d10_asympt_0,d2_square_1,t11_funct_2,d6_asympt_0,t46_square_1,t2_xreal_1,t39_power,t53_power,t70_xreal_1,t92_real_1,t10_asympt_0,t12_asympt_0]),
    [file(asympt_1,t1_asympt_1),interesting(0.00)]).

fof(t30_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & v2_asympt_0(C)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( ( r2_hidden(A,k7_asympt_0(B))
                  & r2_hidden(B,k7_asympt_0(C)) )
               => r2_hidden(A,k7_asympt_0(C)) ) ) ) ) ),
    file(asympt_0,t30_asympt_0),
    [interesting(0.00)]).

fof(t29_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( r2_hidden(A,k7_asympt_0(B))
           => r2_hidden(B,k7_asympt_0(A)) ) ) ) ),
    file(asympt_0,t29_asympt_0),
    [interesting(0.00)]).

fof(t28_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => r2_hidden(A,k7_asympt_0(A)) ) ),
    file(asympt_0,t28_asympt_0),
    [interesting(0.00)]).

fof(t20_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( r2_hidden(A,k7_asympt_0(B))
          <=> k7_asympt_0(A) = k7_asympt_0(B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t27_asympt_0,t27_asympt_0,d4_asympt_0,d4_asympt_0,t46_square_1,t2_xreal_1,t66_xreal_1,d4_asympt_0,t30_asympt_0,t46_square_1,t2_xreal_1,t66_xreal_1,d4_asympt_0,t29_asympt_0,t30_asympt_0,t2_tarski,t28_asympt_0]),
    [file(asympt_1,t20_asympt_1),interesting(0.00)]).

fof(t60_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( A != 0
       => k7_xcmplx_0(A,A) = 1 ) ) ),
    file(xcmplx_1,t60_xcmplx_1),
    [interesting(0.00)]).

fof(t100_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k3_xcmplx_0(A,k7_xcmplx_0(1,B)) = k7_xcmplx_0(A,B) ) ) ),
    file(xcmplx_1,t100_xcmplx_1),
    [interesting(0.00)]).

fof(t107_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( A != 0
       => k3_xcmplx_0(A,k7_xcmplx_0(1,A)) = 1 ) ) ),
    file(xcmplx_1,t107_xcmplx_1),
    [interesting(0.00)]).

fof(t59_int_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( k1_int_1(A) = k2_int_1(A)
      <=> v1_int_1(A) ) ) ),
    file(int_1,t59_int_1),
    [interesting(0.00)]).

fof(t78_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ~ ( r1_xreal_0(0,A)
              & ~ r1_xreal_0(B,A)
              & r1_xreal_0(k5_square_1(B),k5_square_1(A)) ) ) ) ),
    file(square_1,t78_square_1),
    [interesting(0.00)]).

fof(t66_int_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( k1_int_1(A) = k2_int_1(A)
      <=> k2_xcmplx_0(k1_int_1(A),1) != k2_int_1(A) ) ) ),
    file(int_1,t66_int_1),
    [interesting(0.00)]).

fof(d4_int_1,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_int_1(B)
         => ( B = k1_int_1(A)
          <=> ( r1_xreal_0(B,A)
              & ~ r1_xreal_0(B,k6_xcmplx_0(A,1)) ) ) ) ) ),
    file(int_1,d4_int_1),
    [interesting(0.00)]).

fof(t178_real_2,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( ~ ( ~ r1_xreal_0(A,0)
                    & ~ r1_xreal_0(C,k3_xcmplx_0(B,A))
                    & r1_xreal_0(k7_xcmplx_0(C,A),B) )
                & ~ ( ~ r1_xreal_0(0,A)
                    & ~ r1_xreal_0(C,k3_xcmplx_0(B,A))
                    & r1_xreal_0(B,k7_xcmplx_0(C,A)) )
                & ~ ( ~ r1_xreal_0(A,0)
                    & ~ r1_xreal_0(k3_xcmplx_0(B,A),C)
                    & r1_xreal_0(B,k7_xcmplx_0(C,A)) )
                & ~ ( ~ r1_xreal_0(0,A)
                    & ~ r1_xreal_0(k3_xcmplx_0(B,A),C)
                    & r1_xreal_0(k7_xcmplx_0(C,A),B) ) ) ) ) ) ),
    file(real_2,t178_real_2),
    [interesting(0.00)]).

fof(t79_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k7_xcmplx_0(A,k3_xcmplx_0(B,C)) = k7_xcmplx_0(k7_xcmplx_0(A,B),C) ) ) ) ),
    file(xcmplx_1,t79_xcmplx_1),
    [interesting(0.00)]).

fof(d2_asympt_1,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( A = k2_asympt_1
      <=> ( k2_seq_1(k5_numbers,k1_numbers,A,0) = 0
          & ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ( ~ r1_xreal_0(B,0)
               => k2_seq_1(k5_numbers,k1_numbers,A,B) = k6_power(2,B) ) ) ) ) ) ),
    file(asympt_1,d2_asympt_1),
    [interesting(0.00)]).

fof(t22_seq_2,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( v4_seq_2(B)
           => k2_seq_2(k14_seq_1(B,A)) = k3_xcmplx_0(A,k2_seq_2(B)) ) ) ) ),
    file(seq_2,t22_seq_2),
    [interesting(0.00)]).

fof(t21_seq_2,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( v4_seq_2(B)
           => v4_seq_2(k14_seq_1(B,A)) ) ) ) ),
    file(seq_2,t21_seq_2),
    [interesting(0.00)]).

fof(l53_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ! [D] : 
                  ( m1_subset_1(D,k1_numbers)
                 => ( ( v4_seq_2(A)
                      & k2_seq_2(A) = D
                      & ! [E] : 
                          ( m2_subset_1(E,k1_numbers,k5_numbers)
                         => ( r1_xreal_0(C,E)
                           => k2_seq_1(k5_numbers,k1_numbers,A,E) = k2_seq_1(k5_numbers,k1_numbers,B,E) ) ) )
                   => ( v4_seq_2(B)
                      & k2_seq_2(B) = D ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_seq_2,t46_square_1,t2_xreal_1,d6_seq_2,d7_seq_2]),
    [file(asympt_1,l53_asympt_1),interesting(0.00)]).

fof(t11_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( r2_hidden(A,k5_asympt_0(B))
           => r1_tarski(k5_asympt_0(A),k5_asympt_0(B)) ) ) ) ),
    file(asympt_0,t11_asympt_0),
    [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(l11_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( r2_hidden(A,k5_asympt_0(B))
              & r2_hidden(B,k5_asympt_0(A)) )
          <=> k5_asympt_0(A) = k5_asympt_0(B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t11_asympt_0,d10_xboole_0,t10_asympt_0]),
    [file(asympt_1,l11_asympt_1),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(t4_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( r1_tarski(k5_asympt_0(A),k5_asympt_0(B))
             => ( k5_asympt_0(A) = k5_asympt_0(B)
                | ( r2_hidden(A,k5_asympt_0(B))
                  & ~ r2_hidden(A,k6_asympt_0(B)) ) ) )
            & ( r2_hidden(A,k5_asympt_0(B))
             => ( r2_hidden(A,k6_asympt_0(B))
                | ( r1_tarski(k5_asympt_0(A),k5_asympt_0(B))
                  & k5_asympt_0(A) != k5_asympt_0(B) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_asympt_0,t19_asympt_0,l11_asympt_1,d4_asympt_0,t12_asympt_0,d3_tarski,l11_asympt_1,t19_asympt_0]),
    [file(asympt_1,t4_asympt_1),interesting(0.00)]).

fof(t215_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k5_xcmplx_0(k7_xcmplx_0(A,B)) = k7_xcmplx_0(B,A) ) ) ),
    file(xcmplx_1,t215_xcmplx_1),
    [interesting(0.00)]).

fof(t103_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k3_xcmplx_0(k7_xcmplx_0(1,A),k7_xcmplx_0(1,B)) = k7_xcmplx_0(1,k3_xcmplx_0(A,B)) ) ) ),
    file(xcmplx_1,t103_xcmplx_1),
    [interesting(0.00)]).

fof(t56_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(1,k7_xcmplx_0(1,A)) = A ) ),
    file(xcmplx_1,t56_xcmplx_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(t35_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ~ ( ~ r1_xreal_0(A,0)
                  & ~ r1_xreal_0(B,0)
                  & k3_power(k3_xcmplx_0(A,B),C) != k3_xcmplx_0(k3_power(A,C),k3_power(B,C)) ) ) ) ) ),
    file(power,t35_power),
    [interesting(0.00)]).

fof(l41_asympt_1,theorem,(
    ! [A] : 
      ( ( v2_xreal_0(A)
        & m1_subset_1(A,k1_numbers) )
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k1_numbers)
             => v4_asympt_0(k1_asympt_1(A,B,C)) ) ) ) ),
    file(asympt_1,l41_asympt_1),
    [interesting(0.00)]).

fof(t57_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k7_xcmplx_0(1,k7_xcmplx_0(A,B)) = k7_xcmplx_0(B,A) ) ) ),
    file(xcmplx_1,t57_xcmplx_1),
    [interesting(0.00)]).

fof(l56_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ~ ( ~ r1_xreal_0(A,0)
          & ~ r1_xreal_0(1,A)
          & ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ? [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                  & r1_xreal_0(B,C)
                  & r1_xreal_0(k5_real_1(k4_real_1(C,k6_power(2,k3_real_1(1,A))),k4_real_1(8,k6_power(2,C))),k4_real_1(8,k6_power(2,C))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l23_asympt_1,t8_xreal_1,t65_power,t59_power,t70_xreal_1,d7_seq_2,t46_square_1,t2_xreal_1,t12_pre_ff,t60_power,l10_asympt_1,d2_asympt_1,d3_asympt_1,t39_power,t124_xreal_1,t70_xreal_1,d9_xcmplx_0,d1_absvalue,t2_xreal_1,t44_power,t151_real_2,t30_power,t70_xreal_1,t100_xcmplx_1,t100_xcmplx_1,t2_xreal_1,t124_xreal_1,t70_xreal_1,d9_xcmplx_0,t151_real_2,t57_xcmplx_1,t57_xcmplx_1,t70_xreal_1,t88_xcmplx_1,t70_xreal_1,t88_xcmplx_1,t11_xreal_1]),
    [file(asympt_1,l56_asympt_1),interesting(0.00)]).

fof(l6_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k1_numbers)
             => ~ ( ~ r1_xreal_0(A,0)
                  & ~ r1_xreal_0(C,0)
                  & C != 1
                  & k4_power(A,B) != k4_power(C,k4_real_1(B,k6_power(C,A))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t39_power,t63_power,d3_power]),
    [file(asympt_1,l6_asympt_1),interesting(0.00)]).

fof(t73_real_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( ~ r1_xreal_0(A,0)
               => ( ~ ( ~ r1_xreal_0(C,B)
                      & r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A)) )
                  & ~ ( ~ r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A))
                      & r1_xreal_0(C,B) ) ) ) ) ) ) ),
    file(real_1,t73_real_1),
    [interesting(0.00)]).

fof(t14_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k6_xcmplx_0(A,A) = 0 ) ),
    file(xcmplx_1,t14_xcmplx_1),
    [interesting(0.00)]).

fof(t36_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ~ ( ~ r1_xreal_0(A,0)
                  & ~ r1_xreal_0(B,0)
                  & k3_power(k7_xcmplx_0(A,B),C) != k7_xcmplx_0(k3_power(A,C),k3_power(B,C)) ) ) ) ) ),
    file(power,t36_power),
    [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(t95_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ~ ( r1_xreal_0(0,A)
              & ~ r1_xreal_0(B,A)
              & r1_xreal_0(k8_square_1(B),k8_square_1(A)) ) ) ) ),
    file(square_1,t95_square_1),
    [interesting(0.00)]).

fof(t89_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( r1_xreal_0(0,A)
       => k8_square_1(k5_square_1(A)) = A ) ) ),
    file(square_1,t89_square_1),
    [interesting(0.00)]).

fof(t71_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ~ ( ~ r1_xreal_0(0,A)
                  & ~ r1_xreal_0(C,B)
                  & r1_xreal_0(k3_xcmplx_0(B,A),k3_xcmplx_0(C,A)) ) ) ) ) ),
    file(xreal_1,t71_xreal_1),
    [interesting(0.00)]).

fof(t82_square_1,theorem,(
    k9_square_1(0) = 0 ),
    file(square_1,t82_square_1),
    [interesting(0.00)]).

fof(t93_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ~ ( ~ r1_xreal_0(A,0)
          & r1_xreal_0(k8_square_1(A),0) ) ) ),
    file(square_1,t93_square_1),
    [interesting(0.00)]).

fof(d4_square_1,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( r1_xreal_0(0,A)
       => ! [B] : 
            ( v1_xreal_0(B)
           => ( B = k8_square_1(A)
            <=> ( r1_xreal_0(0,B)
                & k5_square_1(B) = A ) ) ) ) ) ),
    file(square_1,d4_square_1),
    [interesting(0.00)]).

fof(t26_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( r1_xreal_0(A,B)
          <=> r1_xreal_0(k4_xcmplx_0(B),k4_xcmplx_0(A)) ) ) ) ),
    file(xreal_1,t26_xreal_1),
    [interesting(0.00)]).

fof(t177_real_2,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( ( r1_xreal_0(k3_xcmplx_0(B,A),C)
                 => ( r1_xreal_0(A,0)
                    | r1_xreal_0(B,k7_xcmplx_0(C,A)) ) )
                & ( r1_xreal_0(k3_xcmplx_0(B,A),C)
                 => ( r1_xreal_0(0,A)
                    | r1_xreal_0(k7_xcmplx_0(C,A),B) ) )
                & ( r1_xreal_0(C,k3_xcmplx_0(B,A))
                 => ( r1_xreal_0(A,0)
                    | r1_xreal_0(k7_xcmplx_0(C,A),B) ) )
                & ( r1_xreal_0(C,k3_xcmplx_0(B,A))
                 => ( r1_xreal_0(0,A)
                    | r1_xreal_0(B,k7_xcmplx_0(C,A)) ) ) ) ) ) ) ),
    file(real_2,t177_real_2),
    [interesting(0.00)]).

fof(t7_absvalue,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( A = 0
      <=> k18_complex1(A) = 0 ) ) ),
    file(absvalue,t7_absvalue),
    [interesting(0.00)]).

fof(t15_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v4_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v4_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( v4_seq_2(k19_seq_1(A,B))
           => ( r1_xreal_0(k2_seq_2(k19_seq_1(A,B)),0)
              | k5_asympt_0(A) = k5_asympt_0(B) ) ) ) ) ),
    file(asympt_0,t15_asympt_0),
    [interesting(0.00)]).

fof(t28_asympt_1,theorem,(
    ? [A] : 
      ( v1_funct_1(A)
      & v1_funct_2(A,k5_numbers,k1_numbers)
      & v4_asympt_0(A)
      & m2_relset_1(A,k5_numbers,k1_numbers)
      & ? [B] : 
          ( v1_funct_1(B)
          & v1_funct_2(B,k5_numbers,k1_numbers)
          & v4_asympt_0(B)
          & m2_relset_1(B,k5_numbers,k1_numbers)
          & A = k1_asympt_1(2,1,0)
          & B = k1_asympt_1(2,1,1)
          & k5_asympt_0(A) = k5_asympt_0(B) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_asympt_1,d1_asympt_1,l10_asympt_1,t34_power,t33_power,t30_power,t7_absvalue,d6_seq_2,d7_seq_2,t15_asympt_0]),
    [file(asympt_1,t28_asympt_1),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(t29_asympt_1,theorem,(
    ? [A] : 
      ( v1_funct_1(A)
      & v1_funct_2(A,k5_numbers,k1_numbers)
      & v4_asympt_0(A)
      & m2_relset_1(A,k5_numbers,k1_numbers)
      & ? [B] : 
          ( v1_funct_1(B)
          & v1_funct_2(B,k5_numbers,k1_numbers)
          & v4_asympt_0(B)
          & m2_relset_1(B,k5_numbers,k1_numbers)
          & A = k1_asympt_1(2,1,0)
          & B = k1_asympt_1(2,2,0)
          & r1_tarski(k5_asympt_0(A),k5_asympt_0(B))
          & k5_asympt_0(A) != k5_asympt_0(B) ) ) ),
    inference(mizar_proof,[status(thm)],[l10_asympt_1,d1_asympt_1,d1_asympt_1,t34_power,t124_xreal_1,t217_xcmplx_1,t46_square_1,t49_square_1,t16_int_1,t39_power,d1_absvalue,t10_pre_ff,t10_pre_ff,t31_xreal_1,d5_int_1,t2_xreal_1,t44_power,t2_xreal_1,t2_xreal_1,d3_power,t70_xreal_1,t88_xcmplx_1,t39_power,t124_xreal_1,t70_xreal_1,t39_power,d7_xcmplx_0,t217_xcmplx_1,t33_power,d6_seq_2,d7_seq_2,t16_asympt_0,t19_asympt_0,t4_asympt_1]),
    [file(asympt_1,t29_asympt_1),interesting(0.00)]).

fof(d3_asympt_0,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( v1_asympt_0(A)
      <=> ( ~ r1_xreal_0(A,0)
          & A != 1 ) ) ) ),
    file(asympt_0,d3_asympt_0),
    [interesting(0.00)]).

fof(l3_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_asympt_0(A)
        & m1_subset_1(A,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( k2_seq_1(k5_numbers,k1_numbers,B,0) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,0)
                   => k2_seq_1(k5_numbers,k1_numbers,B,C) = k6_power(A,C) ) ) )
           => ( r1_xreal_0(A,1)
              | v4_asympt_0(B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_asympt_0,d5_int_1,d5_int_1,t16_int_1,t10_xreal_1,t2_xreal_1,t65_power,t12_pre_ff,t60_power,d6_asympt_0]),
    [file(asympt_1,l3_asympt_1),interesting(0.00)]).

fof(t2_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_asympt_0(A)
        & m1_subset_1(A,k1_numbers) )
     => ! [B] : 
          ( ( v1_asympt_0(B)
            & m1_subset_1(B,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k5_numbers,k1_numbers)
                    & m2_relset_1(D,k5_numbers,k1_numbers) )
                 => ~ ( ~ r1_xreal_0(A,1)
                      & ~ r1_xreal_0(B,1)
                      & k2_seq_1(k5_numbers,k1_numbers,C,0) = 0
                      & ! [E] : 
                          ( m2_subset_1(E,k1_numbers,k5_numbers)
                         => ( ~ r1_xreal_0(E,0)
                           => k2_seq_1(k5_numbers,k1_numbers,C,E) = k6_power(A,E) ) )
                      & k2_seq_1(k5_numbers,k1_numbers,D,0) = 0
                      & ! [E] : 
                          ( m2_subset_1(E,k1_numbers,k5_numbers)
                         => ( ~ r1_xreal_0(E,0)
                           => k2_seq_1(k5_numbers,k1_numbers,D,E) = k6_power(B,E) ) )
                      & ! [E] : 
                          ( ( v1_funct_1(E)
                            & v1_funct_2(E,k5_numbers,k1_numbers)
                            & v4_asympt_0(E)
                            & m2_relset_1(E,k5_numbers,k1_numbers) )
                         => ! [F] : 
                              ( ( v1_funct_1(F)
                                & v1_funct_2(F,k5_numbers,k1_numbers)
                                & v4_asympt_0(F)
                                & m2_relset_1(F,k5_numbers,k1_numbers) )
                             => ~ ( E = C
                                  & F = D
                                  & k5_asympt_0(E) = k5_asympt_0(F) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l3_asympt_1,l3_asympt_1,d3_asympt_0,d3_asympt_0,t65_power,t59_power,t70_xreal_1,t10_xreal_1,t2_xreal_1,t64_power,t65_power,t59_power,t70_xreal_1,t10_xreal_1,t2_xreal_1,t64_power,t2_tarski]),
    [file(asympt_1,t2_asympt_1),interesting(0.00)]).

fof(t92_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k7_xcmplx_0(B,C) = k7_xcmplx_0(k3_xcmplx_0(B,A),k3_xcmplx_0(C,A)) ) ) ) ) ),
    file(xcmplx_1,t92_xcmplx_1),
    [interesting(0.00)]).

fof(t20_newton,theorem,(
    k6_newton(2) = 2 ),
    file(newton,t20_newton),
    [interesting(0.00)]).

fof(t77_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k3_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,D)) = k7_xcmplx_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,D)) ) ) ) ) ),
    file(xcmplx_1,t77_xcmplx_1),
    [interesting(0.00)]).

fof(l70_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(10,A)
          & r1_xreal_0(k6_real_1(1,k4_power(2,k5_real_1(A,9))),k6_real_1(k3_series_1(2,k2_nat_1(2,A)),k11_newton(A))) ) ) ),
    inference(mizar_proof,[status(thm)],[t21_newton,t32_power,t30_power,t92_xcmplx_1,t21_newton,t21_newton,l15_asympt_1,t32_power,t92_xcmplx_1,t21_newton,l62_asympt_1,t32_power,l15_asympt_1,t32_power,t30_power,t21_newton,l69_asympt_1,t30_power,t39_power,t124_xreal_1,t70_xreal_1,d9_xcmplx_0,t39_power,t33_power,t32_power,t21_newton,t77_xcmplx_1,t70_xreal_1,t39_power,t66_xreal_1,d9_xcmplx_0,t32_power,l15_asympt_1,d9_xcmplx_0,t107_xcmplx_1,t66_xreal_1,t88_xcmplx_1,t21_xreal_1,t2_xreal_1,t70_xreal_1,t2_xreal_1,t103_xcmplx_1,t32_power,s1_int_2]),
    [file(asympt_1,l70_asympt_1),interesting(0.00)]).

fof(s1_seq_1,theorem,(
    ? [A] : 
      ( v1_funct_1(A)
      & v1_funct_2(A,k5_numbers,k1_numbers)
      & m2_relset_1(A,k5_numbers,k1_numbers)
      & ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => k2_seq_1(k5_numbers,k1_numbers,A,B) = f1_s1_seq_1(B) ) ) ),
    file(seq_1,s1_seq_1),
    [interesting(0.00)]).

fof(t85_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k7_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,D)) = k7_xcmplx_0(k3_xcmplx_0(A,D),k3_xcmplx_0(B,C)) ) ) ) ) ),
    file(xcmplx_1,t85_xcmplx_1),
    [interesting(0.00)]).

fof(l74_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k1_numbers)
             => ! [D] : 
                  ( m1_subset_1(D,k1_numbers)
                 => k6_real_1(k6_real_1(A,B),k6_real_1(C,D)) = k4_real_1(k6_real_1(A,C),k6_real_1(D,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t85_xcmplx_1,t77_xcmplx_1]),
    [file(asympt_1,l74_asympt_1),interesting(0.00)]).

fof(t104_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k3_xcmplx_0(k7_xcmplx_0(1,A),k7_xcmplx_0(B,C)) = k7_xcmplx_0(B,k3_xcmplx_0(C,A)) ) ) ) ),
    file(xcmplx_1,t104_xcmplx_1),
    [interesting(0.00)]).

fof(t75_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k3_xcmplx_0(A,k7_xcmplx_0(B,C)) = k7_xcmplx_0(k3_xcmplx_0(A,B),C) ) ) ) ),
    file(xcmplx_1,t75_xcmplx_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(t114_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k2_xcmplx_0(k7_xcmplx_0(B,A),C) = k7_xcmplx_0(k2_xcmplx_0(B,k3_xcmplx_0(A,C)),A) ) ) ) ) ),
    file(xcmplx_1,t114_xcmplx_1),
    [interesting(0.00)]).

fof(t121_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,B)) = k7_xcmplx_0(k6_xcmplx_0(A,C),B) ) ) ) ),
    file(xcmplx_1,t121_xcmplx_1),
    [interesting(0.00)]).

fof(t137_real_2,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ~ ( ( ( ~ r1_xreal_0(A,1)
                  & ~ ( r1_xreal_0(B,1)
                      & ~ r1_xreal_0(1,B) ) )
                | ( ~ r1_xreal_0(k4_xcmplx_0(1),A)
                  & ~ ( r1_xreal_0(k4_xcmplx_0(1),B)
                      & ~ r1_xreal_0(B,k4_xcmplx_0(1)) ) ) )
              & r1_xreal_0(k3_xcmplx_0(A,B),1) ) ) ) ),
    file(real_2,t137_real_2),
    [interesting(0.00)]).

fof(t2_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ~ ( ~ r1_xreal_0(A,1)
          & r1_xreal_0(1,k7_xcmplx_0(1,A)) ) ) ),
    file(square_1,t2_square_1),
    [interesting(0.00)]).

fof(t56_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( ~ r1_xreal_0(A,k1_real_1(1))
           => r1_xreal_0(k2_xcmplx_0(1,k3_xcmplx_0(B,A)),k3_power(k2_xcmplx_0(1,A),B)) ) ) ) ),
    file(power,t56_power),
    [interesting(0.00)]).

fof(t84_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k7_xcmplx_0(k3_xcmplx_0(A,B),k3_xcmplx_0(C,D)) = k7_xcmplx_0(k3_xcmplx_0(k7_xcmplx_0(A,C),B),D) ) ) ) ) ),
    file(xcmplx_1,t84_xcmplx_1),
    [interesting(0.00)]).

fof(t128_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k6_xcmplx_0(B,k7_xcmplx_0(C,A)) = k7_xcmplx_0(k6_xcmplx_0(k3_xcmplx_0(B,A),C),A) ) ) ) ) ),
    file(xcmplx_1,t128_xcmplx_1),
    [interesting(0.00)]).

fof(t118_real_2,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ~ r1_xreal_0(A,0)
           => ( ( r1_xreal_0(1,k7_xcmplx_0(B,A))
               => r1_xreal_0(A,B) )
              & ( r1_xreal_0(k7_xcmplx_0(B,A),1)
               => r1_xreal_0(B,A) )
              & ( r1_xreal_0(k4_xcmplx_0(1),k7_xcmplx_0(B,A))
               => ( r1_xreal_0(k4_xcmplx_0(A),B)
                  & r1_xreal_0(k4_xcmplx_0(B),A) ) )
              & ( r1_xreal_0(k7_xcmplx_0(B,A),k4_xcmplx_0(1))
               => ( r1_xreal_0(B,k4_xcmplx_0(A))
                  & r1_xreal_0(A,k4_xcmplx_0(B)) ) ) ) ) ) ) ),
    file(real_2,t118_real_2),
    [interesting(0.00)]).

fof(d13_seqm_3,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v3_seqm_3(A)
      <=> ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,B),k2_seq_1(k5_numbers,k1_numbers,A,k1_nat_1(B,1))) ) ) ) ),
    file(seqm_3,d13_seqm_3),
    [interesting(0.00)]).

fof(t63_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k2_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,B)) = k7_xcmplx_0(k2_xcmplx_0(A,C),B) ) ) ) ),
    file(xcmplx_1,t63_xcmplx_1),
    [interesting(0.00)]).

fof(l78_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ( r1_xreal_0(1,A)
       => r1_xreal_0(k4_power(k6_real_1(k1_nat_1(A,1),A),A),k4_power(k6_real_1(k1_nat_1(A,2),k1_nat_1(A,1)),k1_nat_1(A,1))) ) ) ),
    inference(mizar_proof,[status(thm)],[s1_seq_1,l77_asympt_1,t21_xreal_1,t16_int_1,d13_seqm_3,t60_xcmplx_1,t63_xcmplx_1,t60_xcmplx_1,t63_xcmplx_1]),
    [file(asympt_1,l78_asympt_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(t101_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k7_xcmplx_0(A,k7_xcmplx_0(1,B)) = k3_xcmplx_0(A,B) ) ) ),
    file(xcmplx_1,t101_xcmplx_1),
    [interesting(0.00)]).

fof(d6_bhsp_4,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => k5_bhsp_4(A,B) = k2_seq_1(k5_numbers,k1_numbers,k1_series_1(A),B) ) ) ),
    file(bhsp_4,d6_bhsp_4),
    [interesting(0.00)]).

fof(d1_series_1,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( B = k1_series_1(A)
          <=> ( k8_funct_2(k5_numbers,k1_numbers,B,0) = k8_funct_2(k5_numbers,k1_numbers,A,0)
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => k8_funct_2(k5_numbers,k1_numbers,B,k1_nat_1(C,1)) = k3_real_1(k8_funct_2(k5_numbers,k1_numbers,B,C),k8_funct_2(k5_numbers,k1_numbers,A,k1_nat_1(C,1))) ) ) ) ) ) ),
    file(series_1,d1_series_1),
    [interesting(0.00)]).

fof(t48_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( A != 0
           => k3_power(A,B) = k2_newton(A,B) ) ) ) ),
    file(power,t48_power),
    [interesting(0.00)]).

fof(t41_newton,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v4_ordinal2(C)
             => k2_newton(k2_xcmplx_0(A,B),C) = k15_rvsum_1(k9_newton(A,B,C)) ) ) ) ),
    file(newton,t41_newton),
    [interesting(0.00)]).

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)) ) ) ),
    file(rvsum_1,t106_rvsum_1),
    [interesting(0.00)]).

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)) ) ) ),
    file(rvsum_1,t117_rvsum_1),
    [interesting(0.00)]).

fof(d4_newton,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v4_ordinal2(C)
             => ! [D] : 
                  ( m2_finseq_1(D,k1_numbers)
                 => ( D = k9_newton(A,B,C)
                  <=> ( k3_finseq_1(D) = k2_xcmplx_0(C,1)
                      & ! [E] : 
                          ( v4_ordinal2(E)
                         => ! [F] : 
                              ( v4_ordinal2(F)
                             => ! [G] : 
                                  ( v4_ordinal2(G)
                                 => ( ( r2_hidden(E,k4_finseq_1(D))
                                      & G = k6_xcmplx_0(E,1)
                                      & F = k6_xcmplx_0(C,G) )
                                   => k1_funct_1(D,E) = k3_xcmplx_0(k3_xcmplx_0(k8_newton(G,C),k2_newton(A,F)),k2_newton(B,G)) ) ) ) ) ) ) ) ) ) ) ),
    file(newton,d4_newton),
    [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(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(t6_newton,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,k1_numbers)
         => k3_finseq_1(k9_rvsum_1(A,B)) = k3_finseq_1(B) ) ) ),
    file(newton,t6_newton),
    [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(t39_newton,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => k1_funct_1(k9_newton(B,C,A),1) = k2_newton(B,A) ) ) ) ),
    file(newton,t39_newton),
    [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)) ) ) ) ) ),
    file(rvsum_1,t67_rvsum_1),
    [interesting(0.00)]).

fof(t58_finseq_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => k1_funct_1(k7_finseq_1(k9_finseq_1(A),B),1) = A ) ),
    file(finseq_1,t58_finseq_1),
    [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(t37_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] : 
              ( v4_ordinal2(C)
             => ( r1_xreal_0(C,k3_finseq_1(k7_finseq_1(A,B)))
               => ( r1_xreal_0(C,k3_finseq_1(A))
                  | k1_funct_1(k7_finseq_1(A,B),C) = k1_funct_1(B,k6_xcmplx_0(C,k3_finseq_1(A))) ) ) ) ) ) ),
    file(finseq_1,t37_finseq_1),
    [interesting(0.00)]).

fof(t30_newton,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( r1_xreal_0(B,A)
           => ! [C] : 
                ( v4_ordinal2(C)
               => ( C = k6_xcmplx_0(A,B)
                 => k8_newton(B,A) = k8_newton(C,A) ) ) ) ) ) ),
    file(newton,t30_newton),
    [interesting(0.00)]).

fof(t15_newton,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => k3_newton(1,A) = 1 ) ),
    file(newton,t15_newton),
    [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(d3_newton,definition,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ! [C] : 
              ( ( r1_xreal_0(A,B)
               => ( C = k7_newton(A,B)
                <=> ! [D] : 
                      ( v4_ordinal2(D)
                     => ( D = k6_xcmplx_0(B,A)
                       => C = k7_xcmplx_0(k6_newton(B),k3_xcmplx_0(k6_newton(A),k6_newton(D))) ) ) ) )
              & ( ~ r1_xreal_0(A,B)
               => ( C = k7_newton(A,B)
                <=> C = 0 ) ) ) ) ) ),
    file(newton,d3_newton),
    [interesting(0.00)]).

fof(l86_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( r1_xreal_0(A,B)
           => r1_xreal_0(k6_real_1(k8_newton(A,k1_nat_1(B,1)),k1_nat_1(B,1)),k8_newton(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_xreal_1,t2_xreal_1,t18_int_1,d3_newton,t21_newton,d9_xcmplx_0,d9_xcmplx_0,t77_xcmplx_1,t60_xcmplx_1,t21_newton,t77_xcmplx_1,d3_newton,t23_newton,t70_xreal_1,t124_xreal_1,t70_xreal_1,d9_xcmplx_0,d3_newton,t8_xreal_1,t152_real_2,t66_xreal_1]),
    [file(asympt_1,l86_asympt_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)) ) ) ) ) ),
    file(rvsum_1,t112_rvsum_1),
    [interesting(0.00)]).

fof(t33_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ( r1_xreal_0(1,A)
       => ! [B] : 
            ( ( v1_funct_1(B)
              & v1_funct_2(B,k5_numbers,k1_numbers)
              & m2_relset_1(B,k5_numbers,k1_numbers) )
           => ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => ( ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => k2_seq_1(k5_numbers,k1_numbers,B,D) = k5_bhsp_4(k3_asympt_1(C),D) )
                 => r1_xreal_0(k6_real_1(k3_series_1(A,k1_nat_1(C,1)),k1_nat_1(C,1)),k2_seq_1(k5_numbers,k1_numbers,B,A)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_bhsp_4,d1_series_1,d1_series_1,d3_asympt_1,t31_power,d3_asympt_1,t31_power,t8_xreal_1,t152_real_2,d6_bhsp_4,d1_series_1,d6_bhsp_4,t8_xreal_1,d3_asympt_1,t48_power,t41_newton,t106_rvsum_1,d9_xcmplx_0,t48_power,t41_newton,t117_rvsum_1,d4_newton,t57_finseq_1,t35_finseq_1,t110_finseq_2,t6_newton,d4_newton,t110_finseq_2,d4_newton,t110_finseq_2,t3_finseq_1,t39_newton,t67_rvsum_1,t48_power,d9_xcmplx_0,t58_finseq_1,t11_xreal_1,t16_int_1,t20_int_1,t21_xreal_1,t16_int_1,t22_xreal_1,t21_xreal_1,t16_int_1,t11_xreal_1,d4_newton,d3_finseq_1,t3_finseq_1,t37_finseq_1,d4_newton,t30_newton,t15_newton,t48_power,t21_xreal_1,d4_newton,d3_finseq_1,d4_newton,t67_rvsum_1,t30_newton,t15_newton,t48_power,t92_real_1,l86_asympt_1,d9_xcmplx_0,t66_xreal_1,d5_real_1,t112_rvsum_1,t2_xreal_1,s1_int_2]),
    [file(asympt_1,t33_asympt_1),interesting(0.00)]).

fof(t21_int_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ( ~ r1_xreal_0(0,A)
       => r1_xreal_0(A,k1_real_1(1)) ) ) ),
    file(int_1,t21_int_1),
    [interesting(0.00)]).

fof(l26_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => ( r1_xreal_0(C,B)
                 => r1_xreal_0(0,k2_seq_1(k5_numbers,k1_numbers,A,C)) ) )
           => r1_xreal_0(0,k5_bhsp_4(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_series_1,d6_bhsp_4,t9_xreal_1,t9_xreal_1,d6_bhsp_4,d1_series_1,d6_bhsp_4,s1_nat_1]),
    [file(asympt_1,l26_asympt_1),interesting(0.00)]).

fof(d7_bhsp_4,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => k6_bhsp_4(A,B,C) = k5_real_1(k5_bhsp_4(A,B),k5_bhsp_4(A,C)) ) ) ) ),
    file(bhsp_4,d7_bhsp_4),
    [interesting(0.00)]).

fof(t54_int_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( k2_int_1(A) = A
      <=> v1_int_1(A) ) ) ),
    file(int_1,t54_int_1),
    [interesting(0.00)]).

fof(l29_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => k3_real_1(k6_bhsp_4(A,B,C),k2_seq_1(k5_numbers,k1_numbers,A,k1_nat_1(B,1))) = k6_bhsp_4(A,k1_nat_1(B,1),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_bhsp_4,d6_bhsp_4,d1_series_1,d6_bhsp_4,d7_bhsp_4]),
    [file(asympt_1,l29_asympt_1),interesting(0.00)]).

fof(l30_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ! [D] : 
                  ( m2_subset_1(D,k1_numbers,k5_numbers)
                 => ( ( r1_xreal_0(k1_nat_1(C,1),D)
                      & ! [E] : 
                          ( m2_subset_1(E,k1_numbers,k5_numbers)
                         => ( ( r1_xreal_0(k1_nat_1(C,1),E)
                              & r1_xreal_0(E,D) )
                           => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,E),k2_seq_1(k5_numbers,k1_numbers,B,E)) ) ) )
                   => r1_xreal_0(k6_bhsp_4(A,D,C),k6_bhsp_4(B,D,C)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_bhsp_4,d6_bhsp_4,d1_series_1,d6_bhsp_4,d7_bhsp_4,d6_bhsp_4,d1_series_1,d6_bhsp_4,t9_xreal_1,t9_xreal_1,t9_xreal_1,l29_asympt_1,l29_asympt_1,s1_int_2]),
    [file(asympt_1,l30_asympt_1),interesting(0.00)]).

fof(l28_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( ( k2_seq_1(k5_numbers,k1_numbers,A,0) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,0)
                   => k2_seq_1(k5_numbers,k1_numbers,A,C) = B ) ) )
           => ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => k5_bhsp_4(A,C) = k4_real_1(B,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_series_1,d6_bhsp_4,d6_bhsp_4,d1_series_1,d6_bhsp_4,s1_nat_1]),
    [file(asympt_1,l28_asympt_1),interesting(0.00)]).

fof(l32_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ( ( k2_seq_1(k5_numbers,k1_numbers,A,0) = 0
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ( ~ r1_xreal_0(D,0)
                       => k2_seq_1(k5_numbers,k1_numbers,A,D) = B ) ) )
               => ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k6_bhsp_4(A,C,D) = k4_real_1(B,k5_real_1(C,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_bhsp_4,d1_series_1,d7_bhsp_4,l28_asympt_1,d7_bhsp_4,d6_bhsp_4,d1_series_1,d6_bhsp_4,d7_bhsp_4,s1_nat_1]),
    [file(asympt_1,l32_asympt_1),interesting(0.00)]).

fof(t62_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ~ ( ~ r1_xreal_0(A,0)
                  & A != 1
                  & ~ r1_xreal_0(B,0)
                  & ~ r1_xreal_0(C,0)
                  & k6_xcmplx_0(k5_power(A,B),k5_power(A,C)) != k5_power(A,k7_xcmplx_0(B,C)) ) ) ) ) ),
    file(power,t62_power),
    [interesting(0.00)]).

fof(t18_newton,theorem,(
    k6_newton(0) = 1 ),
    file(newton,t18_newton),
    [interesting(0.00)]).

fof(l88_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => k2_seq_1(k5_numbers,k1_numbers,A,B) = k6_power(2,k11_newton(B)) )
       => ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => k2_seq_1(k5_numbers,k1_numbers,A,B) = k5_bhsp_4(k2_asympt_1,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t18_newton,t59_power,d6_bhsp_4,d1_series_1,d2_asympt_1,t23_newton,t21_newton,t61_power,d2_asympt_1,d6_bhsp_4,d1_series_1,d6_bhsp_4,s1_nat_1]),
    [file(asympt_1,l88_asympt_1),interesting(0.00)]).

fof(l27_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ( ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => ( r1_xreal_0(D,C)
                     => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,D),k2_seq_1(k5_numbers,k1_numbers,B,D)) ) )
               => r1_xreal_0(k5_bhsp_4(A,C),k5_bhsp_4(B,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_series_1,d1_series_1,d6_bhsp_4,d6_bhsp_4,t9_xreal_1,t9_xreal_1,d6_bhsp_4,d1_series_1,d6_bhsp_4,d6_bhsp_4,d1_series_1,d6_bhsp_4,s1_nat_1]),
    [file(asympt_1,l27_asympt_1),interesting(0.00)]).

fof(d8_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v6_asympt_0(A)
      <=> ? [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
            & ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => ( r1_xreal_0(B,C)
                 => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,C),k2_seq_1(k5_numbers,k1_numbers,A,k1_nat_1(C,1))) ) ) ) ) ) ),
    file(asympt_0,d8_asympt_0),
    [interesting(0.00)]).

fof(t35_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & v6_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ~ ( ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ( k4_nat_1(C,2) = 0
                     => k2_seq_1(k5_numbers,k1_numbers,B,C) = 1 )
                    & ( k4_nat_1(C,2) = 1
                     => k2_seq_1(k5_numbers,k1_numbers,B,C) = C ) ) )
              & r2_hidden(B,k7_asympt_0(A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t27_asympt_0,d8_asympt_0,t46_square_1,t46_square_1,t2_xreal_1,t49_square_1,t16_int_1,t177_real_2,t124_xreal_1,t10_xreal_1,d5_int_1,t2_xreal_1,t2_xreal_1,t70_xreal_1,d9_xcmplx_0,t100_xcmplx_1,d7_xcmplx_0,t2_xreal_1,t2_xreal_1,t8_euler_2,t64_nat_1,t77_nat_1,t10_xreal_1,t2_xreal_1,t70_xreal_1,t107_xcmplx_1,t8_euler_2,t64_nat_1,t64_nat_1,t10_xreal_1,t2_xreal_1,t177_real_2,t124_xreal_1,t10_xreal_1,d5_int_1,t2_xreal_1,t2_xreal_1,t2_xreal_1,t70_xreal_1,d9_xcmplx_0,t100_xcmplx_1,d7_xcmplx_0,t2_xreal_1,t2_xreal_1,t2_xreal_1,t8_euler_2,t77_nat_1,t78_nat_1,t10_xreal_1,t2_xreal_1,t70_xreal_1,t107_xcmplx_1,t62_nat_1]),
    [file(asympt_1,t35_asympt_1),interesting(0.00)]).

fof(d7_asympt_1,definition,(
    ! [A] : 
      ( ( v2_xreal_0(A)
        & m1_subset_1(A,k1_numbers) )
     => ! [B] : 
          ( ( v2_xreal_0(B)
            & m1_subset_1(B,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( C = k8_asympt_1(A,B)
              <=> ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k2_seq_1(k5_numbers,k1_numbers,C,D) = k7_asympt_1(D,A,B) ) ) ) ) ) ),
    file(asympt_1,d7_asympt_1),
    [interesting(0.00)]).

fof(d11_finseq_1,definition,(
    ! [A,B] : 
      ( B = k13_finseq_1(A)
    <=> ! [C] : 
          ( r2_hidden(C,B)
        <=> m2_finseq_1(C,A) ) ) ),
    file(finseq_1,d11_finseq_1),
    [interesting(0.00)]).

fof(t80_int_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( r1_xreal_0(0,A)
       => ( r1_xreal_0(0,k2_int_1(A))
          & r1_xreal_0(0,k1_int_1(A))
          & m2_subset_1(k2_int_1(A),k1_numbers,k5_numbers)
          & m2_subset_1(k1_int_1(A),k1_numbers,k5_numbers) ) ) ) ),
    file(int_1,t80_int_1),
    [interesting(0.00)]).

fof(s2_recdef_1,theorem,
    ( ! [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
       => ! [B] : 
            ( m1_subset_1(B,f1_s2_recdef_1)
           => ? [C] : 
                ( m1_subset_1(C,f1_s2_recdef_1)
                & p1_s2_recdef_1(A,B,C) ) ) )
   => ? [A] : 
        ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,f1_s2_recdef_1)
        & m2_relset_1(A,k5_numbers,f1_s2_recdef_1)
        & k8_funct_2(k5_numbers,f1_s2_recdef_1,A,0) = f2_s2_recdef_1
        & ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => p1_s2_recdef_1(B,k8_funct_2(k5_numbers,f1_s2_recdef_1,A,B),k8_funct_2(k5_numbers,f1_s2_recdef_1,A,k1_nat_1(B,1))) ) ) ),
    file(recdef_1,s2_recdef_1),
    [interesting(0.00)]).

fof(l92_asympt_1,theorem,(
    ! [A] : 
      ( ( v2_xreal_0(A)
        & m1_subset_1(A,k1_numbers) )
     => ! [B] : 
          ( ( v2_xreal_0(B)
            & m1_subset_1(B,k1_numbers) )
         => ? [C] : 
              ( v1_funct_1(C)
              & v1_funct_2(C,k5_numbers,k3_finseq_2(k1_numbers))
              & m2_relset_1(C,k5_numbers,k3_finseq_2(k1_numbers))
              & k6_asympt_1(C,0) = k12_finseq_1(k1_numbers,A)
              & ! [D] : 
                  ( m2_subset_1(D,k1_numbers,k5_numbers)
                 => ? [E] : 
                      ( m2_subset_1(E,k1_numbers,k5_numbers)
                      & E = k2_int_1(k6_real_1(k1_nat_1(k1_nat_1(D,1),1),2))
                      & k6_asympt_1(C,k1_nat_1(D,1)) = k8_finseq_1(k1_numbers,k6_asympt_1(C,D),k12_finseq_1(k1_numbers,k3_real_1(k4_real_1(4,k4_finseq_4(k5_numbers,k1_numbers,k6_asympt_1(C,D),E)),k4_real_1(B,k1_nat_1(k1_nat_1(D,1),1))))) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_finseq_1,t80_int_1,d11_finseq_1,s2_recdef_1]),
    [file(asympt_1,l92_asympt_1),interesting(0.00)]).

fof(d6_asympt_1,definition,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( v2_xreal_0(B)
            & m1_subset_1(B,k1_numbers) )
         => ! [C] : 
              ( ( v2_xreal_0(C)
                & m1_subset_1(C,k1_numbers) )
             => ! [D] : 
                  ( m1_subset_1(D,k1_numbers)
                 => ( ( A = 0
                     => ( D = k7_asympt_1(A,B,C)
                      <=> D = 0 ) )
                    & ( A != 0
                     => ( D = k7_asympt_1(A,B,C)
                      <=> ? [E] : 
                            ( m2_subset_1(E,k1_numbers,k5_numbers)
                            & ? [F] : 
                                ( v1_funct_1(F)
                                & v1_funct_2(F,k5_numbers,k3_finseq_2(k1_numbers))
                                & m2_relset_1(F,k5_numbers,k3_finseq_2(k1_numbers))
                                & k1_nat_1(E,1) = A
                                & D = k4_finseq_4(k5_numbers,k1_numbers,k6_asympt_1(F,E),A)
                                & k6_asympt_1(F,0) = k12_finseq_1(k1_numbers,B)
                                & ! [G] : 
                                    ( m2_subset_1(G,k1_numbers,k5_numbers)
                                   => ? [H] : 
                                        ( m2_subset_1(H,k1_numbers,k5_numbers)
                                        & H = k2_int_1(k6_real_1(k1_nat_1(k1_nat_1(G,1),1),2))
                                        & k6_asympt_1(F,k1_nat_1(G,1)) = k8_finseq_1(k1_numbers,k6_asympt_1(F,G),k12_finseq_1(k1_numbers,k3_real_1(k4_real_1(4,k4_finseq_4(k5_numbers,k1_numbers,k6_asympt_1(F,G),H)),k4_real_1(C,k1_nat_1(k1_nat_1(G,1),1))))) ) ) ) ) ) ) ) ) ) ) ) ),
    file(asympt_1,d6_asympt_1),
    [interesting(0.00)]).

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 ) ) ),
    file(finseq_4,t25_finseq_4),
    [interesting(0.00)]).

fof(t26_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ~ ( r1_xreal_0(A,k2_xcmplx_0(B,1))
              & ~ r1_xreal_0(A,B)
              & A != k2_xcmplx_0(B,1) ) ) ) ),
    file(nat_1,t26_nat_1),
    [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(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) ) ) ) ) ) ),
    file(finseq_4,t83_finseq_4),
    [interesting(0.00)]).

fof(t58_int_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_int_1(B)
         => k2_xcmplx_0(k2_int_1(A),B) = k2_int_1(k2_xcmplx_0(A,B)) ) ) ),
    file(int_1,t58_int_1),
    [interesting(0.00)]).

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) ) ) ) ) ) ),
    file(finseq_4,t84_finseq_4),
    [interesting(0.00)]).

fof(l96_asympt_1,theorem,(
    ! [A] : 
      ( ( v2_xreal_0(A)
        & m1_subset_1(A,k1_numbers) )
     => ! [B] : 
          ( ( v2_xreal_0(B)
            & m1_subset_1(B,k1_numbers) )
         => ( k7_asympt_1(0,A,B) = 0
            & k7_asympt_1(1,A,B) = A
            & ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => ~ ( r1_xreal_0(2,C)
                    & ! [D] : 
                        ( m2_subset_1(D,k1_numbers,k5_numbers)
                       => ~ ( D = k2_int_1(k6_real_1(C,2))
                            & k7_asympt_1(C,A,B) = k3_real_1(k4_real_1(4,k7_asympt_1(D,A,B)),k4_real_1(B,C)) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l92_asympt_1,d6_asympt_1,t25_finseq_4,d6_asympt_1,t11_xreal_1,t16_int_1,t57_finseq_1,d6_asympt_1,t57_finseq_1,t35_finseq_1,t26_nat_1,t9_xreal_1,t27_finseq_3,t83_finseq_4,d6_asympt_1,s1_nat_1,t70_xreal_1,d9_xcmplx_0,d5_int_1,t20_int_1,t21_xreal_1,t16_int_1,t57_finseq_1,t27_finseq_3,d8_xcmplx_0,t58_int_1,t54_int_1,t20_int_1,t20_int_1,d5_int_1,t2_xreal_1,t20_int_1,t21_xreal_1,d5_int_1,t2_xreal_1,d5_real_1,t20_int_1,l95_asympt_1,d5_real_1,t84_finseq_4,t25_finseq_4]),
    [file(asympt_1,l96_asympt_1),interesting(0.00)]).

fof(t101_newton,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( k5_int_1(A,B) = k3_nat_1(A,B)
            & k6_int_1(A,B) = k4_nat_1(A,B) ) ) ) ),
    file(newton,t101_newton),
    [interesting(0.00)]).

fof(d8_int_1,definition,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( v1_int_1(B)
         => ( ( B != 0
             => k6_int_1(A,B) = k6_xcmplx_0(A,k3_xcmplx_0(k5_int_1(A,B),B)) )
            & ( B = 0
             => k6_int_1(A,B) = 0 ) ) ) ) ),
    file(int_1,d8_int_1),
    [interesting(0.00)]).

fof(d9_int_1,definition,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( v1_int_1(B)
         => ( r2_int_1(A,B)
          <=> ? [C] : 
                ( v1_int_1(C)
                & B = k3_xcmplx_0(A,C) ) ) ) ) ),
    file(int_1,d9_int_1),
    [interesting(0.00)]).

fof(t9_wsierp_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( v1_int_1(B)
         => ! [C] : 
              ( v1_int_1(C)
             => ( ( r2_int_1(A,B)
                  & r2_int_1(A,C) )
               => r2_int_1(A,k2_xcmplx_0(B,C)) ) ) ) ) ),
    file(wsierp_1,t9_wsierp_1),
    [interesting(0.00)]).

fof(t22_wsierp_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( v1_int_1(B)
         => ( A != 0
           => ( r2_int_1(A,B)
            <=> v1_int_1(k7_xcmplx_0(B,A)) ) ) ) ) ),
    file(wsierp_1,t22_wsierp_1),
    [interesting(0.00)]).

fof(s2_int_2,theorem,
    ( ! [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
       => ( ( r1_xreal_0(f1_s2_int_2,A)
            & ! [B] : 
                ( m2_subset_1(B,k1_numbers,k5_numbers)
               => ( r1_xreal_0(f1_s2_int_2,B)
                 => ( r1_xreal_0(A,B)
                    | p1_s2_int_2(B) ) ) ) )
         => p1_s2_int_2(A) ) )
   => ! [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
       => ( r1_xreal_0(f1_s2_int_2,A)
         => p1_s2_int_2(A) ) ) ),
    file(int_2,s2_int_2),
    [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(d18_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( C = k11_asympt_0(A,B)
              <=> ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k2_seq_1(k5_numbers,k1_numbers,C,D) = k2_seq_1(k5_numbers,k1_numbers,A,k2_nat_1(B,D)) ) ) ) ) ) ),
    file(asympt_0,d18_asympt_0),
    [interesting(0.00)]).

fof(d19_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( r2_asympt_0(A,B)
          <=> ( v6_asympt_0(A)
              & r2_hidden(k11_asympt_0(A,B),k5_asympt_0(A)) ) ) ) ) ),
    file(asympt_0,d19_asympt_0),
    [interesting(0.00)]).

fof(t37_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( ? [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
            & r1_xreal_0(2,B)
            & r2_asympt_0(A,B) )
       => v7_asympt_0(A) ) ) ),
    file(asympt_0,t37_asympt_0),
    [interesting(0.00)]).

fof(t47_int_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( k1_int_1(A) = A
      <=> v1_int_1(A) ) ) ),
    file(int_1,t47_int_1),
    [interesting(0.00)]).

fof(t11_pre_ff,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( r1_xreal_0(B,A)
           => r1_xreal_0(k1_int_1(B),k1_int_1(A)) ) ) ) ),
    file(pre_ff,t11_pre_ff),
    [interesting(0.00)]).

fof(t38_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ~ ( k2_seq_1(k5_numbers,k1_numbers,A,0) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,0)
                   => k2_seq_1(k5_numbers,k1_numbers,A,C) = k3_power(C,k3_power(2,k1_int_1(k6_power(2,C)))) ) )
              & k2_seq_1(k5_numbers,k1_numbers,B,0) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,0)
                   => k2_seq_1(k5_numbers,k1_numbers,B,C) = k3_series_1(C,C) ) )
              & ! [C] : 
                  ( ( v1_funct_1(C)
                    & v1_funct_2(C,k5_numbers,k1_numbers)
                    & v4_asympt_0(C)
                    & m2_relset_1(C,k5_numbers,k1_numbers) )
                 => ~ ( C = B
                      & r2_hidden(A,k10_asympt_0(C,k9_asympt_1))
                      & ~ r2_hidden(A,k7_asympt_0(C))
                      & v6_asympt_0(A)
                      & v6_asympt_0(C)
                      & ~ r2_asympt_0(C,2) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_asympt_0,t39_power,t27_asympt_0,t11_funct_2,t63_power,t60_power,t47_int_1,t124_xreal_1,t217_xcmplx_1,t46_square_1,t46_square_1,t2_xreal_1,t49_square_1,t16_int_1,l1_asympt_1,t10_xreal_1,t2_xreal_1,t10_xreal_1,t2_xreal_1,t2_xreal_1,t63_power,t60_power,t65_power,t2_xreal_1,l100_asympt_1,t22_xreal_1,t65_power,t63_power,t60_power,t11_pre_ff,t47_int_1,t20_int_1,d4_int_1,t2_xreal_1,d5_real_1,t34_power,t30_power,t39_power,d5_int_1,t2_xreal_1,t2_xreal_1,t10_xreal_1,t151_real_2,t56_xcmplx_1,t57_xcmplx_1,t70_xreal_1,t88_xcmplx_1,t10_xreal_1,t12_pre_ff,t60_power,t11_pre_ff,t47_int_1,t44_power,t42_power,t65_power,t11_pre_ff,t10_pre_ff,t10_pre_ff,t2_xreal_1,t10_xreal_1,t8_xreal_1,t2_xreal_1,t44_power,t42_power,t2_xreal_1,d19_asympt_0,t46_square_1,t46_square_1,t2_xreal_1,t2_xreal_1,t70_xreal_1,t49_square_1,t16_int_1,d18_asympt_0,t42_power,t2_xreal_1,t8_xreal_1,t10_pre_ff,t2_xreal_1,t32_power,t30_power,d5_int_1,t2_xreal_1,t66_xreal_1,t2_xreal_1,d8_asympt_0]),
    [file(asympt_1,t38_asympt_1),interesting(0.00)]).

fof(t39_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ~ ( ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ( ( r2_hidden(B,k9_asympt_1)
                 => k2_seq_1(k5_numbers,k1_numbers,A,B) = B )
                & ( ~ r2_hidden(B,k9_asympt_1)
                 => k2_seq_1(k5_numbers,k1_numbers,A,B) = k3_series_1(B,2) ) ) )
          & ! [B] : 
              ( ( v1_funct_1(B)
                & v1_funct_2(B,k5_numbers,k1_numbers)
                & v4_asympt_0(B)
                & m2_relset_1(B,k5_numbers,k1_numbers) )
             => ~ ( B = A
                  & r2_hidden(k3_asympt_1(1),k10_asympt_0(B,k9_asympt_1))
                  & ~ r2_hidden(k3_asympt_1(1),k7_asympt_0(B))
                  & r2_hidden(k11_asympt_0(B,2),k5_asympt_0(B))
                  & v6_asympt_0(k3_asympt_1(1))
                  & ~ v6_asympt_0(B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_asympt_0,t39_power,t11_funct_2,d3_asympt_1,t30_power,t27_asympt_0,t46_square_1,t46_square_1,t2_xreal_1,t49_square_1,t16_int_1,t39_power,t38_nat_1,t21_xreal_1,t16_int_1,l1_asympt_1,t22_xreal_1,t2_xreal_1,t2_xreal_1,d5_int_1,t2_xreal_1,t70_xreal_1,t70_xreal_1,t88_xcmplx_1,l101_asympt_1,t53_power,d3_asympt_1,t30_power,t11_funct_2,d18_asympt_0,t30_power,t32_power,t66_xreal_1,t29_power,t38_nat_1,t38_nat_1,t21_xreal_1,t32_power,t30_power,t16_int_1,t53_power,t53_power,d18_asympt_0,d18_asympt_0,d3_asympt_1,d3_asympt_1,t30_power,d3_asympt_1,t30_power,t8_xreal_1,d8_asympt_0,t10_pre_ff,t29_power,t11_xreal_1,t46_square_1,t66_xreal_1,t16_int_1,l101_asympt_1,t66_xreal_1,t10_pre_ff,t53_power,t11_xreal_1,t2_xreal_1,l99_asympt_1,t53_power,t46_square_1,l1_asympt_1,t22_xreal_1,t66_xreal_1,t2_xreal_1,t2_xreal_1,d8_asympt_0]),
    [file(asympt_1,t39_asympt_1),interesting(0.00)]).

fof(t3_asympt_1,theorem,(
    ! [A] : 
      ( ( v2_xreal_0(A)
        & m1_subset_1(A,k1_numbers) )
     => ! [B] : 
          ( ( v2_xreal_0(B)
            & m1_subset_1(B,k1_numbers) )
         => ~ ( ~ r1_xreal_0(B,A)
              & r2_hidden(k1_asympt_1(B,1,0),k5_asympt_0(k1_asympt_1(A,1,0))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t65_power,t22_xreal_1,t46_square_1,t49_square_1,t16_int_1,t39_power,t10_xreal_1,t2_xreal_1,d5_int_1,t2_xreal_1,t70_xreal_1,t88_xcmplx_1,t44_power,d3_power,t34_power,t70_xreal_1,t88_xcmplx_1,l6_asympt_1,l6_asympt_1,d1_asympt_1,d1_asympt_1]),
    [file(asympt_1,t3_asympt_1),interesting(0.00)]).

fof(d20_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v7_asympt_0(A)
      <=> ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => ( r1_xreal_0(2,B)
             => r2_asympt_0(A,B) ) ) ) ) ),
    file(asympt_0,d20_asympt_0),
    [interesting(0.00)]).

fof(t19_newton,theorem,(
    k6_newton(1) = 1 ),
    file(newton,t19_newton),
    [interesting(0.00)]).

fof(t40_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ~ ( ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => k2_seq_1(k5_numbers,k1_numbers,A,B) = k10_asympt_1(B) )
          & ! [B] : 
              ( ( v1_funct_1(B)
                & v1_funct_2(B,k5_numbers,k1_numbers)
                & v4_asympt_0(B)
                & m2_relset_1(B,k5_numbers,k1_numbers) )
             => ~ ( B = A
                  & v6_asympt_0(A)
                  & ! [C] : 
                      ( m2_subset_1(C,k1_numbers,k5_numbers)
                     => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,C),k2_seq_1(k5_numbers,k1_numbers,k3_asympt_1(1),C)) )
                  & ~ v7_asympt_0(B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_asympt_0,d9_asympt_1,t23_newton,d9_asympt_1,t29_nat_1,d9_asympt_1,t20_int_1,t2_xreal_1,d9_asympt_1,t10_xreal_1,t23_newton,t70_xreal_1,t21_newton,d9_asympt_1,t29_nat_1,l106_asympt_1,d5_real_1,d9_asympt_1,d3_asympt_1,d9_asympt_1,d3_asympt_1,t30_power,d20_asympt_0,d19_asympt_0,t46_square_1,t46_square_1,t2_xreal_1,t49_square_1,t16_int_1,t2_xreal_1,l106_asympt_1,t20_newton,t11_xreal_1,t16_int_1,t11_xreal_1,t16_int_1,l109_asympt_1,t20_int_1,t21_xreal_1,t2_xreal_1,t92_real_1,t21_newton,l106_asympt_1,t19_newton,t2_xreal_1,t21_xreal_1,l45_asympt_1,t66_xreal_1,t21_newton,t8_xreal_1,t21_xreal_1,t177_real_2,t92_xcmplx_1,d9_asympt_1,d18_asympt_0,t66_xreal_1,t38_nat_1,t70_xreal_1,t21_newton,t2_xreal_1,t70_xreal_1,t2_xreal_1,t8_xreal_1,t21_xreal_1,d9_asympt_1,t21_newton,t10_xreal_1,d5_int_1,t2_xreal_1,t2_xreal_1,t23_newton,t70_xreal_1,d8_asympt_0]),
    [file(asympt_1,t40_asympt_1),interesting(0.00)]).

fof(t13_funcop_1,theorem,(
    ! [A,B,C] : 
      ( r2_hidden(B,A)
     => k1_funct_1(k2_funcop_1(A,C),B) = C ) ),
    file(funcop_1,t13_funcop_1),
    [interesting(0.00)]).

fof(t15_seq_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => k10_seq_1(A,B) = k9_seq_1(A,k17_seq_1(B)) ) ) ),
    file(seq_1,t15_seq_1),
    [interesting(0.00)]).

fof(t14_seq_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( A = k17_seq_1(B)
          <=> ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => k2_seq_1(k5_numbers,k1_numbers,A,C) = k1_real_1(k2_seq_1(k5_numbers,k1_numbers,B,C)) ) ) ) ) ),
    file(seq_1,t14_seq_1),
    [interesting(0.00)]).

fof(t41_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( A = k10_seq_1(k3_asympt_1(1),k4_asympt_1(1))
       => k12_asympt_0(k5_numbers,k7_asympt_0(A),k7_asympt_0(k3_asympt_1(1))) = k7_asympt_0(k3_asympt_1(1)) ) ) ),
    inference(mizar_proof,[status(thm)],[t27_asympt_0,t27_asympt_0,t46_square_1,t2_xreal_1,t8_xreal_1,t2_xreal_1,t8_xreal_1,t8_xreal_1,t2_xreal_1,d3_asympt_1,t30_power,t13_funcop_1,t15_seq_1,t11_seq_1,t14_seq_1,d3_asympt_1,t30_power,t26_xreal_1,t66_xreal_1,t8_xreal_1,t2_xreal_1,t8_xreal_1,t2_xreal_1,t26_xreal_1,t8_xreal_1,t2_xreal_1,t70_xreal_1,t11_funct_2,t46_square_1,t2_xreal_1,t66_xreal_1,t13_funcop_1,t15_seq_1,t11_seq_1,t14_seq_1,d3_asympt_1,t30_power,d3_asympt_1,t30_power,t92_real_1,t66_xreal_1,t2_xreal_1,t13_seq_1,t8_xreal_1,t21_xreal_1,t66_xreal_1,t66_xreal_1,t2_xreal_1,t13_seq_1,t2_xreal_1,t66_xreal_1,t13_seq_1,t13_seq_1,t2_tarski]),
    [file(asympt_1,t41_asympt_1),interesting(0.00)]).

fof(t10_fraenkel,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & v1_funct_2(C,A,B)
        & m2_relset_1(C,A,B) )
     => m1_fraenkel(k2_setwiseo(k1_zfmisc_1(k2_zfmisc_1(A,B)),C),A,B) ) ),
    file(fraenkel,t10_fraenkel),
    [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(t9_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ? [B] : 
          ( m1_fraenkel(B,k5_numbers,k1_numbers)
          & B = k6_domain_1(k1_zfmisc_1(k2_zfmisc_1(k5_numbers,k1_numbers)),k3_asympt_1(1))
          & ~ ( r2_hidden(A,k14_asympt_0(B,k5_asympt_0(k4_asympt_1(1))))
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ! [D] : 
                      ( m1_subset_1(D,k1_numbers)
                     => ! [E] : 
                          ( m2_subset_1(E,k1_numbers,k5_numbers)
                         => ~ ( ~ r1_xreal_0(D,0)
                              & ! [F] : 
                                  ( m2_subset_1(F,k1_numbers,k5_numbers)
                                 => ( r1_xreal_0(C,F)
                                   => ( r1_xreal_0(1,k2_seq_1(k5_numbers,k1_numbers,A,F))
                                      & r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,F),k4_real_1(D,k2_seq_1(k5_numbers,k1_numbers,k3_asympt_1(E),F))) ) ) ) ) ) ) ) )
          & ( ? [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
                & ? [D] : 
                    ( m1_subset_1(D,k1_numbers)
                    & ? [E] : 
                        ( m2_subset_1(E,k1_numbers,k5_numbers)
                        & ~ r1_xreal_0(D,0)
                        & ! [F] : 
                            ( m2_subset_1(F,k1_numbers,k5_numbers)
                           => ( r1_xreal_0(C,F)
                             => ( r1_xreal_0(1,k2_seq_1(k5_numbers,k1_numbers,A,F))
                                & r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,F),k4_real_1(D,k2_seq_1(k5_numbers,k1_numbers,k3_asympt_1(E),F))) ) ) ) ) ) )
           => r2_hidden(A,k14_asympt_0(B,k5_asympt_0(k4_asympt_1(1)))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_fraenkel,d1_tarski,t46_square_1,t2_xreal_1,t46_square_1,d5_int_1,d5_int_1,t16_int_1,t2_xreal_1,t13_funcop_1,t2_xreal_1,d3_asympt_1,t30_power,t10_pre_ff,t29_power,t10_pre_ff,t10_pre_ff,t2_xreal_1,d3_asympt_1,t11_funct_2,t46_square_1,t2_xreal_1,t46_square_1,t46_square_1,t2_xreal_1,t11_funct_2,s3_funct_2,t11_funct_2,t2_xreal_1,d3_asympt_1,t30_power,d3_power,d1_tarski,t59_power,t65_power,t8_xreal_1,t2_xreal_1,t2_xreal_1,t2_xreal_1,l36_asympt_1,d3_asympt_1,t39_power,t66_xreal_1,t2_xreal_1,t12_pre_ff,d3_asympt_1,t30_power,t63_power,t60_power,t61_power,t63_power,t60_power,t8_xreal_1,t13_funcop_1,t2_xreal_1,t12_pre_ff,t59_power]),
    [file(asympt_1,t9_asympt_1),interesting(0.00)]).

fof(t41_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ~ ( ~ r1_xreal_0(A,1)
              & ~ r1_xreal_0(0,B)
              & r1_xreal_0(1,k3_power(A,B)) ) ) ) ),
    file(power,t41_power),
    [interesting(0.00)]).

fof(t42_asympt_1,theorem,(
    ? [A] : 
      ( m1_fraenkel(A,k5_numbers,k1_numbers)
      & A = k6_domain_1(k1_zfmisc_1(k2_zfmisc_1(k5_numbers,k1_numbers)),k3_asympt_1(1))
      & ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,k3_asympt_1(k1_real_1(1)),B),k2_seq_1(k5_numbers,k1_numbers,k3_asympt_1(1),B)) )
      & ~ r2_hidden(k3_asympt_1(k1_real_1(1)),k14_asympt_0(A,k5_asympt_0(k4_asympt_1(1)))) ) ),
    inference(mizar_proof,[status(thm)],[t10_fraenkel,d3_asympt_1,d3_asympt_1,t20_int_1,t31_power,t10_pre_ff,d5_real_1,t9_asympt_1,t46_square_1,t2_xreal_1,t2_xreal_1,d3_asympt_1,t41_power]),
    [file(asympt_1,t42_asympt_1),interesting(0.00)]).

fof(d9_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( C = k2_asympt_0(A,B)
              <=> ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k2_seq_1(k5_numbers,k1_numbers,C,D) = k2_xcmplx_0(B,k2_seq_1(k5_numbers,k1_numbers,A,D)) ) ) ) ) ) ),
    file(asympt_0,d9_asympt_0),
    [interesting(0.00)]).

fof(t43_asympt_1,theorem,(
    ! [A] : 
      ( ( ~ v3_xreal_0(A)
        & m1_subset_1(A,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & v2_asympt_0(C)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( r2_hidden(B,k5_asympt_0(k2_asympt_0(C,A)))
               => ( ! [D] : 
                      ( m1_subset_1(D,k1_numbers)
                     => ! [E] : 
                          ( m2_subset_1(E,k1_numbers,k5_numbers)
                         => ~ ( ~ r1_xreal_0(D,0)
                              & ! [F] : 
                                  ( m2_subset_1(F,k1_numbers,k5_numbers)
                                 => ( r1_xreal_0(E,F)
                                   => r1_xreal_0(D,k2_seq_1(k5_numbers,k1_numbers,C,F)) ) ) ) ) )
                  | r2_hidden(B,k5_asympt_0(C)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t46_square_1,t70_xreal_1,t46_square_1,t46_square_1,t2_xreal_1,d9_asympt_0,t66_xreal_1,t8_xreal_1,t2_xreal_1,t107_xcmplx_1,t100_xcmplx_1,t66_xreal_1,t2_xreal_1,t66_xreal_1,t2_xreal_1,t70_xreal_1,t8_xreal_1,t2_xreal_1,t66_xreal_1,t2_xreal_1]),
    [file(asympt_1,t43_asympt_1),interesting(0.00)]).

fof(t56_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k1_numbers)
             => ~ ( ~ r1_xreal_0(A,0)
                  & ~ r1_xreal_0(C,0)
                  & C != 1
                  & k4_power(A,B) != k4_power(C,k4_real_1(B,k6_power(C,A))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l6_asympt_1]),
    [file(asympt_1,t56_asympt_1),interesting(0.00)]).

fof(l107_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(1,A)
          & ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ~ ( r1_xreal_0(k11_newton(B),A)
                  & ~ r1_xreal_0(k11_newton(k1_nat_1(B,1)),A)
                  & ! [C] : 
                      ( m2_subset_1(C,k1_numbers,k5_numbers)
                     => ( r1_xreal_0(k11_newton(C),A)
                       => ( r1_xreal_0(k11_newton(k1_nat_1(C,1)),A)
                          | C = B ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t19_newton,t20_newton,t38_nat_1,l105_asympt_1,t19_newton,t38_nat_1,t1_xreal_1,t20_int_1,t8_xreal_1,t2_xreal_1,t38_nat_1,l106_asympt_1,t2_xreal_1,t38_nat_1,l106_asympt_1,t2_xreal_1,t29_nat_1,t2_xreal_1,d5_real_1,t8_xreal_1,t23_newton,t70_xreal_1,t21_newton,t38_nat_1,l106_asympt_1,t2_xreal_1,t8_xreal_1,t2_xreal_1,t23_newton,t70_xreal_1,t21_newton,t38_nat_1,l106_asympt_1,d5_real_1,d5_real_1,s1_int_2]),
    [file(asympt_1,l107_asympt_1),interesting(0.00)]).

fof(t63_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(1,A)
          & ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ~ ( r1_xreal_0(k11_newton(B),A)
                  & ~ r1_xreal_0(k11_newton(k1_nat_1(B,1)),A)
                  & ! [C] : 
                      ( m2_subset_1(C,k1_numbers,k5_numbers)
                     => ( r1_xreal_0(k11_newton(C),A)
                       => ( r1_xreal_0(k11_newton(k1_nat_1(C,1)),A)
                          | C = B ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l107_asympt_1]),
    [file(asympt_1,t63_asympt_1),interesting(0.00)]).

fof(t68_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_asympt_0(A)
        & m1_subset_1(A,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( k2_seq_1(k5_numbers,k1_numbers,B,0) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,0)
                   => k2_seq_1(k5_numbers,k1_numbers,B,C) = k6_power(A,C) ) ) )
           => ( r1_xreal_0(A,1)
              | v4_asympt_0(B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l3_asympt_1]),
    [file(asympt_1,t68_asympt_1),interesting(0.00)]).

fof(t69_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( r2_hidden(A,k5_asympt_0(B))
              & r2_hidden(B,k5_asympt_0(A)) )
          <=> k5_asympt_0(A) = k5_asympt_0(B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l11_asympt_1]),
    [file(asympt_1,t69_asympt_1),interesting(0.00)]).

fof(t76_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => ( r1_xreal_0(C,B)
                 => r1_xreal_0(0,k2_seq_1(k5_numbers,k1_numbers,A,C)) ) )
           => r1_xreal_0(0,k5_bhsp_4(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l26_asympt_1]),
    [file(asympt_1,t76_asympt_1),interesting(0.00)]).

fof(t77_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ( ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => ( r1_xreal_0(D,C)
                     => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,D),k2_seq_1(k5_numbers,k1_numbers,B,D)) ) )
               => r1_xreal_0(k5_bhsp_4(A,C),k5_bhsp_4(B,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l27_asympt_1]),
    [file(asympt_1,t77_asympt_1),interesting(0.00)]).

fof(t78_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( ( k2_seq_1(k5_numbers,k1_numbers,A,0) = 0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ~ r1_xreal_0(C,0)
                   => k2_seq_1(k5_numbers,k1_numbers,A,C) = B ) ) )
           => ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => k5_bhsp_4(A,C) = k4_real_1(B,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l28_asympt_1]),
    [file(asympt_1,t78_asympt_1),interesting(0.00)]).

fof(t79_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => k3_real_1(k6_bhsp_4(A,B,C),k2_seq_1(k5_numbers,k1_numbers,A,k1_nat_1(B,1))) = k6_bhsp_4(A,k1_nat_1(B,1),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l29_asympt_1]),
    [file(asympt_1,t79_asympt_1),interesting(0.00)]).

fof(t7_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => k2_seq_1(k5_numbers,k1_numbers,A,C) = k5_bhsp_4(k3_asympt_1(B),C) )
           => r2_hidden(A,k7_asympt_0(k3_asympt_1(k1_nat_1(B,1)))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t11_funct_2,t39_power,t124_xreal_1,s3_funct_2,d3_asympt_1,d3_asympt_1,l13_asympt_1,l27_asympt_1,l28_asympt_1,t30_power,t32_power,d3_asympt_1,d3_asympt_1,d3_asympt_1,l26_asympt_1,s3_funct_2,d3_asympt_1,t70_xreal_1,d9_xcmplx_0,d5_int_1,t16_int_1,t21_int_1,t8_xreal_1,d9_xcmplx_0,t16_int_1,d3_asympt_1,d3_asympt_1,l26_asympt_1,d7_bhsp_4,t29_nat_1,t22_xreal_1,t2_xreal_1,l31_asympt_1,t2_xreal_1,l26_asympt_1,t9_xreal_1,t22_xreal_1,d9_xcmplx_0,d3_asympt_1,t2_xreal_1,l13_asympt_1,l31_asympt_1,t8_xreal_1,t21_xreal_1,l30_asympt_1,l32_asympt_1,d5_int_1,t21_xreal_1,t8_xreal_1,t21_xreal_1,t39_power,t66_xreal_1,t30_power,t32_power,t36_power,d9_xcmplx_0,t2_xreal_1,t2_xreal_1,d3_xboole_0]),
    [file(asympt_1,t7_asympt_1),interesting(0.00)]).

fof(t80_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ! [D] : 
                  ( m2_subset_1(D,k1_numbers,k5_numbers)
                 => ( ( r1_xreal_0(k1_nat_1(C,1),D)
                      & ! [E] : 
                          ( m2_subset_1(E,k1_numbers,k5_numbers)
                         => ( ( r1_xreal_0(k1_nat_1(C,1),E)
                              & r1_xreal_0(E,D) )
                           => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,E),k2_seq_1(k5_numbers,k1_numbers,B,E)) ) ) )
                   => r1_xreal_0(k6_bhsp_4(A,D,C),k6_bhsp_4(B,D,C)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l30_asympt_1]),
    [file(asympt_1,t80_asympt_1),interesting(0.00)]).

fof(t82_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ( ( k2_seq_1(k5_numbers,k1_numbers,A,0) = 0
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ( ~ r1_xreal_0(D,0)
                       => k2_seq_1(k5_numbers,k1_numbers,A,D) = B ) ) )
               => ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k6_bhsp_4(A,C,D) = k4_real_1(B,k5_real_1(C,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l32_asympt_1]),
    [file(asympt_1,t82_asympt_1),interesting(0.00)]).

fof(t83_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ! [D] : 
                  ( m1_subset_1(D,k1_numbers)
                 => ( ( v4_seq_2(A)
                      & k2_seq_2(A) = D
                      & ! [E] : 
                          ( m2_subset_1(E,k1_numbers,k5_numbers)
                         => ( r1_xreal_0(C,E)
                           => k2_seq_1(k5_numbers,k1_numbers,A,E) = k2_seq_1(k5_numbers,k1_numbers,B,E) ) ) )
                   => ( v4_seq_2(B)
                      & k2_seq_2(B) = D ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l53_asympt_1]),
    [file(asympt_1,t83_asympt_1),interesting(0.00)]).

fof(t86_asympt_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ~ ( ~ r1_xreal_0(A,0)
          & ~ r1_xreal_0(1,A)
          & ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ? [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                  & r1_xreal_0(B,C)
                  & r1_xreal_0(k5_real_1(k4_real_1(C,k6_power(2,k3_real_1(1,A))),k4_real_1(8,k6_power(2,C))),k4_real_1(8,k6_power(2,C))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l56_asympt_1]),
    [file(asympt_1,t86_asympt_1),interesting(0.00)]).

fof(t87_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( r1_xreal_0(10,A)
          & r1_xreal_0(k6_real_1(1,k4_power(2,k5_real_1(A,9))),k6_real_1(k3_series_1(2,k2_nat_1(2,A)),k11_newton(A))) ) ) ),
    inference(mizar_proof,[status(thm)],[l70_asympt_1]),
    [file(asympt_1,t87_asympt_1),interesting(0.00)]).

fof(t8_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ~ ( k2_seq_1(k5_numbers,k1_numbers,A,0) = 0
          & ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ( ~ r1_xreal_0(B,0)
               => k2_seq_1(k5_numbers,k1_numbers,A,B) = k4_power(B,k6_power(2,B)) ) )
          & ! [B] : 
              ( ( v1_funct_1(B)
                & v1_funct_2(B,k5_numbers,k1_numbers)
                & v4_asympt_0(B)
                & m2_relset_1(B,k5_numbers,k1_numbers) )
             => ~ ( B = A
                  & ~ v7_asympt_0(B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_asympt_0,t39_power,d20_asympt_0,d19_asympt_0,t49_square_1,t46_square_1,t46_square_1,t2_xreal_1,t49_square_1,t16_int_1,t10_xreal_1,t2_xreal_1,t39_power,t70_xreal_1,d3_power,t35_power,t30_power,t32_power,t60_power,t61_power,t93_square_1,t93_square_1,t93_square_1,d5_int_1,t2_xreal_1,t70_xreal_1,t88_xcmplx_1,t78_square_1,d4_square_1,d4_square_1,t70_xreal_1,d18_asympt_0]),
    [file(asympt_1,t8_asympt_1),interesting(0.00)]).

fof(t92_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ( r1_xreal_0(1,A)
       => r1_xreal_0(k4_power(k6_real_1(k1_nat_1(A,1),A),A),k4_power(k6_real_1(k1_nat_1(A,2),k1_nat_1(A,1)),k1_nat_1(A,1))) ) ) ),
    inference(mizar_proof,[status(thm)],[l78_asympt_1]),
    [file(asympt_1,t92_asympt_1),interesting(0.00)]).

fof(t93_asympt_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( r1_xreal_0(A,B)
           => r1_xreal_0(k6_real_1(k8_newton(A,k1_nat_1(B,1)),k1_nat_1(B,1)),k8_newton(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l86_asympt_1]),
    [file(asympt_1,t93_asympt_1),interesting(0.00)]).

fof(t94_asympt_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => k2_seq_1(k5_numbers,k1_numbers,A,B) = k6_power(2,k11_newton(B)) )
       => ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => k2_seq_1(k5_numbers,k1_numbers,A,B) = k5_bhsp_4(k2_asympt_1,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l88_asympt_1]),
    [file(asympt_1,t94_asympt_1),interesting(0.00)]).

fof(t96_asympt_1,theorem,(
    ! [A] : 
      ( ( v2_xreal_0(A)
        & m1_subset_1(A,k1_numbers) )
     => ! [B] : 
          ( ( v2_xreal_0(B)
            & m1_subset_1(B,k1_numbers) )
         => ( k7_asympt_1(0,A,B) = 0
            & k7_asympt_1(1,A,B) = A
            & ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => ~ ( r1_xreal_0(2,C)
                    & ! [D] : 
                        ( m2_subset_1(D,k1_numbers,k5_numbers)
                       => ~ ( D = k2_int_1(k6_real_1(C,2))
                            & k7_asympt_1(C,A,B) = k3_real_1(k4_real_1(4,k7_asympt_1(D,A,B)),k4_real_1(B,C)) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l96_asympt_1]),
    [file(asympt_1,t96_asympt_1),interesting(0.00)]).