Detailed syntax breakdown of Definition df-an
Step | Hyp | Ref
| Expression |
1 | | kt 8 |
. 2
term ⊤ |
2 | | tan 119 |
. . 3
term ∧ |
3 | | hb 3 |
. . . 4
type ∗ |
4 | | vp |
. . . 4
var p |
5 | | vq |
. . . . 5
var q |
6 | 3, 3 | ht 2 |
. . . . . . . 8
type (∗ →
∗) |
7 | 3, 6 | ht 2 |
. . . . . . 7
type (∗ → (∗ →
∗)) |
8 | | vf |
. . . . . . 7
var f |
9 | 3, 4 | tv 1 |
. . . . . . . 8
term p:∗ |
10 | 3, 5 | tv 1 |
. . . . . . . 8
term q:∗ |
11 | 7, 8 | tv 1 |
. . . . . . . 8
term f:(∗ → (∗ →
∗)) |
12 | 9, 10, 11 | kbr 9 |
. . . . . . 7
term [p:∗f:(∗ → (∗ →
∗))q:∗] |
13 | 7, 8, 12 | kl 6 |
. . . . . 6
term λf:(∗ → (∗ → ∗))
[p:∗f:(∗ → (∗ →
∗))q:∗] |
14 | 1, 1, 11 | kbr 9 |
. . . . . . 7
term [⊤f:(∗ → (∗ →
∗))⊤] |
15 | 7, 8, 14 | kl 6 |
. . . . . 6
term λf:(∗ → (∗ → ∗))
[⊤f:(∗ → (∗
→ ∗))⊤] |
16 | | ke 7 |
. . . . . 6
term = |
17 | 13, 15, 16 | kbr 9 |
. . . . 5
term [λf:(∗ → (∗ → ∗))
[p:∗f:(∗ → (∗ →
∗))q:∗] =
λf:(∗ → (∗
→ ∗)) [⊤f:(∗
→ (∗ → ∗))⊤]] |
18 | 3, 5, 17 | kl 6 |
. . . 4
term λq:∗ [λf:(∗ → (∗ → ∗))
[p:∗f:(∗ → (∗ →
∗))q:∗] =
λf:(∗ → (∗
→ ∗)) [⊤f:(∗
→ (∗ → ∗))⊤]] |
19 | 3, 4, 18 | kl 6 |
. . 3
term λp:∗ λq:∗ [λf:(∗ → (∗ → ∗))
[p:∗f:(∗ → (∗ →
∗))q:∗] =
λf:(∗ → (∗
→ ∗)) [⊤f:(∗
→ (∗ → ∗))⊤]] |
20 | 2, 19, 16 | kbr 9 |
. 2
term [ ∧ =
λp:∗
λq:∗
[λf:(∗ →
(∗ → ∗)) [p:∗f:(∗ → (∗ →
∗))q:∗] =
λf:(∗ → (∗
→ ∗)) [⊤f:(∗
→ (∗ → ∗))⊤]]] |
21 | 1, 20 | wffMMJ2 11 |
1
wff ⊤⊧[ ∧ = λp:∗ λq:∗ [λf:(∗ → (∗ → ∗))
[p:∗f:(∗ → (∗ →
∗))q:∗] =
λf:(∗ → (∗
→ ∗)) [⊤f:(∗
→ (∗ → ∗))⊤]]] |