---

Step * 1 1 1 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. ¬(vs = [] ∈ (Atom List))
8. ws : Atom List
9. set-equal(Atom;vs;ws)
10. null(ws) ~ ff
11. ∀[x:Atom]. (¬(x ∈ ws-[hd(ws)]))
12. x : Atom
13. (x ∈ vs) ∧ (¬(x = hd(vs) ∈ Atom))
14. ¬((x ∈ ws) ∧ (¬(x = hd(ws) ∈ Atom)))
15. ¬(hd(ws) = hd(vs) ∈ Atom)
⊢ False
BY
{ ((D -5 With ⌜hd(vs)⌝  THENA Auto) THEN D -1 THEN RWW "member-list-diff member_singleton" 0 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.  \mneg{}(vs  =  [])
8.  ws  :  Atom  List
9.  set-equal(Atom;vs;ws)
10.  null(ws)  \msim{}  ff
11.  \mforall{}[x:Atom].  (\mneg{}(x  \mmember{}  ws-[hd(ws)]))
12.  x  :  Atom
13.  (x  \mmember{}  vs)  \mwedge{}  (\mneg{}(x  =  hd(vs)))
14.  \mneg{}((x  \mmember{}  ws)  \mwedge{}  (\mneg{}(x  =  hd(ws))))
15.  \mneg{}(hd(ws)  =  hd(vs))
\mvdash{}  False


By

---

Latex:
((D  -5  With  \mkleeneopen{}hd(vs)\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  RWW  "member-list-diff  member\_singleton"  0
  THEN  Auto)

---

Home Index