---

Step * 5 1 1 1 of Lemma FormSafe1_functionality


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. ∀x:Atom. ((x ∈ ws) ⇒ (x ∈ vs))
8. ¬(var ∈ vs)
9. FormSafe1(body) [var / vs]
10. ¬(var ∈ ws)
11. x : Atom
12. (x ∈ ws) ⇒ (x ∈ vs)
⊢ (x ∈ [var / ws]) ⇒ (x ∈ [var / vs])
BY
{ ((RWO "cons_member" 0 THEN Auto) THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  Type
2.  var  :  Atom
3.  body  :  Form(C)
4.  \mforall{}vs,ws:Atom  List.    (l\_subset(Atom;ws;vs)  {}\mRightarrow{}  (FormSafe1(body)  vs)  {}\mRightarrow{}  (FormSafe1(body)  ws))
5.  vs  :  Atom  List
6.  ws  :  Atom  List
7.  \mforall{}x:Atom.  ((x  \mmember{}  ws)  {}\mRightarrow{}  (x  \mmember{}  vs))
8.  \mneg{}(var  \mmember{}  vs)
9.  FormSafe1(body)  [var  /  vs]
10.  \mneg{}(var  \mmember{}  ws)
11.  x  :  Atom
12.  (x  \mmember{}  ws)  {}\mRightarrow{}  (x  \mmember{}  vs)
\mvdash{}  (x  \mmember{}  [var  /  ws])  {}\mRightarrow{}  (x  \mmember{}  [var  /  vs])


By

---

Latex:
((RWO  "cons\_member"  0  THEN  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index