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

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

(add-ids (list (list "Even" (make-arity (py "nat")) "nat"))
	 '("Even 0" "InitEven")
	 '("allnc n^(Even n^ -> Even(n^ +2))" "GenEven"))

(add-ids (list (list "Odd" (make-arity (py "nat")) "nat"))
	 '("Odd 1" "InitOdd")
	 '("allnc n^(Odd n^ -> Odd(n^ +2))" "GenOdd"))

(display-pconst "NatDouble")

(set-goal "allnc n^(Odd n^ -> Even(NatDouble n^))")
(assume "n^" "On")
(elim "On")
;; 3,4
(ng)
(use ...)
(use ...)
;; 4
(assume "m^" "Om" "IH")
(ng)
(use ...)
(use ...)
(use ...)
;; Proof finished.

(define proof (current-proof))
(proof-to-expr-with-formulas proof)
(define eterm (proof-to-extracted-term proof))
(pp (rename-variables eterm))