---

Step * of Lemma oal_merge_sd_ordered

No Annotations
∀a:LOSet. ∀b:AbDMon. ∀ps,qs:(|a| × |b|) List.
  ((↑sd_ordered(map(λx.(fst(x));ps))) ⇒ (↑sd_ordered(map(λx.(fst(x));qs))) ⇒ (↑sd_ordered(map(λx.(fst(x));ps ++ qs))))
BY
{ ((RepeatMFor 2 (D 0) 
THENM BLemma `list_pr_length_ind` 
THENM D 0 THENM D 0) THENA Auto) }

1
1. a : LOSet
2. b : AbDMon
3. ps : (|a| × |b|) List
4. qs : (|a| × |b|) List
⊢ (∀us,vs:(|a| × |b|) List.
     (||us|| + ||vs|| < ||ps|| + ||qs||
     ⇒ (↑sd_ordered(map(λx.(fst(x));us)))
     ⇒ (↑sd_ordered(map(λx.(fst(x));vs)))
     ⇒ (↑sd_ordered(map(λx.(fst(x));us ++ vs)))))
⇒ (↑sd_ordered(map(λx.(fst(x));ps)))
⇒ (↑sd_ordered(map(λx.(fst(x));qs)))
⇒ (↑sd_ordered(map(λx.(fst(x));ps ++ qs)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}ps,qs:(|a|  \mtimes{}  |b|)  List.
    ((\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));ps)))
    {}\mRightarrow{}  (\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));qs)))
    {}\mRightarrow{}  (\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));ps  ++  qs))))


By

---

Latex:
((RepeatMFor  2  (D  0) 
THENM  BLemma  `list\_pr\_length\_ind` 
THENM  D  0  THENM  D  0)  THENA  Auto)

---

Home Index