---

Step * 3 1 of Lemma FormSafe1-Fvs-subset


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 : Atom List
9. bs : Atom List
10. set-equal(Atom;vs;as @ bs)
11. FormSafe1(left) as
12. FormSafe1(right) bs
13. l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left))
⊢ l_subset(Atom;vs;FormFvs(left) ⋃ FormFvs(right))
BY
{ ((Assert l_subset(Atom;as;FormFvs(left)) BY
          ((BackThruSomeHyp THEN Auto) THEN D 0 THEN Auto))
   THEN (Assert l_subset(Atom;bs;FormFvs(right)) BY
               ((BackThruSomeHyp THEN Auto) THEN D 0 THEN Auto))
   THEN D 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. as : Atom List
9. bs : Atom List
10. set-equal(Atom;vs;as @ bs)
11. FormSafe1(left) as
12. FormSafe1(right) bs
13. l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left))
14. l_subset(Atom;as;FormFvs(left))
15. l_subset(Atom;bs;FormFvs(right))
16. x : Atom
17. (x ∈ vs)
⊢ (x ∈ FormFvs(left) ⋃ FormFvs(right))

---

Latex:

---

Latex:

1.  C  :  Type
2.  \mforall{}[P:Form(C)  {}\mrightarrow{}  \mBbbP{}]
          ((\mforall{}name:Atom.  P[Vname])
          {}\mRightarrow{}  (\mforall{}value:C.  P[Const(value)])
          {}\mRightarrow{}  (\mforall{}var:Atom.  \mforall{}phi:Form(C).    (P[phi]  {}\mRightarrow{}  P[\{var  |  phi\}]))
          {}\mRightarrow{}  (\mforall{}left,right:Form(C).    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[left  =  right]))
          {}\mRightarrow{}  (\mforall{}element,set:Form(C).    (P[element]  {}\mRightarrow{}  P[set]  {}\mRightarrow{}  P[element  \mmember{}  set]))
          {}\mRightarrow{}  (\mforall{}left,right:Form(C).    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[left  \mwedge{}  right)]))
          {}\mRightarrow{}  (\mforall{}left,right:Form(C).    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[left  \mvee{}  right]))
          {}\mRightarrow{}  (\mforall{}body:Form(C).  (P[body]  {}\mRightarrow{}  P[\mneg{}(body)]))
          {}\mRightarrow{}  (\mforall{}var:Atom.  \mforall{}body:Form(C).    (P[body]  {}\mRightarrow{}  P[\mforall{}var.  body]))
          {}\mRightarrow{}  (\mforall{}var:Atom.  \mforall{}body:Form(C).    (P[body]  {}\mRightarrow{}  P[\mexists{}var.  body]))
          {}\mRightarrow{}  \{\mforall{}v:Form(C).  P[v]\})
3.  left  :  Form(C)
4.  right  :  Form(C)
5.  \mforall{}vs:Atom  List.  ((FormSafe1(left)  vs)  {}\mRightarrow{}  l\_subset(Atom;vs;FormFvs(left)))
6.  \mforall{}vs:Atom  List.  ((FormSafe1(right)  vs)  {}\mRightarrow{}  l\_subset(Atom;vs;FormFvs(right)))
7.  vs  :  Atom  List
8.  as  :  Atom  List
9.  bs  :  Atom  List
10.  set-equal(Atom;vs;as  @  bs)
11.  FormSafe1(left)  as
12.  FormSafe1(right)  bs
13.  l\_disjoint(Atom;as;FormFvs(right))  \mvee{}  l\_disjoint(Atom;bs;FormFvs(left))
\mvdash{}  l\_subset(Atom;vs;FormFvs(left)  \mcup{}  FormFvs(right))


By

---

Latex:
((Assert  l\_subset(Atom;as;FormFvs(left))  BY
                ((BackThruSomeHyp  THEN  Auto)  THEN  D  0  THEN  Auto))
  THEN  (Assert  l\_subset(Atom;bs;FormFvs(right))  BY
                          ((BackThruSomeHyp  THEN  Auto)  THEN  D  0  THEN  Auto))
  THEN  D  0
  THEN  Auto)

---

Home Index