---

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


1. C : Type
2. left : Form(C)
3. right : Form(C)
4. vs : Atom List
5. as : Atom List
6. bs : Atom List
7. set-equal(Atom;vs;as @ bs)
8. FormSafe1(left) as
9. FormSafe1(right) bs
10. 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)))
BY
{ ParallelLast }

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

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

---

Latex:

---

Latex:

1.  C  :  Type
2.  left  :  Form(C)
3.  right  :  Form(C)
4.  vs  :  Atom  List
5.  as  :  Atom  List
6.  bs  :  Atom  List
7.  set-equal(Atom;vs;as  @  bs)
8.  FormSafe1(left)  as
9.  FormSafe1(right)  bs
10.  l\_disjoint(Atom;as;FormFvs(right))  \mvee{}  l\_disjoint(Atom;bs;FormFvs(left))
\mvdash{}  (\mexists{}theta:Atom  List
        (l\_subset(Atom;theta;vs-FormFvs(right))
        \mwedge{}  (FormSafe1(left)  theta)
        \mwedge{}  (FormSafe1(right)  vs-theta)))
\mvee{}  (\mexists{}phi:Atom  List
        (l\_subset(Atom;phi;vs-FormFvs(left))  \mwedge{}  (FormSafe1(left)  vs-phi)  \mwedge{}  (FormSafe1(right)  phi)))


By

---

Latex:
ParallelLast

---

Home Index