fof(t76_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ! [C] : 
              ( ( ~ v1_xboole_0(C)
                & v1_trees_1(C) )
             => ! [D] : 
                  ( ( ~ v1_xboole_0(D)
                    & v1_trees_1(D) )
                 => ( k15_trees_3(A,B) = k15_trees_3(C,D)
                   => ( A = C
                      & B = D ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t72_trees_3,t72_trees_3,d1_trees_2,d1_trees_2,t73_trees_3,t73_trees_3]),
    [file(trees_3,t76_trees_3),interesting(1.00)]).

fof(t83_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A)
        & v1_trees_1(A) )
     => k6_trees_1(k14_trees_3(A)) = k1_nat_1(k6_trees_1(A),1) ) ),
    inference(mizar_proof,[status(thm)],[t55_finseq_1,d1_tarski,d1_tarski,t82_trees_3]),
    [file(trees_3,t83_trees_3),interesting(0.93)]).

fof(t55_trees_3,theorem,(
    k13_trees_3(k1_xboole_0) = k2_trees_1(0) ),
    inference(mizar_proof,[status(thm)],[d1_trees_2,d15_trees_3,t23_trees_3,d1_tarski,t56_trees_1,t25_finseq_1,d1_tarski,t56_trees_1,d15_trees_3,t23_trees_3]),
    [file(trees_3,t55_trees_3),interesting(0.92)]).

fof(t69_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => k5_trees_1(k14_trees_3(A),k12_finseq_1(k5_numbers,0),B) = k14_trees_3(B) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_finseq_1,t47_finseq_1,t23_trees_3,t60_trees_3]),
    [file(trees_3,t69_trees_3),interesting(0.92)]).

fof(t3_trees_3,theorem,(
    ! [A,B] : 
      ( ( v1_trees_3(A)
        & v1_trees_3(B) )
    <=> v1_trees_3(k2_xboole_0(A,B)) ) ),
    inference(mizar_proof,[status(thm)],[d3_trees_3,d3_trees_3,d2_xboole_0,d3_trees_3,d3_trees_3,d2_xboole_0,d3_trees_3,d2_xboole_0]),
    [file(trees_3,t3_trees_3),interesting(0.91)]).

fof(t6_trees_3,theorem,(
    ! [A,B] : 
      ( ( v2_trees_3(A)
        & v2_trees_3(B) )
    <=> v2_trees_3(k2_xboole_0(A,B)) ) ),
    inference(mizar_proof,[status(thm)],[d4_trees_3,d4_trees_3,d2_xboole_0,d4_trees_3,d4_trees_3,d2_xboole_0,d4_trees_3,d2_xboole_0]),
    [file(trees_3,t6_trees_3),interesting(0.90)]).

fof(t9_trees_3,theorem,(
    ! [A,B] : 
      ( ( v3_trees_3(A)
        & v3_trees_3(B) )
    <=> v3_trees_3(k2_xboole_0(A,B)) ) ),
    inference(mizar_proof,[status(thm)],[d5_trees_3,d5_trees_3,d2_xboole_0,d5_trees_3,d5_trees_3,d2_xboole_0,d5_trees_3,d2_xboole_0]),
    [file(trees_3,t9_trees_3),interesting(0.90)]).

fof(t13_trees_3,theorem,(
    ! [A] : 
      ( v1_trees_3(k1_tarski(A))
    <=> ( ~ v1_xboole_0(A)
        & v1_trees_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_trees_3,d1_tarski,d3_trees_3,d1_tarski]),
    [file(trees_3,t13_trees_3),interesting(0.89)]).

fof(t39_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v6_trees_3(A) )
     => ( k1_relat_1(k2_funct_6(A)) = k1_relat_1(A)
        & v4_trees_3(k2_funct_6(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_funct_6,t167_relat_1,d10_xboole_0,d3_tarski,t26_trees_3,t28_funct_6,t28_funct_6,t26_trees_3,t31_funct_6,t24_trees_3]),
    [file(trees_3,t39_trees_3),interesting(0.88)]).

fof(t23_trees_3,theorem,
    ( v4_trees_3(k1_xboole_0)
    & v5_trees_3(k1_xboole_0)
    & v6_trees_3(k1_xboole_0) ),
    inference(mizar_proof,[status(thm)],[t12_trees_3,t27_finseq_1,d9_trees_3,t12_trees_3,t27_finseq_1,d10_trees_3,t12_trees_3,t27_finseq_1,d11_trees_3]),
    [file(trees_3,t23_trees_3),interesting(0.87)]).

fof(t70_trees_3,theorem,(
    k14_trees_3(k2_trees_1(0)) = k2_trees_1(1) ),
    inference(mizar_proof,[status(thm)],[t73_finseq_2,t57_trees_3]),
    [file(trees_3,t70_trees_3),interesting(0.86)]).

fof(l51_trees_3,theorem,(
    ! [A,B] : 
      ( ~ v1_xboole_0(k9_finseq_1(A))
      & ~ v1_xboole_0(k10_finseq_1(A,B)) ) ),
    inference(mizar_proof,[status(thm)],[t57_finseq_1,t61_finseq_1,t4_finseq_1,d3_finseq_1,d1_tarski,d2_tarski,t8_funct_1]),
    [file(trees_3,l51_trees_3),interesting(0.85)]).

fof(t14_trees_3,theorem,(
    ! [A] : 
      ( v2_trees_3(k1_tarski(A))
    <=> ( ~ v1_xboole_0(A)
        & v1_finset_1(A)
        & v1_trees_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_trees_3,d1_tarski,d4_trees_3,d1_tarski]),
    [file(trees_3,t14_trees_3),interesting(0.85)]).

fof(t15_trees_3,theorem,(
    ! [A] : 
      ( v3_trees_3(k1_tarski(A))
    <=> ( v1_relat_1(A)
        & v1_funct_1(A)
        & v3_trees_2(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_trees_3,d1_tarski,d5_trees_3,d1_tarski]),
    [file(trees_3,t15_trees_3),interesting(0.85)]).

fof(t16_trees_3,theorem,(
    ! [A,B] : 
      ( v1_trees_3(k2_tarski(A,B))
    <=> ( ~ v1_xboole_0(A)
        & v1_trees_1(A)
        & ~ v1_xboole_0(B)
        & v1_trees_1(B) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_trees_3,d2_tarski,d3_trees_3,d2_tarski]),
    [file(trees_3,t16_trees_3),interesting(0.85)]).

fof(t12_trees_3,theorem,
    ( v1_trees_3(k1_xboole_0)
    & v2_trees_3(k1_xboole_0)
    & v3_trees_3(k1_xboole_0) ),
    inference(mizar_proof,[status(thm)],[d3_trees_3,d4_trees_3,d5_trees_3]),
    [file(trees_3,t12_trees_3),interesting(0.84)]).

fof(t68_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => k4_trees_1(k14_trees_3(A),k12_finseq_1(k5_numbers,0)) = A ) ),
    inference(mizar_proof,[status(thm)],[t57_finseq_1,t52_trees_3]),
    [file(trees_3,t68_trees_3),interesting(0.84)]).

fof(t1_trees_3,theorem,(
    ! [A] : 
      ( v1_trees_3(A)
    <=> r1_tarski(A,k1_trees_3) ) ),
    inference(mizar_proof,[status(thm)],[d3_trees_3,d3_tarski,d1_trees_3,d3_trees_3,d1_trees_3]),
    [file(trees_3,t1_trees_3),interesting(0.83)]).

fof(t57_trees_3,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => k2_trees_1(A) = k13_trees_3(k2_finseq_2(A,k2_trees_1(0))) ) ),
    inference(mizar_proof,[status(thm)],[d1_trees_2,t69_finseq_2,t56_trees_3,d15_trees_3,d2_finseq_2,l62_trees_3,t19_funcop_1,d1_tarski,d1_tarski,t56_trees_1,t47_finseq_1,t55_trees_1,t47_trees_1]),
    [file(trees_3,t57_trees_3),interesting(0.83)]).

fof(t2_trees_3,theorem,(
    ! [A] : 
      ( v2_trees_3(A)
    <=> r1_tarski(A,k2_trees_3) ) ),
    inference(mizar_proof,[status(thm)],[d4_trees_3,d3_tarski,d2_trees_3,d4_trees_3,d2_trees_3]),
    [file(trees_3,t2_trees_3),interesting(0.82)]).

fof(t56_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ( v4_trees_3(A)
       => r1_tarski(k2_trees_1(k3_finseq_1(A)),k13_trees_3(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_trees_3,d15_trees_3,d3_tarski,d2_xboole_0,d1_tarski,t47_trees_1,l62_trees_3,d3_trees_3,t47_finseq_1,t47_trees_1,d15_trees_3]),
    [file(trees_3,t56_trees_3),interesting(0.81)]).

fof(t19_trees_3,theorem,(
    ! [A,B] : 
      ( ( v1_trees_3(A)
        & r1_tarski(B,A) )
     => v1_trees_3(B) ) ),
    inference(mizar_proof,[status(thm)],[d3_trees_3,d3_trees_3]),
    [file(trees_3,t19_trees_3),interesting(0.80)]).

fof(t20_trees_3,theorem,(
    ! [A,B] : 
      ( ( v2_trees_3(A)
        & r1_tarski(B,A) )
     => v2_trees_3(B) ) ),
    inference(mizar_proof,[status(thm)],[d4_trees_3,d4_trees_3]),
    [file(trees_3,t20_trees_3),interesting(0.80)]).

fof(t21_trees_3,theorem,(
    ! [A,B] : 
      ( ( v3_trees_3(A)
        & r1_tarski(B,A) )
     => v3_trees_3(B) ) ),
    inference(mizar_proof,[status(thm)],[d5_trees_3,d5_trees_3]),
    [file(trees_3,t21_trees_3),interesting(0.80)]).

fof(t30_trees_3,theorem,(
    ! [A] : 
      ( v4_trees_3(k9_finseq_1(A))
    <=> ( ~ v1_xboole_0(A)
        & v1_trees_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t13_trees_3,t56_finseq_1,d9_trees_3]),
    [file(trees_3,t30_trees_3),interesting(0.80)]).

fof(t10_trees_3,theorem,(
    ! [A,B] : 
      ( ( v3_trees_3(A)
        & v3_trees_3(B) )
     => v3_trees_3(k5_xboole_0(A,B)) ) ),
    inference(mizar_proof,[status(thm)],[d5_trees_3,d5_trees_3,t1_xboole_0]),
    [file(trees_3,t10_trees_3),interesting(0.79)]).

fof(t22_trees_3,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => r1_tarski(k5_trees_3(A),k4_trees_3(A)) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d6_trees_3,d7_trees_3]),
    [file(trees_3,t22_trees_3),interesting(0.79)]).

fof(t17_trees_3,theorem,(
    ! [A,B] : 
      ( v2_trees_3(k2_tarski(A,B))
    <=> ( ~ v1_xboole_0(A)
        & v1_finset_1(A)
        & v1_trees_1(A)
        & ~ v1_xboole_0(B)
        & v1_finset_1(B)
        & v1_trees_1(B) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_trees_3,d2_tarski,d4_trees_3,d2_tarski]),
    [file(trees_3,t17_trees_3),interesting(0.79)]).

fof(t18_trees_3,theorem,(
    ! [A,B] : 
      ( v3_trees_3(k2_tarski(A,B))
    <=> ( v1_relat_1(A)
        & v1_funct_1(A)
        & v3_trees_2(A)
        & v1_relat_1(B)
        & v1_funct_1(B)
        & v3_trees_2(B) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_trees_3,d2_tarski,d5_trees_3,d2_tarski]),
    [file(trees_3,t18_trees_3),interesting(0.79)]).

fof(t4_trees_3,theorem,(
    ! [A,B] : 
      ( ( v1_trees_3(A)
        & v1_trees_3(B) )
     => v1_trees_3(k5_xboole_0(A,B)) ) ),
    inference(mizar_proof,[status(thm)],[d3_trees_3,d3_trees_3,t1_xboole_0]),
    [file(trees_3,t4_trees_3),interesting(0.79)]).

fof(t7_trees_3,theorem,(
    ! [A,B] : 
      ( ( v2_trees_3(A)
        & v2_trees_3(B) )
     => v2_trees_3(k5_xboole_0(A,B)) ) ),
    inference(mizar_proof,[status(thm)],[d4_trees_3,d4_trees_3,t1_xboole_0]),
    [file(trees_3,t7_trees_3),interesting(0.79)]).

fof(t40_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A)
        & v6_trees_3(A) )
     => k3_finseq_1(k2_funct_6(A)) = k3_finseq_1(A) ) ),
    inference(mizar_proof,[status(thm)],[t39_trees_3,d3_finseq_1,t8_finseq_1]),
    [file(trees_3,t40_trees_3),interesting(0.78)]).

