---

Step * of Lemma oal_merge_non_id_vals

∀a:LOSet. ∀b:AbDMon. ∀ps,qs:(|a| × |b|) List.
  ((¬↑(e ∈b map(λx.(snd(x));ps))) ⇒ (¬↑(e ∈b map(λx.(snd(x));qs))) ⇒ (¬↑(e ∈b map(λx.(snd(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||
     ⇒ (¬↑(e ∈b map(λx.(snd(x));us)))
     ⇒ (¬↑(e ∈b map(λx.(snd(x));vs)))
     ⇒ (¬↑(e ∈b map(λx.(snd(x));us ++ vs)))))
⇒ (¬↑(e ∈b map(λx.(snd(x));ps)))
⇒ (¬↑(e ∈b map(λx.(snd(x));qs)))
⇒ (¬↑(e ∈b map(λx.(snd(x));ps ++ qs)))

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}ps,qs:(|a|  \mtimes{}  |b|)  List.
    ((\mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps)))
    {}\mRightarrow{}  (\mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));qs)))
    {}\mRightarrow{}  (\mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps  ++  qs))))


By

---

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

---

Home Index