---

Step * 6 of Lemma PZF_safe_functionality


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)
⊢ (¬bvar ∈b vs) ∧b PZF_safe(body;[var / vs]) = (¬bvar ∈b ws) ∧b PZF_safe(body;[var / ws])
BY
{ ((BLemma `iff_imp_equal_bool` THENA Auto) THEN (RW assert_pushdownC 0 THENA Auto)) }

1
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)
⊢ (¬(var ∈ vs)) ∧ (↑PZF_safe(body;[var / vs])) ⇐⇒ (¬(var ∈ ws)) ∧ (↑PZF_safe(body;[var / ws]))

---

Latex:

---

Latex:

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)
\mvdash{}  (\mneg{}\msubb{}var  \mmember{}\msubb{}  vs)  \mwedge{}\msubb{}  PZF\_safe(body;[var  /  vs])  =  (\mneg{}\msubb{}var  \mmember{}\msubb{}  ws)  \mwedge{}\msubb{}  PZF\_safe(body;[var  /  ws])


By

---

Latex:
((BLemma  `iff\_imp\_equal\_bool`  THENA  Auto)  THEN  (RW  assert\_pushdownC  0  THENA  Auto))

---

Home Index