%"(:
;;;****************************************************************************************
;;;
;;; 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
abs-one :  abs(1) = 1; used for : s,ls;
abs-01    :   abs(abs(x)) = abs(x) ;
  used for : s, ls ;
  remarks : proved ;
abs-02    :   abs(0) = 0 ;
  used for : s, ls ;
  remarks : proved, used ;
abs-03    :   0  abs(x) ;
  used for : s, ls ;
  remarks : proved, used ;
abs-04    :   0  x  abs(x + 1) = abs(x) + 1 ;
  used for : s, ls ;
  remarks : proved, used ;
abs-05    :   x < 0  abs(x + 1) = abs(x) - 1 ;
  used for : s, ls ;
  remarks : proved ;
abs-06    :   0 < abs(x)  x  0;
  used for : s, ls ;
  remarks : proved, used ;
abs-07    :   abs(x) = 0  x = 0 ;
  used for : s, ls ;
  remarks : proved ;
abs-08    :   x < 0  abs(x) = ~ x ;
  used for : ls ;
  remarks : proved, used ;
abs-09    :   0 < x  abs(x - 1) = abs(x) - 1 ;
  used for : s, ls ;
  remarks : proved ;
abs-10    :   abs(x) - 1 < 0  x = 0 ;
  used for : s, ls ;
  remarks : proved ;
abs-11    :   0 < abs(x)  x  0 ;
  used for : s, ls ;
  remarks : proved ;
abs-12    :   0  x  0  y  abs(x + y) = abs(x) + abs(y) ;
  used for : s, ls ;
  remarks : proved, used ;
abs-14    :   y < 0  0 < x + y  abs(y) < x ;
  used for : s, ls ;
  remarks : proved ;
abs-15    :   y < 0  x + y  0   abs(y) < x ;
  used for : s, ls ;
  remarks : proved ;
abs-16    :   0 < y  abs(y) = y ;
  used for : s, ls ;
  remarks : proved ;
abs-17    :   0 < y  abs(y + 1) = y + 1 ;
  used for : s, ls ;
  remarks : proved ;
abs-18    :   abs(x) = x  0  x ;
  used for : s, ls ;
  remarks : proved, used ;
abs-19    :   y  x  y  abs(x) ;
  used for : s, ls ;
  remarks : proved, used ;
abs-21    :   x  y  (abs(x) = abs(y)  x = ~ y) ;
  used for : s, ls ;
  remarks : proved ;
abs-ls    :   x < y  y < 0  abs(y) < abs(x) ;
  used for : s, ls ;
  remarks : proved ;
abs-ls-01 :   y < x  0  y  abs(y - x)  abs(x) ;
  used for : s, ls ;
  remarks : proved ;
abs-ls-02 :   y  z  z  x  abs(z - y)  abs(x - y) ;
  used for : s, ls ;
  remarks : proved ;
abs-ls-03 :   y < x  (x < abs(y - x)  y < 0) ;
  used for : s, ls ;
  remarks : proved ;
abs-neg   :   abs(~ x) = abs(x) ;
  used for : s, ls ;
  remarks : proved, used ;
abs-succ  :   x < 0  (x + 1 = abs(y)  x = ~1  y = 0) ;
  used for : s, ls ;
  remarks : proved ;
absneg    :   abs(x) = x  abs(x) = ~ x ;
  remarks : proved, used ;
absneg-01 :   abs(x)  x  abs(x) = ~ x ;
  used for : ls ;
  remarks : proved, used ;
absneg-02 :   abs(x)  ~ x  abs(x) = x ;
  used for : s, ls ;
  remarks : proved ;
absp      : 0  y, y < x  abs(y - x)  abs(x) ;
  remarks : proved ;
absp-01   : y  z, x  y  abs(y - x)  abs(z - x) ;
  remarks : proved ;
ls        : 0  x, abs(y) < x  0  x + y ;
  remarks : proved ;
neg       :   0 < ~ x  x < 0 ;
  used for : s, ls ;
  remarks : proved, used ;
neg-01    :   ~ y < ~ x  x < y ;
  used for : s, ls ;
  remarks : proved ;
neg-02    :   ~ ~ x = x ;
  used for : s, ls ;
  remarks : proved ;
neg-03    :   ~ x + x = 0 ;
  used for : s, ls ;
  remarks : proved ;
neg-04    :   ~ 0 = 0 ;
  used for : s, ls ;
  remarks : proved ;
neg-05    :   ~ x < 0  0 < x ;
  used for : s, ls ;
  remarks : proved ;
neg-06    :   0 - x = ~ x ;
  used for : s ;
  remarks : proved ;
neg-07    :   x < ~ y  x + y < 0 ;
  used for : s, ls ;
  remarks : proved ;
neg-08    :   x + ~ y < 0  x < y ;
  used for : s, ls ;
  remarks : proved ;
neg-09    :   0 < x + ~ y  y < x ;
  used for : s, ls ;
  remarks : proved ;
neg-10    :   ~ x = 0  x = 0 ;
  used for : s, ls ;
  remarks : proved ;
neg-11    :   ~ x + ~ y = ~ (x + y) ;
  used for : s, ls ;
  remarks : proved, used ;
neg-12    :   ~ x = ~ y  x = y ;
  used for : s, ls ;
  remarks : proved ;
neg-13    :   ~ x < y  0 < y + x ;
  used for : s, ls ;
  remarks : proved ;
neg-14    :   x = ~ x  x = 0 ;
  used for : s, ls ;
  remarks : proved ;
neg-15    :   x + ~ y = x - y ;
  used for : s, ls ;
  remarks : proved ;
negadd    :   x + ~ y < ~ z  x + z < y ;
  used for : s, ls ;
  remarks : proved ;
sgn       :   sgn(x)  1  sgn(x) = ~1 ;
  used for : s, ls ;
  remarks : proved, used ;
sgn-01    :   sgn(x) = 1  0  x ;
  used for : s, ls ;
  remarks : proved ;
sgn-02    :   sgn(x) = ~1  x < 0 ;
  used for : s, ls ;
  remarks : proved, used ;
sgn-03    :   sgn(x) = 1  sgn(x) = ~1 ;
  remarks : proved ;
sgn-04    :   y  x  sgn(x - y) = 1 ;
  used for : s, ls ;
  remarks : proved ;
sgn-05    :   y + z  x  sgn(x - z + y) = 1 ;
  used for : s, ls ;
  remarks : proved ;
sgn-06    :   x < y  sgn(x - y) = ~1 ;
  used for : s, ls ;
  remarks : proved ;
sgn-07    :   x < y + z  sgn(x - z + y) = ~1 ;
  used for : ls ;
  remarks : proved ;
sgn-08    :   sgn(x)  0 ;
  used for : s, ls ;
  remarks : proved ;
sneg      :   ~ x = y  (~ y = x  true) ;
  used for : s, ls ;
  remarks : proved ;
sr        :   sgn(x)  1  sgn(x) = ~1 ;
  remarks : proved ;

"

exit

;;; AXIOMS

%"lemmas

ax-01 :   ~ x = 0 - x ;
ax-02 :   y < 0  sgn(y) = 0 -1 ;
ax-03 :    y < 0  sgn(y) = 0 +1 ;
ax-04 :   y < 0  abs(y) = 0 - y ;
ax-05 :    y < 0  abs(y) = y ;


"

