---

Step * 5 of Lemma PZF_safe_functionality


1. C : Type
2. body : Form(C)
3. ∀vs,ws:Atom List.  (set-equal(Atom;vs;ws) ⇒ PZF_safe(body;vs) = PZF_safe(body;ws))
4. vs : Atom List
5. ws : Atom List
6. set-equal(Atom;vs;ws)
⊢ null(vs) ∧b PZF_safe(body;[]) = null(ws) ∧b PZF_safe(body;[])
BY
{ ((EqCD THEN Auto)
   THEN (BLemma `iff_imp_equal_bool` THENA Auto)
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN (RWO "nil-iff-no-member" 0 THEN Auto)
   THEN D -2 With ⌜x⌝ 
   THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  Type
2.  body  :  Form(C)
3.  \mforall{}vs,ws:Atom  List.    (set-equal(Atom;vs;ws)  {}\mRightarrow{}  PZF\_safe(body;vs)  =  PZF\_safe(body;ws))
4.  vs  :  Atom  List
5.  ws  :  Atom  List
6.  set-equal(Atom;vs;ws)
\mvdash{}  null(vs)  \mwedge{}\msubb{}  PZF\_safe(body;[])  =  null(ws)  \mwedge{}\msubb{}  PZF\_safe(body;[])


By

---

Latex:
((EqCD  THEN  Auto)
  THEN  (BLemma  `iff\_imp\_equal\_bool`  THENA  Auto)
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  (RWO  "nil-iff-no-member"  0  THEN  Auto)
  THEN  D  -2  With  \mkleeneopen{}x\mkleeneclose{} 
  THEN  Auto)

---

Home Index