%"(:
;;;****************************************************************************************
;;;
;;; This file is used to add additional lemmas
;;; 
;;; You can add new variables after the 'variables' keyword (initially in comments)
;;; and new lemmas after the 'lemmas' keyword in the form:
;;; <name> : <sequent> ; used for : <some_flags> ; comment : <some_comment> ;
;;; 'used for' and 'comment' are optional.
;;; <some_comment> may be any text not containing a ;
;;; <some_flags> is a comma separated list with information that the lemma should
;;; be used as a simplifier rule or something like that. Since you can add or delete
;;; simplifier rules etc. by menu commands, you can always omit 'used for' if you want.
;;; Possible flags are:
;;;
;;;     simplifier rule:       simp, s, S, simplifier_rule, simplifier, simplification
;;;     local simplifier rule: localsimp, ls, LS, local_simplifier_rule,
;;;                            locsimp, local_simplifier, local_simplification
;;;     elimination:           elim, e, E, elimination
;;;     forward:               forward, f, F
;;;     local forward:         localforward, lf, LF, local_forward
;;;     cut:                   cut, c, C
;;;     local cut:             localcut, lc, LC, local_cut
;;;
;;;****************************************************************************************
:)

(: variables    ; :)

lemmas

max    :   max(x, y) = y   y < x ;
  used for : s, ls ;
  remarks : proved ;
max-01 :   max(x, y) < z  x < z  y < z ;
  used for : s, ls ;
  remarks : proved ;
max-a  :   max(x, max(y, z)) = max(max(x, y), z) ;
  used for : s, ls ;
  remarks : proved, used ;
max-c  :   max(x, y) = max(y, x) ;
  used for : s, ls ;
  remarks : proved, used ;
min    :   z < x  z < y  min(x, y)  z ;
  used for : s, ls ;
  remarks : proved ;
min-01 :   z < x  z < y  z < min(x, y) ;
  used for : s, ls ;
  remarks : proved ;
min-02 :   z < x  z < y   min(x, y) < z ;
  used for : s, ls ;
  remarks : proved ;
min-03 :    x < min(x, y) ;
  used for : s, ls ;
  remarks : proved ;
min-a  :   min(x, min(y, z)) = min(min(x, y), z) ;
  used for : s, ls ;
  remarks : proved, used ;
min-c  :   min(x, y) = min(y, x) ;
  used for : s, ls ;
  remarks : proved, used ;

"

exit

;;; AXIOMS

%"lemmas

ax-01 :   y < x  max(y, x) = x ;
ax-02 :    y < x  max(y, x) = y ;
ax-03 :   y < x  min(y, x) = y ;
ax-04 :    y < x  min(y, x) = x ;


"

