---

Step * of Lemma PZF_safe_functionality

∀[C:Type]. ∀[phi:Form(C)]. ∀[vs,ws:Atom List].  PZF_safe(phi;vs) = PZF_safe(phi;ws) supposing set-equal(Atom;vs;ws)
BY
{ ((Auto THEN RepeatFor 4 (MoveToConcl  (-1)))
   THEN (BLemma `Form-induction` THENW Auto)
        THEN (Intros
              THEN RepUR ``PZF_safe FormSafe2`` 0
              THEN (Try (Fold `FormSafe2` 0) THEN Try (Fold `PZF_safe` 0))
              THEN Try ((Fold `member` 0 THEN Auto)))
   ) }

1
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)
⊢ null(vs)
  ∨blet x = hd(vs) in
        null(vs-[x])
        ∧b ((FormVar?(left) ∧b FormVar-name(left) =a x ∧b (¬bx ∈b FormFvs(right)))
           ∨b(FormVar?(right) ∧b FormVar-name(right) =a x ∧b (¬bx ∈b FormFvs(left)))) 
= null(ws)
  ∨blet x = hd(ws) in
        null(ws-[x])
        ∧b ((FormVar?(left) ∧b FormVar-name(left) =a x ∧b (¬bx ∈b FormFvs(right)))
           ∨b(FormVar?(right) ∧b FormVar-name(right) =a x ∧b (¬bx ∈b FormFvs(left))))

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. ws : Atom List
8. set-equal(Atom;vs;ws)
⊢ null(vs)
  ∨blet x = hd(vs) in
        null(vs-[x])
        ∧b FormVar?(element)
        ∧b FormVar-name(element) =a x
        ∧b ((FormVar?(set) ∧b FormVar-name(set) =a x) ∨b(¬bx ∈b FormFvs(set))) 
= null(ws)
  ∨blet x = hd(ws) in
        null(ws-[x])
        ∧b FormVar?(element)
        ∧b FormVar-name(element) =a x
        ∧b ((FormVar?(set) ∧b FormVar-name(set) =a x) ∨b(¬bx ∈b FormFvs(set)))

3
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)
⊢ eval as = FormFvs(left) in
  eval bs = FormFvs(right) in
    eval theta = vs-bs in
    PZF_safe(left;theta) ∧b PZF_safe(right;vs-theta)
    ∨beval phi = vs-as in
      PZF_safe(left;vs-phi) ∧b PZF_safe(right;phi) 
= eval as = FormFvs(left) in
  eval bs = FormFvs(right) in
    eval theta = ws-bs in
    PZF_safe(left;theta) ∧b PZF_safe(right;ws-theta)
    ∨beval phi = ws-as in
      PZF_safe(left;ws-phi) ∧b PZF_safe(right;phi)

4
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)

5
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;[])

6
1. C : Type
2. var : Atom
3. body : Form(C)
4. ∀vs,ws:Atom List.  (set-equal(Atom;vs;ws) ⇒ PZF_safe(body;vs) = PZF_safe(body;ws))
5. vs : Atom List
6. ws : Atom List
7. set-equal(Atom;vs;ws)
⊢ (¬bvar ∈b vs) ∧b PZF_safe(body;[var / vs]) = (¬bvar ∈b ws) ∧b PZF_safe(body;[var / ws])

---

Latex:

---

Latex:
\mforall{}[C:Type].  \mforall{}[phi:Form(C)].  \mforall{}[vs,ws:Atom  List].
    PZF\_safe(phi;vs)  =  PZF\_safe(phi;ws)  supposing  set-equal(Atom;vs;ws)


By

---

Latex:
((Auto  THEN  RepeatFor  4  (MoveToConcl    (-1)))
  THEN  (BLemma  `Form-induction`  THENW  Auto)
            THEN  (Intros
                        THEN  RepUR  ``PZF\_safe  FormSafe2``  0
                        THEN  (Try  (Fold  `FormSafe2`  0)  THEN  Try  (Fold  `PZF\_safe`  0))
                        THEN  Try  ((Fold  `member`  0  THEN  Auto)))
  )

---

Home Index