---

Step * of Lemma FormSafe1'-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 Auto
   THEN ParallelLast) }

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. ∃theta:Atom List. (l_subset(Atom;theta;vs-FormFvs(right)) ∧ (FormSafe1'(left) theta) ∧ (FormSafe1'(right) vs-theta))
⊢ let theta = vs-FormFvs(right) in
      (FormSafe1''(left) theta) ∧ (FormSafe1''(right) vs-theta)

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. ∃phi:Atom List. (l_subset(Atom;phi;vs-FormFvs(left)) ∧ (FormSafe1'(left) vs-phi) ∧ (FormSafe1'(right) phi))
⊢ let phi = vs-FormFvs(left) in
      (FormSafe1''(left) vs-phi) ∧ (FormSafe1''(right) phi)

3
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. let theta = vs-FormFvs(right) in
       (FormSafe1''(left) theta) ∧ (FormSafe1''(right) vs-theta)
⊢ ∃theta:Atom List. (l_subset(Atom;theta;vs-FormFvs(right)) ∧ (FormSafe1'(left) theta) ∧ (FormSafe1'(right) vs-theta))

4
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. let phi = vs-FormFvs(left) in
       (FormSafe1''(left) vs-phi) ∧ (FormSafe1''(right) phi)
⊢ ∃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\mbackslash{}'  FormSafe1\mbackslash{}'\mbackslash{}'``  0
  THEN  Try  (Folds  ``FormSafe1\mbackslash{}'  FormSafe1\mbackslash{}'\mbackslash{}'``  0\mcdot{})
  THEN  Auto
  THEN  ParallelLast)

---

Home Index