---

Step * 4 of Lemma FormSafe1_functionality


1. C : Type
⊢ ∀body:Form(C)
    ((∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(body) vs) ⇒ (FormSafe1(body) ws)))
    ⇒ (∀vs,ws:Atom List.
          (l_subset(Atom;ws;vs) ⇒ ((↑null(vs)) ∧ (FormSafe1(body) [])) ⇒ ((↑null(ws)) ∧ (FormSafe1(body) [])))))
BY
{ Auto }

1
1. C : Type
2. body : Form(C)
3. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(body) vs) ⇒ (FormSafe1(body) ws))
4. vs : Atom List
5. ws : Atom List
6. l_subset(Atom;ws;vs)
7. ↑null(vs)
8. FormSafe1(body) []
⊢ ws = [] ∈ (Atom List)

---

Latex:

---

Latex:

1.  C  :  Type
\mvdash{}  \mforall{}body:Form(C)
        ((\mforall{}vs,ws:Atom  List.    (l\_subset(Atom;ws;vs)  {}\mRightarrow{}  (FormSafe1(body)  vs)  {}\mRightarrow{}  (FormSafe1(body)  ws)))
        {}\mRightarrow{}  (\mforall{}vs,ws:Atom  List.
                    (l\_subset(Atom;ws;vs)
                    {}\mRightarrow{}  ((\muparrow{}null(vs))  \mwedge{}  (FormSafe1(body)  []))
                    {}\mRightarrow{}  ((\muparrow{}null(ws))  \mwedge{}  (FormSafe1(body)  [])))))


By

---

Latex:
Auto

---

Home Index