---

Step * 1 1 of Lemma oal_merge_sd_ordered


1. a : LOSet
2. b : AbDMon
3. p : |a| × |b|
4. ps' : (|a| × |b|) List
5. q : |a| × |b|
6. qs' : (|a| × |b|) List
7. ∀us,vs:(|a| × |b|) List.
     (||us|| + ||vs|| < ||[p / ps']|| + ||[q / qs']||
     ⇒ (↑sd_ordered(map(λx.(fst(x));us)))
     ⇒ (↑sd_ordered(map(λx.(fst(x));vs)))
     ⇒ (↑sd_ordered(map(λx.(fst(x));us ++ vs))))
8. ↑sd_ordered(map(λx.(fst(x));[p / ps']))
9. ↑sd_ordered(map(λx.(fst(x));[q / qs']))
⊢ ↑sd_ordered(map(λx.(fst(x));[p / ps'] ++ [q / qs']))
BY
{ New [`pk';`pv'] (D 5) 
THEN New [`qk';`qv'] (D 3) }

1
1. a : LOSet
2. b : AbDMon
3. qk : |a|
4. qv : |b|
5. ps' : (|a| × |b|) List
6. pk : |a|
7. pv : |b|
8. qs' : (|a| × |b|) List
9. ∀us,vs:(|a| × |b|) List.
     (||us|| + ||vs|| < ||[<qk, qv> / ps']|| + ||[<pk, pv> / qs']||
     ⇒ (↑sd_ordered(map(λx.(fst(x));us)))
     ⇒ (↑sd_ordered(map(λx.(fst(x));vs)))
     ⇒ (↑sd_ordered(map(λx.(fst(x));us ++ vs))))
10. ↑sd_ordered(map(λx.(fst(x));[<qk, qv> / ps']))
11. ↑sd_ordered(map(λx.(fst(x));[<pk, pv> / qs']))
⊢ ↑sd_ordered(map(λx.(fst(x));[<qk, qv> / ps'] ++ [<pk, pv> / qs']))

---

Latex:

---

Latex:

1.  a  :  LOSet
2.  b  :  AbDMon
3.  p  :  |a|  \mtimes{}  |b|
4.  ps'  :  (|a|  \mtimes{}  |b|)  List
5.  q  :  |a|  \mtimes{}  |b|
6.  qs'  :  (|a|  \mtimes{}  |b|)  List
7.  \mforall{}us,vs:(|a|  \mtimes{}  |b|)  List.
          (||us||  +  ||vs||  <  ||[p  /  ps']||  +  ||[q  /  qs']||
          {}\mRightarrow{}  (\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));us)))
          {}\mRightarrow{}  (\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));vs)))
          {}\mRightarrow{}  (\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));us  ++  vs))))
8.  \muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));[p  /  ps']))
9.  \muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));[q  /  qs']))
\mvdash{}  \muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));[p  /  ps']  ++  [q  /  qs']))


By

---

Latex:
New  [`pk';`pv']  (D  5) 
THEN  New  [`qk';`qv']  (D  3)

---

Home Index