%------------------------------------------------------------------------------
% File     : COM001+1 : 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    :    6 (   1 unit)
%            Number of atoms       :   14 (   0 equality)
%            Maximal formula depth :    7 (   6 average)
%            Number of connectives :   11 (   3   ~;   0   |;   3   &)
%                                         (   0 <=>;   5  =>;   0  <=;   0 <~>)
%                                         (   0  ~|;   0  ~&)
%            Number of predicates  :    3 (   0 propositional; 2-3 arity)
%            Number of functors    :    3 (   0 constant; 1-3 arity)
%            Number of variables   :   17 (   0 sgn;  17   !;   0   ?)
%            Maximal term depth    :    4 (   1 average)
% SPC      :

% Comments : Requires COM001+0.ax
%------------------------------------------------------------------------------
fof('alpha-equiv-refl',axiom,(
    ! [Ve] : valphaEquivalent(Ve,Ve) )).

fof('alpha-equiv-sym',axiom,(
    ! [Ve2,Ve1] :
      ( valphaEquivalent(Ve1,Ve2)
     => valphaEquivalent(Ve2,Ve1) ) )).

fof('alpha-equiv-trans',axiom,(
    ! [Ve2,Ve1,Ve3] :
      ( ( valphaEquivalent(Ve1,Ve2)
        & valphaEquivalent(Ve2,Ve3) )
     => valphaEquivalent(Ve1,Ve3) ) )).

fof('alpha-equiv-subst-abs',axiom,(
    ! [VS,Vx,Vy,Ve] :
      ( ~ visFreeVar(Vy,Ve)
     => valphaEquivalent(vabs(Vx,VS,Ve),vabs(Vy,VS,vsubst(Vx,vvar(Vy),Ve))) ) )).

fof('alpha-equiv-typing',axiom,(
    ! [Ve,VC,Ve1,VT] :
      ( ( vtcheck(VC,Ve,VT)
        & valphaEquivalent(Ve,Ve1) )
     => vtcheck(VC,Ve1,VT) ) )).

fof('alpha-equiv-FreeVar',axiom,(
    ! [Ve,Vx,Ve1] :
      ( ( ~ visFreeVar(Vx,Ve)
        & valphaEquivalent(Ve,Ve1) )
     => ~ visFreeVar(Vx,Ve1) ) )).

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