---

Step * of Lemma lookup_merge

No Annotations
∀a:LOSet. ∀b:AbDMon. ∀k:|a|. ∀ps,qs:|oal(a;b)|.  (((ps ++ qs)[k]) = ((ps[k]) * (qs[k])) ∈ |b|)
BY
{ ((RepeatMFor 3 (D 0)) THENA Auto) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}k:|a|.  \mforall{}ps,qs:|oal(a;b)|.    (((ps  ++  qs)[k])  =  ((ps[k])  *  (qs[k])))


By

---

Latex:
((RepeatMFor  3  (D  0))  THENA  Auto)

---

Home Index