fof(t79_trees_3,theorem,(
    k15_trees_3(k2_trees_1(0),k2_trees_1(0)) = k2_trees_1(2) ),
    inference(mizar_proof,[status(thm)],[t75_finseq_2,t57_trees_3]),
    [file(trees_3,t79_trees_3),interesting(0.78)]).

fof(t32_trees_3,theorem,(
    ! [A] : 
      ( v6_trees_3(k9_finseq_1(A))
    <=> ( v1_relat_1(A)
        & v1_funct_1(A)
        & v3_trees_2(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t15_trees_3,t56_finseq_1,d11_trees_3]),
    [file(trees_3,t32_trees_3),interesting(0.76)]).

fof(t53_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A)
        & v4_trees_3(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B)
            & v4_trees_3(B) )
         => ( k13_trees_3(A) = k13_trees_3(B)
           => A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t52_trees_3,t57_finseq_1,d5_real_1,t28_nat_1,t38_nat_1,t52_trees_3,t18_finseq_1]),
    [file(trees_3,t53_trees_3),interesting(0.76)]).

fof(t65_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => r1_tarski(k2_trees_1(1),k14_trees_3(A)) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t47_finseq_1,t9_modal_1,d2_tarski,t47_trees_1,t63_trees_3]),
    [file(trees_3,t65_trees_3),interesting(0.76)]).

fof(t31_trees_3,theorem,(
    ! [A] : 
      ( v5_trees_3(k9_finseq_1(A))
    <=> ( ~ v1_xboole_0(A)
        & v1_finset_1(A)
        & v1_trees_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t14_trees_3,t56_finseq_1,d10_trees_3]),
    [file(trees_3,t31_trees_3),interesting(0.75)]).

fof(t72_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( r2_hidden(C,A)
              <=> r2_hidden(k7_finseq_1(k12_finseq_1(k5_numbers,0),C),k15_trees_3(A,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_finseq_1,t47_finseq_1,d9_finseq_1,t23_trees_3,t54_trees_3]),
    [file(trees_3,t72_trees_3),interesting(0.75)]).

fof(t43_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => m9_trees_3(A,k2_trees_1(0)) ) ),
    inference(mizar_proof,[status(thm)],[d14_trees_3,d1_tarski,t56_trees_1,t2_xboole_1,d8_xboole_0]),
    [file(trees_3,t43_trees_3),interesting(0.74)]).

fof(t67_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ( k14_trees_3(A) = k14_trees_3(B)
           => A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_trees_2,t64_trees_3]),
    [file(trees_3,t67_trees_3),interesting(0.74)]).

