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


1. Type
2. left Form(C)
3. right Form(C)
4. ∀vs:Atom List. (FormSafe1'(left) vs ⇐⇒ FormSafe1''(left) vs)
5. ∀vs:Atom List. (FormSafe1'(right) vs ⇐⇒ FormSafe1''(right) vs)
6. vs Atom List
7. theta Atom List
8. l_subset(Atom;theta;vs-FormFvs(right))
9. FormSafe1(left) theta
10. FormSafe1(right) vs-theta
11. Atom
12. (t ∈ vs-FormFvs(right))
13. ¬(t ∈ theta)
14. (t ∈ vs-theta)  (t ∈ FormFvs(right))
⊢ (t ∈ theta)
BY
(All (RWO "member-list-diff") THEN Auto) }

1
1. Type
2. left Form(C)
3. right Form(C)
4. ∀vs:Atom List. (FormSafe1'(left) vs ⇐⇒ FormSafe1''(left) vs)
5. ∀vs:Atom List. (FormSafe1'(right) vs ⇐⇒ FormSafe1''(right) vs)
6. vs Atom List
7. theta Atom List
8. l_subset(Atom;theta;vs-FormFvs(right))
9. FormSafe1(left) theta
10. FormSafe1(right) vs-theta
11. Atom
12. (t ∈ vs)
13. ¬(t ∈ FormFvs(right))
14. ¬(t ∈ theta)
15. ((t ∈ vs) ∧ (t ∈ theta)))  (t ∈ FormFvs(right))
⊢ (t ∈ theta)


Latex:


Latex:

1.  C  :  Type
2.  left  :  Form(C)
3.  right  :  Form(C)
4.  \mforall{}vs:Atom  List.  (FormSafe1'(left)  vs  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(left)  vs)
5.  \mforall{}vs:Atom  List.  (FormSafe1'(right)  vs  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(right)  vs)
6.  vs  :  Atom  List
7.  theta  :  Atom  List
8.  l\_subset(Atom;theta;vs-FormFvs(right))
9.  FormSafe1(left)  theta
10.  FormSafe1(right)  vs-theta
11.  t  :  Atom
12.  (t  \mmember{}  vs-FormFvs(right))
13.  \mneg{}(t  \mmember{}  theta)
14.  (t  \mmember{}  vs-theta)  {}\mRightarrow{}  (t  \mmember{}  FormFvs(right))
\mvdash{}  (t  \mmember{}  theta)


By


Latex:
(All  (RWO  "member-list-diff")  THEN  Auto)




Home Index