---

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


1. fmla : mFOL()
⊢ value-type(mFOL-abstract(fmla) Unit (λn,L. True) (λz.⋅))
BY
{ (SimpleDatatypeInduction (-1)
   THEN RepUR ``mFOL-abstract`` 0
   THEN Try (Fold `mFOL-abstract` 0)
   THEN RepUR ``AbstractFOAtomic FOQuantifier FOConnective FOSatWith let`` 0
   THEN Repeat (AutoSplit)
   THEN Auto
   THEN D 0) }

1
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.⋅))

2
1. isall : 𝔹
2. var : ℤ
3. f3 : mFOL()
4. value-type(mFOL-abstract(f3) Unit (λn,L. True) (λz.⋅))
5. ↑isall
⊢ ∃v:Unit. value-type(mFOL-abstract(f3) Unit (λn,L. True) λz.⋅[var := v])

---

Latex:



1.  fmla  :  mFOL()
\mvdash{}  value-type(mFOL-abstract(fmla)  Unit  (\mlambda{}n,L.  True)  (\mlambda{}z.\mcdot{}))


By

(SimpleDatatypeInduction  (-1)
  THEN  RepUR  ``mFOL-abstract``  0
  THEN  Try  (Fold  `mFOL-abstract`  0)
  THEN  RepUR  ``AbstractFOAtomic  FOQuantifier  FOConnective  FOSatWith  let``  0
  THEN  Repeat  (AutoSplit)
  THEN  Auto
  THEN  D  0)

---

Home Index