---

Step * 3 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. l_subset(Atom;ws;vs)
9. as : Atom List
10. bs : Atom List
11. set-equal(Atom;vs;as @ bs)
12. FormSafe1(left) as
13. FormSafe1(right) bs
14. l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left))
⊢ ∃as,bs:Atom List
   (set-equal(Atom;ws;as @ bs)
   ∧ (FormSafe1(left) as)
   ∧ (FormSafe1(right) bs)
   ∧ (l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left))))
BY
{ (InstConcl [⌜(ws ⋂ as)⌝;⌜(ws ⋂ bs)⌝]⋅ THEN 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. l_subset(Atom;ws;vs)
9. as : Atom List
10. bs : Atom List
11. set-equal(Atom;vs;as @ bs)
12. FormSafe1(left) as
13. FormSafe1(right) bs
14. l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left))
⊢ set-equal(Atom;ws;(ws ⋂ as) @ (ws ⋂ 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. l_subset(Atom;ws;vs)
9. as : Atom List
10. bs : Atom List
11. set-equal(Atom;vs;as @ bs)
12. FormSafe1(left) as
13. FormSafe1(right) bs
14. l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left))
15. set-equal(Atom;ws;(ws ⋂ as) @ (ws ⋂ bs))
⊢ FormSafe1(left) (ws ⋂ as)

3
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. l_subset(Atom;ws;vs)
9. as : Atom List
10. bs : Atom List
11. set-equal(Atom;vs;as @ bs)
12. FormSafe1(left) as
13. FormSafe1(right) bs
14. l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left))
15. set-equal(Atom;ws;(ws ⋂ as) @ (ws ⋂ bs))
16. FormSafe1(left) (ws ⋂ as)
⊢ FormSafe1(right) (ws ⋂ bs)

4
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. l_subset(Atom;ws;vs)
9. as : Atom List
10. bs : Atom List
11. set-equal(Atom;vs;as @ bs)
12. FormSafe1(left) as
13. FormSafe1(right) bs
14. l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left))
15. set-equal(Atom;ws;(ws ⋂ as) @ (ws ⋂ bs))
16. FormSafe1(left) (ws ⋂ as)
17. FormSafe1(right) (ws ⋂ bs)
⊢ l_disjoint(Atom;(ws ⋂ as);FormFvs(right)) ∨ l_disjoint(Atom;(ws ⋂ bs);FormFvs(left))

---

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.  l\_subset(Atom;ws;vs)
9.  as  :  Atom  List
10.  bs  :  Atom  List
11.  set-equal(Atom;vs;as  @  bs)
12.  FormSafe1(left)  as
13.  FormSafe1(right)  bs
14.  l\_disjoint(Atom;as;FormFvs(right))  \mvee{}  l\_disjoint(Atom;bs;FormFvs(left))
\mvdash{}  \mexists{}as,bs:Atom  List
      (set-equal(Atom;ws;as  @  bs)
      \mwedge{}  (FormSafe1(left)  as)
      \mwedge{}  (FormSafe1(right)  bs)
      \mwedge{}  (l\_disjoint(Atom;as;FormFvs(right))  \mvee{}  l\_disjoint(Atom;bs;FormFvs(left))))


By

---

Latex:
(InstConcl  [\mkleeneopen{}(ws  \mcap{}  as)\mkleeneclose{};\mkleeneopen{}(ws  \mcap{}  bs)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index