---

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


1. C : Type
2. left : Form(C)
3. right : Form(C)
4. vs : Atom List
5. theta : Atom List
6. l_subset(Atom;theta;vs-FormFvs(right))
7. FormSafe1(left) theta
8. FormSafe1(right) vs-theta
9. set-equal(Atom;vs;theta @ vs-theta)
10. FormSafe1(left) theta
11. FormSafe1(right) vs-theta
⊢ l_disjoint(Atom;theta;FormFvs(right)) ∨ l_disjoint(Atom;vs-theta;FormFvs(left))
BY
{ ((OrLeft THEN Auto) THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. C : Type
2. left : Form(C)
3. right : Form(C)
4. vs : Atom List
5. theta : Atom List
6. l_subset(Atom;theta;vs-FormFvs(right))
7. FormSafe1(left) theta
8. FormSafe1(right) vs-theta
9. set-equal(Atom;vs;theta @ vs-theta)
10. FormSafe1(left) theta
11. FormSafe1(right) vs-theta
12. x : Atom
13. (x ∈ theta) ∧ (x ∈ FormFvs(right))
⊢ False

---

Latex:

---

Latex:

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


By

---

Latex:
((OrLeft  THEN  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index