; $Id: nat.scm,v 1.8 2008/01/25 13:30:14 logik Exp $

(display "loading nat.scm ...") (newline)


(add-alg "nat" '("Zero" "nat") '("Succ" "nat=>nat"))

; Notice that nat.scm and numbers.scm cannot be loaded together.
; Reason: make-numeric-term (used by the parser) only gets a number.

; In order to make nat.scm compatible with numbers.scm,
; we first define make-numeric-term-in-nat.

(define (make-numeric-term-in-nat n)
  (if (= n 0)
      (pt "Zero")
      (make-term-in-app-form
       (pt "Succ")
       (make-numeric-term-in-nat (- n 1)))))

(define make-numeric-term make-numeric-term-in-nat)

(define (is-numeric-term-in-nat? term)
  (or
   (and (term-in-const-form? term)
        (string=? "Zero"
                  (const-to-name (term-in-const-form-to-const term))))
   (and (term-in-app-form? term)
        (let ((op (term-in-app-form-to-op term)))
          (and (term-in-const-form? op)
               (string=?
                "Succ" (const-to-name (term-in-const-form-to-const op)))
               (is-numeric-term-in-nat?
                (term-in-app-form-to-arg term)))))))

(define is-numeric-term? is-numeric-term-in-nat?)

(define (numeric-term-in-nat-to-number term)
  (if (equal? term (pt "Zero"))
      0
      (+ 1 (numeric-term-in-nat-to-number
            (term-in-app-form-to-arg term)))))

(define numeric-term-to-number numeric-term-in-nat-to-number)


; PROGRAM CONSTANTS

; We add first all program constants in order to be able to define 
; the functions (add-nat-tokens) and (remove-nat-tokens).

(add-program-constant "NatPlus"  (py "nat=>nat=>nat")   t-deg-one)
(add-program-constant "NatTimes" (py "nat=>nat=>nat")   t-deg-one)
(add-program-constant "NatLt"    (py "nat=>nat=>boole") t-deg-one)
(add-program-constant "NatLe"    (py "nat=>nat=>boole") t-deg-one)
(add-program-constant "Pred"     (py "nat=>nat")        t-deg-one)
(add-program-constant "NatMinus" (py "nat=>nat=>nat")   t-deg-one)
(add-program-constant "NatMax"   (py "nat=>nat=>nat")   t-deg-one)
(add-program-constant "NatMin"   (py "nat=>nat=>nat")   t-deg-one)
(add-program-constant "AllBNat"
                      (py "nat=>(nat=>boole)=>boole") t-deg-one)


; (add-nat-tokens) adds all tokens at once.

