---

Step * of Lemma FOStruct-false-subtype-evidence

∀Dom:Type. ∀S:FOStruct+{i:l}(Dom). ∀fmla:mFOL(). ∀a:FOAssignment(mFOL-freevars(fmla),Dom).
  ((S "false" []) ⊆r Dom,S,a +|= FOL-abstract(fmla))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (BLemma `mFOL-induction`  THENA Auto)
   THEN RepUR ``FOL-abstract mFOL-freevars`` 0
   THEN (Try (Fold `FOL-abstract` 0) THEN Try (Fold `mFOL-freevars` 0))
   THEN RepUR ``AbstractFOAtomic+ FOConnective+ FOQuantifier+ FOSatWith+`` 0
   THEN (UnivCD THENA Auto)) }

1
1. Dom : Type
2. S : FOStruct+{i:l}(Dom)
3. name : Atom
4. vars : ℤ List
5. a : FOAssignment(remove-repeats(IntDeq;vars),Dom)
⊢ (S "false" []) ⊆r ((S name map(a;vars)) ⋃ (S "false" []))

2
1. Dom : Type
2. S : FOStruct+{i:l}(Dom)
3. knd : Atom
4. left : mFOL()
5. right : mFOL()
6. ∀a:FOAssignment(mFOL-freevars(left),Dom). ((S "false" []) ⊆r (FOL-abstract(left) Dom S a))
7. ∀a:FOAssignment(mFOL-freevars(right),Dom). ((S "false" []) ⊆r (FOL-abstract(right) Dom S a))
8. a : FOAssignment(val-union(IntDeq;mFOL-freevars(left);mFOL-freevars(right)),Dom)
⊢ (S "false" []) ⊆r let p = FOL-abstract(left) Dom S a in
                     let q = FOL-abstract(right) Dom S a in
                     if knd =a "and" then (p ∧ q) ⋃ (S "false" [])
                     if knd =a "or" then (p ∨ q) ⋃ (S "false" [])
                     else (p ⇒ q) ⋃ (S "false" [])
                     fi 

3
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 

---

Latex:

---

Latex:
\mforall{}Dom:Type.  \mforall{}S:FOStruct+\{i:l\}(Dom).  \mforall{}fmla:mFOL().  \mforall{}a:FOAssignment(mFOL-freevars(fmla),Dom).
    ((S  "false"  [])  \msubseteq{}r  Dom,S,a  +|=  FOL-abstract(fmla))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (BLemma  `mFOL-induction`    THENA  Auto)
  THEN  RepUR  ``FOL-abstract  mFOL-freevars``  0
  THEN  (Try  (Fold  `FOL-abstract`  0)  THEN  Try  (Fold  `mFOL-freevars`  0))
  THEN  RepUR  ``AbstractFOAtomic+  FOConnective+  FOQuantifier+  FOSatWith+``  0
  THEN  (UnivCD  THENA  Auto))

---

Home Index