---

Step * 3 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)
          ⇒ (∃as,bs:Atom List
               (set-equal(Atom;vs;as @ bs)
               ∧ (FormSafe1(left) as)
               ∧ (FormSafe1(right) bs)
               ∧ (l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left)))))
          ⇒ (∃as,bs:Atom List
               (set-equal(Atom;ws;as @ bs)
               ∧ (FormSafe1(left) as)
               ∧ (FormSafe1(right) bs)
               ∧ (l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left))))))))
BY
{ (Auto THEN ExRepD) }

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. as : Atom List
10. bs : Atom List
11. set-equal(Atom;vs;as @ bs)
12. FormSafe1(left) as
13. FormSafe1(right) bs
14. l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left))
⊢ ∃as,bs:Atom List
   (set-equal(Atom;ws;as @ bs)
   ∧ (FormSafe1(left) as)
   ∧ (FormSafe1(right) bs)
   ∧ (l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;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{}  (\mexists{}as,bs:Atom  List
                              (set-equal(Atom;vs;as  @  bs)
                              \mwedge{}  (FormSafe1(left)  as)
                              \mwedge{}  (FormSafe1(right)  bs)
                              \mwedge{}  (l\_disjoint(Atom;as;FormFvs(right))  \mvee{}  l\_disjoint(Atom;bs;FormFvs(left)))))
                    {}\mRightarrow{}  (\mexists{}as,bs:Atom  List
                              (set-equal(Atom;ws;as  @  bs)
                              \mwedge{}  (FormSafe1(left)  as)
                              \mwedge{}  (FormSafe1(right)  bs)
                              \mwedge{}  (l\_disjoint(Atom;as;FormFvs(right))  \mvee{}  l\_disjoint(Atom;bs;FormFvs(left))))))))


By

---

Latex:
(Auto  THEN  ExRepD)

---

Home Index