Step
*
1
1
2
2
1
1
1
of Lemma
Girard-theorem
1. Type ∈ Type
2. WFO{i:l}() ∈ Type
3. max-WO{i:l}() ∈ WFO{i:l}()
4. v : WFO{i:l}()
5. p : v order-type-less() v
6. f : ¬(∀i:ℕ. (v order-type-less() v))
⊢ f (λn.p) ∈ False
BY
{ TACTIC:Auto }
Latex:
Latex:
1. Type \mmember{} Type
2. WFO\{i:l\}() \mmember{} Type
3. max-WO\{i:l\}() \mmember{} WFO\{i:l\}()
4. v : WFO\{i:l\}()
5. p : v order-type-less() v
6. f : \mneg{}(\mforall{}i:\mBbbN{}. (v order-type-less() v))
\mvdash{} f (\mlambda{}n.p) \mmember{} False
By
Latex:
TACTIC:Auto
Home
Index