fof(t73_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( r2_hidden(C,B)
              <=> r2_hidden(k7_finseq_1(k12_finseq_1(k5_numbers,1),C),k15_trees_3(A,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t47_finseq_1,t57_finseq_1,d9_finseq_1,t23_trees_3,t54_trees_3]),
    [file(trees_3,t73_trees_3),interesting(0.74)]).

fof(t33_trees_3,theorem,(
    ! [A,B] : 
      ( v4_trees_3(k10_finseq_1(A,B))
    <=> ( ~ v1_xboole_0(A)
        & v1_trees_1(A)
        & ~ v1_xboole_0(B)
        & v1_trees_1(B) ) ) ),
    inference(mizar_proof,[status(thm)],[t16_trees_3,t147_finseq_2,d9_trees_3]),
    [file(trees_3,t33_trees_3),interesting(0.73)]).

fof(t5_trees_3,theorem,(
    ! [A,B] : 
      ( v1_trees_3(A)
     => ( v1_trees_3(k3_xboole_0(A,B))
        & v1_trees_3(k3_xboole_0(B,A))
        & v1_trees_3(k4_xboole_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_trees_3,d3_trees_3,d3_xboole_0,d3_trees_3,d4_xboole_0]),
    [file(trees_3,t5_trees_3),interesting(0.72)]).

fof(t11_trees_3,theorem,(
    ! [A,B] : 
      ( v3_trees_3(A)
     => ( v3_trees_3(k3_xboole_0(A,B))
        & v3_trees_3(k3_xboole_0(B,A))
        & v3_trees_3(k4_xboole_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_trees_3,d5_trees_3,d3_xboole_0,d5_trees_3,d4_xboole_0]),
    [file(trees_3,t11_trees_3),interesting(0.71)]).

fof(t26_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v6_trees_3(A)
      <=> ! [B] : 
            ( r2_hidden(B,k1_relat_1(A))
           => ( v1_relat_1(k1_funct_1(A,B))
              & v1_funct_1(k1_funct_1(A,B))
              & v3_trees_2(k1_funct_1(A,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_trees_3,d11_trees_3,d5_funct_1,d5_trees_3,d11_trees_3,d5_funct_1]),
    [file(trees_3,t26_trees_3),interesting(0.71)]).

fof(t24_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v4_trees_3(A)
      <=> ! [B] : 
            ( r2_hidden(B,k1_relat_1(A))
           => ( ~ v1_xboole_0(k1_funct_1(A,B))
              & v1_trees_1(k1_funct_1(A,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_trees_3,d9_trees_3,d5_funct_1,d3_trees_3,d9_trees_3,d5_funct_1]),
    [file(trees_3,t24_trees_3),interesting(0.71)]).

fof(t42_trees_3,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v3_trees_2(C)
                & m3_trees_2(C,k2_zfmisc_1(A,B)) )
             => k6_trees_3(A,B,k10_trees_3(A,B,C),k11_trees_3(A,B,C)) = C ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_funct_2,d9_trees_2,t46_relat_1,t70_funct_3,t69_funct_3,t41_trees_3,t41_trees_3,t23_mcart_1,t9_funct_1]),
    [file(trees_3,t42_trees_3),interesting(0.71)]).

fof(t66_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ( r1_tarski(A,B)
           => r1_tarski(k14_trees_3(A),k14_trees_3(B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t63_trees_3,t63_trees_3]),
    [file(trees_3,t66_trees_3),interesting(0.71)]).

fof(t81_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A)
        & v5_trees_3(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_finset_1(B)
            & v1_trees_1(B) )
         => ~ ( r2_hidden(B,k2_relat_1(A))
              & r1_xreal_0(k6_trees_1(k13_trees_3(A)),k6_trees_1(B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_funct_1,t27_finseq_3,t28_nat_1,t47_finseq_1,t38_nat_1,t47_trees_1,d15_trees_3,t52_trees_3,t85_trees_1]),
    [file(trees_3,t81_trees_3),interesting(0.71)]).

fof(t84_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_finset_1(B)
            & v1_trees_1(B) )
         => k6_trees_1(k15_trees_3(A,B)) = k2_xcmplx_0(k4_square_1(k6_trees_1(A),k6_trees_1(B)),1) ) ) ),
    inference(mizar_proof,[status(thm)],[t147_finseq_2,d2_square_1,d2_tarski,d2_tarski,t46_square_1,t82_trees_3]),
    [file(trees_3,t84_trees_3),interesting(0.71)]).

fof(t8_trees_3,theorem,(
    ! [A,B] : 
      ( v2_trees_3(A)
     => ( v2_trees_3(k3_xboole_0(A,B))
        & v2_trees_3(k3_xboole_0(B,A))
        & v2_trees_3(k4_xboole_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_trees_3,d4_trees_3,d3_xboole_0,d4_trees_3,d4_xboole_0]),
    [file(trees_3,t8_trees_3),interesting(0.71)]).

fof(t74_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => r1_tarski(k2_trees_1(2),k15_trees_3(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d1_enumset1,t47_finseq_1,t10_modal_1,t47_trees_1,t71_trees_3]),
    [file(trees_3,t74_trees_3),interesting(0.70)]).

fof(t29_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ( ( v6_trees_3(A)
              & v6_trees_3(B) )
          <=> v6_trees_3(k7_finseq_1(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t44_finseq_1,d11_trees_3,t9_trees_3,d11_trees_3,d11_trees_3,t9_trees_3,d11_trees_3,t9_trees_3,d11_trees_3]),
    [file(trees_3,t29_trees_3),interesting(0.68)]).

fof(t27_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ( ( v4_trees_3(A)
              & v4_trees_3(B) )
          <=> v4_trees_3(k7_finseq_1(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t44_finseq_1,d9_trees_3,t3_trees_3,d9_trees_3,d9_trees_3,t3_trees_3,d9_trees_3,t3_trees_3,d9_trees_3]),
    [file(trees_3,t27_trees_3),interesting(0.67)]).

fof(t28_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ( ( v5_trees_3(A)
              & v5_trees_3(B) )
          <=> v5_trees_3(k7_finseq_1(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t44_finseq_1,d10_trees_3,t6_trees_3,d10_trees_3,d10_trees_3,t6_trees_3,d10_trees_3,t6_trees_3,d10_trees_3]),
    [file(trees_3,t28_trees_3),interesting(0.67)]).

fof(t35_trees_3,theorem,(
    ! [A,B] : 
      ( v6_trees_3(k10_finseq_1(A,B))
    <=> ( v1_relat_1(A)
        & v1_funct_1(A)
        & v3_trees_2(A)
        & v1_relat_1(B)
        & v1_funct_1(B)
        & v3_trees_2(B) ) ) ),
    inference(mizar_proof,[status(thm)],[t18_trees_3,t147_finseq_2,d11_trees_3]),
    [file(trees_3,t35_trees_3),interesting(0.67)]).

fof(t34_trees_3,theorem,(
    ! [A,B] : 
      ( v5_trees_3(k10_finseq_1(A,B))
    <=> ( ~ v1_xboole_0(A)
        & v1_finset_1(A)
        & v1_trees_1(A)
        & ~ v1_xboole_0(B)
        & v1_finset_1(B)
        & v1_trees_1(B) ) ) ),
    inference(mizar_proof,[status(thm)],[t17_trees_3,t147_finseq_2,d10_trees_3]),
    [file(trees_3,t34_trees_3),interesting(0.66)]).

fof(t64_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ( r2_hidden(B,A)
          <=> r2_hidden(k7_finseq_1(k12_finseq_1(k5_numbers,0),B),k14_trees_3(A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t63_trees_3,d15_trees_3,t58_finseq_1,t46_finseq_1,t57_finseq_1]),
    [file(trees_3,t64_trees_3),interesting(0.64)]).

fof(l54_trees_3,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v3_trees_2(B)
            & m3_trees_2(B,A) )
         => ( v1_funct_1(B)
            & v1_funct_2(B,k1_relat_1(B),A)
            & m2_relset_1(B,k1_relat_1(B),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_trees_2,d1_funct_2,t11_relset_1]),
    [file(trees_3,l54_trees_3),interesting(0.61)]).

fof(t75_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ! [C] : 
              ( ( ~ v1_xboole_0(C)
                & v1_trees_1(C) )
             => ! [D] : 
                  ( ( ~ v1_xboole_0(D)
                    & v1_trees_1(D) )
                 => ( ( r1_tarski(A,C)
                      & r1_tarski(B,D) )
                   => r1_tarski(k15_trees_3(A,B),k15_trees_3(C,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t71_trees_3,t71_trees_3]),
    [file(trees_3,t75_trees_3),interesting(0.61)]).

fof(t46_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ! [C] : 
              ( m2_finseq_1(C,k5_numbers)
             => ( r2_hidden(C,k3_trees_1(A))
               => r1_tarski(A,k5_trees_1(A,C,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d8_trees_1,d12_trees_1]),
    [file(trees_3,t46_trees_3),interesting(0.59)]).

fof(t61_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => k14_trees_3(A) = k5_trees_1(k2_trees_1(1),k12_finseq_1(k5_numbers,0),A) ) ),
    inference(mizar_proof,[status(thm)],[d1_trees_2,t57_finseq_1,t47_trees_1,t9_modal_1,d2_tarski,d15_trees_3,t50_finseq_1,t38_nat_1,d12_trees_1,t47_trees_1,d12_trees_1,t47_finseq_1,t9_modal_1,d2_tarski,d15_trees_3,d15_trees_3]),
    [file(trees_3,t61_trees_3),interesting(0.58)]).

fof(t36_trees_3,theorem,(
    ! [A,B] : 
      ( m2_subset_1(B,k1_numbers,k5_numbers)
     => ( B != 0
       => ( v4_trees_3(k2_finseq_2(B,A))
        <=> ( ~ v1_xboole_0(A)
            & v1_trees_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_finseq_1,d2_finseq_2,t14_funcop_1,d9_trees_3,t13_trees_3]),
    [file(trees_3,t36_trees_3),interesting(0.54)]).

fof(t47_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v3_trees_2(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v3_trees_2(B) )
         => ! [C] : 
              ( m1_trees_1(C,k1_relat_1(A))
             => k1_funct_1(k8_trees_2(A,C,B),C) = k1_funct_1(B,k1_xboole_0) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d12_trees_1,d12_trees_2,d12_trees_2,t47_finseq_1,t46_finseq_1]),
    [file(trees_3,t47_trees_3),interesting(0.54)]).

fof(t59_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A)
        & v4_trees_3(A) )
     => k13_trees_3(k7_finseq_1(A,k9_finseq_1(k2_trees_1(0)))) = k2_xboole_0(k13_trees_3(A),k2_trees_1(k1_nat_1(k3_finseq_1(A),1))) ) ),
    inference(mizar_proof,[status(thm)],[t38_nat_1,t55_trees_1,d2_xboole_0,t47_trees_1,t56_trees_1,t37_zfmisc_1,d3_tarski,d9_trees_1,t57_trees_1,t57_finseq_1,t35_finseq_1,t25_finseq_1,t47_trees_1,t58_finseq_1,t57_finseq_1,d15_trees_3,t50_trees_3,d10_xboole_0,t58_trees_3,t8_trees_2]),
    [file(trees_3,t59_trees_3),interesting(0.54)]).

fof(t38_trees_3,theorem,(
    ! [A,B] : 
      ( m2_subset_1(B,k1_numbers,k5_numbers)
     => ( B != 0
       => ( v6_trees_3(k2_finseq_2(B,A))
        <=> ( v1_relat_1(A)
            & v1_funct_1(A)
            & v3_trees_2(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_finseq_1,d2_finseq_2,t14_funcop_1,d11_trees_3,t15_trees_3]),
    [file(trees_3,t38_trees_3),interesting(0.49)]).

fof(l1_trees_3,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( ( r1_xreal_0(1,A)
                  & r1_xreal_0(A,k3_finseq_1(B)) )
               => k1_funct_1(k7_finseq_1(B,C),A) = k1_funct_1(B,A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t27_finseq_3,d7_finseq_1]),
    [file(trees_3,l1_trees_3),interesting(0.49)]).

fof(t37_trees_3,theorem,(
    ! [A,B] : 
      ( m2_subset_1(B,k1_numbers,k5_numbers)
     => ( B != 0
       => ( v5_trees_3(k2_finseq_2(B,A))
        <=> ( ~ v1_xboole_0(A)
            & v1_finset_1(A)
            & v1_trees_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_finseq_1,d2_finseq_2,t14_funcop_1,d10_trees_3,t14_trees_3]),
    [file(trees_3,t37_trees_3),interesting(0.48)]).

fof(t25_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v5_trees_3(A)
      <=> ! [B] : 
            ( r2_hidden(B,k1_relat_1(A))
           => ( ~ v1_xboole_0(k1_funct_1(A,B))
              & v1_finset_1(k1_funct_1(A,B))
              & v1_trees_1(k1_funct_1(A,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_trees_3,d10_trees_3,d5_funct_1,d4_trees_3,d10_trees_3,d5_funct_1]),
    [file(trees_3,t25_trees_3),interesting(0.47)]).

fof(t63_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( r2_hidden(B,k14_trees_3(A))
        <=> ~ ( B != k1_xboole_0
              & ! [C] : 
                  ( ( v1_relat_1(C)
                    & v1_funct_1(C)
                    & v1_finseq_1(C) )
                 => ~ ( r2_hidden(C,A)
                      & B = k7_finseq_1(k12_finseq_1(k5_numbers,0),C) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t57_finseq_1,d15_trees_3,t38_nat_1,d15_trees_3]),
    [file(trees_3,t63_trees_3),interesting(0.46)]).

fof(t82_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A)
        & v5_trees_3(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_finset_1(B)
            & v1_trees_1(B) )
         => ( ( r2_hidden(B,k2_relat_1(A))
              & ! [C] : 
                  ( ( ~ v1_xboole_0(C)
                    & v1_finset_1(C)
                    & v1_trees_1(C) )
                 => ( r2_hidden(C,k2_relat_1(A))
                   => r1_xreal_0(k6_trees_1(C),k6_trees_1(B)) ) ) )
           => k6_trees_1(k13_trees_3(A)) = k1_nat_1(k6_trees_1(B),1) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t81_trees_3,t80_trees_3,t38_nat_1,t1_xreal_1]),
    [file(trees_3,t82_trees_3),interesting(0.45)]).

fof(t54_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B)
            & v4_trees_3(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C)
                & v4_trees_3(C) )
             => ! [D] : 
                  ( ( ~ v1_xboole_0(D)
                    & v1_trees_1(D) )
                 => ( r2_hidden(A,D)
                  <=> r2_hidden(k7_finseq_1(k12_finseq_1(k5_numbers,k3_finseq_1(B)),A),k13_trees_3(k7_finseq_1(k7_finseq_1(B,k9_finseq_1(D)),C))) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t35_finseq_1,t57_finseq_1,t29_nat_1,t38_nat_1,t2_xreal_1,t29_nat_1,t27_finseq_3,d7_finseq_1,t59_finseq_1,d15_trees_3,d15_trees_3,t58_finseq_1,t46_finseq_1]),
    [file(trees_3,t54_trees_3),interesting(0.42)]).

fof(t60_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A)
        & v4_trees_3(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B)
            & v4_trees_3(B) )
         => ! [C] : 
              ( ( ~ v1_xboole_0(C)
                & v1_trees_1(C) )
             => ! [D] : 
                  ( ( ~ v1_xboole_0(D)
                    & v1_trees_1(D) )
                 => k13_trees_3(k7_finseq_1(k7_finseq_1(A,k9_finseq_1(C)),B)) = k5_trees_1(k13_trees_3(k7_finseq_1(k7_finseq_1(A,k9_finseq_1(D)),B)),k12_finseq_1(k5_numbers,k3_finseq_1(A)),C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t57_finseq_1,t35_finseq_1,t29_nat_1,t38_nat_1,t2_xreal_1,d9_trees_3,l62_trees_3,d3_trees_3,t47_finseq_1,t47_trees_1,d15_trees_3,d1_trees_2,d15_trees_3,t50_finseq_1,t38_nat_1,l62_trees_3,t39_finseq_1,d7_finseq_1,d7_finseq_1,d15_trees_3,t6_modal_1,d8_xboole_0,d12_trees_1,t59_finseq_1,t38_nat_1,l62_trees_3,d7_finseq_1,d12_trees_1,t38_nat_1,t9_xreal_1,t36_finseq_1,d15_trees_3,t38_nat_1,t6_modal_1,d8_xboole_0,d12_trees_1,d5_real_1,t47_trees_1,d12_trees_1,d15_trees_3,t59_finseq_1,t29_nat_1,t38_nat_1,l62_trees_3,t2_xreal_1,d7_finseq_1,d15_trees_3,t50_finseq_1,d15_trees_3,t33_trees_1,t47_trees_1,d15_trees_3,d5_real_1,t45_finseq_1,t29_nat_1,t38_nat_1,t8_xreal_1,l1_trees_3,t37_finseq_1,d15_trees_3]),
    [file(trees_3,t60_trees_3),interesting(0.41)]).

fof(t41_trees_3,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v3_trees_2(C)
                & m3_trees_2(C,k2_zfmisc_1(A,B)) )
             => ! [D] : 
                  ( m1_trees_1(D,k1_relat_1(C))
                 => ( k2_domain_1(A,B,k3_trees_2(k2_zfmisc_1(A,B),C,D)) = k1_funct_1(k10_trees_3(A,B,C),D)
                    & k1_funct_1(k11_trees_3(A,B,C),D) = k3_domain_1(A,B,k3_trees_2(k2_zfmisc_1(A,B),C,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_funct_2,d9_trees_2,t46_relat_1,t22_funct_1,t23_mcart_1,d5_funct_3,d6_funct_3]),
    [file(trees_3,t41_trees_3),interesting(0.39)]).

fof(t58_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B)
            & v4_trees_3(B) )
         => k13_trees_3(k7_finseq_1(B,k9_finseq_1(A))) = k5_trees_1(k2_xboole_0(k13_trees_3(B),k2_trees_1(k1_nat_1(k3_finseq_1(B),1))),k12_finseq_1(k5_numbers,k3_finseq_1(B)),A) ) ) ),
    inference(mizar_proof,[status(thm)],[t57_finseq_1,t35_finseq_1,t38_nat_1,t55_trees_1,d2_xboole_0,d1_trees_2,d15_trees_3,t50_finseq_1,t38_nat_1,l62_trees_3,d7_finseq_1,d15_trees_3,d2_xboole_0,t6_modal_1,d8_xboole_0,d12_trees_1,t59_finseq_1,d12_trees_1,d5_real_1,t47_trees_1,t59_finseq_1,t38_nat_1,d15_trees_3,d2_xboole_0,d15_trees_3,l62_trees_3,t38_nat_1,t2_xreal_1,d7_finseq_1,d15_trees_3,t57_trees_1,t47_trees_1,d9_trees_3,l62_trees_3,d3_trees_3,t47_trees_1,t47_finseq_1,d15_trees_3,t38_nat_1,t1_xreal_1,t59_finseq_1,t38_nat_1,t47_trees_1,d15_trees_3,d12_trees_1]),
    [file(trees_3,t58_trees_3),interesting(0.39)]).

fof(l62_trees_3,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ( ~ r1_xreal_0(k3_finseq_1(B),A)
           => ( r2_hidden(k1_nat_1(A,1),k4_finseq_1(B))
              & r2_hidden(k1_funct_1(B,k1_nat_1(A,1)),k2_relat_1(B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t38_nat_1,t27_finseq_3,d5_funct_1]),
    [file(trees_3,l62_trees_3),interesting(0.38)]).

fof(t80_trees_3,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B)
            & v5_trees_3(B) )
         => ( ! [C] : 
                ( ( ~ v1_xboole_0(C)
                  & v1_finset_1(C)
                  & v1_trees_1(C) )
               => ( r2_hidden(C,k2_relat_1(B))
                 => r1_xreal_0(k6_trees_1(C),A) ) )
           => r1_xreal_0(k6_trees_1(k13_trees_3(B)),k1_nat_1(A,1)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_trees_1,d15_trees_3,t25_finseq_1,d10_trees_3,l62_trees_3,d4_trees_3,t50_finseq_1,t57_finseq_1,d15_trees_1,t2_xreal_1,t35_finseq_1,t9_xreal_1]),
    [file(trees_3,t80_trees_3),interesting(0.31)]).

fof(t71_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ! [C] : 
              ( r2_hidden(C,k15_trees_3(A,B))
            <=> ~ ( C != k1_xboole_0
                  & ! [D] : 
                      ( ( v1_relat_1(D)
                        & v1_funct_1(D)
                        & v1_finseq_1(D) )
                     => ( ~ ( r2_hidden(D,A)
                            & C = k7_finseq_1(k12_finseq_1(k5_numbers,0),D) )
                        & ~ ( r2_hidden(D,B)
                            & C = k7_finseq_1(k12_finseq_1(k5_numbers,1),D) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t61_finseq_1,d15_trees_3,t38_nat_1,d5_real_1,t38_nat_1,t58_finseq_1,t61_finseq_1,d15_trees_3]),
    [file(trees_3,t71_trees_3),interesting(0.30)]).

fof(t52_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ( v4_trees_3(A)
       => ( k2_trees_2(k13_trees_3(A),1) = a_1_0_trees_3(A)
          & ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ( ~ r1_xreal_0(k3_finseq_1(A),B)
               => k4_trees_1(k13_trees_3(A),k12_finseq_1(k5_numbers,B)) = k1_funct_1(A,k1_nat_1(B,1)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_trees_3,d3_tarski,t57_finseq_1,d15_trees_3,t6_trees_1,d10_xboole_0,d3_tarski,l62_trees_3,d3_trees_3,t47_finseq_1,d11_finseq_1,t47_trees_1,d15_trees_3,t56_finseq_1,l62_trees_3,d3_trees_3,t47_finseq_1,d11_finseq_1,t47_trees_1,d15_trees_3,d1_trees_2,d9_trees_1,d15_trees_3,t58_finseq_1,t46_finseq_1,d15_trees_3,t46_trees_1,d9_trees_1]),
    [file(trees_3,t52_trees_3),interesting(0.25)]).

fof(t44_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ( ( r1_tarski(k2_trees_2(A,1),k2_trees_2(B,1))
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( r2_hidden(k12_finseq_1(k5_numbers,C),A)
                   => k4_trees_1(A,k12_finseq_1(k5_numbers,C)) = k4_trees_1(B,k12_finseq_1(k5_numbers,C)) ) ) )
           => r1_tarski(A,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t4_modal_1,t56_finseq_1,t46_trees_1,d9_trees_1,d9_trees_1,t47_trees_1]),
    [file(trees_3,t44_trees_3),interesting(0.15)]).

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(t61_finseq_1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C)
        & v1_finseq_1(C) )
     => ( C = k10_finseq_1(A,B)
      <=> ( k3_finseq_1(C) = 2
          & k1_funct_1(C,1) = A
          & k1_funct_1(C,2) = B ) ) ) ),
    file(finseq_1,t61_finseq_1),
    [interesting(0.00)]).

fof(t4_finseq_1,theorem,
    ( k2_finseq_1(0) = k1_xboole_0
    & k2_finseq_1(1) = k1_tarski(1)
    & k2_finseq_1(2) = k2_tarski(1,2) ),
    file(finseq_1,t4_finseq_1),
    [interesting(0.00)]).

fof(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(d1_tarski,definition,(
    ! [A,B] : 
      ( B = k1_tarski(A)
    <=> ! [C] : 
          ( r2_hidden(C,B)
        <=> C = A ) ) ),
    file(tarski,d1_tarski),
    [interesting(0.00)]).

fof(d2_tarski,definition,(
    ! [A,B,C] : 
      ( C = k2_tarski(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( D = A
            | D = B ) ) ) ),
    file(tarski,d2_tarski),
    [interesting(0.00)]).

fof(t8_funct_1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( r2_hidden(k4_tarski(A,B),C)
      <=> ( r2_hidden(A,k1_relat_1(C))
          & B = k1_funct_1(C,A) ) ) ) ),
    file(funct_1,t8_funct_1),
    [interesting(0.00)]).

fof(d9_trees_2,definition,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => ( m3_trees_2(B,A)
      <=> r1_tarski(k2_relat_1(B),A) ) ) ),
    file(trees_2,d9_trees_2),
    [interesting(0.00)]).

fof(d1_funct_2,definition,(
    ! [A,B,C] : 
      ( m2_relset_1(C,A,B)
     => ( ( ( B = k1_xboole_0
           => A = k1_xboole_0 )
         => ( v1_funct_2(C,A,B)
          <=> A = k4_relset_1(A,B,C) ) )
        & ( B = k1_xboole_0
         => ( A = k1_xboole_0
            | ( v1_funct_2(C,A,B)
            <=> C = k1_xboole_0 ) ) ) ) ) ),
    file(funct_2,d1_funct_2),
    [interesting(0.00)]).

fof(t11_relset_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => ( ( r1_tarski(k1_relat_1(C),A)
          & r1_tarski(k2_relat_1(C),B) )
       => m2_relset_1(C,A,B) ) ) ),
    file(relset_1,t11_relset_1),
    [interesting(0.00)]).

fof(d5_trees_3,definition,(
    ! [A] : 
      ( v3_trees_3(A)
    <=> ! [B] : 
          ( r2_hidden(B,A)
         => ( v1_relat_1(B)
            & v1_funct_1(B)
            & v3_trees_2(B) ) ) ) ),
    file(trees_3,d5_trees_3),
    [interesting(0.00)]).

fof(t1_xboole_0,theorem,(
    ! [A,B,C] : 
      ( r2_hidden(A,k5_xboole_0(B,C))
    <=> ~ ( r2_hidden(A,B)
        <=> r2_hidden(A,C) ) ) ),
    file(xboole_0,t1_xboole_0),
    [interesting(0.00)]).

fof(d3_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k3_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            & r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d3_xboole_0),
    [interesting(0.00)]).

fof(d4_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k4_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            & ~ r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d4_xboole_0),
    [interesting(0.00)]).

fof(d3_trees_3,definition,(
    ! [A] : 
      ( v1_trees_3(A)
    <=> ! [B] : 
          ( r2_hidden(B,A)
         => ( ~ v1_xboole_0(B)
            & v1_trees_1(B) ) ) ) ),
    file(trees_3,d3_trees_3),
    [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(d1_trees_3,definition,(
    ! [A] : 
      ( A = k1_trees_3
    <=> ! [B] : 
          ( r2_hidden(B,A)
        <=> ( ~ v1_xboole_0(B)
            & v1_trees_1(B) ) ) ) ),
    file(trees_3,d1_trees_3),
    [interesting(0.00)]).

fof(d4_trees_3,definition,(
    ! [A] : 
      ( v2_trees_3(A)
    <=> ! [B] : 
          ( r2_hidden(B,A)
         => ( ~ v1_xboole_0(B)
            & v1_finset_1(B)
            & v1_trees_1(B) ) ) ) ),
    file(trees_3,d4_trees_3),
    [interesting(0.00)]).

fof(d6_trees_3,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m4_trees_3(B,A)
        <=> ! [C] : 
              ( r2_hidden(C,B)
             => ( v1_funct_1(C)
                & v3_trees_2(C)
                & m3_trees_2(C,A) ) ) ) ) ),
    file(trees_3,d6_trees_3),
    [interesting(0.00)]).

fof(d7_trees_3,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m4_trees_3(B,A)
         => ( B = k4_trees_3(A)
          <=> ! [C] : 
                ( ( v1_funct_1(C)
                  & v3_trees_2(C)
                  & m3_trees_2(C,A) )
               => r2_hidden(C,B) ) ) ) ) ),
    file(trees_3,d7_trees_3),
    [interesting(0.00)]).

