reference defs.hlk;

define proof inf-proof
  proves
    :- all y ( ( O(y) and not empty( y ) ) impl INF(y) );

  with all right
    :- ( O(x) and not empty( x ) ) impl INF(x);
  with auto propositional
    O(x) :- INF(x), empty( x );
  with undef empty
    :- not ex n ( n \in x );
  with not right
    ex n ( n \in x ) :- ;
  with ex left
    k \in x :-;
  with undef O
    all m ( ( m \in x ) impl ( ex t ( \nu( m, t + 1 ) \subseteq x ) ) ) :- ;
  with all left
    ( k \in x ) impl ( ex t ( \nu( k, t + 1 ) \subseteq x ) ) :- ;
  with impl left
    ex t ( \nu( k, t + 1 ) \subseteq x ) :-
    left auto propositional k \in x :- k \in x;
  with ex left
    \nu( k, l_0 + 1 ) \subseteq x :- ;
  with cut INF( \nu( k, l_0 + 1 ) )
    left by proof inf-proof-p1
    right by proof inf-proof-p2( \nu( k, l_0 + 1 ) );
;

define proof inf-proof-p1
  proves
    :- INF( \nu( k, l_0 + 1 ) );

  with undef INF
    :- all m ex n ( m + n + 1 \in \nu( k, l_0 + 1 ) );
  with all right
    :- ex n ( m_0 + n + 1 \in \nu( k, l_0 + 1 ) );
  with ex right
    :- m_0 + ( k * (l_0 + 1 + 1) + l_0 * (m_0 + 1) ) + 1 \in \nu( k, l_0 + 1 );
  with undef \nu
    :- ex r ( m_0 + ( k * (l_0 + 1 + 1) + l_0 * (m_0 + 1) ) + 1 = k + r * (l_0 + 1) );

  continued by proof inf-proof-p1_1;
;

define proof inf-proof-p1_1
  proves
    :- ex r ( m_0 + ( k * (l_0 + 1 + 1) + l_0 * (m_0 + 1) ) + 1 = k + r * (l_0 + 1) );

  with ex right
    :- m_0 + ( k * (l_0 + 1 + 1) + l_0 * (m_0 + 1) ) + 1 =
       k + (k + m_0 + 1) * (l_0 + 1);
