---

Step * 1 of Lemma FormSafe-iff-FormSafe1'


1. C : Type
⊢ ∀left,right:Form(C).
    ((∀vs:Atom List. (FormSafe1(left) vs ⇐⇒ FormSafe1'(left) vs))
    ⇒ (∀vs:Atom List. (FormSafe1(right) vs ⇐⇒ FormSafe1'(right) vs))
    ⇒ (∀vs:Atom List
          (∃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))))
          ⇐⇒ (∃theta:Atom List
                (l_subset(Atom;theta;vs-FormFvs(right)) ∧ (FormSafe1'(left) theta) ∧ (FormSafe1'(right) vs-theta)))
              ∨ (∃phi:Atom List
                  (l_subset(Atom;phi;vs-FormFvs(left)) ∧ (FormSafe1'(left) vs-phi) ∧ (FormSafe1'(right) phi))))))
BY
{ Auto }

1
1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs:Atom List. (FormSafe1(left) vs ⇐⇒ FormSafe1'(left) vs)
5. ∀vs:Atom List. (FormSafe1(right) vs ⇐⇒ FormSafe1'(right) vs)
6. vs : Atom List
7. ∃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))))
⊢ (∃theta:Atom List. (l_subset(Atom;theta;vs-FormFvs(right)) ∧ (FormSafe1'(left) theta) ∧ (FormSafe1'(right) vs-theta)))
∨ (∃phi:Atom List. (l_subset(Atom;phi;vs-FormFvs(left)) ∧ (FormSafe1'(left) vs-phi) ∧ (FormSafe1'(right) phi)))

2
1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs:Atom List. (FormSafe1(left) vs ⇐⇒ FormSafe1'(left) vs)
5. ∀vs:Atom List. (FormSafe1(right) vs ⇐⇒ FormSafe1'(right) vs)
6. vs : Atom List
7. (∃theta:Atom List
     (l_subset(Atom;theta;vs-FormFvs(right)) ∧ (FormSafe1'(left) theta) ∧ (FormSafe1'(right) vs-theta)))
∨ (∃phi:Atom List. (l_subset(Atom;phi;vs-FormFvs(left)) ∧ (FormSafe1'(left) vs-phi) ∧ (FormSafe1'(right) phi)))
⊢ ∃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))))

---

Latex:

---

Latex:

1.  C  :  Type
\mvdash{}  \mforall{}left,right:Form(C).
        ((\mforall{}vs:Atom  List.  (FormSafe1(left)  vs  \mLeftarrow{}{}\mRightarrow{}  FormSafe1'(left)  vs))
        {}\mRightarrow{}  (\mforall{}vs:Atom  List.  (FormSafe1(right)  vs  \mLeftarrow{}{}\mRightarrow{}  FormSafe1'(right)  vs))
        {}\mRightarrow{}  (\mforall{}vs:Atom  List
                    (\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))))
                    \mLeftarrow{}{}\mRightarrow{}  (\mexists{}theta:Atom  List
                                (l\_subset(Atom;theta;vs-FormFvs(right))
                                \mwedge{}  (FormSafe1'(left)  theta)
                                \mwedge{}  (FormSafe1'(right)  vs-theta)))
                            \mvee{}  (\mexists{}phi:Atom  List
                                    (l\_subset(Atom;phi;vs-FormFvs(left))
                                    \mwedge{}  (FormSafe1'(left)  vs-phi)
                                    \mwedge{}  (FormSafe1'(right)  phi))))))


By

---

Latex:
Auto

---

Home Index