%------------------------------------------------------------------------------
% File     : COM001+0 : TPTP v7.2.0. Released v6.4.0.
% Domain   : Computing Theory
% Axioms   : Common axioms for progress/preservation proof
% Version  : [Gre15] axioms : Especial.
% English  :

% Refs     : [Pie02] Pierce (2002), Programming Languages
%          : [Gre15] Grewe (2015), Email to Geoff Sutcliffe
%          : [GE+15] Grewe et al. (2015), Type Systems for the Masses: Deri
% Source   : [Gre15]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of formulae    :   54 (   6 unit)
%            Number of atoms       :  285 ( 227 equality)
%            Maximal formula depth :   23 (   9 average)
%            Number of connectives :  267 (  36   ~;  17   |; 120   &)
%                                         (   0 <=>;  94  =>;   0  <=;   0 <~>)
%                                         (   0  ~|;   0  ~&)
%            Number of predicates  :    7 (   1 propositional; 0-3 arity)
%            Number of functors    :   16 (   3 constant; 0-3 arity)
%            Number of variables   :  307 (   0 sgn; 239   !;  68   ?)
%            Maximal term depth    :    5 (   1 average)
% SPC      :

% Comments : 
%------------------------------------------------------------------------------
fof('EQ-var',axiom,(
    ! [VVar0,VVar1] :
      ( ( vvar(VVar0) = vvar(VVar1)
       => VVar0 = VVar1 )
      & ( VVar0 = VVar1
       => vvar(VVar0) = vvar(VVar1) ) ) )).

fof('EQ-abs',axiom,(
    ! [VVar0,VTyp0,VExp0,VVar1,VTyp1,VExp1] :
      ( ( vabs(VVar0,VTyp0,VExp0) = vabs(VVar1,VTyp1,VExp1)
       => ( VVar0 = VVar1
          & VTyp0 = VTyp1
          & VExp0 = VExp1 ) )
      & ( ( VVar0 = VVar1
          & VTyp0 = VTyp1
          & VExp0 = VExp1 )
       => vabs(VVar0,VTyp0,VExp0) = vabs(VVar1,VTyp1,VExp1) ) ) )).

fof('EQ-app',axiom,(
    ! [VExp0,VExp1,VExp2,VExp3] :
      ( ( vapp(VExp0,VExp1) = vapp(VExp2,VExp3)
       => ( VExp0 = VExp2
          & VExp1 = VExp3 ) )
      & ( ( VExp0 = VExp2
          & VExp1 = VExp3 )
       => vapp(VExp0,VExp1) = vapp(VExp2,VExp3) ) ) )).

fof('DIFF-var-abs',axiom,(
    ! [VVar0,VVar1,VTyp0,VExp0] : vvar(VVar0) != vabs(VVar1,VTyp0,VExp0) )).

fof('DIFF-var-app',axiom,(
    ! [VVar0,VExp0,VExp1] : vvar(VVar0) != vapp(VExp0,VExp1) )).

fof('DIFF-abs-app',axiom,(
    ! [VVar0,VTyp0,VExp0,VExp1,VExp2] : vabs(VVar0,VTyp0,VExp0) != vapp(VExp1,VExp2) )).

fof(isValue0,axiom,(
    ! [Vx,VS,Ve,VExp0] :
      ( VExp0 = vabs(Vx,VS,Ve)
     => visValue(VExp0) ) )).

fof(isValue1,axiom,(
    ! [Vx,VExp0] :
      ( VExp0 = vvar(Vx)
     => ~ visValue(VExp0) ) )).

fof(isValue2,axiom,(
    ! [Ve1,Ve2,VExp0] :
      ( VExp0 = vapp(Ve1,Ve2)
     => ~ visValue(VExp0) ) )).

fof(isFreeVar0,axiom,(
    ! [VVar0,VExp0,Vx,Vv] :
      ( ( VVar0 = Vv
        & VExp0 = vvar(Vx) )
     => ( ( Vx = Vv
         => visFreeVar(VVar0,VExp0) )
        & ( visFreeVar(VVar0,VExp0)
         => Vx = Vv ) ) ) )).

