---

Step * 2 1 1 of Lemma oal_lk_merge_2


1. s : LOSet
2. g : AbDMon
3. ps : |oal(s;g)|
4. x : |s|
5. y : |g|
6. ↑before(x;map(λx.(fst(x));ps))
7. ¬(y = e ∈ |g|)
8. qs : |oal(s;g)|
9. x1 : |s|
10. y1 : |g|
11. ↑before(x1;map(λx.(fst(x));qs))
12. ¬(y1 = e ∈ |g|)
13. ¬(oal_cons_pr(x;y;ps) = 00 ∈ |oal(s;g)|)
14. ¬(oal_cons_pr(x1;y1;qs) = 00 ∈ |oal(s;g)|)
15. oal_cons_pr(x;y;ps) ++ oal_cons_pr(x1;y1;qs) ∈ |oal(s;g)|
16. ¬((oal_cons_pr(x;y;ps) ++ oal_cons_pr(x1;y1;qs)) = 00 ∈ |oal(s;g)|)
17. lk(oal_cons_pr(x;y;ps)) = lk(oal_cons_pr(x1;y1;qs)) ∈ |s|
18. ¬((lv(oal_cons_pr(x;y;ps)) * lv(oal_cons_pr(x1;y1;qs))) = e ∈ |g|)
⊢ lk(oal_cons_pr(x;y;ps) ++ oal_cons_pr(x1;y1;qs)) = lk(oal_cons_pr(x1;y1;qs)) ∈ |s|
BY
{ (All (RepUR ``oal_cons_pr``) THEN AutoSplit) }

---

Latex:

---

Latex:

1.  s  :  LOSet
2.  g  :  AbDMon
3.  ps  :  |oal(s;g)|
4.  x  :  |s|
5.  y  :  |g|
6.  \muparrow{}before(x;map(\mlambda{}x.(fst(x));ps))
7.  \mneg{}(y  =  e)
8.  qs  :  |oal(s;g)|
9.  x1  :  |s|
10.  y1  :  |g|
11.  \muparrow{}before(x1;map(\mlambda{}x.(fst(x));qs))
12.  \mneg{}(y1  =  e)
13.  \mneg{}(oal\_cons\_pr(x;y;ps)  =  00)
14.  \mneg{}(oal\_cons\_pr(x1;y1;qs)  =  00)
15.  oal\_cons\_pr(x;y;ps)  ++  oal\_cons\_pr(x1;y1;qs)  \mmember{}  |oal(s;g)|
16.  \mneg{}((oal\_cons\_pr(x;y;ps)  ++  oal\_cons\_pr(x1;y1;qs))  =  00)
17.  lk(oal\_cons\_pr(x;y;ps))  =  lk(oal\_cons\_pr(x1;y1;qs))
18.  \mneg{}((lv(oal\_cons\_pr(x;y;ps))  *  lv(oal\_cons\_pr(x1;y1;qs)))  =  e)
\mvdash{}  lk(oal\_cons\_pr(x;y;ps)  ++  oal\_cons\_pr(x1;y1;qs))  =  lk(oal\_cons\_pr(x1;y1;qs))


By

---

Latex:
(All  (RepUR  ``oal\_cons\_pr``)  THEN  AutoSplit)

---

Home Index