---

Step * 6 1 2 of Lemma PZF_safe_functionality

.....antecedent..... 
1. C : Type
2. var : Atom
3. body : Form(C)
4. ∀vs,ws:Atom List.  (set-equal(Atom;vs;ws) ⇒ PZF_safe(body;vs) = PZF_safe(body;ws))
5. vs : Atom List
6. ws : Atom List
7. set-equal(Atom;vs;ws)
8. ¬(var ∈ ws)
9. ↑PZF_safe(body;[var / ws])
⊢ set-equal(Atom;[var / vs];[var / ws])
BY
{ (RepeatFor 2 (ParallelOp 7) THEN RWO "cons_member" 0 THEN Auto THEN ParallelLast THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  C  :  Type
2.  var  :  Atom
3.  body  :  Form(C)
4.  \mforall{}vs,ws:Atom  List.    (set-equal(Atom;vs;ws)  {}\mRightarrow{}  PZF\_safe(body;vs)  =  PZF\_safe(body;ws))
5.  vs  :  Atom  List
6.  ws  :  Atom  List
7.  set-equal(Atom;vs;ws)
8.  \mneg{}(var  \mmember{}  ws)
9.  \muparrow{}PZF\_safe(body;[var  /  ws])
\mvdash{}  set-equal(Atom;[var  /  vs];[var  /  ws])


By

---

Latex:
(RepeatFor  2  (ParallelOp  7)  THEN  RWO  "cons\_member"  0  THEN  Auto  THEN  ParallelLast  THEN  Auto)

---

Home Index