(add-pvar-name "A" "B" "C" (make-arity))
;;Preparation:
;;Disjunction and Conjunction
;;Disjunction is written 'ord' (the 'd' will make more sense later)
;;ord is given by 2 intro rules
(set-goal "A -> A ord B")
(assume "u")
;;here
(intro 0)
(use "u")
(set-goal "B -> A ord B")
(assume "u")
;;and here
(intro 1)
(use "u")
;;and an elimination rule
(set-goal "A ord B -> (A -> C) -> (B -> C) -> C")
(assume "Disj" "ImpI" "ImpII")
(elim "Disj")
;; ?_3:A -> C
;; ?_4:B -> C
(use "ImpI")
(use "ImpII")
;;(Conjunction) 'andd' has one intro
(set-goal "A -> B -> A andd B")
(assume "u" "v")
(intro 0)
;; can also use (split) instead
(use "u")
(use "v")
;;and an elim
(set-goal "A andd B -> (A -> B -> C) -> C")
(assume "Conj" "Hyp")
(elim "Conj")
(use "Hyp")
;; Now the exercises
;;Ex5/i
(set-goal "((A ord B) -> C) -> ((A -> C) andd (B -> C))")
;; ...
(set-goal "((A -> C) andd (B -> C)) -> ((A ord B) -> C)")
;; ...
;;Ex5/ii
;; ...