fof(d10_trees_3,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v5_trees_3(A)
      <=> v2_trees_3(k2_relat_1(A)) ) ) ),
    file(trees_3,d10_trees_3),
    [interesting(0.00)]).

fof(d5_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( B = k2_relat_1(A)
        <=> ! [C] : 
              ( r2_hidden(C,B)
            <=> ? [D] : 
                  ( r2_hidden(D,k1_relat_1(A))
                  & C = k1_funct_1(A,D) ) ) ) ) ),
    file(funct_1,d5_funct_1),
    [interesting(0.00)]).

fof(t44_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => k2_relat_1(k7_finseq_1(A,B)) = k2_xboole_0(k2_relat_1(A),k2_relat_1(B)) ) ) ),
    file(finseq_1,t44_finseq_1),
    [interesting(0.00)]).

fof(d9_trees_3,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v4_trees_3(A)
      <=> v1_trees_3(k2_relat_1(A)) ) ) ),
    file(trees_3,d9_trees_3),
    [interesting(0.00)]).

fof(d2_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k2_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            | r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d2_xboole_0),
    [interesting(0.00)]).

fof(d11_trees_3,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v6_trees_3(A)
      <=> v3_trees_3(k2_relat_1(A)) ) ) ),
    file(trees_3,d11_trees_3),
    [interesting(0.00)]).

