---

Step * 1 of Lemma FormSafe1_functionality


1. C : Type
⊢ ∀left,right:Form(C).
    ((∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(left) vs) ⇒ (FormSafe1(left) ws)))
    ⇒ (∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(right) vs) ⇒ (FormSafe1(right) ws)))
    ⇒ (∀vs,ws:Atom List.
          (l_subset(Atom;ws;vs)
          ⇒ ((↑null(vs))
             ∨ (∃x:Atom
                 (set-equal(Atom;vs;[x])
                 ∧ (((↑FormVar?(left)) ∧ (FormVar-name(left) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(right))))
                   ∨ ((↑FormVar?(right)) ∧ (FormVar-name(right) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(left))))))))
          ⇒ ((↑null(ws))
             ∨ (∃x:Atom
                 (set-equal(Atom;ws;[x])
                 ∧ (((↑FormVar?(left)) ∧ (FormVar-name(left) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(right))))
                   ∨ ((↑FormVar?(right)) ∧ (FormVar-name(right) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(left)))))))))))
BY
{ (Auto THEN D -1) }

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. ws : Atom List
8. l_subset(Atom;ws;vs)
9. ↑null(vs)
⊢ (↑null(ws))
∨ (∃x:Atom
    (set-equal(Atom;ws;[x])
    ∧ (((↑FormVar?(left)) ∧ (FormVar-name(left) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(right))))
      ∨ ((↑FormVar?(right)) ∧ (FormVar-name(right) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(left)))))))

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

---

Latex:

---

Latex:

1.  C  :  Type
\mvdash{}  \mforall{}left,right:Form(C).
        ((\mforall{}vs,ws:Atom  List.    (l\_subset(Atom;ws;vs)  {}\mRightarrow{}  (FormSafe1(left)  vs)  {}\mRightarrow{}  (FormSafe1(left)  ws)))
        {}\mRightarrow{}  (\mforall{}vs,ws:Atom  List.    (l\_subset(Atom;ws;vs)  {}\mRightarrow{}  (FormSafe1(right)  vs)  {}\mRightarrow{}  (FormSafe1(right)  ws)))
        {}\mRightarrow{}  (\mforall{}vs,ws:Atom  List.
                    (l\_subset(Atom;ws;vs)
                    {}\mRightarrow{}  ((\muparrow{}null(vs))
                          \mvee{}  (\mexists{}x:Atom
                                  (set-equal(Atom;vs;[x])
                                  \mwedge{}  (((\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))))))))
                    {}\mRightarrow{}  ((\muparrow{}null(ws))
                          \mvee{}  (\mexists{}x:Atom
                                  (set-equal(Atom;ws;[x])
                                  \mwedge{}  (((\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)))))))))))


By

---

Latex:
(Auto  THEN  D  -1)

---

Home Index