-
Notifications
You must be signed in to change notification settings - Fork 0
/
test.atm
27 lines (27 loc) · 812 Bytes
/
test.atm
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
jdg wff
jdg |-
opr -> 2
opr -. 1
axm { wff a => wff (-. a) }: wn
axm { wff a, wff b => wff (a -> b) }: wi
axm { wff a, wff b, |- a, |- (a -> b) => |- b }: ax-mp
axm { wff a, wff b => |- (a -> (b -> a)) }: ax-1
axm { wff a, wff b, wff c => |- ((a -> (b -> c)) -> ((a -> b) -> (a -> c))) }: ax-2
axm { wff a, wff b => |- (((-. a) -> (-. b)) -> (b -> a)) }: ax-3
cmb ax-mp(1) <- wi
cmb $(3) <- wi
cmb $(1) <- wi
cmb $(1) <- wi
cmb $(3) <- wi
cmb $(9) <- ax-2 { wff a, wff b, wff c, |- (a -> (b -> c)) => |- ((a -> b) -> (a -> c)) }: a2i
cmb ax-mp(1) <- wi
cmb $(1) <- wi
cmb $(6) <- a2i { wff a, wff b, wff c, |- (a -> b), |- (a -> (b -> c)) => |- (a -> c) }: mpd
smp ax-1 (a ~ b)
cmb mpd(2) <- wi
cmb $(5) <- 1
cmb ax-1(2) <- wi
smp $ (a ~ b)
smp $ (a ~ b)
smp $ (a ~ b)
cmb 3(3) <- $ { wff a => |- (a -> a) }: id