---

Step * 2 1 1 1 of Lemma assert-PZF_safe


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])))
11. ↑(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))))
12. vs-[x] = [] ∈ (Atom List) ⇐⇒ set-equal(Atom;vs;[x])
⊢ (vs-[x] = [] ∈ (Atom List))
∧ (↑FormVar?(element))
∧ (FormVar-name(element) = x ∈ Atom)
∧ (((↑FormVar?(set)) ∧ (FormVar-name(set) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(set))))
BY
{ ((RWO "assert_of_band" (-2) THENA Auto) THEN ParallelOp -2) }

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])))
11. ↑(FormVar?(element)
∧b FormVar-name(element) =a x
∧b ((FormVar?(set) ∧b FormVar-name(set) =a x) ∨b(¬bx ∈b FormFvs(set))))
12. ↑null(vs-[x])
13. vs-[x] = [] ∈ (Atom List) ⇐⇒ set-equal(Atom;vs;[x])
⊢ vs-[x] = [] ∈ (Atom List)

2
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])))
11. ↑null(vs-[x])
12. ↑(FormVar?(element)
∧b FormVar-name(element) =a x
∧b ((FormVar?(set) ∧b FormVar-name(set) =a x) ∨b(¬bx ∈b FormFvs(set))))
13. vs-[x] = [] ∈ (Atom List) ⇐⇒ 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
2.  element  :  Form(C)
3.  set  :  Form(C)
4.  \mforall{}vs:Atom  List.  (\muparrow{}(FormSafe2(element)  vs)  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(element)  vs)
5.  \mforall{}vs:Atom  List.  (\muparrow{}(FormSafe2(set)  vs)  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(set)  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])))
11.  \muparrow{}(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))))
12.  vs-[x]  =  []  \mLeftarrow{}{}\mRightarrow{}  set-equal(Atom;vs;[x])
\mvdash{}  (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:
((RWO  "assert\_of\_band"  (-2)  THENA  Auto)  THEN  ParallelOp  -2)

---

Home Index