---

Step * 2 of Lemma assert-PZF_safe


1. C : Type
⊢ ∀element,set:Form(C).
    ((∀vs:Atom List. (↑(FormSafe2(element) vs) ⇐⇒ FormSafe1''(element) vs))
    ⇒ (∀vs:Atom List. (↑(FormSafe2(set) vs) ⇐⇒ FormSafe1''(set) vs))
    ⇒ (∀vs:Atom List
          (↑(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(vs))
              ∨ (∃x:Atom
                  (set-equal(Atom;vs;[x])
                  ∧ (↑FormVar?(element))
                  ∧ (FormVar-name(element) = x ∈ Atom)
                  ∧ (((↑FormVar?(set)) ∧ (FormVar-name(set) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(set)))))))))
BY
{ (Intros
   THEN ((BoolCase ⌜null(vs)⌝⋅ THENA Auto)
         THENL [Auto; ((GenConcl ⌜hd(vs) = x ∈ Atom⌝⋅ THENA Auto) THEN RepUR ``let`` 0)]
   )
   THEN (Assert ∀x:Atom. ((x ∈ vs) ⇒ (vs-[x] = [] ∈ (Atom List) ⇐⇒ set-equal(Atom;vs;[x]))) BY
               (All Thin
                THEN ((RW assert_pushdownC 0 THENA Auto) THEN (RWO "nil-iff-no-member" 0 THENA Auto))
                THEN (RepeatFor 5 ((D 0 THENA Auto))
                      THENL [((D -2 With ⌜t⌝  THENA Auto)
                              THEN (RWW "member-list-diff member_singleton" (-1) THENA Auto)
                              THEN ((Auto THEN SupposeNot THEN Auto)
                                    THENL [(D -3 THEN Auto); (RWO "member_singleton" (-2) THEN Auto)]
                              ))
                            ; ((D -2 With ⌜x1⌝  THENA Auto) THEN RWW "member-list-diff -1" 0 THEN Auto)]
                )))) }

1
1. C : Type
2. element : Form(C)
3. set : Form(C)
4. ∀vs:Atom List. (↑(FormSafe2(element) vs) ⇐⇒ FormSafe1''(element) vs)
5. ∀vs:Atom List. (↑(FormSafe2(set) vs) ⇐⇒ FormSafe1''(set) vs)
6. vs : Atom List
7. ¬(vs = [] ∈ (Atom List))
8. x : Atom
9. hd(vs) = x ∈ Atom
10. ∀x:Atom. ((x ∈ vs) ⇒ (vs-[x] = [] ∈ (Atom List) ⇐⇒ set-equal(Atom;vs;[x])))
⊢ ↑(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))))
⇐⇒ False
    ∨ (∃x:Atom
        (set-equal(Atom;vs;[x])
        ∧ (↑FormVar?(element))
        ∧ (FormVar-name(element) = x ∈ Atom)
        ∧ (((↑FormVar?(set)) ∧ (FormVar-name(set) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(set))))))

---

Latex:

---

Latex:

1.  C  :  Type
\mvdash{}  \mforall{}element,set:Form(C).
        ((\mforall{}vs:Atom  List.  (\muparrow{}(FormSafe2(element)  vs)  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(element)  vs))
        {}\mRightarrow{}  (\mforall{}vs:Atom  List.  (\muparrow{}(FormSafe2(set)  vs)  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(set)  vs))
        {}\mRightarrow{}  (\mforall{}vs:Atom  List
                    (\muparrow{}(null(vs)
                      \mvee{}\msubb{}let  x  =  hd(vs)  in
                                  null(vs-[x])
                                  \mwedge{}\msubb{}  FormVar?(element)
                                  \mwedge{}\msubb{}  FormVar-name(element)  =a  x
                                  \mwedge{}\msubb{}  ((FormVar?(set)  \mwedge{}\msubb{}  FormVar-name(set)  =a  x)  \mvee{}\msubb{}(\mneg{}\msubb{}x  \mmember{}\msubb{}  FormFvs(set))))
                    \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}null(vs))
                            \mvee{}  (\mexists{}x:Atom
                                    (set-equal(Atom;vs;[x])
                                    \mwedge{}  (\muparrow{}FormVar?(element))
                                    \mwedge{}  (FormVar-name(element)  =  x)
                                    \mwedge{}  (((\muparrow{}FormVar?(set))  \mwedge{}  (FormVar-name(set)  =  x))  \mvee{}  (\mneg{}(x  \mmember{}  FormFvs(set)))))))))


By

---

Latex:
(Intros
  THEN  ((BoolCase  \mkleeneopen{}null(vs)\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [Auto;  ((GenConcl  \mkleeneopen{}hd(vs)  =  x\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  RepUR  ``let``  0)]
  )
  THEN  (Assert  \mforall{}x:Atom.  ((x  \mmember{}  vs)  {}\mRightarrow{}  (vs-[x]  =  []  \mLeftarrow{}{}\mRightarrow{}  set-equal(Atom;vs;[x])))  BY
                          (All  Thin
                            THEN  ((RW  assert\_pushdownC  0  THENA  Auto)  THEN  (RWO  "nil-iff-no-member"  0  THENA  Auto))
                            THEN  (RepeatFor  5  ((D  0  THENA  Auto))
                                        THENL  [((D  -2  With  \mkleeneopen{}t\mkleeneclose{}    THENA  Auto)
                                                        THEN  (RWW  "member-list-diff  member\_singleton"  (-1)  THENA  Auto)
                                                        THEN  ((Auto  THEN  SupposeNot  THEN  Auto)
                                                                    THENL  [(D  -3  THEN  Auto);  (RWO  "member\_singleton"  (-2)  THEN  Auto)]
                                                        ))
                                                    ;  ((D  -2  With  \mkleeneopen{}x1\mkleeneclose{}    THENA  Auto)
                                                          THEN  RWW  "member-list-diff  -1"  0
                                                          THEN  Auto)]
                            ))))

---

Home Index