---

Step * of Lemma FormSafe-iff-FormSafe1'

∀C:Type. ∀f:Form(C). ∀vs:Atom List.  (FormSafe1(f) vs ⇐⇒ FormSafe1'(f) vs)
BY
{ (Intro
   THEN (BLemma `Form-induction` THENW Auto)
   THEN RepUR ``FormSafe1 FormSafe1\'`` 0
   THEN Try (Folds ``FormSafe1 FormSafe1\'`` 0⋅)
   THEN Try (QuickAuto)) }

1
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))))))

---

Latex:

---

Latex:
\mforall{}C:Type.  \mforall{}f:Form(C).  \mforall{}vs:Atom  List.    (FormSafe1(f)  vs  \mLeftarrow{}{}\mRightarrow{}  FormSafe1'(f)  vs)


By

---

Latex:
(Intro
  THEN  (BLemma  `Form-induction`  THENW  Auto)
  THEN  RepUR  ``FormSafe1  FormSafe1\mbackslash{}'``  0
  THEN  Try  (Folds  ``FormSafe1  FormSafe1\mbackslash{}'``  0\mcdot{})
  THEN  Try  (QuickAuto))

---

Home Index