% Mizar ND problem: t3_binari_3,binari_3,141,60 
fof(dh_c1_3__binari_3,definition,
    ( ( ( v1_relat_1(c1_3__binari_3)
        & v1_funct_1(c1_3__binari_3)
        & v1_finseq_1(c1_3__binari_3) )
     => ! [A] : 
          ( ( v1_relat_1(A)
            & v1_funct_1(A)
            & v1_finseq_1(A) )
         => ( k3_finseq_5(c1_3__binari_3) = k3_finseq_5(A)
           => c1_3__binari_3 = A ) ) )
   => ! [B] : 
        ( ( v1_relat_1(B)
          & v1_funct_1(B)
          & v1_finseq_1(B) )
       => ! [C] : 
            ( ( v1_relat_1(C)
              & v1_funct_1(C)
              & v1_finseq_1(C) )
           => ( k3_finseq_5(B) = k3_finseq_5(C)
             => B = C ) ) ) ),
    introduced(definition,[new_symbol(c1_3__binari_3),file(binari_3,c1_3__binari_3)]),
    [interesting(0.8),axiom,file(binari_3,c1_3__binari_3)]).

fof(dh_c2_3__binari_3,definition,
    ( ( ( v1_relat_1(c2_3__binari_3)
        & v1_funct_1(c2_3__binari_3)
        & v1_finseq_1(c2_3__binari_3) )
     => ( k3_finseq_5(c1_3__binari_3) = k3_finseq_5(c2_3__binari_3)
       => c1_3__binari_3 = c2_3__binari_3 ) )
   => ! [A] : 
        ( ( v1_relat_1(A)
          & v1_funct_1(A)
          & v1_finseq_1(A) )
       => ( k3_finseq_5(c1_3__binari_3) = k3_finseq_5(A)
         => c1_3__binari_3 = A ) ) ),
    introduced(definition,[new_symbol(c2_3__binari_3),file(binari_3,c2_3__binari_3)]),
    [interesting(0.8),axiom,file(binari_3,c2_3__binari_3)]).

fof(e1_3__binari_3,assumption,(
    k3_finseq_5(c1_3__binari_3) = k3_finseq_5(c2_3__binari_3) ),
    introduced(assumption,[file(binari_3,e1_3__binari_3)]),
    [interesting(0.8),axiom,file(binari_3,e1_3__binari_3)]).

fof(dt_k3_finseq_5,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ( v1_relat_1(k3_finseq_5(A))
        & v1_funct_1(k3_finseq_5(A))
        & v1_finseq_1(k3_finseq_5(A)) ) ) ),
    file(finseq_5,k3_finseq_5),
    [interesting(0.9),axiom,file(finseq_5,k3_finseq_5)]).

fof(dt_c1_3__binari_3,assumption,
    ( v1_relat_1(c1_3__binari_3)
    & v1_funct_1(c1_3__binari_3)
    & v1_finseq_1(c1_3__binari_3) ),
    introduced(assumption,[file(binari_3,c1_3__binari_3)]),
    [interesting(0.8),axiom,file(binari_3,c1_3__binari_3)]).

fof(t29_finseq_6,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => k3_finseq_5(k3_finseq_5(A)) = A ) ),
    file(finseq_6,t29_finseq_6),
    [interesting(0.9),axiom,file(finseq_6,t29_finseq_6)]).

fof(e1_3_1__binari_3,plain,(
    c1_3__binari_3 = k3_finseq_5(k3_finseq_5(c1_3__binari_3)) ),
    inference(mizar_by,[status(thm),assumptions([dt_c1_3__binari_3])],[dt_k3_finseq_5,dt_c1_3__binari_3,t29_finseq_6]),
    [interesting(0.65),file(binari_3,e1_3_1__binari_3),[file(binari_3,e1_3_1__binari_3)]]).