fof(d2_trees_3,definition,(
    ! [A] : 
      ( m1_subset_1(A,k1_zfmisc_1(k1_trees_3))
     => ( A = k2_trees_3
      <=> ! [B] : 
            ( r2_hidden(B,A)
          <=> ( ~ v1_xboole_0(B)
              & v1_finset_1(B)
              & v1_trees_1(B) ) ) ) ) ),
    file(trees_3,d2_trees_3),
    [interesting(0.00)]).

fof(t56_finseq_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => ( B = k9_finseq_1(A)
      <=> ( k3_finseq_1(B) = 1
          & k2_relat_1(B) = k1_tarski(A) ) ) ) ),
    file(finseq_1,t56_finseq_1),
    [interesting(0.00)]).

fof(t147_finseq_2,theorem,(
    ! [A,B] : k2_relat_1(k10_finseq_1(A,B)) = k2_tarski(A,B) ),
    file(finseq_2,t147_finseq_2),
    [interesting(0.00)]).

fof(t5_finseq_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ( A = 0
        | r2_hidden(A,k2_finseq_1(A)) ) ) ),
    file(finseq_1,t5_finseq_1),
    [interesting(0.00)]).

fof(d2_finseq_2,definition,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : k2_finseq_2(A,B) = k2_funcop_1(k2_finseq_1(A),B) ) ),
    file(finseq_2,d2_finseq_2),
    [interesting(0.00)]).

