(set! COMMENT-FLAG #f)
(libload "nat.scm")
(set! COMMENT-FLAG #t)
(display-pconst "NatPlus")
;; they are available as theorems, to search for theorems we use (search-about ...).
(search-about 'all "NatPlus" "Comp")
;; partial (or general variables are written with a hat) e.g. n^, the all-quantifier for these vars
;; is allnc
(set-goal "allnc n^(TotalNat n^ -> 0 + n^ eqd n^)")
(assume "n^0" "Tn0")
;; we do induction by elimination of TotalNat n^0
(elim "Tn0")
(simp "NatPlus0CompRule")
(intro 0)
(assume "n^" "Tn" "IH")
(simp "NatPlus1CompRule")
(simp "IH")
(intro 0)
;;ex 33
(display-idpc "TotalNat")
(pp (aconst-to-formula (imp-formulas-to-elim-aconst (pf "TotalNat n^ -> (Pvar nat) n^"))))
(set-goal ...)