---

Step * of Lemma FormSafe1-Fvs-subset

∀C:Type. ∀phi:Form(C). ∀vs:Atom List.  ((FormSafe1(phi) vs) ⇒ l_subset(Atom;vs;FormFvs(phi)))
BY
{ (Intro
   THEN (InstLemma `Form-induction` [⌜C⌝]⋅ THENA Auto)
   THEN (BHyp -1  THENW Auto)
   THEN RepUR ``FormSafe1 FormFvs`` 0
   THEN Try (Fold `FormFvs` 0)
   THEN Try (Fold `FormSafe1` 0)
   THEN Auto) }

1
1. C : Type
2. ∀[P:Form(C) ⟶ ℙ]
     ((∀name:Atom. P[Vname])
     ⇒ (∀value:C. P[Const(value)])
     ⇒ (∀var:Atom. ∀phi:Form(C).  (P[phi] ⇒ P[{var | phi}]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left = right]))
     ⇒ (∀element,set:Form(C).  (P[element] ⇒ P[set] ⇒ P[element ∈ set]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∧ right)]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∨ right]))
     ⇒ (∀body:Form(C). (P[body] ⇒ P[¬(body)]))
     ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∀var. body]))
     ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∃var. body]))
     ⇒ {∀v:Form(C). P[v]})
3. left : Form(C)
4. right : Form(C)
5. ∀vs:Atom List. ((FormSafe1(left) vs) ⇒ l_subset(Atom;vs;FormFvs(left)))
6. ∀vs:Atom List. ((FormSafe1(right) vs) ⇒ l_subset(Atom;vs;FormFvs(right)))
7. vs : Atom List
8. (↑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)))))))
⊢ l_subset(Atom;vs;FormFvs(left) ⋃ FormFvs(right))

2
1. C : Type
2. ∀[P:Form(C) ⟶ ℙ]
     ((∀name:Atom. P[Vname])
     ⇒ (∀value:C. P[Const(value)])
     ⇒ (∀var:Atom. ∀phi:Form(C).  (P[phi] ⇒ P[{var | phi}]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left = right]))
     ⇒ (∀element,set:Form(C).  (P[element] ⇒ P[set] ⇒ P[element ∈ set]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∧ right)]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∨ right]))
     ⇒ (∀body:Form(C). (P[body] ⇒ P[¬(body)]))
     ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∀var. body]))
     ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∃var. body]))
     ⇒ {∀v:Form(C). P[v]})
3. element : Form(C)
4. set : Form(C)
5. ∀vs:Atom List. ((FormSafe1(element) vs) ⇒ l_subset(Atom;vs;FormFvs(element)))
6. ∀vs:Atom List. ((FormSafe1(set) vs) ⇒ l_subset(Atom;vs;FormFvs(set)))
7. vs : Atom List
8. (↑null(vs))
∨ (∃x:Atom
    (set-equal(Atom;vs;[x])
    ∧ (↑FormVar?(element))
    ∧ (FormVar-name(element) = x ∈ Atom)
    ∧ (((↑FormVar?(set)) ∧ (FormVar-name(set) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(set))))))
⊢ l_subset(Atom;vs;FormFvs(element) ⋃ FormFvs(set))

3
1. C : Type
2. ∀[P:Form(C) ⟶ ℙ]
     ((∀name:Atom. P[Vname])
     ⇒ (∀value:C. P[Const(value)])
     ⇒ (∀var:Atom. ∀phi:Form(C).  (P[phi] ⇒ P[{var | phi}]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left = right]))
     ⇒ (∀element,set:Form(C).  (P[element] ⇒ P[set] ⇒ P[element ∈ set]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∧ right)]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∨ right]))
     ⇒ (∀body:Form(C). (P[body] ⇒ P[¬(body)]))
     ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∀var. body]))
     ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∃var. body]))
     ⇒ {∀v:Form(C). P[v]})
3. left : Form(C)
4. right : Form(C)
5. ∀vs:Atom List. ((FormSafe1(left) vs) ⇒ l_subset(Atom;vs;FormFvs(left)))
6. ∀vs:Atom List. ((FormSafe1(right) vs) ⇒ l_subset(Atom;vs;FormFvs(right)))
7. vs : Atom List
8. ∃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))))
⊢ l_subset(Atom;vs;FormFvs(left) ⋃ FormFvs(right))

