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