fof(isFreeVar1,axiom,(
    ! [VT,VVar0,VExp0,Vx,Vv,Ve] :
      ( ( VVar0 = Vv
        & VExp0 = vabs(Vx,VT,Ve) )
     => ( ( ( Vx != Vv
            & visFreeVar(Vv,Ve) )
         => visFreeVar(VVar0,VExp0) )
        & ( visFreeVar(VVar0,VExp0)
         => ( Vx != Vv
            & visFreeVar(Vv,Ve) ) ) ) ) )).

fof(isFreeVar2,axiom,(
    ! [VVar0,VExp0,Ve1,Vv,Ve2] :
      ( ( VVar0 = Vv
        & VExp0 = vapp(Ve1,Ve2) )
     => ( ( ( visFreeVar(Vv,Ve1)
            | visFreeVar(Vv,Ve2) )
         => visFreeVar(VVar0,VExp0) )
        & ( visFreeVar(VVar0,VExp0)
         => ( visFreeVar(Vv,Ve1)
            | visFreeVar(Vv,Ve2) ) ) ) ) )).

fof('EQ-empty',axiom,
    ( ( vempty = vempty
     => $true )
    & ( $true
     => vempty = vempty ) )).

fof('EQ-bind',axiom,(
    ! [VVar0,VTyp0,VCtx0,VVar1,VTyp1,VCtx1] :
      ( ( vbind(VVar0,VTyp0,VCtx0) = vbind(VVar1,VTyp1,VCtx1)
       => ( VVar0 = VVar1
          & VTyp0 = VTyp1
          & VCtx0 = VCtx1 ) )
      & ( ( VVar0 = VVar1
          & VTyp0 = VTyp1
          & VCtx0 = VCtx1 )
       => vbind(VVar0,VTyp0,VCtx0) = vbind(VVar1,VTyp1,VCtx1) ) ) )).

fof('EQ-noType',axiom,
    ( ( vnoType = vnoType
     => $true )
    & ( $true
     => vnoType = vnoType ) )).

fof('EQ-someType',axiom,(
    ! [VTyp0,VTyp1] :
      ( ( vsomeType(VTyp0) = vsomeType(VTyp1)
       => VTyp0 = VTyp1 )
      & ( VTyp0 = VTyp1
       => vsomeType(VTyp0) = vsomeType(VTyp1) ) ) )).

fof('DIFF-empty-bind',axiom,(
    ! [VVar0,VTyp0,VCtx0] : vempty != vbind(VVar0,VTyp0,VCtx0) )).

fof('DIFF-noType-someType',axiom,(
    ! [VTyp0] : vnoType != vsomeType(VTyp0) )).

fof(isSomeType0,axiom,(
    ! [VOptTyp0] :
      ( VOptTyp0 = vnoType
     => ~ visSomeType(VOptTyp0) ) )).

fof(isSomeType1,axiom,(
    ! [Ve,VOptTyp0] :
      ( VOptTyp0 = vsomeType(Ve)
     => visSomeType(VOptTyp0) ) )).

fof(getSomeType0,axiom,(
    ! [VOptTyp0,RESULT,Ve] :
      ( VOptTyp0 = vsomeType(Ve)
     => ( RESULT = vgetSomeType(VOptTyp0)
       => RESULT = Ve ) ) )).

fof(lookup0,axiom,(
    ! [Vx,VVar0,VCtx0,RESULT] :
      ( ( VVar0 = Vx
        & VCtx0 = vempty )
     => ( RESULT = vlookup(VVar0,VCtx0)
       => RESULT = vnoType ) ) )).

fof(lookup1,axiom,(
    ! [VC,Vx,Vy,VVar0,VCtx0,RESULT,VTy] :
      ( ( VVar0 = Vx
        & VCtx0 = vbind(Vy,VTy,VC) )
     => ( Vx = Vy
       => ( RESULT = vlookup(VVar0,VCtx0)
         => RESULT = vsomeType(VTy) ) ) ) )).

