---

Step * 2 1 of Lemma PZF_safe_functionality

.....equality..... 
1. C : Type
2. element : Form(C)
3. set : Form(C)
4. ∀vs,ws:Atom List.  (set-equal(Atom;vs;ws) ⇒ PZF_safe(element;vs) = PZF_safe(element;ws))
5. ∀vs,ws:Atom List.  (set-equal(Atom;vs;ws) ⇒ PZF_safe(set;vs) = PZF_safe(set;ws))
6. vs : Atom List
7. ¬(vs = [] ∈ (Atom List))
8. ws : Atom List
9. set-equal(Atom;vs;ws)
10. null(ws) ~ ff
⊢ null(ws-[hd(ws)]) ~ null(vs-[hd(vs)])
BY
{ (Auto
   THEN BLemma `iff_imp_equal_bool`
   THEN Auto
   THEN (RW assert_pushdownC (-1) THENA Auto)
   THEN (RWO "nil-iff-no-member" (-1) THENA Auto)
   THEN (RWO "nil-iff-no-member" 0 THENA Auto)
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN (RWW "member-list-diff member_singleton" (-1) THENA Auto)
   THEN (InstHyp [⌜x⌝] (-3)⋅ THENA Auto)
   THEN (RWW "member-list-diff member_singleton" (-1) THENA Auto)
   THEN (Assert ¬(hd(ws) = hd(vs) ∈ Atom) BY
               (ParallelLast THEN Auto))) }

1
1. C : Type
2. element : Form(C)
3. set : Form(C)
4. ∀vs,ws:Atom List.  (set-equal(Atom;vs;ws) ⇒ PZF_safe(element;vs) = PZF_safe(element;ws))
5. ∀vs,ws:Atom List.  (set-equal(Atom;vs;ws) ⇒ PZF_safe(set;vs) = PZF_safe(set;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

2
1. C : Type
2. element : Form(C)
3. set : Form(C)
4. ∀vs,ws:Atom List.  (set-equal(Atom;vs;ws) ⇒ PZF_safe(element;vs) = PZF_safe(element;ws))
5. ∀vs,ws:Atom List.  (set-equal(Atom;vs;ws) ⇒ PZF_safe(set;vs) = PZF_safe(set;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 ∈ vs-[hd(vs)]))
12. x : Atom
13. (x ∈ ws) ∧ (¬(x = hd(ws) ∈ Atom))
14. ¬((x ∈ vs) ∧ (¬(x = hd(vs) ∈ Atom)))
15. ¬(hd(ws) = hd(vs) ∈ Atom)
⊢ False

---

Latex:

---

Latex:
.....equality..... 
1.  C  :  Type
2.  element  :  Form(C)
3.  set  :  Form(C)
4.  \mforall{}vs,ws:Atom  List.    (set-equal(Atom;vs;ws)  {}\mRightarrow{}  PZF\_safe(element;vs)  =  PZF\_safe(element;ws))
5.  \mforall{}vs,ws:Atom  List.    (set-equal(Atom;vs;ws)  {}\mRightarrow{}  PZF\_safe(set;vs)  =  PZF\_safe(set;ws))
6.  vs  :  Atom  List
7.  \mneg{}(vs  =  [])
8.  ws  :  Atom  List
9.  set-equal(Atom;vs;ws)
10.  null(ws)  \msim{}  ff
\mvdash{}  null(ws-[hd(ws)])  \msim{}  null(vs-[hd(vs)])


By

---

Latex:
(Auto
  THEN  BLemma  `iff\_imp\_equal\_bool`
  THEN  Auto
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  (RWO  "nil-iff-no-member"  (-1)  THENA  Auto)
  THEN  (RWO  "nil-iff-no-member"  0  THENA  Auto)
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  (RWW  "member-list-diff  member\_singleton"  (-1)  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  (RWW  "member-list-diff  member\_singleton"  (-1)  THENA  Auto)
  THEN  (Assert  \mneg{}(hd(ws)  =  hd(vs))  BY
                          (ParallelLast  THEN  Auto)))

---

Home Index