fof(t14_funcop_1,theorem,(
    ! [A,B] : 
      ( A != k1_xboole_0
     => k2_relat_1(k2_funcop_1(A,B)) = k1_tarski(B) ) ),
    file(funcop_1,t14_funcop_1),
    [interesting(0.00)]).

fof(d2_funct_6,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( B = k2_funct_6(A)
          <=> ( k1_relat_1(B) = k10_relat_1(A,k1_funct_6(k2_relat_1(A)))
              & ! [C] : 
                  ( r2_hidden(C,k10_relat_1(A,k1_funct_6(k2_relat_1(A))))
                 => k1_funct_1(B,C) = k1_funct_5(k1_funct_1(A,C)) ) ) ) ) ) ),
    file(funct_6,d2_funct_6),
    [interesting(0.00)]).

fof(t167_relat_1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => r1_tarski(k10_relat_1(B,A),k1_relat_1(B)) ) ),
    file(relat_1,t167_relat_1),
    [interesting(0.00)]).

fof(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(t28_funct_6,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ( r2_hidden(A,k10_relat_1(B,k1_funct_6(k2_relat_1(B))))
      <=> ( r2_hidden(A,k1_relat_1(B))
          & v1_relat_1(k1_funct_1(B,A))
          & v1_funct_1(k1_funct_1(B,A)) ) ) ) ),
    file(funct_6,t28_funct_6),
    [interesting(0.00)]).

fof(t31_funct_6,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ! [C] : 
          ( ( v1_relat_1(C)
            & v1_funct_1(C) )
         => ( ( r2_hidden(A,k1_relat_1(B))
              & C = k1_funct_1(B,A) )
           => ( r2_hidden(A,k1_relat_1(k2_funct_6(B)))
              & k1_funct_1(k2_funct_6(B),A) = k1_relat_1(C)
              & r2_hidden(A,k1_relat_1(k3_funct_6(B)))
              & k1_funct_1(k3_funct_6(B),A) = k2_relat_1(C) ) ) ) ) ),
    file(funct_6,t31_funct_6),
    [interesting(0.00)]).

fof(t8_finseq_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( k2_finseq_1(A) = k2_finseq_1(B)
           => A = B ) ) ) ),
    file(finseq_1,t8_finseq_1),
    [interesting(0.00)]).

fof(t46_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( r1_tarski(k2_relat_1(A),k1_relat_1(B))
           => k1_relat_1(k5_relat_1(A,B)) = k1_relat_1(A) ) ) ) ),
    file(relat_1,t46_relat_1),
    [interesting(0.00)]).

fof(t70_funct_3,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ! [C] : 
          ( ( v1_relat_1(C)
            & v1_funct_1(C) )
         => ( ( k1_relat_1(B) = A
              & k1_relat_1(C) = A )
           => k1_relat_1(k13_funct_3(B,C)) = A ) ) ) ),
    file(funct_3,t70_funct_3),
    [interesting(0.00)]).

fof(t69_funct_3,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ! [D] : 
          ( ( v1_relat_1(D)
            & v1_funct_1(D) )
         => ( ( k1_relat_1(C) = B
              & k1_relat_1(D) = B
              & r2_hidden(A,B) )
           => k1_funct_1(k13_funct_3(C,D),A) = k4_tarski(k1_funct_1(C,A),k1_funct_1(D,A)) ) ) ) ),
    file(funct_3,t69_funct_3),
    [interesting(0.00)]).

fof(t22_funct_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ! [C] : 
          ( ( v1_relat_1(C)
            & v1_funct_1(C) )
         => ( r2_hidden(A,k1_relat_1(k5_relat_1(C,B)))
           => k1_funct_1(k5_relat_1(C,B),A) = k1_funct_1(B,k1_funct_1(C,A)) ) ) ) ),
    file(funct_1,t22_funct_1),
    [interesting(0.00)]).

fof(t23_mcart_1,theorem,(
    ! [A,B,C] : 
      ( r2_hidden(A,k2_zfmisc_1(B,C))
     => A = k4_tarski(k1_mcart_1(A),k2_mcart_1(A)) ) ),
    file(mcart_1,t23_mcart_1),
    [interesting(0.00)]).

fof(d5_funct_3,definition,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( C = k7_funct_3(A,B)
      <=> ( k1_relat_1(C) = k2_zfmisc_1(A,B)
          & ! [D,E] : 
              ( ( r2_hidden(D,A)
                & r2_hidden(E,B) )
             => k1_funct_1(C,k4_tarski(D,E)) = D ) ) ) ) ),
    file(funct_3,d5_funct_3),
    [interesting(0.00)]).

fof(d6_funct_3,definition,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( C = k8_funct_3(A,B)
      <=> ( k1_relat_1(C) = k2_zfmisc_1(A,B)
          & ! [D,E] : 
              ( ( r2_hidden(D,A)
                & r2_hidden(E,B) )
             => k1_funct_1(C,k4_tarski(D,E)) = E ) ) ) ) ),
    file(funct_3,d6_funct_3),
    [interesting(0.00)]).

fof(t9_funct_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( ( k1_relat_1(A) = k1_relat_1(B)
              & ! [C] : 
                  ( r2_hidden(C,k1_relat_1(A))
                 => k1_funct_1(A,C) = k1_funct_1(B,C) ) )
           => A = B ) ) ) ),
    file(funct_1,t9_funct_1),
    [interesting(0.00)]).

fof(d14_trees_3,definition,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ( m9_trees_3(B,A)
          <=> ! [C] : 
                ( m1_trees_1(C,B)
               => ~ ( ~ r2_hidden(C,A)
                    & ! [D] : 
                        ( m8_trees_3(D,A)
                       => ~ r2_xboole_0(D,C) ) ) ) ) ) ) ),
    file(trees_3,d14_trees_3),
    [interesting(0.00)]).

fof(t56_trees_1,theorem,(
    k2_trees_1(0) = k1_tarski(k1_xboole_0) ),
    file(trees_1,t56_trees_1),
    [interesting(0.00)]).

fof(t2_xboole_1,theorem,(
    ! [A] : r1_tarski(k1_xboole_0,A) ),
    file(xboole_1,t2_xboole_1),
    [interesting(0.00)]).

fof(d8_xboole_0,definition,(
    ! [A,B] : 
      ( r2_xboole_0(A,B)
    <=> ( r1_tarski(A,B)
        & A != B ) ) ),
    file(xboole_0,d8_xboole_0),
    [interesting(0.00)]).

fof(t4_modal_1,theorem,(
    ! [A] : 
      ( m2_finseq_1(A,k5_numbers)
     => ~ ( A != k1_xboole_0
          & ! [B] : 
              ( m2_finseq_1(B,k5_numbers)
             => ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => A != k8_finseq_1(k5_numbers,k12_finseq_1(k5_numbers,C),B) ) ) ) ) ),
    file(modal_1,t4_modal_1),
    [interesting(0.00)]).

fof(t46_trees_1,theorem,(
    ! [A] : 
      ( m2_finseq_1(A,k5_numbers)
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( r2_hidden(k7_finseq_1(A,C),B)
               => r2_hidden(A,B) ) ) ) ) ),
    file(trees_1,t46_trees_1),
    [interesting(0.00)]).

fof(d9_trees_1,definition,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( m2_finseq_1(B,k5_numbers)
         => ( r2_hidden(B,A)
           => ! [C] : 
                ( ( ~ v1_xboole_0(C)
                  & v1_trees_1(C) )
               => ( C = k4_trees_1(A,B)
                <=> ! [D] : 
                      ( m2_finseq_1(D,k5_numbers)
                     => ( r2_hidden(D,C)
                      <=> r2_hidden(k8_finseq_1(k5_numbers,B,D),A) ) ) ) ) ) ) ) ),
    file(trees_1,d9_trees_1),
    [interesting(0.00)]).

fof(t47_trees_1,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ( r2_hidden(k1_xboole_0,A)
        & r2_hidden(k6_finseq_1(k5_numbers),A) ) ) ),
    file(trees_1,t47_trees_1),
    [interesting(0.00)]).

fof(t45_trees_3,theorem,(
    $true ),
    file(trees_3,t45_trees_3),
    [interesting(0.00)]).

fof(d8_trees_1,definition,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => ( B = k3_trees_1(A)
          <=> ! [C] : 
                ( m2_finseq_1(C,k5_numbers)
               => ( r2_hidden(C,B)
                <=> ( r2_hidden(C,A)
                    & ! [D] : 
                        ( m2_finseq_1(D,k5_numbers)
                       => ~ ( r2_hidden(D,A)
                            & r2_xboole_0(C,D) ) ) ) ) ) ) ) ) ),
    file(trees_1,d8_trees_1),
    [interesting(0.00)]).

