---

Step * 1 of Lemma assert-PZF_safe


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

---

Latex:

---

Latex:

1.  C  :  Type
\mvdash{}  \mforall{}left,right:Form(C).
        ((\mforall{}vs:Atom  List.  (\muparrow{}(FormSafe2(left)  vs)  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(left)  vs))
        {}\mRightarrow{}  (\mforall{}vs:Atom  List.  (\muparrow{}(FormSafe2(right)  vs)  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(right)  vs))
        {}\mRightarrow{}  (\mforall{}vs:Atom  List
                    (\muparrow{}(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)))))
                    \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}null(vs))
                            \mvee{}  (\mexists{}x:Atom
                                    (set-equal(Atom;vs;[x])
                                    \mwedge{}  (((\muparrow{}FormVar?(left))  \mwedge{}  (FormVar-name(left)  =  x)  \mwedge{}  (\mneg{}(x  \mmember{}  FormFvs(right))))
                                        \mvee{}  ((\muparrow{}FormVar?(right))
                                            \mwedge{}  (FormVar-name(right)  =  x)
                                            \mwedge{}  (\mneg{}(x  \mmember{}  FormFvs(left))))))))))


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