fof(lookup2,axiom,(
    ! [VTy,Vy,VVar0,VCtx0,RESULT,Vx,VC] :
      ( ( VVar0 = Vx
        & VCtx0 = vbind(Vy,VTy,VC) )
     => ( Vx != Vy
       => ( RESULT = vlookup(VVar0,VCtx0)
         => RESULT = vlookup(Vx,VC) ) ) ) )).

fof('lookup-INV',axiom,(
    ! [VVar0,VCtx0,RESULT] :
      ( vlookup(VVar0,VCtx0) = RESULT
     => ( ? [Vx] :
            ( VVar0 = Vx
            & VCtx0 = vempty
            & RESULT = vnoType )
        | ? [VC,Vx,Vy,VTy] :
            ( VVar0 = Vx
            & VCtx0 = vbind(Vy,VTy,VC)
            & Vx = Vy
            & RESULT = vsomeType(VTy) )
        | ? [VTy,Vy,Vx,VC] :
            ( VVar0 = Vx
            & VCtx0 = vbind(Vy,VTy,VC)
            & Vx != Vy
            & RESULT = vlookup(Vx,VC) ) ) ) )).

fof('T-Context-Duplicate',axiom,(
    ! [Vy,VTy,Vx,VTx,VC,Ve,VT] :
      ( ( Vx = Vy
        & vtcheck(vbind(Vx,VTx,vbind(Vy,VTy,VC)),Ve,VT) )
     => vtcheck(vbind(Vx,VTx,VC),Ve,VT) ) )).

fof('T-Context-Swap',axiom,(
    ! [Vy,VTy,Vx,VTx,VC,Ve,VT] :
      ( ( Vx != Vy
        & vtcheck(vbind(Vx,VTx,vbind(Vy,VTy,VC)),Ve,VT) )
     => vtcheck(vbind(Vy,VTy,vbind(Vx,VTx,VC)),Ve,VT) ) )).

fof('gensym-is-fresh',axiom,(
    ! [Vv,Ve] :
      ( vgensym(Ve) = Vv
     => ~ visFreeVar(Vv,Ve) ) )).

fof(subst0,axiom,(
    ! [Vx,Vy,VVar0,VExp0,VExp1,RESULT,Ve] :
      ( ( VVar0 = Vx
        & VExp0 = Ve
        & VExp1 = vvar(Vy) )
     => ( Vx = Vy
       => ( RESULT = vsubst(VVar0,VExp0,VExp1)
         => RESULT = Ve ) ) ) )).

fof(subst1,axiom,(
    ! [Ve,Vx,VVar0,VExp0,VExp1,RESULT,Vy] :
      ( ( VVar0 = Vx
        & VExp0 = Ve
        & VExp1 = vvar(Vy) )
     => ( Vx != Vy
       => ( RESULT = vsubst(VVar0,VExp0,VExp1)
         => RESULT = vvar(Vy) ) ) ) )).

fof(subst2,axiom,(
    ! [VVar0,VExp0,VExp1,RESULT,Ve1,Vx,Ve,Ve2] :
      ( ( VVar0 = Vx
        & VExp0 = Ve
        & VExp1 = vapp(Ve1,Ve2) )
     => ( RESULT = vsubst(VVar0,VExp0,VExp1)
       => RESULT = vapp(vsubst(Vx,Ve,Ve1),vsubst(Vx,Ve,Ve2)) ) ) )).

fof(subst3,axiom,(
    ! [Ve,Vx,VVar0,VExp0,VExp1,RESULT,Vy,VT,Ve1] :
      ( ( VVar0 = Vx
        & VExp0 = Ve
        & VExp1 = vabs(Vy,VT,Ve1) )
     => ( Vx = Vy
       => ( RESULT = vsubst(VVar0,VExp0,VExp1)
         => RESULT = vabs(Vy,VT,Ve1) ) ) ) )).

