---

Step * 1 1 of Lemma assert-PZF_safe


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)))))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THENL [(OrRight THENA Auto); (D -1 THEN Try (Trivial) THEN ExRepD)]) }

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])))
11. ↑(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)))))
⊢ ∃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))))))

2
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])))
11. x1 : Atom
12. set-equal(Atom;vs;[x1])
13. ((↑FormVar?(left)) ∧ (FormVar-name(left) = x1 ∈ Atom) ∧ (¬(x1 ∈ FormFvs(right))))
∨ ((↑FormVar?(right)) ∧ (FormVar-name(right) = x1 ∈ Atom) ∧ (¬(x1 ∈ FormFvs(left))))
⊢ ↑(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)))))

---

Latex:

---

Latex:

1.  C  :  Type
2.  left  :  Form(C)
3.  right  :  Form(C)
4.  \mforall{}vs:Atom  List.  (\muparrow{}(FormSafe2(left)  vs)  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(left)  vs)
5.  \mforall{}vs:Atom  List.  (\muparrow{}(FormSafe2(right)  vs)  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(right)  vs)
6.  vs  :  Atom  List
7.  \mneg{}(vs  =  [])
8.  x  :  Atom
9.  hd(vs)  =  x
10.  \mforall{}x:Atom.  ((x  \mmember{}  vs)  {}\mRightarrow{}  (vs-[x]  =  []  \mLeftarrow{}{}\mRightarrow{}  set-equal(Atom;vs;[x])))
\mvdash{}  \muparrow{}(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{}  False
        \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:
(RepeatFor  2  ((D  0  THENA  Auto))  THENL  [(OrRight  THENA  Auto);  (D  -1  THEN  Try  (Trivial)  THEN  ExRepD)])

---

Home Index