;(load "~/minlogsvn/init.scm")
(load "~/temp/ind.scm"); change the path

(add-program-constant "Fib" (py "nat=>nat"))
(add-computation-rules
 "Fib Zero" "Zero"
 "Fib (Succ Zero)" "Succ Zero"
 "Fib(Succ(Succ n))" "Fib n + Fib(Succ n)")

(add-ids (list (list "TotalNat" (make-arity (py "nat")) "algTotalNat"))
	 '("TotalNat 0" "TotalNatZero")
	 '("allnc n^(TotalNat n^ -> TotalNat(Succ n^))" "TotalNatSucc"))

(set-goal "all n(TotalNat (Fib n))")
(use "CVInd")
(cases)
(assume "H")
(intro 0)
(cases)
(assume "H")
(intro 1)
(intro 0)
(assume "n" "IH")
(ng #t)
(use "NatPlusTotal")
(use "IH")
(use "NatLtTrans" (pt "Succ n"))
(use "Truth-Axiom")
(use "Truth-Axiom")
(use "IH")
(use "Truth-Axiom")
(save "FibonacciTotal")