fof(subst4,axiom,(
    ! [VVar0,VExp0,VExp1,RESULT,Vx,Ve,VT,Vy,Vfresh,Ve1] :
      ( ( VVar0 = Vx
        & VExp0 = Ve
        & VExp1 = vabs(Vy,VT,Ve1) )
     => ( ( Vx != Vy
          & visFreeVar(Vy,Ve)
          & Vfresh = vgensym(vapp(vapp(Ve,Ve1),vvar(Vx))) )
       => ( RESULT = vsubst(VVar0,VExp0,VExp1)
         => RESULT = vsubst(Vx,Ve,vabs(Vfresh,VT,vsubst(Vy,vvar(Vfresh),Ve1))) ) ) ) )).

fof(subst5,axiom,(
    ! [VVar0,VExp0,VExp1,RESULT,Vy,VT,Vx,Ve,Ve1] :
      ( ( VVar0 = Vx
        & VExp0 = Ve
        & VExp1 = vabs(Vy,VT,Ve1) )
     => ( ( Vx != Vy
          & ~ visFreeVar(Vy,Ve) )
       => ( RESULT = vsubst(VVar0,VExp0,VExp1)
         => RESULT = vabs(Vy,VT,vsubst(Vx,Ve,Ve1)) ) ) ) )).

fof('subst-INV',axiom,(
    ! [VVar0,VExp0,VExp1,RESULT] :
      ( vsubst(VVar0,VExp0,VExp1) = RESULT
     => ( ? [Vx,Vy,Ve] :
            ( VVar0 = Vx
            & VExp0 = Ve
            & VExp1 = vvar(Vy)
            & Vx = Vy
            & RESULT = Ve )
        | ? [Ve,Vx,Vy] :
            ( VVar0 = Vx
            & VExp0 = Ve
            & VExp1 = vvar(Vy)
            & Vx != Vy
            & RESULT = vvar(Vy) )
        | ? [Ve1,Vx,Ve,Ve2] :
            ( VVar0 = Vx
            & VExp0 = Ve
            & VExp1 = vapp(Ve1,Ve2)
            & RESULT = vapp(vsubst(Vx,Ve,Ve1),vsubst(Vx,Ve,Ve2)) )
        | ? [Ve,Vx,Vy,VT,Ve1] :
            ( VVar0 = Vx
            & VExp0 = Ve
            & VExp1 = vabs(Vy,VT,Ve1)
            & Vx = Vy
            & RESULT = vabs(Vy,VT,Ve1) )
        | ? [Vx,Ve,VT,Vy,Vfresh,Ve1] :
            ( VVar0 = Vx
            & VExp0 = Ve
            & VExp1 = vabs(Vy,VT,Ve1)
            & Vx != Vy
            & visFreeVar(Vy,Ve)
            & Vfresh = vgensym(vapp(vapp(Ve,Ve1),vvar(Vx)))
            & RESULT = vsubst(Vx,Ve,vabs(Vfresh,VT,vsubst(Vy,vvar(Vfresh),Ve1))) )
        | ? [Vy,VT,Vx,Ve,Ve1] :
            ( VVar0 = Vx
            & VExp0 = Ve
            & VExp1 = vabs(Vy,VT,Ve1)
            & Vx != Vy
            & ~ visFreeVar(Vy,Ve)
            & RESULT = vabs(Vy,VT,vsubst(Vx,Ve,Ve1)) ) ) ) )).

fof('EQ-noExp',axiom,
    ( ( vnoExp = vnoExp
     => $true )
    & ( $true
     => vnoExp = vnoExp ) )).

fof('EQ-someExp',axiom,(
    ! [VExp0,VExp1] :
      ( ( vsomeExp(VExp0) = vsomeExp(VExp1)
       => VExp0 = VExp1 )
      & ( VExp0 = VExp1
       => vsomeExp(VExp0) = vsomeExp(VExp1) ) ) )).

fof('DIFF-noExp-someExp',axiom,(
    ! [VExp0] : vnoExp != vsomeExp(VExp0) )).

