---

Step * of Lemma FOConnective+_wf

∀[vsa,vsb:ℤ List].
  ∀knd:Atom
    (FOConnective+(knd) ∈ AbstractFOFormula+(vsa)
     ⟶ AbstractFOFormula+(vsb)
     ⟶ AbstractFOFormula+(val-union(IntDeq;vsa;vsb)))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN Unfold `FOConnective+` 0
   THEN RepeatFor 2 ((MemCD THENA Auto))
   THEN Unfold `AbstractFOFormula+` 0
   THEN RepeatFor 3 ((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))
   THEN (Assert a ∈ FOAssignment(vsa,Dom) BY
               (DoSubsume THEN Auto THEN BLemma `subtype_rel_FOAssignment` THEN Auto))
   THEN (GenConclTerm ⌜Dom,S,a +|= x⌝⋅ THENA Auto)
   THEN Thin (-3)
   THEN (Assert a ∈ FOAssignment(vsb,Dom) BY
               (DoSubsume THEN Auto THEN BLemma `subtype_rel_FOAssignment` THEN Auto))
   THEN (GenConclTerm ⌜Dom,S,a +|= y⌝⋅ THENA Auto)
   THEN Thin (-3)
   THEN GenConclTerm ⌜S "false" []⌝⋅
   THEN Auto) }

---

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:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  Unfold  `FOConnective+`  0
  THEN  RepeatFor  2  ((MemCD  THENA  Auto))
  THEN  Unfold  `AbstractFOFormula+`  0
  THEN  RepeatFor  3  ((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))
  THEN  (Assert  a  \mmember{}  FOAssignment(vsa,Dom)  BY
                          (DoSubsume  THEN  Auto  THEN  BLemma  `subtype\_rel\_FOAssignment`  THEN  Auto))
  THEN  (GenConclTerm  \mkleeneopen{}Dom,S,a  +|=  x\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-3)
  THEN  (Assert  a  \mmember{}  FOAssignment(vsb,Dom)  BY
                          (DoSubsume  THEN  Auto  THEN  BLemma  `subtype\_rel\_FOAssignment`  THEN  Auto))
  THEN  (GenConclTerm  \mkleeneopen{}Dom,S,a  +|=  y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-3)
  THEN  GenConclTerm  \mkleeneopen{}S  "false"  []\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index