;; 2024-04-16.  ueb01.scm

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

;; Aufgabe 1a
(set-goal "(A -> B) -> (B -> bot) -> A -> bot")
;; Für den Beweis sind nur die Befehle
;; (assume …)
;; (use …)
;; nötig. Für Anwendungsbeispiele kann ueb00.scm herangezogen werden.

(proof-to-expr-with-formulas)

;; Aufgabe 1b
(set-goal "((A -> B) -> bot) -> B -> bot")
;; Für den Beweis sind nur die Befehle
;; (assume …)
;; (use …)
;; nötig. Für Anwendungsbeispiele kann ueb00.scm herangezogen werden.

(proof-to-expr-with-formulas)