---

Step * 5 of Lemma FormSafe1_functionality


1. C : Type
⊢ ∀var:Atom. ∀body:Form(C).
    ((∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(body) vs) ⇒ (FormSafe1(body) ws)))
    ⇒ (∀vs,ws:Atom List.
          (l_subset(Atom;ws;vs)
          ⇒ ((¬(var ∈ vs)) ∧ (FormSafe1(body) [var / vs]))
          ⇒ ((¬(var ∈ ws)) ∧ (FormSafe1(body) [var / ws])))))
BY
{ Auto }

1
1. C : Type
2. var : Atom
3. body : Form(C)
4. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(body) vs) ⇒ (FormSafe1(body) ws))
5. vs : Atom List
6. ws : Atom List
7. l_subset(Atom;ws;vs)
8. ¬(var ∈ vs)
9. FormSafe1(body) [var / vs]
10. ¬(var ∈ ws)
⊢ FormSafe1(body) [var / ws]

---

Latex:

---

Latex:

1.  C  :  Type
\mvdash{}  \mforall{}var:Atom.  \mforall{}body:Form(C).
        ((\mforall{}vs,ws:Atom  List.    (l\_subset(Atom;ws;vs)  {}\mRightarrow{}  (FormSafe1(body)  vs)  {}\mRightarrow{}  (FormSafe1(body)  ws)))
        {}\mRightarrow{}  (\mforall{}vs,ws:Atom  List.
                    (l\_subset(Atom;ws;vs)
                    {}\mRightarrow{}  ((\mneg{}(var  \mmember{}  vs))  \mwedge{}  (FormSafe1(body)  [var  /  vs]))
                    {}\mRightarrow{}  ((\mneg{}(var  \mmember{}  ws))  \mwedge{}  (FormSafe1(body)  [var  /  ws])))))


By

---

Latex:
Auto

---

Home Index