---

Step * 1 2 2 of Lemma FormSafe-iff-FormSafe1'


1. C : Type
2. left : Form(C)
3. right : Form(C)
4. vs : Atom List
5. phi : Atom List
6. l_subset(Atom;phi;vs-FormFvs(left))
7. FormSafe1(left) vs-phi
8. 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))))
BY
{ (InstConcl [⌜vs-phi⌝;⌜phi⌝]⋅ THEN Auto) }

1
1. C : Type
2. left : Form(C)
3. right : Form(C)
4. vs : Atom List
5. phi : Atom List
6. l_subset(Atom;phi;vs-FormFvs(left))
7. FormSafe1(left) vs-phi
8. FormSafe1(right) phi
⊢ set-equal(Atom;vs;vs-phi @ phi)

2
1. C : Type
2. left : Form(C)
3. right : Form(C)
4. vs : Atom List
5. phi : Atom List
6. l_subset(Atom;phi;vs-FormFvs(left))
7. FormSafe1(left) vs-phi
8. FormSafe1(right) phi
9. set-equal(Atom;vs;vs-phi @ phi)
10. FormSafe1(left) vs-phi
11. FormSafe1(right) phi
⊢ l_disjoint(Atom;vs-phi;FormFvs(right)) ∨ l_disjoint(Atom;phi;FormFvs(left))

---

Latex:

---

Latex:

1.  C  :  Type
2.  left  :  Form(C)
3.  right  :  Form(C)
4.  vs  :  Atom  List
5.  phi  :  Atom  List
6.  l\_subset(Atom;phi;vs-FormFvs(left))
7.  FormSafe1(left)  vs-phi
8.  FormSafe1(right)  phi
\mvdash{}  \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))))


By

---

Latex:
(InstConcl  [\mkleeneopen{}vs-phi\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index