---

Step * 1 2 of Lemma PZF_safe_functionality

.....equality..... 
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. vs-[hd(vs)] = [] ∈ (Atom List)
⊢ hd(ws) ~ hd(vs)
BY
{ (Auto
   THEN SupposeNot
   THEN Auto
   THEN (Assert (hd(ws) ∈ vs-[hd(vs)]) BY
               (GenListD 0 THEN Auto))
   THEN RWO "-3" (-1)
   THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
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.  vs-[hd(vs)]  =  []
\mvdash{}  hd(ws)  \msim{}  hd(vs)


By

---

Latex:
(Auto
  THEN  SupposeNot
  THEN  Auto
  THEN  (Assert  (hd(ws)  \mmember{}  vs-[hd(vs)])  BY
                          (GenListD  0  THEN  Auto))
  THEN  RWO  "-3"  (-1)
  THEN  Auto)

---

Home Index