fof(d12_trees_1,definition,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( m2_finseq_1(B,k5_numbers)
         => ! [C] : 
              ( ( ~ v1_xboole_0(C)
                & v1_trees_1(C) )
             => ( r2_hidden(B,A)
               => ! [D] : 
                    ( ( ~ v1_xboole_0(D)
                      & v1_trees_1(D) )
                   => ( D = k5_trees_1(A,B,C)
                    <=> ! [E] : 
                          ( m2_finseq_1(E,k5_numbers)
                         => ( r2_hidden(E,D)
                          <=> ~ ( ~ ( r2_hidden(E,A)
                                    & ~ r2_xboole_0(B,E) )
                                & ! [F] : 
                                    ( m2_finseq_1(F,k5_numbers)
                                   => ~ ( r2_hidden(F,C)
                                        & E = k8_finseq_1(k5_numbers,B,F) ) ) ) ) ) ) ) ) ) ) ) ),
    file(trees_1,d12_trees_1),
    [interesting(0.00)]).

fof(d12_trees_2,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v3_trees_2(A) )
     => ! [B] : 
          ( m2_finseq_1(B,k5_numbers)
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v3_trees_2(C) )
             => ( r2_hidden(B,k1_relat_1(A))
               => ! [D] : 
                    ( ( v1_relat_1(D)
                      & v1_funct_1(D)
                      & v3_trees_2(D) )
                   => ( D = k8_trees_2(A,B,C)
                    <=> ( k1_relat_1(D) = k5_trees_1(k1_relat_1(A),B,k1_relat_1(C))
                        & ! [E] : 
                            ( m2_finseq_1(E,k5_numbers)
                           => ~ ( r2_hidden(E,k5_trees_1(k1_relat_1(A),B,k1_relat_1(C)))
                                & ~ ( ~ r1_tarski(B,E)
                                    & k1_funct_1(D,E) = k1_funct_1(A,E) )
                                & ! [F] : 
                                    ( m2_finseq_1(F,k5_numbers)
                                   => ~ ( r2_hidden(F,k1_relat_1(C))
                                        & E = k8_finseq_1(k5_numbers,B,F)
                                        & k1_funct_1(D,E) = k1_funct_1(C,F) ) ) ) ) ) ) ) ) ) ) ) ),
    file(trees_2,d12_trees_2),
    [interesting(0.00)]).

fof(t47_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ( k7_finseq_1(A,k1_xboole_0) = A
        & k7_finseq_1(k1_xboole_0,A) = A ) ) ),
    file(finseq_1,t47_finseq_1),
    [interesting(0.00)]).

fof(t46_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( ( k7_finseq_1(A,B) = k7_finseq_1(C,B)
                  | k7_finseq_1(B,A) = k7_finseq_1(B,C) )
               => A = C ) ) ) ) ),
    file(finseq_1,t46_finseq_1),
    [interesting(0.00)]).

fof(t8_trees_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ( r1_tarski(A,B)
          <=> ? [C] : 
                ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C)
                & B = k7_finseq_1(A,C) ) ) ) ) ),
    file(trees_1,t8_trees_1),
    [interesting(0.00)]).

fof(t9_trees_2,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ! [C] : 
              ( m2_finseq_1(C,k5_numbers)
             => ! [D] : 
                  ( m2_finseq_1(D,k5_numbers)
                 => ( ( r2_hidden(C,A)
                      & r2_hidden(D,A) )
                   => ( r1_tarski(C,D)
                      | r2_hidden(D,k5_trees_1(A,C,B)) ) ) ) ) ) ) ),
    file(trees_2,t9_trees_2),
    [interesting(0.00)]).

fof(t48_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v3_trees_2(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v3_trees_2(B) )
         => ! [C] : 
              ( m1_trees_1(C,k1_relat_1(A))
             => ! [D] : 
                  ( m1_trees_1(D,k1_relat_1(A))
                 => ( ~ r1_tarski(C,D)
                   => k1_funct_1(k8_trees_2(A,C,B),D) = k1_funct_1(A,D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_trees_1,t9_trees_2,d12_trees_2,d12_trees_2]),
    [file(trees_3,t48_trees_3),interesting(0.00)]).

fof(t49_trees_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v3_trees_2(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v3_trees_2(B) )
         => ! [C] : 
              ( m1_trees_1(C,k1_relat_1(A))
             => ! [D] : 
                  ( m1_trees_1(D,k1_relat_1(B))
                 => k1_funct_1(k8_trees_2(A,C,B),k8_finseq_1(k5_numbers,C,D)) = k1_funct_1(B,D) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_trees_1,d12_trees_1,d12_trees_2,d12_trees_2,t46_finseq_1]),
    [file(trees_3,t49_trees_3),interesting(0.00)]).

fof(d15_trees_3,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ( v4_trees_3(A)
       => ! [B] : 
            ( ( ~ v1_xboole_0(B)
              & v1_trees_1(B) )
           => ( B = k13_trees_3(A)
            <=> ! [C] : 
                  ( r2_hidden(C,B)
                <=> ~ ( C != k1_xboole_0
                      & ! [D] : 
                          ( m2_subset_1(D,k1_numbers,k5_numbers)
                         => ! [E] : 
                              ( ( v1_relat_1(E)
                                & v1_funct_1(E)
                                & v1_finseq_1(E) )
                             => ~ ( ~ r1_xreal_0(k3_finseq_1(A),D)
                                  & r2_hidden(E,k1_funct_1(A,k1_nat_1(D,1)))
                                  & C = k7_finseq_1(k12_finseq_1(k5_numbers,D),E) ) ) ) ) ) ) ) ) ) ),
    file(trees_3,d15_trees_3),
    [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(t51_trees_3,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( v4_trees_3(B)
               => ( r2_hidden(k7_finseq_1(k12_finseq_1(k5_numbers,A),C),k13_trees_3(B))
                <=> ( ~ r1_xreal_0(k3_finseq_1(B),A)
                    & r2_hidden(C,k1_funct_1(B,k1_nat_1(A,1))) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_trees_3,t58_finseq_1,t46_finseq_1,d15_trees_3]),
    [file(trees_3,t51_trees_3),interesting(0.00)]).

fof(t6_trees_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => ! [C] : 
          ( ( v1_relat_1(C)
            & v1_funct_1(C)
            & v1_finseq_1(C) )
         => ~ ( k7_finseq_1(B,C) = k9_finseq_1(A)
              & ~ ( B = k9_finseq_1(A)
                  & C = k1_xboole_0 )
              & ~ ( B = k1_xboole_0
                  & C = k9_finseq_1(A) ) ) ) ) ),
    file(trees_1,t6_trees_1),
    [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(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(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(d1_trees_2,definition,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ( A = B
          <=> ! [C] : 
                ( m2_finseq_1(C,k5_numbers)
               => ( r2_hidden(C,A)
                <=> r2_hidden(C,B) ) ) ) ) ) ),
    file(trees_2,d1_trees_2),
    [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(t28_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ~ ( r1_xreal_0(A,B)
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => B != k2_xcmplx_0(A,C) ) ) ) ) ),
    file(nat_1,t28_nat_1),
    [interesting(0.00)]).

fof(t18_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ( ( k3_finseq_1(A) = k3_finseq_1(B)
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ( r1_xreal_0(1,C)
                      & r1_xreal_0(C,k3_finseq_1(A)) )
                   => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) )
           => A = B ) ) ) ),
    file(finseq_1,t18_finseq_1),
    [interesting(0.00)]).

fof(t27_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ( A = k1_xboole_0
      <=> k2_relat_1(A) = k1_xboole_0 ) ) ),
    file(finseq_1,t27_finseq_1),
    [interesting(0.00)]).

fof(t25_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ( k3_finseq_1(A) = 0
      <=> A = k1_xboole_0 ) ) ),
    file(finseq_1,t25_finseq_1),
    [interesting(0.00)]).

fof(t55_trees_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)
           => r2_hidden(k12_finseq_1(k5_numbers,A),k2_trees_1(B)) ) ) ) ),
    file(trees_1,t55_trees_1),
    [interesting(0.00)]).

fof(t37_zfmisc_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(k1_tarski(A),B)
    <=> r2_hidden(A,B) ) ),
    file(zfmisc_1,t37_zfmisc_1),
    [interesting(0.00)]).

fof(t57_trees_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_finseq_1(B,k5_numbers)
         => ~ ( r2_hidden(B,k2_trees_1(A))
              & B != k1_xboole_0
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ~ ( ~ r1_xreal_0(A,C)
                      & B = k12_finseq_1(k5_numbers,C) ) ) ) ) ) ),
    file(trees_1,t57_trees_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(t50_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ! [C] : 
              ( m1_trees_1(C,k2_xboole_0(A,B))
             => ( ( ( r2_hidden(C,A)
                    & r2_hidden(C,B) )
                 => k4_trees_1(k2_xboole_0(A,B),C) = k2_xboole_0(k4_trees_1(A,C),k4_trees_1(B,C)) )
                & ( ~ r2_hidden(C,A)
                 => k4_trees_1(k2_xboole_0(A,B),C) = k4_trees_1(B,C) )
                & ( ~ r2_hidden(C,B)
                 => k4_trees_1(k2_xboole_0(A,B),C) = k4_trees_1(A,C) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_trees_2,d9_trees_1,d2_xboole_0,d9_trees_1,d2_xboole_0,d2_xboole_0,d9_trees_1,d2_xboole_0,d9_trees_1,d2_xboole_0,d1_trees_2,d9_trees_1,d2_xboole_0,t46_trees_1,d9_trees_1,d9_trees_1,d2_xboole_0,d9_trees_1]),
    [file(trees_3,t50_trees_3),interesting(0.00)]).

fof(t50_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ! [C] : 
              ( m2_finseq_1(k7_finseq_1(A,B),C)
             => ( m2_finseq_1(A,C)
                & m2_finseq_1(B,C) ) ) ) ) ),
    file(finseq_1,t50_finseq_1),
    [interesting(0.00)]).

