---

Step * of Lemma FOConnective_wf

∀[vsa,vsb:ℤ List].
  ∀knd:Atom
    (FOConnective(knd) ∈ AbstractFOFormula(vsa)
     ⟶ AbstractFOFormula(vsb)
     ⟶ AbstractFOFormula(val-union(IntDeq;vsa;vsb)))
BY
{ (Auto
   THEN Unfold `AbstractFOFormula` 0
   THEN Unfold `FOConnective` 0
   THEN RepeatFor 5 ((MemCD THENA Auto))
   THEN (Assert vsa ⊆ val-union(IntDeq;vsa;vsb) ∧ vsb ⊆ val-union(IntDeq;vsa;vsb) BY
               (RWO "val-union-l-union" 0 THEN Auto))) }

1
1. vsa : ℤ List
2. vsb : ℤ List
3. knd : Atom
4. x : Dom:Type ⟶ S:FOStruct(Dom) ⟶ FOAssignment(vsa,Dom) ⟶ ℙ
5. y : Dom:Type ⟶ S:FOStruct(Dom) ⟶ FOAssignment(vsb,Dom) ⟶ ℙ
6. Dom : Type
7. S : FOStruct(Dom)
8. a : FOAssignment(val-union(IntDeq;vsa;vsb),Dom)
9. vsa ⊆ val-union(IntDeq;vsa;vsb) ∧ vsb ⊆ val-union(IntDeq;vsa;vsb)
⊢ let p = Dom,S,a |= x in
   let q = Dom,S,a |= y in
   if knd =a "and" then p ∧ q
   if knd =a "or" then p ∨ q
   else p ⇒ q
   fi  ∈ ℙ

---

Latex:

---

Latex:
\mforall{}[vsa,vsb:\mBbbZ{}  List].
    \mforall{}knd:Atom
        (FOConnective(knd)  \mmember{}  AbstractFOFormula(vsa)
          {}\mrightarrow{}  AbstractFOFormula(vsb)
          {}\mrightarrow{}  AbstractFOFormula(val-union(IntDeq;vsa;vsb)))


By

---

Latex:
(Auto
  THEN  Unfold  `AbstractFOFormula`  0
  THEN  Unfold  `FOConnective`  0
  THEN  RepeatFor  5  ((MemCD  THENA  Auto))
  THEN  (Assert  vsa  \msubseteq{}  val-union(IntDeq;vsa;vsb)  \mwedge{}  vsb  \msubseteq{}  val-union(IntDeq;vsa;vsb)  BY
                          (RWO  "val-union-l-union"  0  THEN  Auto)))

---

Home Index