---

Step * 3 1 1 1 1 1 of Lemma FormSafe1_functionality


1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(left) vs) ⇒ (FormSafe1(left) ws))
5. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(right) vs) ⇒ (FormSafe1(right) ws))
6. vs : Atom List
7. ws : Atom List
8. as : Atom List
9. bs : Atom List
10. ∀t:Atom. ((t ∈ vs) ⇐⇒ (t ∈ as @ bs))
11. FormSafe1(left) as
12. FormSafe1(right) bs
13. l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left))
14. t : Atom
15. (t ∈ vs) ⇐⇒ (t ∈ as) ∨ (t ∈ bs)
16. (t ∈ ws) ⇒ (t ∈ vs)
⊢ (t ∈ ws) ⇐⇒ ((t ∈ ws) ∧ (t ∈ as)) ∨ ((t ∈ ws) ∧ (t ∈ bs))
BY
{ Auto }

1
1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(left) vs) ⇒ (FormSafe1(left) ws))
5. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(right) vs) ⇒ (FormSafe1(right) ws))
6. vs : Atom List
7. ws : Atom List
8. as : Atom List
9. bs : Atom List
10. ∀t:Atom. ((t ∈ vs) ⇐⇒ (t ∈ as @ bs))
11. FormSafe1(left) as
12. FormSafe1(right) bs
13. l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left))
14. t : Atom
15. (t ∈ vs) ⇐ (t ∈ as) ∨ (t ∈ bs)
16. (t ∈ ws)
17. (t ∈ vs)
18. (t ∈ as) ∨ (t ∈ bs)
⊢ ((t ∈ ws) ∧ (t ∈ as)) ∨ ((t ∈ ws) ∧ (t ∈ bs))

2
1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(left) vs) ⇒ (FormSafe1(left) ws))
5. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(right) vs) ⇒ (FormSafe1(right) ws))
6. vs : Atom List
7. ws : Atom List
8. as : Atom List
9. bs : Atom List
10. ∀t:Atom. ((t ∈ vs) ⇐⇒ (t ∈ as @ bs))
11. FormSafe1(left) as
12. FormSafe1(right) bs
13. l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left))
14. t : Atom
15. (t ∈ vs) ⇒ ((t ∈ as) ∨ (t ∈ bs))
16. (t ∈ vs) ⇐ (t ∈ as) ∨ (t ∈ bs)
17. (t ∈ ws) ⇒ (t ∈ vs)
18. ((t ∈ ws) ∧ (t ∈ as)) ∨ ((t ∈ ws) ∧ (t ∈ bs))
⊢ (t ∈ ws)

---

Latex:

---

Latex:

1.  C  :  Type
2.  left  :  Form(C)
3.  right  :  Form(C)
4.  \mforall{}vs,ws:Atom  List.    (l\_subset(Atom;ws;vs)  {}\mRightarrow{}  (FormSafe1(left)  vs)  {}\mRightarrow{}  (FormSafe1(left)  ws))
5.  \mforall{}vs,ws:Atom  List.    (l\_subset(Atom;ws;vs)  {}\mRightarrow{}  (FormSafe1(right)  vs)  {}\mRightarrow{}  (FormSafe1(right)  ws))
6.  vs  :  Atom  List
7.  ws  :  Atom  List
8.  as  :  Atom  List
9.  bs  :  Atom  List
10.  \mforall{}t:Atom.  ((t  \mmember{}  vs)  \mLeftarrow{}{}\mRightarrow{}  (t  \mmember{}  as  @  bs))
11.  FormSafe1(left)  as
12.  FormSafe1(right)  bs
13.  l\_disjoint(Atom;as;FormFvs(right))  \mvee{}  l\_disjoint(Atom;bs;FormFvs(left))
14.  t  :  Atom
15.  (t  \mmember{}  vs)  \mLeftarrow{}{}\mRightarrow{}  (t  \mmember{}  as)  \mvee{}  (t  \mmember{}  bs)
16.  (t  \mmember{}  ws)  {}\mRightarrow{}  (t  \mmember{}  vs)
\mvdash{}  (t  \mmember{}  ws)  \mLeftarrow{}{}\mRightarrow{}  ((t  \mmember{}  ws)  \mwedge{}  (t  \mmember{}  as))  \mvee{}  ((t  \mmember{}  ws)  \mwedge{}  (t  \mmember{}  bs))


By

---

Latex:
Auto

---

Home Index