fof(d7_finseq_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( C = k7_finseq_1(A,B)
              <=> ( k4_finseq_1(C) = k2_finseq_1(k1_nat_1(k3_finseq_1(A),k3_finseq_1(B)))
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ( r2_hidden(D,k4_finseq_1(A))
                       => k1_funct_1(C,D) = k1_funct_1(A,D) ) )
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ( r2_hidden(D,k4_finseq_1(B))
                       => k1_funct_1(C,k1_nat_1(k3_finseq_1(A),D)) = k1_funct_1(B,D) ) ) ) ) ) ) ) ),
    file(finseq_1,d7_finseq_1),
    [interesting(0.00)]).

fof(t6_modal_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( m2_finseq_1(C,k5_numbers)
             => ~ ( A != B
                  & r1_tarski(k12_finseq_1(k5_numbers,A),k8_finseq_1(k5_numbers,k12_finseq_1(k5_numbers,B),C)) ) ) ) ) ),
    file(modal_1,t6_modal_1),
    [interesting(0.00)]).

fof(t59_finseq_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => k1_funct_1(k7_finseq_1(B,k9_finseq_1(A)),k1_nat_1(k3_finseq_1(B),1)) = A ) ),
    file(finseq_1,t59_finseq_1),
    [interesting(0.00)]).

fof(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(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(t8_trees_2,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( m2_finseq_1(B,k5_numbers)
         => ( r2_hidden(B,A)
           => A = k5_trees_1(A,B,k4_trees_1(A,B)) ) ) ) ),
    file(trees_2,t8_trees_2),
    [interesting(0.00)]).

fof(t9_modal_1,theorem,(
    k2_trees_1(1) = k2_tarski(k1_xboole_0,k12_finseq_1(k5_numbers,0)) ),
    file(modal_1,t9_modal_1),
    [interesting(0.00)]).

fof(d1_enumset1,definition,(
    ! [A,B,C,D] : 
      ( D = k1_enumset1(A,B,C)
    <=> ! [E] : 
          ( r2_hidden(E,D)
        <=> ~ ( E != A
              & E != B
              & E != C ) ) ) ),
    file(enumset1,d1_enumset1),
    [interesting(0.00)]).

fof(t7_modal_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ~ r2_xboole_0(k12_finseq_1(k5_numbers,A),k12_finseq_1(k5_numbers,B)) ) ) ),
    file(modal_1,t7_modal_1),
    [interesting(0.00)]).

fof(t10_modal_1,theorem,(
    k2_trees_1(2) = k1_enumset1(k1_xboole_0,k12_finseq_1(k5_numbers,0),k12_finseq_1(k5_numbers,1)) ),
    file(modal_1,t10_modal_1),
    [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(t62_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => k15_trees_3(A,B) = k5_trees_1(k5_trees_1(k2_trees_1(2),k12_finseq_1(k5_numbers,0),A),k12_finseq_1(k5_numbers,1),B) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_trees_2,t61_finseq_1,t47_trees_1,d1_enumset1,t7_modal_1,t10_modal_1,d12_trees_1,d15_trees_3,t50_finseq_1,t6_modal_1,d12_trees_1,d8_xboole_0,d12_trees_1,t38_nat_1,t26_nat_1,d12_trees_1,t47_trees_1,d12_trees_1,d12_trees_1,d1_enumset1,t47_finseq_1,t10_modal_1,d15_trees_3,d15_trees_3,d15_trees_3]),
    [file(trees_3,t62_trees_3),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(t39_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => r1_tarski(k4_finseq_1(A),k4_finseq_1(k7_finseq_1(A,B))) ) ) ),
    file(finseq_1,t39_finseq_1),
    [interesting(0.00)]).

fof(t9_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ! [D] : 
                  ( v1_xreal_0(D)
                 => ( ( r1_xreal_0(A,B)
                      & r1_xreal_0(C,D) )
                   => r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,D)) ) ) ) ) ) ),
    file(xreal_1,t9_xreal_1),
    [interesting(0.00)]).

fof(t36_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(k1_nat_1(k3_finseq_1(A),1),C)
                  & r1_xreal_0(C,k1_nat_1(k3_finseq_1(A),k3_finseq_1(B))) )
               => k1_funct_1(k7_finseq_1(A,B),C) = k1_funct_1(B,k6_xcmplx_0(C,k3_finseq_1(A))) ) ) ) ) ),
    file(finseq_1,t36_finseq_1),
    [interesting(0.00)]).

fof(t33_trees_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) )
         => ( ~ ( ~ r2_xboole_0(k1_xboole_0,A)
                & k1_xboole_0 = A )
           => r2_xboole_0(B,k7_finseq_1(B,A)) ) ) ) ),
    file(trees_1,t33_trees_1),
    [interesting(0.00)]).

fof(t45_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => k7_finseq_1(k7_finseq_1(A,B),C) = k7_finseq_1(A,k7_finseq_1(B,C)) ) ) ) ),
    file(finseq_1,t45_finseq_1),
    [interesting(0.00)]).

fof(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(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(t73_finseq_2,theorem,(
    ! [A] : k2_finseq_2(1,A) = k9_finseq_1(A) ),
    file(finseq_2,t73_finseq_2),
    [interesting(0.00)]).

fof(t69_finseq_2,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : k3_finseq_1(k2_finseq_2(A,B)) = A ) ),
    file(finseq_2,t69_finseq_2),
    [interesting(0.00)]).

fof(t19_funcop_1,theorem,(
    ! [A,B] : 
      ( k1_relat_1(k2_funcop_1(A,B)) = A
      & r1_tarski(k2_relat_1(k2_funcop_1(A,B)),k1_tarski(B)) ) ),
    file(funcop_1,t19_funcop_1),
    [interesting(0.00)]).

fof(d9_finseq_1,definition,(
    ! [A,B] : k10_finseq_1(A,B) = k7_finseq_1(k9_finseq_1(A),k9_finseq_1(B)) ),
    file(finseq_1,d9_finseq_1),
    [interesting(0.00)]).

fof(t77_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ( k4_trees_1(k15_trees_3(A,B),k12_finseq_1(k5_numbers,0)) = A
            & k4_trees_1(k15_trees_3(A,B),k12_finseq_1(k5_numbers,1)) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t61_finseq_1,t52_trees_3]),
    [file(trees_3,t77_trees_3),interesting(0.00)]).

fof(t78_trees_3,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v1_trees_1(B) )
         => ! [C] : 
              ( ( ~ v1_xboole_0(C)
                & v1_trees_1(C) )
             => ( k5_trees_1(k15_trees_3(B,C),k12_finseq_1(k5_numbers,0),A) = k15_trees_3(A,C)
                & k5_trees_1(k15_trees_3(B,C),k12_finseq_1(k5_numbers,1),A) = k15_trees_3(B,A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_finseq_1,t47_finseq_1,t57_finseq_1,d9_finseq_1,t23_trees_3,t60_trees_3]),
    [file(trees_3,t78_trees_3),interesting(0.00)]).

fof(t75_finseq_2,theorem,(
    ! [A] : k2_finseq_2(2,A) = k10_finseq_1(A,A) ),
    file(finseq_2,t75_finseq_2),
    [interesting(0.00)]).

fof(t55_finseq_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => ( B = k9_finseq_1(A)
      <=> ( k4_finseq_1(B) = k2_finseq_1(1)
          & k2_relat_1(B) = k1_tarski(A) ) ) ) ),
    file(finseq_1,t55_finseq_1),
    [interesting(0.00)]).

fof(t85_trees_1,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( m1_trees_1(B,A)
         => ~ ( B != k1_xboole_0
              & r1_xreal_0(k6_trees_1(A),k6_trees_1(k4_trees_1(A,B))) ) ) ) ),
    file(trees_1,t85_trees_1),
    [interesting(0.00)]).

fof(d15_trees_1,definition,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A)
        & v1_trees_1(A) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( B = k6_trees_1(A)
          <=> ( ? [C] : 
                  ( m2_finseq_1(C,k5_numbers)
                  & r2_hidden(C,A)
                  & k3_finseq_1(C) = B )
              & ! [C] : 
                  ( m2_finseq_1(C,k5_numbers)
                 => ( r2_hidden(C,A)
                   => r1_xreal_0(k3_finseq_1(C),B) ) ) ) ) ) ) ),
    file(trees_1,d15_trees_1),
    [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(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)]).