---

Step * 2 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)|)
⊢ (¬((oal_cons_pr(x;y;ps) ++ oal_cons_pr(x1;y1;qs)) = 00 ∈ |oal(s;g)|))
⇒ (lk(oal_cons_pr(x;y;ps)) = lk(oal_cons_pr(x1;y1;qs)) ∈ |s|)
⇒ (¬((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
{ ((Assert oal_cons_pr(x;y;ps) ++ oal_cons_pr(x1;y1;qs) ∈ |oal(s;g)| BY Auto) THEN Auto) }

1
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|

---

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)
\mvdash{}  (\mneg{}((oal\_cons\_pr(x;y;ps)  ++  oal\_cons\_pr(x1;y1;qs))  =  00))
{}\mRightarrow{}  (lk(oal\_cons\_pr(x;y;ps))  =  lk(oal\_cons\_pr(x1;y1;qs)))
{}\mRightarrow{}  (\mneg{}((lv(oal\_cons\_pr(x;y;ps))  *  lv(oal\_cons\_pr(x1;y1;qs)))  =  e))
{}\mRightarrow{}  (lk(oal\_cons\_pr(x;y;ps)  ++  oal\_cons\_pr(x1;y1;qs))  =  lk(oal\_cons\_pr(x1;y1;qs)))


By

---

Latex:
((Assert  oal\_cons\_pr(x;y;ps)  ++  oal\_cons\_pr(x1;y1;qs)  \mmember{}  |oal(s;g)|  BY  Auto)  THEN  Auto)

---

Home Index