---

Step * 1 1 1 1 2 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))
11. l_subset(Atom;as;vs-FormFvs(right))
12. FormSafe1(left) as
13. x : Atom
⊢ ((x ∈ vs) ∧ (¬(x ∈ as))) ⇒ (x ∈ bs)
BY
{ ((D -4 With ⌜x⌝  THENA Auto) THEN (D 7 With ⌜x⌝  THENA Auto)) }

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. FormSafe1(left) as
8. FormSafe1(right) bs
9. l_subset(Atom;as;vs-FormFvs(right))
10. FormSafe1(left) as
11. x : Atom
12. ¬((x ∈ as) ∧ (x ∈ FormFvs(right)))
13. (x ∈ vs) ⇐⇒ (x ∈ as @ bs)
⊢ ((x ∈ vs) ∧ (¬(x ∈ as))) ⇒ (x ∈ bs)

---

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))
11.  l\_subset(Atom;as;vs-FormFvs(right))
12.  FormSafe1(left)  as
13.  x  :  Atom
\mvdash{}  ((x  \mmember{}  vs)  \mwedge{}  (\mneg{}(x  \mmember{}  as)))  {}\mRightarrow{}  (x  \mmember{}  bs)


By

---

Latex:
((D  -4  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)  THEN  (D  7  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto))

---

Home Index