#  with paramod left auto propositional
#    :- m_0 + ( k * (l_0 + 1 + 1) + l_0 * (m_0 + 1) ) + 1 =
#       k + (k * l_0 + ( m_0 + 1) * l_0) + (k * 1 + ( m_0 + 1 ) * 1);
#  with paramod by k * 1 = k
#    right :- m_0 + ( k * (l_0 + 1 + 1) + l_0 * (m_0 + 1) ) + 1 =
#       k + (k * l_0 + ( m_0 + 1) * l_0) + (k + ( m_0 + 1 ) * 1);
#  with paramod by ( m_0 + 1 ) * 1 = ( m_0 + 1 )
#    right :- m_0 + ( k * (l_0 + 1 + 1) + l_0 * (m_0 + 1) ) + 1 =
#       k + (k * l_0 + ( m_0 + 1) * l_0) + (k + ( m_0 + 1 ) );
#  with paramod by ( m_0 + 1) * l_0 = ( m_0 * l_0 + 1 * l_0)
#    right :- m_0 + ( k * (l_0 + 1 + 1) + l_0 * (m_0 + 1) ) + 1 =
#       k + (k * l_0 + ( m_0 * l_0 + 1 * l_0)) + (k + ( m_0 + 1 ) );
#  with paramod by 1 * l_0 = l_0
#    right :- m_0 + ( k * (l_0 + 1 + 1) + l_0 * (m_0 + 1) ) + 1 =
#       k + (k * l_0 + ( m_0 * l_0 + l_0)) + (k + ( m_0 + 1 ) );
#  with paramod by k * (l_0 + 1 + 1) = ( k * l_0 ) + k * ( 1 + 1 )
#    right :- m_0 + ( (( k * l_0 ) + k * ( 1 + 1 )) + l_0 * (m_0 + 1) ) + 1 =
#       k + (k * l_0 + ( m_0 * l_0 + l_0)) + (k + ( m_0 + 1 ) );
#  with paramod by k * ( 1 + 1 ) = k * 1 + k * 1
#    right :- m_0 + ( (( k * l_0 ) + ( k * 1 + k * 1 )) + l_0 * (m_0 + 1) ) + 1 =
#       k + (k * l_0 + ( m_0 * l_0 + l_0)) + (k + ( m_0 + 1 ) );
#  with paramod by k * 1 = k
#    right :- m_0 + ( (( k * l_0 ) + ( k + k )) + l_0 * (m_0 + 1) ) + 1 =
#       k + (k * l_0 + ( m_0 * l_0 + l_0)) + (k + ( m_0 + 1 ) );
#  with paramod by l_0 * (m_0 + 1) = l_0 * m_0 + l_0 * 1
#    right :- m_0 + ( (( k * l_0 ) + ( k + k )) + (l_0 * m_0 + l_0 * 1) ) + 1 =
#       k + (k * l_0 + ( m_0 * l_0 + l_0)) + (k + ( m_0 + 1 ) );
#  with paramod by l_0 * 1 = l_0
#    right :- m_0 + ( ( k * l_0 + ( k + k )) + (l_0 * m_0 + l_0) ) + 1 =
#       k + (k * l_0 + ( m_0 * l_0 + l_0)) + (k + ( m_0 + 1 ) );
##  with paramod # by k * l_0 + ( k + k ) = (k * l_0) + k
##    left auto propositional
##    :- m_0 + ( (( k * l_0 + k ) + k) + (l_0 * m_0 + l_0) ) + 1 =
##       k + (k * l_0 + ( m_0 * l_0 + l_0)) + (k + ( m_0 + 1 ) );
#  with paramod by k * l_0 + ( k + k ) = ((k * l_0) + k) + k
#    right :- m_0 + ( (( k * l_0 + k ) + k) + (l_0 * m_0 + l_0) ) + 1 =
#       k + (k * l_0 + ( m_0 * l_0 + l_0)) + (k + ( m_0 + 1 ) );
# with paramod by k * l_0 + ( k + k ) = ( k * l_0 + k ) + k
#   right :- m_0 + ( ( ( k * l_0 + k ) + k ) + (l_0 * m_0 + l_0) ) + 1 =
#      k + (k * l_0 + ( m_0 * l_0 + l_0)) + (k + ( m_0 + 1 ) );
# with paramod by
#   right   m_0 + ( ( ( k * l_0 + ( k + k ) ) + ( l_0 * m_0 + l_0 ) ) + 1 ) =
#     ( ( ( k * l_0 + ( k + k ) ) + ( l_0 * m_0 + l_0 ) ) + 1 ) + m_0
#   :- ( ( ( k * l_0 + ( k + k ) ) + ( l_0 * m_0 + l_0 ) ) + 1 ) + m_0 =
#      k + ( ( k * l_0 + ( m_0 * l_0 + l_0 ) ) + ( k + ( m_0 + 1 ) ) )
;

define proof inf-proof-p2
  with meta term y of type any;

  proves
    INF( y ), y \subseteq x :- INF(x);

  with undef INF
    all m ex n ( m + n + 1 \in y ) :- all m ex n ( m + n + 1 \in x );
  with all right
    :- ex n ( m_0 + n + 1 \in x );
  with all left
    ex n ( m_0 + n + 1 \in y ) :- ;
  with ex left
    m_0 + n_0 + 1 \in y :- ;
  with ex right
    :- m_0 + n_0 + 1 \in x;
  with undef \subseteq
    all n ( (n \in y) impl (n \in x) ) :- ;
  with all left
    ( (m_0 + n_0 + 1 \in y) impl (m_0 + n_0 + 1 \in x) ) :- ;

  auto propositional m_0 + n_0 + 1 \in y, ( (m_0 + n_0 + 1 \in y) impl (m_0 + n_0 + 1 \in x) ) :- m_0 + n_0 + 1 \in x;
;