---

Step * 5 1 1 of Lemma FormSafe1_functionality

.....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])
BY
{ RepeatFor 2 (ParallelOp -4) }

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. ∀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])

---

Latex:

---

Latex:
.....antecedent..... 
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{}  l\_subset(Atom;[var  /  ws];[var  /  vs])


By

---

Latex:
RepeatFor  2  (ParallelOp  -4)

---

Home Index