fof(isSomeExp0,axiom,(
    ! [VOptExp0] :
      ( VOptExp0 = vnoExp
     => ~ visSomeExp(VOptExp0) ) )).

fof(isSomeExp1,axiom,(
    ! [Ve,VOptExp0] :
      ( VOptExp0 = vsomeExp(Ve)
     => visSomeExp(VOptExp0) ) )).

fof(getSomeExp0,axiom,(
    ! [VOptExp0,RESULT,Ve] :
      ( VOptExp0 = vsomeExp(Ve)
     => ( RESULT = vgetSomeExp(VOptExp0)
       => RESULT = Ve ) ) )).

fof(reduce0,axiom,(
    ! [Vx,VExp0,RESULT] :
      ( VExp0 = vvar(Vx)
     => ( RESULT = vreduce(VExp0)
       => RESULT = vnoExp ) ) )).

fof(reduce1,axiom,(
    ! [Vx,VS,Ve,VExp0,RESULT] :
      ( VExp0 = vabs(Vx,VS,Ve)
     => ( RESULT = vreduce(VExp0)
       => RESULT = vnoExp ) ) )).

fof(reduce2,axiom,(
    ! [Ve2,VExp0,RESULT,Vx,VS,Ve1,Ve2red] :
      ( VExp0 = vapp(vabs(Vx,VS,Ve1),Ve2)
     => ( ( Ve2red = vreduce(Ve2)
          & visSomeExp(Ve2red) )
       => ( RESULT = vreduce(VExp0)
         => RESULT = vsomeExp(vapp(vabs(Vx,VS,Ve1),vgetSomeExp(Ve2red))) ) ) ) )).

fof(reduce3,axiom,(
    ! [VS,Ve2red,VExp0,RESULT,Vx,Ve2,Ve1] :
      ( VExp0 = vapp(vabs(Vx,VS,Ve1),Ve2)
     => ( ( Ve2red = vreduce(Ve2)
          & ~ visSomeExp(Ve2red)
          & visValue(Ve2) )
       => ( RESULT = vreduce(VExp0)
         => RESULT = vsomeExp(vsubst(Vx,Ve2,Ve1)) ) ) ) )).

fof(reduce4,axiom,(
    ! [Vx,VS,Ve1,Ve2red,Ve2,VExp0,RESULT] :
      ( VExp0 = vapp(vabs(Vx,VS,Ve1),Ve2)
     => ( ( Ve2red = vreduce(Ve2)
          & ~ visSomeExp(Ve2red)
          & ~ visValue(Ve2) )
       => ( RESULT = vreduce(VExp0)
         => RESULT = vnoExp ) ) ) )).

fof(reduce5,axiom,(
    ! [Ve1,VExp0,RESULT,Ve1red,Ve2] :
      ( ( VExp0 = vapp(Ve1,Ve2)
        & ! [VVx0,VVS0,VVe10] : Ve1 != vabs(VVx0,VVS0,VVe10) )
     => ( ( Ve1red = vreduce(Ve1)
          & visSomeExp(Ve1red) )
       => ( RESULT = vreduce(VExp0)
         => RESULT = vsomeExp(vapp(vgetSomeExp(Ve1red),Ve2)) ) ) ) )).

fof(reduce6,axiom,(
    ! [Ve2,Ve1,Ve1red,VExp0,RESULT] :
      ( ( VExp0 = vapp(Ve1,Ve2)
        & ! [VVx0,VVS0,VVe10] : Ve1 != vabs(VVx0,VVS0,VVe10) )
     => ( ( Ve1red = vreduce(Ve1)
          & ~ visSomeExp(Ve1red) )
       => ( RESULT = vreduce(VExp0)
         => RESULT = vnoExp ) ) ) )).

