---

Step * 1 2 1 1 of Lemma FormSafe1_functionality


1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(left) vs) ⇒ (FormSafe1(left) ws))
5. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(right) vs) ⇒ (FormSafe1(right) 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?(left)) ∧ (FormVar-name(left) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(right))))
∨ ((↑FormVar?(right)) ∧ (FormVar-name(right) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(left))))
⊢ set-equal(Atom;[u / v];[x])
BY
{ ((Assert (u ∈ vs) BY
          Auto)
   THEN (Assert (u ∈ [x]) BY
               (D 11 With ⌜u⌝  THEN Auto))
   THEN RWO "member_singleton" (-1)
   THEN Auto) }

1
1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(left) vs) ⇒ (FormSafe1(left) ws))
5. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(right) vs) ⇒ (FormSafe1(right) 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?(left)) ∧ (FormVar-name(left) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(right))))
∨ ((↑FormVar?(right)) ∧ (FormVar-name(right) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(left))))
13. (u ∈ vs)
14. u = x ∈ Atom
⊢ set-equal(Atom;[u / v];[x])

---

Latex:

---

Latex:

1.  C  :  Type
2.  left  :  Form(C)
3.  right  :  Form(C)
4.  \mforall{}vs,ws:Atom  List.    (l\_subset(Atom;ws;vs)  {}\mRightarrow{}  (FormSafe1(left)  vs)  {}\mRightarrow{}  (FormSafe1(left)  ws))
5.  \mforall{}vs,ws:Atom  List.    (l\_subset(Atom;ws;vs)  {}\mRightarrow{}  (FormSafe1(right)  vs)  {}\mRightarrow{}  (FormSafe1(right)  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?(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))))
\mvdash{}  set-equal(Atom;[u  /  v];[x])


By

---

Latex:
((Assert  (u  \mmember{}  vs)  BY
                Auto)
  THEN  (Assert  (u  \mmember{}  [x])  BY
                          (D  11  With  \mkleeneopen{}u\mkleeneclose{}    THEN  Auto))
  THEN  RWO  "member\_singleton"  (-1)
  THEN  Auto)

---

Home Index