;(+ 3 5)
;(+ 2 3)
;(+ 8 13)

;; pp = pretty-print
;; py = parse-type
(py "alpha")
(pp (py "alpha"))
(pp (py "alpha=>alpha"))

(add-var-name "x" (py "alpha"))
(add-var-name "c" (py "alpha"))
(add-var-name "f" (py "alpha=>alpha"))

;; pt = parse-term
(pp (pt "x"))
(pp (pt "f x"))

;; pf = parse-formula
(add-pvar-name "A" (make-arity))
(add-pvar-name "B" (make-arity))
(add-pvar-name "C" (make-arity))
(pp (pf "A -> B"))
(pp (pf "A & B"))
(pp (pf "A ord B"))

(add-pvar-name "d" (make-arity (py "alpha")))
(pp (pf "d x"))
(pp (pf "d (f x)"))
(pp (pf "d x -> d (f x)"))
(pp (pf "ex x (d x -> all x d x)"))

(set-goal (pf "A -> A"))
(assume "u")
(use "u")
(save "Identity")
;; cdp = check-and-display-proof
(cdp)
(cdp "Identity")

(set-goal (pf "A -> B -> A"))
(assume "u" "v")
(use "u")
(cdp)

(set-goal (pf "(A -> B -> C) -> (A -> B) -> A -> C"))
(assume "u" "v" "w")
(use "u")
;; A
(use "w")
;; B
(use "v")
(use "w")
;; qed

(set-goal (pf "A & B -> B & A"))
(assume "u")
(split) ;; /\+
(use "u")
(use "u")
;; qed

(set-goal (pf "(A -> C) -> (B -> C) -> A ord B -> C"))
(assume "u" "v" "w")
(elim "w")
;; A -> C
;;  (use "u")
  (assume "a")
  (use "u")
  (use "a")
;; B -> C
;;  (use "v")
  (assume "b")
  (use "v")
  (use "b")
;; qed

;; 8 
(set-goal (pf "all x (B -> d x) -> (B -> all x d x)"))
(assume "u" "v")
(assume "x")
;;(use-with "u" (pt "x") "v")
(use "u")
(use "v")
(cdp)

(set-goal (pf "all x d x -> ex x d x"))
(assume "u")
(ex-intro (pt "x")) ;; E+
(use-with "u" (pt "x"))
;; (use "u")

;; F = falsity
(set-goal (pf "A ord (A -> F)"))
(use "Stab")
(assume "u")
(use "u")
(intro 1) ;; \/+1
(assume "v")
(use "u")
(intro 0) ;; \/+0
(use "v")

(set-goal (pf "ex x (d x -> all x d x)"))
(use "Stab")
(assume "u")
(use "u")
(ex-intro (pt "c"))
(assume "v" "x")
(use "Stab")
(assume "w")
(use "u")
(ex-intro (pt "x"))
(assume "a")
(use "Efq")
(use "w")
(use "a")

(set-goal (pf "(A -> F) ord (B -> F) -> A & B -> F"))

(set-goal (pf "(ex x d x -> F) -> all x (d x -> F)"))

(set-goal (pf "((A -> B) -> A) -> A"))