4
1. C : Type
2. ∀[P:Form(C) ⟶ ℙ]
     ((∀name:Atom. P[Vname])
     ⇒ (∀value:C. P[Const(value)])
     ⇒ (∀var:Atom. ∀phi:Form(C).  (P[phi] ⇒ P[{var | phi}]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left = right]))
     ⇒ (∀element,set:Form(C).  (P[element] ⇒ P[set] ⇒ P[element ∈ set]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∧ right)]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∨ right]))
     ⇒ (∀body:Form(C). (P[body] ⇒ P[¬(body)]))
     ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∀var. body]))
     ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∃var. body]))
     ⇒ {∀v:Form(C). P[v]})
3. left : Form(C)
4. right : Form(C)
5. ∀vs:Atom List. ((FormSafe1(left) vs) ⇒ l_subset(Atom;vs;FormFvs(left)))
6. ∀vs:Atom List. ((FormSafe1(right) vs) ⇒ l_subset(Atom;vs;FormFvs(right)))
7. vs : Atom List
8. FormSafe1(left) vs
9. FormSafe1(right) vs
⊢ l_subset(Atom;vs;FormFvs(left) ⋃ FormFvs(right))

5
1. C : Type
2. ∀[P:Form(C) ⟶ ℙ]
     ((∀name:Atom. P[Vname])
     ⇒ (∀value:C. P[Const(value)])
     ⇒ (∀var:Atom. ∀phi:Form(C).  (P[phi] ⇒ P[{var | phi}]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left = right]))
     ⇒ (∀element,set:Form(C).  (P[element] ⇒ P[set] ⇒ P[element ∈ set]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∧ right)]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∨ right]))
     ⇒ (∀body:Form(C). (P[body] ⇒ P[¬(body)]))
     ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∀var. body]))
     ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∃var. body]))
     ⇒ {∀v:Form(C). P[v]})
3. body : Form(C)
4. ∀vs:Atom List. ((FormSafe1(body) vs) ⇒ l_subset(Atom;vs;FormFvs(body)))
5. vs : Atom List
6. ↑null(vs)
7. FormSafe1(body) []
⊢ l_subset(Atom;vs;FormFvs(body))

6
1. C : Type
2. ∀[P:Form(C) ⟶ ℙ]
     ((∀name:Atom. P[Vname])
     ⇒ (∀value:C. P[Const(value)])
     ⇒ (∀var:Atom. ∀phi:Form(C).  (P[phi] ⇒ P[{var | phi}]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left = right]))
     ⇒ (∀element,set:Form(C).  (P[element] ⇒ P[set] ⇒ P[element ∈ set]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∧ right)]))
     ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∨ right]))
     ⇒ (∀body:Form(C). (P[body] ⇒ P[¬(body)]))
     ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∀var. body]))
     ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∃var. body]))
     ⇒ {∀v:Form(C). P[v]})
3. var : Atom
4. body : Form(C)
5. ∀vs:Atom List. ((FormSafe1(body) vs) ⇒ l_subset(Atom;vs;FormFvs(body)))
6. vs : Atom List
7. ¬(var ∈ vs)
8. FormSafe1(body) [var / vs]
⊢ l_subset(Atom;vs;filter(λv.(¬bv =a var);FormFvs(body)))

---

Latex:

---

Latex:
\mforall{}C:Type.  \mforall{}phi:Form(C).  \mforall{}vs:Atom  List.    ((FormSafe1(phi)  vs)  {}\mRightarrow{}  l\_subset(Atom;vs;FormFvs(phi)))


By

---

Latex:
(Intro
  THEN  (InstLemma  `Form-induction`  [\mkleeneopen{}C\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (BHyp  -1    THENW  Auto)
  THEN  RepUR  ``FormSafe1  FormFvs``  0
  THEN  Try  (Fold  `FormFvs`  0)
  THEN  Try  (Fold  `FormSafe1`  0)
  THEN  Auto)

---

Home Index