;; 2022-04-28.  ueb01.scm

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

(add-pvar-name "A" "B" "C" (make-arity))

;; Aufgabe 1/a
(set-goal "A -> B -> A")
(assume "u" "v")
(use ...)

(proof-to-expr-with-formulas)

;; Aufgabe 1/b
(set-goal "(A -> B -> C) -> B -> A -> C")
(assume "u" "v" "w")
(use ...)
(use ...)
(use ...)

(proof-to-expr-with-formulas)

;; Aufgabe 1/c
(set-goal
 "(((A -> B) -> bot) -> bot) -> ((A -> bot) -> bot) -> (B -> bot) -> bot")
(assume "u" "v" "w")
(use "u")
(assume "u1")
(use ...)
(assume ...)
(use ...)
(use ...)
(use ...)

(proof-to-expr-with-formulas)

;; Aufgabe 1/d
(set-goal "(bot -> B) ->
 (((A -> bot) -> bot) -> (B -> bot) -> bot) ->
 (((A -> B) -> bot) -> bot) ")
(assume "EfB" "u" "v")
(prop)

(proof-to-expr-with-formulas)

(set-goal "(bot -> B) ->
 (((A -> bot) -> bot) -> (B -> bot) -> bot) ->
 (((A -> B) -> bot) -> bot) ")
(assume "EfB" "u" "v")
(use "u")
(assume "u0")
(use ...)
(assume ...)
(use ...)
(use ...)
(use ...)
(assume ...)
(use ...)
(assume ...)
(use ...)

(proof-to-expr-with-formulas)

;; Aufgabe 2/a

(add-var-name "x" "y" (py "alpha"))
(add-pvar-name "P" (make-arity (py "alpha")))

(set-goal "all x(A -> P x) -> A -> all x P x")
(assume "u" "v" "x")
(use ...)
(use ...)

(proof-to-expr-with-formulas)

;; Aufgabe 2/b

(set-goal "((all x P x -> bot) -> bot) -> all x((P x -> bot) -> bot)")
(assume "u" "x" "v")
(use ...)
(assume ...)
(use ...)
(use ...)

(proof-to-expr-with-formulas)

;; Aufgabe 4/a

(pp (pf "excl x P x"))
(pp (unfold-formula (pf "excl x P x")))
(pp (fold-formula (pf "all x(P x -> bot) -> bot")))
(pp (fold-formula (pf "all x(P1 x -> P2 x -> bot) -> bot")))
(pp (unfold-formula (pf "excl x(P1 x ! P2 x)")))

(add-pvar-name "R" (make-arity (py "alpha") (py "alpha")))

(pp (unfold-formula (pf "excl x,y R x y")))
(pp (unfold-formula (pf "excl x excl y R x y")))

(set-goal "excl x,y R x y -> excl x excl y R x y")
(assume "u" "v")
(use "u")
(assume "x" "y" "Rxy")
(use "v" (pt "x"))
(assume ...)
(use ... ...)
(use ...)

(proof-to-expr-with-formulas)

;; Aufgabe 4/b

(set-goal "excl x excl y R x y -> excl x,y R x y")
(assume "u" "v")
(use ...)
(assume ...)
(use ...)
(use ...)

(proof-to-expr-with-formulas)