---

Step * 3 of Lemma FOStruct-false-subtype-evidence


1. Dom : Type
2. S : FOStruct+{i:l}(Dom)
3. isall : 𝔹
4. var : ℤ
5. body : mFOL()
6. ∀a:FOAssignment(mFOL-freevars(body),Dom). ((S "false" []) ⊆r (FOL-abstract(body) Dom S a))
7. a : FOAssignment(filter(λx.(¬b(x =z var));mFOL-freevars(body)),Dom)
⊢ (S "false" []) ⊆r if isall
    then (∀v:Dom. (FOL-abstract(body) Dom S a[var := v])) ⋃ (S "false" [])
    else (∃v:Dom. (FOL-abstract(body) Dom S a[var := v])) ⋃ (S "false" [])
    fi 
BY
{ (BoolCase ⌜isall⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  Dom  :  Type
2.  S  :  FOStruct+\{i:l\}(Dom)
3.  isall  :  \mBbbB{}
4.  var  :  \mBbbZ{}
5.  body  :  mFOL()
6.  \mforall{}a:FOAssignment(mFOL-freevars(body),Dom).  ((S  "false"  [])  \msubseteq{}r  (FOL-abstract(body)  Dom  S  a))
7.  a  :  FOAssignment(filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  var));mFOL-freevars(body)),Dom)
\mvdash{}  (S  "false"  [])  \msubseteq{}r  if  isall
        then  (\mforall{}v:Dom.  (FOL-abstract(body)  Dom  S  a[var  :=  v]))  \mcup{}  (S  "false"  [])
        else  (\mexists{}v:Dom.  (FOL-abstract(body)  Dom  S  a[var  :=  v]))  \mcup{}  (S  "false"  [])
        fi 


By

---

Latex:
(BoolCase  \mkleeneopen{}isall\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index