---

Step * 2 2 1 1 1 of Lemma FormSafe1_functionality


1. C : Type
2. element : Form(C)
3. set : Form(C)
4. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(element) vs) ⇒ (FormSafe1(element) ws))
5. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(set) vs) ⇒ (FormSafe1(set) ws))
6. vs : Atom List
7. u : Atom
8. v : Atom List
9. l_subset(Atom;[u / v];vs)
10. x : Atom
11. set-equal(Atom;vs;[x])
12. ↑FormVar?(element)
13. FormVar-name(element) = x ∈ Atom
14. ((↑FormVar?(set)) ∧ (FormVar-name(set) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(set)))
15. (u ∈ vs)
16. u = x ∈ Atom
⊢ set-equal(Atom;[u / v];[x])
BY
{ (RepeatFor 2 (ParallelOp -6) THEN D 9 With ⌜t⌝  THEN Auto THEN RWO "member_singleton" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  Type
2.  element  :  Form(C)
3.  set  :  Form(C)
4.  \mforall{}vs,ws:Atom  List.    (l\_subset(Atom;ws;vs)  {}\mRightarrow{}  (FormSafe1(element)  vs)  {}\mRightarrow{}  (FormSafe1(element)  ws))
5.  \mforall{}vs,ws:Atom  List.    (l\_subset(Atom;ws;vs)  {}\mRightarrow{}  (FormSafe1(set)  vs)  {}\mRightarrow{}  (FormSafe1(set)  ws))
6.  vs  :  Atom  List
7.  u  :  Atom
8.  v  :  Atom  List
9.  l\_subset(Atom;[u  /  v];vs)
10.  x  :  Atom
11.  set-equal(Atom;vs;[x])
12.  \muparrow{}FormVar?(element)
13.  FormVar-name(element)  =  x
14.  ((\muparrow{}FormVar?(set))  \mwedge{}  (FormVar-name(set)  =  x))  \mvee{}  (\mneg{}(x  \mmember{}  FormFvs(set)))
15.  (u  \mmember{}  vs)
16.  u  =  x
\mvdash{}  set-equal(Atom;[u  /  v];[x])


By

---

Latex:
(RepeatFor  2  (ParallelOp  -6)
  THEN  D  9  With  \mkleeneopen{}t\mkleeneclose{} 
  THEN  Auto
  THEN  RWO  "member\_singleton"  (-1)
  THEN  Auto)

---

Home Index