---

Step * 4 of Lemma PZF_safe_functionality


1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs,ws:Atom List.  (set-equal(Atom;vs;ws) ⇒ PZF_safe(left;vs) = PZF_safe(left;ws))
5. ∀vs,ws:Atom List.  (set-equal(Atom;vs;ws) ⇒ PZF_safe(right;vs) = PZF_safe(right;ws))
6. vs : Atom List
7. ws : Atom List
8. set-equal(Atom;vs;ws)
⊢ PZF_safe(left;vs) ∧b PZF_safe(right;vs) = PZF_safe(left;ws) ∧b PZF_safe(right;ws)
BY
{ (EqCD THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(EqCD  THEN  Auto)

---

Home Index