---

Step * 1 1 of Lemma mFOL-evidence-value-type


1. knd : Atom
2. knd ≠ "or" ∈ Atom 
3. knd ≠ "and" ∈ Atom 
4. left : mFOL()
5. f3 : mFOL()
6. value-type(mFOL-abstract(f3) Unit (λn,L. True) (λz.⋅))
7. value-type(mFOL-abstract(left) Unit (λn,L. True) (λz.⋅))
⊢ ∃:mFOL-abstract(left) Unit (λn,L. True) (λz.⋅). value-type(mFOL-abstract(f3) Unit (λn,L. True) (λz.⋅))
BY
{ xxxAssert ⌜mFOL-abstract(left) Unit (λn,L. True) (λz.⋅)⌝⋅xxx }

1
.....assertion..... 
1. knd : Atom
2. knd ≠ "or" ∈ Atom 
3. knd ≠ "and" ∈ Atom 
4. left : mFOL()
5. f3 : mFOL()
6. value-type(mFOL-abstract(f3) Unit (λn,L. True) (λz.⋅))
7. value-type(mFOL-abstract(left) Unit (λn,L. True) (λz.⋅))
⊢ mFOL-abstract(left) Unit (λn,L. True) (λz.⋅)

2
1. knd : Atom
2. knd ≠ "or" ∈ Atom 
3. knd ≠ "and" ∈ Atom 
4. left : mFOL()
5. f3 : mFOL()
6. value-type(mFOL-abstract(f3) Unit (λn,L. True) (λz.⋅))
7. value-type(mFOL-abstract(left) Unit (λn,L. True) (λz.⋅))
8. mFOL-abstract(left) Unit (λn,L. True) (λz.⋅)
⊢ ∃:mFOL-abstract(left) Unit (λn,L. True) (λz.⋅). value-type(mFOL-abstract(f3) Unit (λn,L. True) (λz.⋅))

---

Latex:

---

Latex:

1.  knd  :  Atom
2.  knd  \mneq{}  "or"  \mmember{}  Atom 
3.  knd  \mneq{}  "and"  \mmember{}  Atom 
4.  left  :  mFOL()
5.  f3  :  mFOL()
6.  value-type(mFOL-abstract(f3)  Unit  (\mlambda{}n,L.  True)  (\mlambda{}z.\mcdot{}))
7.  value-type(mFOL-abstract(left)  Unit  (\mlambda{}n,L.  True)  (\mlambda{}z.\mcdot{}))
\mvdash{}  \mexists{}:mFOL-abstract(left)  Unit  (\mlambda{}n,L.  True)  (\mlambda{}z.\mcdot{}).  value-type(mFOL-abstract(f3)  Unit  (\mlambda{}n,L.  True)  (\mlambda{}z\000C.\mcdot{}))


By

---

Latex:
xxxAssert  \mkleeneopen{}mFOL-abstract(left)  Unit  (\mlambda{}n,L.  True)  (\mlambda{}z.\mcdot{})\mkleeneclose{}\mcdot{}xxx

---

Home Index