---

Step * 5 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. l_subset(Atom;ws;vs)
8. ¬(var ∈ vs)
9. FormSafe1(body) [var / vs]
10. ¬(var ∈ ws)
⊢ FormSafe1(body) [var / ws]
BY
{ (InstHyp [⌜[var / vs]⌝;⌜[var / ws]⌝] 4⋅ THEN Auto) }

1
.....antecedent..... 
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)
⊢ l_subset(Atom;[var / ws];[var / vs])

---

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.  l\_subset(Atom;ws;vs)
8.  \mneg{}(var  \mmember{}  vs)
9.  FormSafe1(body)  [var  /  vs]
10.  \mneg{}(var  \mmember{}  ws)
\mvdash{}  FormSafe1(body)  [var  /  ws]


By

---

Latex:
(InstHyp  [\mkleeneopen{}[var  /  vs]\mkleeneclose{};\mkleeneopen{}[var  /  ws]\mkleeneclose{}]  4\mcdot{}  THEN  Auto)

---

Home Index