% Mizar problem: t7_recdef_2,recdef_2,256,43 
fof(t7_recdef_2,conjecture,(
    ! [A] : 
      ( ? [B,C,D,E,F] : A = k1_mcart_2(B,C,D,E,F)
     => A = k1_mcart_2(k8_recdef_2(A),k9_recdef_2(A),k10_recdef_2(A),k11_recdef_2(A),k12_recdef_2(A)) ) ),
    inference(mizar_bg_added,[status(thm)],[d10_recdef_2,d11_recdef_2,d12_recdef_2,d8_recdef_2,d9_recdef_2,dt_k10_recdef_2,dt_k11_recdef_2,dt_k12_recdef_2,dt_k1_mcart_2,dt_k8_recdef_2,dt_k9_recdef_2]),
    [file(recdef_2,t7_recdef_2)]).

fof(d10_recdef_2,axiom,(
    ! [A] : 
      ( ? [B,C,D,E,F] : A = k1_mcart_2(B,C,D,E,F)
     => ! [B] : 
          ( B = k10_recdef_2(A)
        <=> ! [C,D,E,F,G] : 
              ( A = k1_mcart_2(C,D,E,F,G)
             => B = E ) ) ) ),
    file(recdef_2,d10_recdef_2),
    []).

fof(d11_recdef_2,axiom,(
    ! [A] : 
      ( ? [B,C,D,E,F] : A = k1_mcart_2(B,C,D,E,F)
     => ! [B] : 
          ( B = k11_recdef_2(A)
        <=> ! [C,D,E,F,G] : 
              ( A = k1_mcart_2(C,D,E,F,G)
             => B = F ) ) ) ),
    file(recdef_2,d11_recdef_2),
    []).

fof(d12_recdef_2,axiom,(
    ! [A] : 
      ( ? [B,C,D,E,F] : A = k1_mcart_2(B,C,D,E,F)
     => ! [B] : 
          ( B = k12_recdef_2(A)
        <=> ! [C,D,E,F,G] : 
              ( A = k1_mcart_2(C,D,E,F,G)
             => B = G ) ) ) ),
    file(recdef_2,d12_recdef_2),
    []).

fof(d8_recdef_2,axiom,(
    ! [A] : 
      ( ? [B,C,D,E,F] : A = k1_mcart_2(B,C,D,E,F)
     => ! [B] : 
          ( B = k8_recdef_2(A)
        <=> ! [C,D,E,F,G] : 
              ( A = k1_mcart_2(C,D,E,F,G)
             => B = C ) ) ) ),
    file(recdef_2,d8_recdef_2),
    []).

fof(d9_recdef_2,axiom,(
    ! [A] : 
      ( ? [B,C,D,E,F] : A = k1_mcart_2(B,C,D,E,F)
     => ! [B] : 
          ( B = k9_recdef_2(A)
        <=> ! [C,D,E,F,G] : 
              ( A = k1_mcart_2(C,D,E,F,G)
             => B = D ) ) ) ),
    file(recdef_2,d9_recdef_2),
    []).

fof(dt_k10_recdef_2,axiom,(
    $true ),
    file(recdef_2,k10_recdef_2),
    []).

fof(dt_k11_recdef_2,axiom,(
    $true ),
    file(recdef_2,k11_recdef_2),
    []).

fof(dt_k12_recdef_2,axiom,(
    $true ),
    file(recdef_2,k12_recdef_2),
    []).

fof(dt_k1_mcart_2,axiom,(
    $true ),
    file(mcart_2,k1_mcart_2),
    []).

fof(dt_k8_recdef_2,axiom,(
    $true ),
    file(recdef_2,k8_recdef_2),
    []).

fof(dt_k9_recdef_2,axiom,(
    $true ),
    file(recdef_2,k9_recdef_2),
    []).