% hol-1.0.elf
% Author: Carsten Schuermann
% -----------------------------------------------------------------------------
% 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   : 
% -----------------------------------------------------------------------------


nat = [A:tp] (A --> A) --> A --> A.

zero      : {A:tp} tm (nat A)
          = [A:tp] \ [s] \ [z] z.

successor : {A:tp} tm (nat A --> nat A)
          = [A:tp] \ [m] \ [s] \ [z] s @ (m @ s @ z).

plus      : {A:tp} tm (nat A --> nat A --> nat A)
	  = [A:tp] \ [m] \ [n] \ [s] \ [z] m @ s @ (n @ s @ z).

times     : {A:tp} tm (nat A --> nat A --> nat A)
	  = [A:tp] \ [m] \ [n] \ [s] \ [z] m @ (n @ s) @ z.

one       : {A:tp} tm (nat A)
	  = [A:tp] \ [s] \ [z] s @ z.

claim     : {A:tp} |- all (\ [n:tm (nat A)] (times A) @ n @ (one A) === n).

% please fill in a proof here.
% logosophere files are only allowed to contain definitions.
% any declarations counts as an undischarged hypothesis and extends therefore the base logic.