fof(dt_c2_3__binari_3,assumption,
    ( v1_relat_1(c2_3__binari_3)
    & v1_funct_1(c2_3__binari_3)
    & v1_finseq_1(c2_3__binari_3) ),
    introduced(assumption,[file(binari_3,c2_3__binari_3)]),
    [interesting(0.8),axiom,file(binari_3,c2_3__binari_3)]).

fof(e2_3_1__binari_3,plain,(
    k3_finseq_5(k3_finseq_5(c1_3__binari_3)) = c2_3__binari_3 ),
    inference(mizar_by,[status(thm),assumptions([dt_c1_3__binari_3,dt_c2_3__binari_3,e1_3__binari_3])],[dt_k3_finseq_5,dt_c1_3__binari_3,dt_c2_3__binari_3,e1_3__binari_3,t29_finseq_6]),
    [interesting(0.65),file(binari_3,e2_3_1__binari_3),[file(binari_3,e2_3_1__binari_3)]]).

fof(e2_3__binari_3,plain,(
    c1_3__binari_3 = c2_3__binari_3 ),
    inference(iterative_eq,[status(thm),assumptions([dt_c1_3__binari_3,dt_c2_3__binari_3,e1_3__binari_3])],[e1_3_1__binari_3,e2_3_1__binari_3]),
    [interesting(0.8),file(binari_3,e2_3__binari_3),[file(binari_3,e2_3__binari_3)]]).

fof(i3_3__binari_3,theorem,(
    $true ),
    introduced(tautology,[file(binari_3,i3_3__binari_3)]),
    [interesting(0.8),trivial,file(binari_3,i3_3__binari_3)]).

fof(i2_3__binari_3,plain,(
    c1_3__binari_3 = c2_3__binari_3 ),
    inference(conclusion,[status(thm),assumptions([dt_c1_3__binari_3,dt_c2_3__binari_3,e1_3__binari_3])],[e2_3__binari_3,i3_3__binari_3]),
    [interesting(0.8),file(binari_3,i2_3__binari_3),[file(binari_3,i2_3__binari_3)]]).

fof(i1_3__binari_3,plain,
    ( k3_finseq_5(c1_3__binari_3) = k3_finseq_5(c2_3__binari_3)
   => c1_3__binari_3 = c2_3__binari_3 ),
    inference(discharge_asm,[status(thm),assumptions([dt_c1_3__binari_3,dt_c2_3__binari_3]),discharge_asm(discharge,[e1_3__binari_3])],[e1_3__binari_3,i2_3__binari_3]),
    [interesting(0.8),file(binari_3,i1_3__binari_3),[file(binari_3,i1_3__binari_3)]]).

fof(i1_3_tmp__binari_3,plain,
    ( ( v1_relat_1(c1_3__binari_3)
      & v1_funct_1(c1_3__binari_3)
      & v1_finseq_1(c1_3__binari_3)
      & v1_relat_1(c2_3__binari_3)
      & v1_funct_1(c2_3__binari_3)
      & v1_finseq_1(c2_3__binari_3) )
   => ( k3_finseq_5(c1_3__binari_3) = k3_finseq_5(c2_3__binari_3)
     => c1_3__binari_3 = c2_3__binari_3 ) ),
    inference(discharge_asm,[status(thm),assumptions([]),discharge_asm(discharge,[dt_c1_3__binari_3,dt_c2_3__binari_3])],[dt_c1_3__binari_3,dt_c2_3__binari_3,i1_3__binari_3]),
    [interesting(1),t3_binari_3]).

fof(t3_binari_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) )
         => ( k3_finseq_5(A) = k3_finseq_5(B)
           => A = B ) ) ) ),
    inference(let,[status(thm),assumptions([])],[i1_3_tmp__binari_3,dh_c1_3__binari_3,dh_c2_3__binari_3]),
    [interesting(1),file(binari_3,t3_binari_3),[file(binari_3,t3_binari_3)]]).