---

Step * 2 2 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. ws : Atom List
8. l_subset(Atom;ws;vs)
9. ∃x:Atom
    (set-equal(Atom;vs;[x])
    ∧ (↑FormVar?(element))
    ∧ (FormVar-name(element) = x ∈ Atom)
    ∧ (((↑FormVar?(set)) ∧ (FormVar-name(set) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(set)))))
⊢ (↑null(ws))
∨ (∃x:Atom
    (set-equal(Atom;ws;[x])
    ∧ (↑FormVar?(element))
    ∧ (FormVar-name(element) = x ∈ Atom)
    ∧ (((↑FormVar?(set)) ∧ (FormVar-name(set) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(set))))))
BY
{ ExRepD }

1
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. ws : Atom List
8. l_subset(Atom;ws;vs)
9. x : Atom
10. set-equal(Atom;vs;[x])
11. ↑FormVar?(element)
12. FormVar-name(element) = x ∈ Atom
13. ((↑FormVar?(set)) ∧ (FormVar-name(set) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(set)))
⊢ (↑null(ws))
∨ (∃x:Atom
    (set-equal(Atom;ws;[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,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.  ws  :  Atom  List
8.  l\_subset(Atom;ws;vs)
9.  \mexists{}x:Atom
        (set-equal(Atom;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)))))
\mvdash{}  (\muparrow{}null(ws))
\mvee{}  (\mexists{}x:Atom
        (set-equal(Atom;ws;[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:
ExRepD

---

Home Index