---

Step * 1 of Lemma lookup_merge


1. a : LOSet
2. b : AbDMon
3. k : |a|
⊢ ∀ps,qs:|oal(a;b)|.  (((ps ++ qs)[k]) = ((ps[k]) * (qs[k])) ∈ |b|)
BY
{ ((BLemma `oalist_pr_length_ind`) THENA Auto) }

1
1. a : LOSet
2. b : AbDMon
3. k : |a|
⊢ ∀ps,qs:|oal(a;b)|.
    ((∀us,vs:|oal(a;b)|.  (||us|| + ||vs|| < ||ps|| + ||qs|| ⇒ (((us ++ vs)[k]) = ((us[k]) * (vs[k])) ∈ |b|)))
    ⇒ (((ps ++ qs)[k]) = ((ps[k]) * (qs[k])) ∈ |b|))

---

Latex:

---

Latex:

1.  a  :  LOSet
2.  b  :  AbDMon
3.  k  :  |a|
\mvdash{}  \mforall{}ps,qs:|oal(a;b)|.    (((ps  ++  qs)[k])  =  ((ps[k])  *  (qs[k])))


By

---

Latex:
((BLemma  `oalist\_pr\_length\_ind`)  THENA  Auto)

---

Home Index