;; 2013-07-04.  ueb10-loesung.scm.
;; 2013-07-09  revised

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

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

(remove-var-name "n" "m" "k")
(add-var-name "x" "y" "n" "m" "k" (py "nat"))
(add-var-name "v" "w" "u" (py "list nat"))

(add-ids
 (list (list "A" (make-arity (py "list nat") (py "list nat") (py "list nat"))))
 '("allnc v^ A(Nil nat)v^ v^" "InitA")
 '("allnc u^,v^,w^,x^(A u^ v^ w^ -> A(x^ ::u^)v^(x^ ::w^))" "GenA"))

;; (display-idpc "A")

;; version 1: by AllPartial-All and All-AllPartial
(set-goal "all u, v^ exl w^ A u v^ w^")
(use "AllPartial-All")
(assume "u^" "Tu")
(elim "Tu")
(assume "v^")
(intro 0 (pt "v^"))
(intro 0)
(use "All-AllPartial")
(assume "x" "v^" "Tv" "IH" "v^0")
(inst-with-to "IH" (pt "v^0") "IHinst")
(by-assume-with "IHinst" "w^0" "Hyp")
(intro 0 (pt "x ::w^0"))
(use "GenA")
(use "Hyp")

;; version 2: by the computational induction scheme
(set-goal "all u, v^ exl w^ A u v^ w^")
(ind)
; base case
(assume "v^")
(intro 0 (pt "v^"))
(use "InitA")
; step case
(assume "x" "v" "IH" "v^0")
(inst-with-to "IH" (pt "v^0") "IHinst")
(by-assume-with "IHinst" "w^0" "Hyp")
(intro 0 (pt "x::w^0"))
(use "GenA")
(use "Hyp")
;; Proof finished

;; version: without total variables, without computational object variables
(set-goal "allnc u^(TotalList u^ -> allnc v^(TotalList v^ -> exr w^ (TotalList w^ andl A u^ v^ w^)))")
(assume "u^" "Tu")
(elim "Tu")
; base
(assume "v^" "Tv")
(intro 0 (pt "v^"))
(intro 0)
(use "Tv")
(intro 0)
; step
(assume "x^" "Tx" "v^" "Tv" "IH" "v^0" "Tv0")
(inst-with-to "IH" (pt "v^0") "Tv0" "IH0")
(by-assume-with "IH0" "w^0" "IH1")
(intro 0 (pt "x^ ::w^0"))
(intro 0)
(intro 1)
(use "Tx")
(use "IH1")
(intro 1)
(use "IH1")
;finished