Step
*
of Lemma
oal_merge_assoc
∀a:LOSet. ∀b:AbDMon. ∀ps,qs,rs:|oal(a;b)|. ((ps ++ qs ++ rs) = ((ps ++ qs) ++ rs) ∈ |oal(a;b)|)
BY
{ ((RepD
THENM BLemma `lookups_same_a`
THENM D 0
THENM RW (SweepDnC (LemmaC `lookup_merge`)) 0
THENM RW AbMonNormC 0) THEN Auto) }
Latex:
Latex:
\mforall{}a:LOSet. \mforall{}b:AbDMon. \mforall{}ps,qs,rs:|oal(a;b)|. ((ps ++ qs ++ rs) = ((ps ++ qs) ++ rs))
By
Latex:
((RepD
THENM BLemma `lookups\_same\_a`
THENM D 0
THENM RW (SweepDnC (LemmaC `lookup\_merge`)) 0
THENM RW AbMonNormC 0) THEN Auto)
Home
Index