---

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


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 
BY
{ (RWO "val-union-l-union" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  Dom  :  Type
2.  S  :  FOStruct+\{i:l\}(Dom)
3.  knd  :  Atom
4.  left  :  mFOL()
5.  right  :  mFOL()
6.  \mforall{}a:FOAssignment(mFOL-freevars(left),Dom).  ((S  "false"  [])  \msubseteq{}r  (FOL-abstract(left)  Dom  S  a))
7.  \mforall{}a:FOAssignment(mFOL-freevars(right),Dom).  ((S  "false"  [])  \msubseteq{}r  (FOL-abstract(right)  Dom  S  a))
8.  a  :  FOAssignment(val-union(IntDeq;mFOL-freevars(left);mFOL-freevars(right)),Dom)
\mvdash{}  (S  "false"  [])  \msubseteq{}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  \mwedge{}  q)  \mcup{}  (S  "false"  [])
                                          if  knd  =a  "or"  then  (p  \mvee{}  q)  \mcup{}  (S  "false"  [])
                                          else  (p  {}\mRightarrow{}  q)  \mcup{}  (S  "false"  [])
                                          fi 


By

---

Latex:
(RWO  "val-union-l-union"  (-1)  THEN  Auto)

---

Home Index