(load "~/git/minlog/init.scm")

(set! COMMENT-FLAG #f)
(libload "nat.scm")
(set! COMMENT-FLAG #t)

(add-pvar-name "P" (make-arity (py "nat")))

(set-goal "allnc n^(
     TotalNat n^ -> 
     0=0 orr exr m^(0=m^ +1 andr TotalNat m^) -> 
     allnc n^(
      n^ =0 orr exr m^(n^ =m^ +1 andr TotalNat m^) -> 
      n^ +1=0 orr exr m^(n^ +1=m^ +1 andr TotalNat m^)) -> 
     n^ =0 orr exr m^(n^ =m^ +1 andr TotalNat m^)) -> 
    allnc n^(TotalNat n^ -> n^ =0 orr exr m^(n^ =m^ +1 andr TotalNat m^))")
(assume ...)
(use ...)
;; 3-5
(use ...)
;; 4
(intro ...)
(use "Truth")
;; 5
(assume ...)
(elim ...)
;; 8-9
(assume "m=0")
(intro ...)
(intro ...)
(simp "m=0")
(intro ...)
(use "Truth")
(use "NatTotalVar")
;; 9
(assume "w")
(intro ...)
(by-assume "w" "m^1" "m1Prop")
(intro 0 (pt "m^1 +1"))
(intro 0)
(use "m1Prop")
(intro ...)
(use "m1Prop")
;; Proof finished.
(save "LemmaA")

(set-goal "allnc n^(
     TotalNat n^ -> 
     0=0 orr exr m^(0=m^ +1 andr TotalNat m^) -> 
     allnc n^(
      n^ =0 orr exr m^(n^ =m^ +1 andr TotalNat m^) -> 
      n^ +1=0 orr exr m^(n^ +1=m^ +1 andr TotalNat m^)) -> 
     n^ =0 orr exr m^(n^ =m^ +1 andr TotalNat m^)) -> 
    allnc n^(TotalNat(n^ +1) -> TotalNat n^)")
(assume ...)
(inst-with-to "LemmaA" ... "LemmaAInst")
(elim "LemmaAInst")
;; 5-6
(ng)
(use "Efq")
;; 6
(assume ...)
(by-assume ...)
(simp ...)
(use ...)
;; Proof finshed.
(save "LemmaB")

(set-goal "allnc n^(
     TotalNat n^ -> 
     0=0 orr exr m^(0=m^ +1 andr TotalNat m^) -> 
     allnc n^(
      n^ =0 orr exr m^(n^ =m^ +1 andr TotalNat m^) -> 
      n^ +1=0 orr exr m^(n^ +1=m^ +1 andr TotalNat m^)) -> 
     n^ =0 orr exr m^(n^ =m^ +1 andr TotalNat m^)) -> 
    allnc n^(
     TotalNat n^ -> 
     (TotalNat 0 -> P 0) -> 
     allnc n^((TotalNat n^ -> P n^) -> TotalNat(n^ +1) -> P(n^ +1)) -> 
     TotalNat n^ -> P n^) -> 
    allnc n^(
     TotalNat n^ -> P 0 -> allnc n^(TotalNat n^ -> P n^ -> P(n^ +1)) -> P n^)")
(assume "u0" ...)
(use ...)
;; 3-5
(use ...)
;; 4
(assume ...)
(use ...)
;; 5
(assume ...)
(use ...)
;; 9-10
(use-with "LemmaB" "u0" ...)
;; 10
(use ...)
(use-with "LemmaB" "u0" ...)
(use ...)
;; Proof finished.
(save "LemmaC")