(define (add-nat-tokens)
  (let ((termcreator
         (lambda (string)
           (lambda (x y)
             (mk-term-in-app-form
              (make-term-in-const-form (pconst-name-to-pconst string))
              x y)))))
    (add-token "+"   'add-op (termcreator "NatPlus"))
    (add-token "*"   'mul-op (termcreator "NatTimes"))
    (add-token "<"   'rel-op (termcreator "NatLt"))
    (add-token "<="  'rel-op (termcreator "NatLe"))
    (add-token "-"   'add-op (termcreator "NatMinus"))
    (add-token "max" 'mul-op (termcreator "NatMax"))
    (add-token "min" 'mul-op (termcreator "NatMin"))))

; (remove-nat-tokens) removes all tokens but it does not change the display !

(define (remove-nat-tokens)
  (remove-token "+")
  (remove-token "*")
  (remove-token "<")
  (remove-token "<=")
  (remove-token "-")
  (remove-token "max")
  (remove-token "min"))

(add-nat-tokens)


; (add-nat-display) will make the displaying of term to use the tokens
; introduced by (add-nat-tokens). Note that (remove-nat-tokens) will not
; remove the tokens from displaying.

(let ((disp-term
       (lambda (const-name symbol token-type)
         (lambda (x)
           (if (term-in-app-form? x)
               (let ((op (term-in-app-form-to-final-op x))
                     (args (term-in-app-form-to-args x)))
                 (if (and (term-in-const-form? op)
                          (string=? const-name
                                    (const-to-name
                                     (term-in-const-form-to-const op)))
                          (= 2 (length args)))
                     (list token-type symbol
                           (term-to-token-tree (car args))
                           (term-to-token-tree (cadr args)))
                     #f))
               #f)))))
  (add-display (py "nat")   (disp-term "NatPlus"  "+"   'add-op))
  (add-display (py "nat")   (disp-term "NatTimes" "*"   'mul-op))
  (add-display (py "boole") (disp-term "NatLt"    "<"   'rel-op))
  (add-display (py "boole") (disp-term "NatLe"    "<="  'rel-op))
  (add-display (py "nat")   (disp-term "NatMinus" "-"   'add-op))
  (add-display (py "nat")   (disp-term "NatMax"   "max" 'mul-op))
  (add-display (py "nat")   (disp-term "NatMin"   "min" 'mul-op)))




; COMPUTATION RULES
; We add all computation rules for all program constats now.

(acrs "nat+0"          "nat"
      "nat1+Succ nat2" "Succ(nat1+nat2)"
; NatTimes *
      "nat*0"          "0"
      "nat1*Succ nat2" "(nat1*nat2)+nat1"
; NatLt <
      "nat<0"                 "False"
      "0<Succ nat"            "True"
      "Succ nat1<Succ nat2"   "nat1<nat2"
; NatLe <=
      "0<=nat"                "True"
      "Succ nat<=0"           "False"
      "Succ nat1<=Succ nat2"  "nat1<=nat2"
; Pred
      "Pred 0"              "0"
      "Pred(Succ nat)"      "nat"
; NatMinus -
      "nat-0"               "nat"
      "nat1-Succ nat2"      "Pred(nat1-nat2)"
; NatMax max
      "nat max 0"                 "nat"
      "0 max Succ nat"            "Succ nat"
      "Succ nat1 max Succ nat2"   "Succ(nat1 max nat2)"
; NatMin min
      "nat min 0"                 "0"
      "0 min Succ nat"            "0"
      "Succ nat1 min Succ nat2"   "Succ(nat1 min nat2)"
; AllBNat
      "AllBNat 0 nat=>boole"     "True"
      "AllBNat(Succ nat)nat=>boole"
          "AllBNat nat nat=>boole andb (nat=>boole)nat")



; We now prove and add some RW-rules.


; Some RW-rules concerning NatPlus +


(sg "all nat 0+nat=nat")
(ind)
  (use-with "Truth-Axiom")
(assume "nat" "IH")
(use-with "IH")
; Proof finished
(arw "0+nat" "nat")


(sg "all nat1,nat2 (Succ nat1)+nat2=Succ(nat1+nat2)")
(assume "nat1")
(ind)
  (use-with "Truth-Axiom")
(assume "nat2" "IH")
(use-with "IH")
; Proof finished
(arw "(Succ nat1)+nat2" "Succ(nat1+nat2)")



(sg "all nat1,nat2,nat3. nat1+(nat2+nat3)=(nat1+nat2)+nat3")
(ind)
  (strip)
  (use-with "Truth-Axiom")
(assume "nat1" "IH")
(use-with "IH")
; Proof finished
(arw "nat1+(nat2+nat3)" "(nat1+nat2)+nat3")


; "NatPlusComm"
(sg  "all nat1,nat2.nat1+nat2=nat2+nat1")
(assume "nat1")
(ind)
  (use-with "Truth-Axiom")
(assume "nat2" "IH")
(use-with "IH")
; Proof finished
(save "NatPlusComm")



; Some RW-rules concerning NatTimes *

(sg "0*nat=0")
(ind)
  (use-with "Truth-Axiom")
(assume "nat" "IH")
(use-with "IH")
; Proof finished
(arw "0*nat" "0")



(sg  "all nat1,nat2 Succ nat1*nat2=(nat1*nat2)+nat2")
(assume "nat1")
(ind)
  (use-with "Truth-Axiom")
(assume "nat2" "IH")
(ng)
(simp-with "IH")
(simp-with (pf"nat1*nat2+nat2+nat1=nat1*nat2+(nat2+nat1)"))
(simp-with "NatPlusComm" (pt "nat2") (pt"nat1"))
(use-with  "Truth-Axiom")
(use-with  "Truth-Axiom")
; Proof finished
(arw "Succ nat1*nat2" "(nat1*nat2)+nat2")


(sg  "nat1*(nat2+nat3)=(nat1*nat2)+(nat1*nat3)")
(ind)
  (strip)
  (use-with "Truth-Axiom")
(assume "nat1" "IH1" "nat2" "nat3")
(ng)
(simp-with "IH1" (pt "nat2")(pt "nat3"))
(simp-with (pf"(((nat1*nat2)+nat2)+(nat1*nat3))=((nat1*nat2)+(nat1*nat3)+nat2)"))
(use-with "Truth-Axiom")
(simp-with (pf"(nat1*nat2+nat2+(nat1*nat3))=(nat1*nat2+(nat2+(nat1*nat3)))"))
(simp-with "NatPlusComm" (pt"nat2")(pt"nat1*nat3"))
(use-with "Truth-Axiom")
(use-with "Truth-Axiom")
; Proof finished
(arw "nat1*(nat2+nat3)" "(nat1*nat2)+(nat1*nat3)")



; "NatTimesComm"
(sg  "nat1*nat2=nat2*nat1")
(ind)
  (strip)
  (use-with "Truth-Axiom")
(assume "nat1" "IH" "nat2")
(ng)
(simp-with "IH" (pt"nat2"))
(use-with  "Truth-Axiom")
;Proof finished
(save "NatTimesComm")


(sg  "(nat1+nat2)*nat3=(nat1*nat3)+(nat2*nat3)")
(assume "nat1" "nat2" "nat3")
(simp-with "NatTimesComm" (pt "nat1+nat2") (pt "nat3"))
(simp-with "NatTimesComm" (pt "nat1") (pt "nat3"))
(simp-with "NatTimesComm" (pt "nat2") (pt "nat3"))
(use-with "Truth-Axiom")
; Proof finished
(arw "(nat1+nat2)*nat3" "(nat1*nat3)+(nat2*nat3)")





(sg  "all nat1,nat2,nat3.nat1*(nat2*nat3)=(nat1*nat2)*nat3")
(ind)
  (strip)
  (use-with "Truth-Axiom")
(assume "nat1" "IH1" "nat2" "nat3")
(ng)
(simp-with "IH1" (pt "nat2")(pt "nat3"))
(use-with "Truth-Axiom")
; Proof finished
(arw "nat1*(nat2*nat3)" "nat1*nat2*nat3")




; Some RW-rules concerning NatLt <

(sg  "all nat nat<Succ nat")
(ind)
  (use-with "Truth-Axiom")
(assume "nat" "IH")
(use-with "IH")
; Proof finished
(arw "nat<Succ nat" "True")





(sg  "all nat.(Succ nat<nat)=F")
(ind)
  (use-with "Truth-Axiom")
(assume "nat" "IH")
(use-with "IH")
; Proof finished
(arw "Succ nat<nat" "F")




; "NatLtTrans"
(sg "all nat1,nat2,nat3.nat1<nat2 -> (nat2<nat3 -> nat1<nat3)")
(ind)
(cases)
  (assume "nat3" "§" "$")
  (use-with "$")
(assume "nat2")
(cases)
(assume "§" "$")
(use-with "$")
(assume "nat3" "§" "$")
(use-with "Truth-Axiom")
(assume "nat1" "IH1")
(cases)
  (assume "nat3" "fal" "0<3")
  (use-with "Efq-Atom" (pt"Succ nat1<nat3") "?")
  (use-with "fal")
(assume "nat2")
(cases)
(assume "§" "$")
(use-with "$")
(use-with "IH1" (pt"nat2"))
; Proof finished
(save "NatLtTrans")



; "NatLtSuccCases"
(sg "all nat2,nat1.
  nat1<Succ nat2 -> (nat1<nat2 -> Pvar^) -> (nat1=nat2 -> Pvar^) -> Pvar^")
(ind)
  (cases)
  (assume "w" "§" "$")
  (use-with "$" "?")
  (use-with "Truth-Axiom")
  (assume "nat1" "§" "$" "%")
  (use-with "$" "?")
  (use-with "§")
(assume "nat2" "IH")
(cases)
(assume "w" "§" "$")
(use-with "§" "?")
(use-with "Truth-Axiom")
(use-with "IH")
; Proof finished
(save "NatLtSuccCases")




(sg  "all nat nat<=nat")
(ind)
  (use-with "Truth-Axiom")
(assume "nat" "IH")
(use-with "IH")
; Proof finished
(arw "nat<=nat" "True")




(sg  "all nat1,nat2 nat1<=(nat1+nat2)")
(ind)
  (assume "nat2")
  (use-with "Truth-Axiom")
(assume "nat" "IH")
(use-with "IH")
; Proof finished
(arw "nat1<=(nat1+nat2)" "True")



(sg  "all nat.(Succ nat<=nat)=F")
(ind)
  (use-with "Truth-Axiom")
(assume "nat" "IH")
(use-with "IH")
; Proof finished
(arw "Succ nat<=nat" "False")


; "NatLeTrans"
(sg  "all nat1,nat2,nat3.nat1<=nat2 -> nat2<=nat3 -> nat1<=nat3")
(ind)
  (strip)
  (use-with "Truth-Axiom")
(assume "nat1" "IH1")
(cases)
  (ng)
  (assume "nat3" "fal" "w")
  (use-with "Efq-Atom" (pt "Succ nat1<=nat3") "?")
  (use-with "fal")
(assume "nat2")
(cases)
(assume "§" "$")
(use-with "$")
(use-with "IH1" (pt"nat2"))
; Proof finished
(save "NatLeTrans")



; "NatLtLeTrans"
(sg  "all nat1,nat2,nat3.nat1<nat2 -> nat2<=nat3 -> nat1<nat3")
(ind)
(cases)
  (assume "nat3" "fal" "w")
  (use-with "Efq-Atom" (pt"0<nat3") "?")
  (use-with "fal")
(assume "nat2")
(cases)
  (assume "§" "fal")
  (use-with "fal")
  (assume "nat3" "§" "$")
(use-with "Truth-Axiom")
(assume "nat1" "IH1")
(cases)
  (assume "nat3" "fal" "w")
  (use-with "Efq-Atom" (pt"Succ nat1<nat3") "?")
  (use-with "fal")
(assume "nat2")
(cases)
(assume "§" "fal")
(use-with "fal")
(use-with "IH1" (pt"nat2"))
; Proof finished
(save "NatLtLeTrans")




; "NatLeLtTrans"
(sg  "all nat1,nat2,nat3.nat1<=nat2 -> nat2<nat3 -> nat1<nat3")
(ind)
  (cases)
    (cases)
    (assume "§" "$")
    (use-with "$")
    (assume "nat3" "§" "$")
    (use-with "$")
  (assume "nat2")
  (cases)
  (assume "§" "$")
  (use-with "$")
  (assume "nat3" "§" "$")
  (use-with "Truth-Axiom")
(assume "nat1" "IH1")
(cases)
  (assume "nat3" "fal" "0<3")
  (use-with "Efq-Atom" (pt"Succ nat1<nat3") "?")
  (use-with "fal")
(assume "nat2")
(cases)
(assume "§" "$")
(use-with "$")
(use-with "IH1" (pt"nat2"))
; Proof finished
(save "NatLeLtTrans")



; "NatLtSuccToLe"
(sg  "all nat1,nat2.nat1<Succ nat2 -> nat1<=nat2")
(ind)
  (strip)
  (use-with "Truth-Axiom")
(assume "nat1" "IH1")
(cases)
(assume "§")
(use-with "§")
(use-with "IH1")
; Proof finished
(save "NatLtSuccToLe")


; "NatLtLtSuccTrans"
(sg  "all nat1,nat2,nat3.nat1<nat2 -> nat2<Succ nat3 -> nat1<nat3")
(assume "nat1" "nat2" "nat3" "1<2" "2<S3")
(use-with "NatLtLeTrans" (pt"nat1") (pt"nat2") (pt"nat3") "?" "?")
(use-with "1<2")
(use-with "NatLtSuccToLe" (pt "nat2") (pt"nat3") "?")
(use-with "2<S3")
; Proof finished
(save "NatLtLtSuccTrans")



; "NatLeToLtSucc"
(sg  "all nat1,nat2.nat1<=nat2 -> nat1<Succ nat2")
(ind)
  (strip)
  (use-with "Truth-Axiom")
(assume "nat1" "IH1")
(cases)
(assume "§")
(use-with "§")
(use-with "IH1")
; Proof finished
(save "NatLeToLtSucc")


; "NatLeCases"
(sg  "all nat2,nat1.nat1<=nat2 -> (nat1<nat2 -> Pvar^) -> 
               (nat1=nat2 -> Pvar^) -> Pvar^")
(ind)
  (cases)
  (assume "§" "$" "%")
  (use-with "%" "?")
  (use-with "Truth-Axiom")
  (assume "nat2"  "§" "$" "%")
  (use-with "%" "?")
  (use-with "§")
(assume "nat1" "IH")
(cases)
(assume "§" "$" "%")
(use-with "$" "?")
(use-with "Truth-Axiom")
(use-with "IH")
; Proof finished
(save "NatLeCases")




; Properties of arithmetic functions max, Pred, -, ...

; "NatPredMinusSucc"
(sg  "all nat1,nat2 Pred(Succ nat1-nat2)=nat1-nat2")
(assume "nat1")
(ind)
  (use-with "Truth-Axiom")
(assume "nat2" "IH")
(ng)
(simp-with "IH")
(use-with  "Truth-Axiom")
; Proof finished
(save "NatPredMinusSucc")
(arw "Pred(Succ nat1-nat2)" "nat1-nat2")



(sg  "all nat nat-nat=0")
(ind)
  (use-with "Truth-Axiom")
(assume "nat" "IH")
(use-with "IH")
; Proof finished
(arw "nat-nat" "0")


(pp(nt(pt "Succ nat<=nat")))
; False




(sg "Succ nat-nat=1")
(ind)
  (use-with "Truth-Axiom")
(assume "nat" "IH")
(use-with "IH")
; Proof finished
(arw "Succ nat-nat" "1")


(sg "0 max nat=nat")
(cases)
  (use-with "Truth-Axiom")
(strip)
(use-with "Truth-Axiom")
; Proof finished
(arw "0 max nat" "nat")


(sg "nat max nat = nat")
(ind)
  (use-with "Truth-Axiom")
(assume "nat" "IH")
(use-with "IH")
; Proof finished
(arw "nat max nat" "nat")



(sg "nat1 max (nat2 max nat3)=(nat1 max nat2) max nat3")
(ind)
  (strip)
  (use-with "Truth-Axiom")
(assume "nat1" "IH1")
(cases)
  (strip)
  (use-with "Truth-Axiom")
(assume "nat2")
(cases)
(use-with "Truth-Axiom")
(use-with "IH1" (pt"nat2"))
; Proof finished
(arw "nat1 max (nat2 max nat3)" "(nat1 max nat2) max nat3")



(sg "nat1 max nat2 = nat2 max nat1")
(ind)
  (strip)
  (use-with "Truth-Axiom")
(assume "nat1" "IH")
(cases)
(use-with "Truth-Axiom")
(use-with "IH")
; Proof finished
(save "NatMaxComm")


; NatMaxUB1
(sg  "all nat1,nat2 nat1<=(nat1 max nat2)")
(ind)
  (assume "nat2")
  (use-with "Truth-Axiom")
(assume "nat1" "IH1")
(cases)
(use-with "Truth-Axiom")
(use-with "IH1")
; Proof finished
(save "NatMaxUB1")


; NatMaxUB2
(sg  "all nat1,nat2 nat2<=(nat1 max nat2)")
(ind)
  (assume "nat2")
  (use-with "Truth-Axiom")
(assume "nat1" "IH1")
(cases)
(use-with "Truth-Axiom")
(use-with "IH1")
; Proof finished
(save "NatMaxUB2")




(sg "0 min nat=0")
(cases)
  (use-with "Truth-Axiom")
(strip)
(use-with "Truth-Axiom")
; Proof finished
(arw "0 min nat" "0")


(sg "nat min nat = nat")
(ind)
  (use-with "Truth-Axiom")
(assume "nat" "§")
(use-with "§")
; Proof finished
(arw "nat min nat" "nat")



(sg "nat1 min (nat2 min nat3)=(nat1 min nat2) min nat3")
(ind)
  (strip)
  (use-with "Truth-Axiom")
(assume "nat1" "IH1")
(cases)
  (strip)
  (use-with "Truth-Axiom")
(assume "nat2")
(cases)
(use-with "Truth-Axiom")
(use-with "IH1" (pt "nat2"))
; Proof finished
(arw "nat1 min (nat2 min nat3)" "(nat1 min nat2) min nat3")




; "NatMinLB1" 
(sg  "all nat1,nat2 nat1 min nat2<=nat1")
(ind)
  (assume "nat2")
  (use-with "Truth-Axiom")
(assume "nat1" "IH1")
(cases)
(use-with "Truth-Axiom")
(use-with "IH1")
; Proof finished
(save "NatMinLB1")



; "NatMinLB2" 
(sg  "all nat1,nat2 nat1 min nat2<=nat2")
(ind)
  (assume "nat2")
  (use-with "Truth-Axiom")
(assume "nat1" "IH1")
(cases)
(use-with "Truth-Axiom")
(use-with "IH1")
; Proof finished
(save "NatMinLB2")




; "AllBNatIntro"
(sg "all nat=>boole^,nat2.
       (all nat1.nat1<nat2 -> nat=>boole^nat1)
    -> AllBNat nat2([nat1]nat=>boole^nat1)")
(assume "nat=>boole^")
(ind)
  (strip)
  (use-with "Truth-Axiom")
(assume "nat2" "IH" "H")
(ng)
(split)
    (use-with "IH" "?")
    (assume "nat1" "nat1<nat2")
    (use-with "H" (pt"nat1") "?")
    (use-with "NatLtTrans" (pt "nat1")(pt "nat2")(pt "Succ nat2") "?" "?")
    (use-with "nat1<nat2")
    (use-with "Truth-Axiom")
(use-with "H" (pt"nat2") "?")
(use-with "Truth-Axiom")
; Proof finished
(save "AllBNatIntro")




; "AllBNatElim"

(sg "all nat=>boole^,nat2,nat1.
  AllBNat nat2 nat=>boole^ impb (nat1<nat2 impb nat=>boole^ nat1)")
(assume "nat=>boole^")
(ind)
  (strip)
  (use-with "Truth-Axiom")
(assume "nat2" "IH")
;(ng)
(assume "nat1" "AllBHyp"  "nat1<Succ nat2")
(ng "AllBHyp")
(use-with "NatLtSuccCases" (pt "nat2") (pt "nat1") "?" "?" "?")
(use-with "nat1<Succ nat2")
(assume "1<2")
(use-with "IH" (pt "nat1") "?" "?")
(use-with "AllBHyp" 'left)
(use-with "1<2")
(assume "nat1=nat2")
(simp-with "nat1=nat2")
(use-with "AllBHyp" 'right)
; Proof finished
(arw
 "AllBNat nat2 nat=>boole^ impb (nat1<nat2 impb nat=>boole^ nat1)"
 "True")


(sg "all nat=>boole^,nat2.
  AllBNat nat2 nat=>boole^ -> all nat1.nat1<nat2 -> nat=>boole^ nat1")
(assume "nat=>boole^" "nat2" "*" "nat1" "1<2")
(use (pf"AllBNat nat2 nat=>boole^
         impb (nat1<nat2 impb nat=>boole^ nat1)"))
(use-with "Truth-Axiom")
(use-with "*")
(use-with "1<2")
; Proof finished
(save "AllBNatElim")




(define (add-more-nat-thms)

; Already shown above, but added as theorem instead of RW-rule

; NatMaxUB1
(add-rewrite-rule (pt"nat1<=(nat1 max nat2)") (pt"True"))
; NatMaxUB2
(add-rewrite-rule (pt"nat2<=(nat1 max nat2)") (pt"True"))
; NatMaxLB1
(add-rewrite-rule (pt"(nat1 min nat2)<=nat1") (pt"True"))
; NatMaxLB2
(add-rewrite-rule (pt"(nat1 min nat2)<=nat2") (pt"True"))





(sg  "all nat.(nat<nat)=F")
(ind)
  (use-with "Truth-Axiom")
(assume "nat" "§")
(use-with "§")
; Proof finished
(arw "nat<nat" "F")


(sg "nat<=Succ nat")
(ind)
  (use-with "Truth-Axiom")
(assume "nat" "§")
(use-with "§")
; Proof finished.
(arw "nat<=Succ nat" "True")



(sg "nat1<=(nat2+nat1)")
(assume "nat1" "nat2")
(simp-with "NatPlusComm" (pt"nat2") (pt"nat1"))
(use-with  "Truth-Axiom")
; Proof finished.
(arw "nat1<=(nat2+nat1)" "T")



(sg "all nat1.nat1<Succ(nat1+nat2)")
(assume "nat2")
(ind)
  (use-with "Truth-Axiom")
(assume "nat1" "IH")
(use-with "IH")
; Proof finished.
(arw "nat1<Succ(nat1+nat2)" "T")



; "natNotLt"

(sg " nat2<=nat1 -> ( False=(nat1<nat2) & (nat1<nat2) = False )")
(ind)
  (cases)
  (strip)
  (split)
  (use-with "Truth-Axiom")
  (use-with "Truth-Axiom")
  (strip)
  (split)
  (use-with "Truth-Axiom")
  (use-with "Truth-Axiom")
(assume "nat2" "IH")
(cases)
(assume "*")
(split)
(use-with "*")
(use-with "*")
(use-with "IH")
; Proof finished.
(add-theorem "natNotLt" (np(current-proof)))



; "natNotLe"

(sg " nat2<nat1 -> ( False=(nat1<=nat2) & (nat1<=nat2) = False )")
(ind)
  (cases)
  (assume "*")
  (split)
  (use-with "*")
  (use-with "*")
  (strip)
  (split)
  (use-with "Truth-Axiom")
  (use-with "Truth-Axiom")
(assume "nat2" "IH")
(cases)
(assume "*")
(split)
(use-with "*")
(use-with "*")
(use-with "IH")
; Proof finished.
(add-theorem "natNotLe" (np(current-proof)))


(sg "all nat1.(nat1<(Succ nat2))=(nat1<=nat2)")
(ind)
  (cases)
  (use-with "Truth-Axiom")
  (strip)
  (use-with "Truth-Axiom")
(assume "nat2" "IH")
(cases)
(use-with "Truth-Axiom")
(use-with "IH")
; Proof finished.
(arw "nat1<(Succ nat2)" "nat1<=nat2")



(add-rewrite-rule
 (pt "NatLe(NatPlus nat1 nat2) Zero")
 (pt "(negb(NatLt Zero nat1)) andb (negb(NatLt Zero nat2))"))
(add-rewrite-rule
 (pt "NatLt(NatPlus nat1 nat2)(NatPlus nat1 nat3)")
 (pt "NatLt nat2 nat3"))
(add-rewrite-rule
 (pt "NatLt(NatPlus nat1 nat1)(NatPlus nat2 nat2)")
 (pt "NatLt nat1 nat2"))
(add-rewrite-rule
 (pt "NatLe(NatPlus nat1 nat1)(NatPlus nat2 nat2)")
 (pt "NatLe nat1 nat2"))
(add-rewrite-rule
 (pt "NatLe(NatPlus nat1 nat1)(Succ (NatPlus nat2 nat2))")
 (pt "NatLe nat1 nat2"))
(add-rewrite-rule
 (pt "NatLe(Succ(NatPlus nat1 nat1))(NatPlus nat2 nat2)")
 (pt "NatLt nat1 nat2"))
(add-rewrite-rule
 (pt "NatLt(Succ(NatPlus nat1 nat1))(NatPlus nat2 nat2)")
 (pt "NatLt nat1 nat2"))


)



; Are these really needed ???
(av "n" "m" "k" (py "nat"))