---

Step * 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. 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))))
BY
{ ((Assert null(ws) ~ null(vs) BY
          (Auto
           THEN (BLemma `iff_imp_equal_bool` THENA Auto)
           THEN (RW assert_pushdownC 0 THENA Auto)
           THEN (RWO "nil-iff-no-member" 0 THEN Auto)
           THEN D -2 With ⌜x⌝ 
           THEN Auto))
   THEN HypSubst'  (-1) 0
   THEN RepUR ``let`` 0
   THEN (BoolCase ⌜null(vs)⌝⋅ THENA Auto)
   THEN Try ((Fold `member` 0 THEN Auto))
   THEN (Subst' null(ws-[hd(ws)]) ~ null(vs-[hd(vs)]) 0
   THENM ((BoolCase ⌜null(vs-[hd(vs)])⌝⋅ THENA Auto)
          THEN Try ((Fold `member` 0 THEN Auto))
          THEN (Subst' hd(ws) ~ hd(vs) 0 THENM Auto))
   )) }

1
.....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
⊢ null(ws-[hd(ws)]) ~ null(vs-[hd(vs)])

2
.....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)

---

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{}  null(vs)
    \mvee{}\msubb{}let  x  =  hd(vs)  in
                null(vs-[x])
                \mwedge{}\msubb{}  ((FormVar?(left)  \mwedge{}\msubb{}  FormVar-name(left)  =a  x  \mwedge{}\msubb{}  (\mneg{}\msubb{}x  \mmember{}\msubb{}  FormFvs(right)))
                      \mvee{}\msubb{}(FormVar?(right)  \mwedge{}\msubb{}  FormVar-name(right)  =a  x  \mwedge{}\msubb{}  (\mneg{}\msubb{}x  \mmember{}\msubb{}  FormFvs(left)))) 
=  null(ws)
    \mvee{}\msubb{}let  x  =  hd(ws)  in
                null(ws-[x])
                \mwedge{}\msubb{}  ((FormVar?(left)  \mwedge{}\msubb{}  FormVar-name(left)  =a  x  \mwedge{}\msubb{}  (\mneg{}\msubb{}x  \mmember{}\msubb{}  FormFvs(right)))
                      \mvee{}\msubb{}(FormVar?(right)  \mwedge{}\msubb{}  FormVar-name(right)  =a  x  \mwedge{}\msubb{}  (\mneg{}\msubb{}x  \mmember{}\msubb{}  FormFvs(left))))


By

---

Latex:
((Assert  null(ws)  \msim{}  null(vs)  BY
                (Auto
                  THEN  (BLemma  `iff\_imp\_equal\_bool`  THENA  Auto)
                  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
                  THEN  (RWO  "nil-iff-no-member"  0  THEN  Auto)
                  THEN  D  -2  With  \mkleeneopen{}x\mkleeneclose{} 
                  THEN  Auto))
  THEN  HypSubst'    (-1)  0
  THEN  RepUR  ``let``  0
  THEN  (BoolCase  \mkleeneopen{}null(vs)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((Fold  `member`  0  THEN  Auto))
  THEN  (Subst'  null(ws-[hd(ws)])  \msim{}  null(vs-[hd(vs)])  0
  THENM  ((BoolCase  \mkleeneopen{}null(vs-[hd(vs)])\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  Try  ((Fold  `member`  0  THEN  Auto))
                THEN  (Subst'  hd(ws)  \msim{}  hd(vs)  0  THENM  Auto))
  ))

---

Home Index