;; (load "~/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"))

(set-goal "allnc n^(Even n^ -> n^ =0 orr exr m^(n^ =m^ +2 andr Even m^))")
(assume ...)
(elim ...)
(intro 0)
(use "Truth")
;;
(assume ...)
(elim ...)
(assume ...)
(intro 1)
(intro 0 (pt "0"))
(simp ...)
(intro 0)
(use "Truth")
(intro 0)
;;
(assume ...)
(by-assume ...)
(intro 1)
(intro 0 (pt "..."))
(intro 0)
(ng)
(use ...)
(intro 1)
(use ...)
(save "LOne")

(set-goal "Even 1 -> F")
(assume ...)
(inst-with-to "LOne" (pt "...") ...)
(elim ...)
(assume ...)
(use ...)
;;
(assume ...)
(by-assume ...)
(use ...)
(save "LTwo")