define type obj fresh variable starts with u;

define variable x,y,z of type obj;
define variable v of type obj;
define constant a of type obj;

define function f of type obj to obj;

define recursive function f_{exp}( x ) to obj
  at level 0 by f( x )
  at level k by f_{exp}[k - 1]( f_{exp}[k - 1]( x ) );

define atom predicate P of type obj, obj;

define predicate T by 
  all x all y all z ( ( P( x, y ) and P( y, z ) ) impl P( x, z ) );

################################################################################

define proof p
  proves
    T, all x P( f_{exp}[0]( x ), x ) :- P( f_{exp}[4]( a ), a );

  continued by proof q[4];
;
    
################################################################################

define recursive proof q
  at level k proves
    T, all x P( f_{exp}[0]( x ), x ) :- P( f_{exp}[k]( a ), a );

  with cut all x P( f_{exp}[k]( x ), x )
    left by proof \varphi[k];
  with all left
    P( f_{exp}[k]( a ), a ) :- ;
;

################################################################################

define recursive proof \varphi
  at level 0 proves
    all x P( f_{exp}[0]( x ), x ) :- all x P( f_{exp}[0]( x ), x );

  at level k + 1 proves
    T, all x P( f_{exp}[0]( x ), x ) :- all x P( f_{exp}[k + 1]( x ), x );

  with cut all x P( f_{exp}[k]( x ), x )
    left by proof \varphi[k];
  with all right
    :- P( f_{exp}[k + 1]( v[k] ), v[k] );
  with undef T
    all x all y all z ( ( P( x, y ) and P( y, z ) ) impl P( x, z ) ) :- ;
  with all left
    ( P( f_{exp}[k + 1]( v[k] ), f_{exp}[k]( v[k] ) ) and
      P( f_{exp}[k]( v[k] ), v[k] ) )
      impl P( f_{exp}[k + 1]( v[k] ), v[k] ) :- ;
  with impl left
    :- P( f_{exp}[k + 1]( v[k] ), f_{exp}[k]( v[k] ) ) and
       P( f_{exp}[k]( v[k] ), v[k] )
#   right by proof r[k + 1];
    right auto propositional P( f_{exp}[k + 1]( v[k] ), v[k] ) :- P( f_{exp}[k + 1]( v[k] ), v[k] ) ;
  with all left
    P( f_{exp}[k]( v[k] ), v[k] ) :- ;
  with and right
    :- P( f_{exp}[k + 1]( v[k] ), f_{exp}[k]( v[k] ) )
    right auto propositional P( f_{exp}[k]( v[k] ), v[k] ) :- P( f_{exp}[k]( v[k] ), v[k] ) ;
  with undef f_{exp}[k + 1]
    :- P( f_{exp}[k]( f_{exp}[k]( v[k] ) ), f_{exp}[k]( v[k] ) );
  with all left
    P( f_{exp}[k]( f_{exp}[k]( v[k] ) ), f_{exp}[k]( v[k] ) ) :- ;

#  continued auto propositional;
;

define recursive proof r
  at level k + 1 proves
:-;
#   P( f_{exp}[k + 1]( v[k] ), v[k] ) :- P( f_{exp}[k + 1]( v[k] ), v[k] );
;