%------------------------------------------------------------------------------
% File     : SYN0011 : TPTP v4.0.0. Released v4.0.0.
% Domain   : Syntactic
% Problem  : 
% Version  : 
% English  : 

% Refs     : [BB05]  Benzmueller & Brown (2005), A Structured Set of Higher
%          : Hindley (or Seldin) ... Basic Simple Type Theory 
% Source   : [BB05]
% Names    : 

% Status   : Theorem (SEMANTICS)
% Rating   : ? v4.0.0
% Syntax   : 

% Comments : 
%------------------------------------------------------------------------------
thof(successor_defn,axiom,
    ( successor
    = ( ! [A:type(0)] :
        ^ [Z:((A > A) > A > A),X:(A > A),Y:A] : 
          (X @ (Z @ X @ Y)) ) )   ).

thof(plus_defn,axiom,
    ( plus
    = ( ! [A:type(0)] :
        ^ [M:((A>A)>A>A),N:((A>A)>A>A)] : 
        ^ [X:(A>A),Y:A] : (M @ X @ (N @ X @ Y)) ) )   ).

thof(times_defn,axiom,
    ( times
    = ( ! [A:type(0)] :
        ^ [M:((A>A)>A>A),N:((A>A)>A>A)] : 
          ((M @ plus) @ zero) ) )   ).

thof(zero,axiom,
    ( zero
    = ( ! [A:type(0)] :
        ^ [F:(A>A),Y:A] : Y ) )   ).
   
thof(one,axiom,
    ( one
    = ( ! [A:type(0)] :
        ^ [F:(A>A),Y:A] : (F @ Y) ) )   ).
   
thof(prove_this,conjecture,
    ! [I:i] :
    ? [N:((I>I)>I>I)] : 
      (times @ N @ one) = ( ^ [F:(I>I)] : F )   ).
%------------------------------------------------------------------------------