1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
(add-var-name "x" "y" "z" (py "alpha"))
(add-predconst-name "R" (make-arity (py "alpha") (py "alpha")))
(add-global-assumption "Symm" (pf "all x,y.R x y -> R y x"))
(add-global-assumption "Trans" (pf "all x,y,z.R x y -> R y z -> R x z"))
(set-goal (pf "all x,y.R x y -> R x x"))
(assume "x" "y" 1)
(use "Trans" (pt "y"))
(use 1)
(use "Symm")
(use 1)
(dp)
; ........all x,y,z.R x y -> R y z -> R x z by global assumption Trans
; ........x
; .......all y,z.R x y -> R y z -> R x z by all elim
; .......y
; ......all z.R x y -> R y z -> R x z by all elim
; ......x
; .....R x y -> R y x -> R x x by all elim
; .....R x y by assumption Hyp0
; ....R y x -> R x x by imp elim
; .......all x,y.R x y -> R y x by global assumption Symm
; .......x
; ......all y.R x y -> R y x by all elim
; ......y
; .....R x y -> R y x by all elim
; .....R x y by assumption Hyp0
; ....R y x by imp elim
; ...R x x by imp elim
; ..R x y -> R x x by imp intro Hyp0
; .all y.R x y -> R x x by all intro
; all x,y.R x y -> R x x by all intro
|