fof('reduce-INV',axiom,(
    ! [VExp0,RESULT] :
      ( vreduce(VExp0) = RESULT
     => ( ? [Vx] :
            ( VExp0 = vvar(Vx)
            & RESULT = vnoExp )
        | ? [Vx,VS,Ve] :
            ( VExp0 = vabs(Vx,VS,Ve)
            & RESULT = vnoExp )
        | ? [Ve2,Vx,VS,Ve1,Ve2red] :
            ( VExp0 = vapp(vabs(Vx,VS,Ve1),Ve2)
            & Ve2red = vreduce(Ve2)
            & visSomeExp(Ve2red)
            & RESULT = vsomeExp(vapp(vabs(Vx,VS,Ve1),vgetSomeExp(Ve2red))) )
        | ? [VS,Ve2red,Vx,Ve2,Ve1] :
            ( VExp0 = vapp(vabs(Vx,VS,Ve1),Ve2)
            & Ve2red = vreduce(Ve2)
            & ~ visSomeExp(Ve2red)
            & visValue(Ve2)
            & RESULT = vsomeExp(vsubst(Vx,Ve2,Ve1)) )
        | ? [Vx,VS,Ve1,Ve2red,Ve2] :
            ( VExp0 = vapp(vabs(Vx,VS,Ve1),Ve2)
            & Ve2red = vreduce(Ve2)
            & ~ visSomeExp(Ve2red)
            & ~ visValue(Ve2)
            & RESULT = vnoExp )
        | ? [Ve1,Ve1red,Ve2] :
            ( VExp0 = vapp(Ve1,Ve2)
            & ! [VVx0,VVS0,VVe10] : Ve1 != vabs(VVx0,VVS0,VVe10)
            & Ve1red = vreduce(Ve1)
            & visSomeExp(Ve1red)
            & RESULT = vsomeExp(vapp(vgetSomeExp(Ve1red),Ve2)) )
        | ? [Ve2,Ve1,Ve1red] :
            ( VExp0 = vapp(Ve1,Ve2)
            & ! [VVx0,VVS0,VVe10] : Ve1 != vabs(VVx0,VVS0,VVe10)
            & Ve1red = vreduce(Ve1)
            & ~ visSomeExp(Ve1red)
            & RESULT = vnoExp ) ) ) )).

fof('EQ-arrow',axiom,(
    ! [VTyp0,VTyp1,VTyp2,VTyp3] :
      ( ( varrow(VTyp0,VTyp1) = varrow(VTyp2,VTyp3)
       => ( VTyp0 = VTyp2
          & VTyp1 = VTyp3 ) )
      & ( ( VTyp0 = VTyp2
          & VTyp1 = VTyp3 )
       => varrow(VTyp0,VTyp1) = varrow(VTyp2,VTyp3) ) ) )).

fof('T-var',axiom,(
    ! [VC,Vx,VT] :
      ( vlookup(Vx,VC) = vsomeType(VT)
     => vtcheck(VC,vvar(Vx),VT) ) )).

fof('T-abs',axiom,(
    ! [VC,Vx,Ve,VS,VT] :
      ( vtcheck(vbind(Vx,VS,VC),Ve,VT)
     => vtcheck(VC,vabs(Vx,VS,Ve),varrow(VS,VT)) ) )).

fof('T-app',axiom,(
    ! [VS,VC,Ve1,Ve2,VT] :
      ( ( vtcheck(VC,Ve1,varrow(VS,VT))
        & vtcheck(VC,Ve2,VS) )
     => vtcheck(VC,vapp(Ve1,Ve2),VT) ) )).

fof('T-inv',axiom,(
    ! [Ve,VT,VC] :
      ( vtcheck(VC,Ve,VT)
     => ( ? [Vx] :
            ( Ve = vvar(Vx)
            & vlookup(Vx,VC) = vsomeType(VT) )
        | ? [Vx,Ve2,VT1,VT2] :
            ( Ve = vabs(Vx,VT1,Ve2)
            & VT = varrow(VT1,VT2)
            & vtcheck(vbind(Vx,VT1,VC),Ve2,VT2) )
        | ? [Ve1,Ve2,VS] :
            ( Ve = vapp(Ve1,Ve2)
            & vtcheck(VC,Ve1,varrow(VS,VT))
            & vtcheck(VC,Ve2,VS) ) ) ) )).

%------------------------------------------------------------------------------