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

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

;;-------------------------
;; Exercice 17 derivations 
;;-------------------------

;; i)
(set-goal "all x(bot -> A x) -> exd x(A x -> bot) ord all x A x -> exd x(A x -> all x A x)")

;; ii)
(set-goal "exd x A x ord all x(A x -> bot) -> exd x((A x -> bot) -> all x (A x -> bot))")

;; iii)
(set-goal "all x(A x ord (A x -> bot)) -> exd x(A x -> all x A x) -> exd x(A x -> bot) ord all x A x")

;; iv)
(set-goal "exd x(A x -> all x A x) -> (all x A x -> bot) -> exd x(A x -> bot)")

;; v)
(set-goal "exd x((A x -> bot) -> all x (A x -> bot)) -> (((exd x ((A x -> bot) -> bot))-> bot) -> bot) -> exd x((A x -> bot) -> bot)")