Step
*
of Lemma
lookup_oal_inj
∀a:LOSet. ∀b:AbDMon. ∀k,k':|a|. ∀v:|b|. ((inj(k,v)[k']) = (when k (=b) k'. v) ∈ |b|)
BY
{ ((RepD THENM Unfold `oal_inj` 0
THENM SplitOnConclITE
THENM Reduce 0) THENA Auto) }
1
1. a : LOSet
2. b : AbDMon
3. k : |a|
4. k' : |a|
5. v : |b|
6. v = e ∈ |b|
⊢ e = (when k (=b) k'. v) ∈ |b|
2
1. a : LOSet
2. b : AbDMon
3. k : |a|
4. k' : |a|
5. v : |b|
6. ¬(v = e ∈ |b|)
⊢ if k (=b) k' then v else e fi = (when k (=b) k'. v) ∈ |b|
Latex:
Latex:
\mforall{}a:LOSet. \mforall{}b:AbDMon. \mforall{}k,k':|a|. \mforall{}v:|b|. ((inj(k,v)[k']) = (when k (=\msubb{}) k'. v))
By
Latex:
((RepD THENM Unfold `oal\_inj` 0
THENM SplitOnConclITE
THENM Reduce 0) THENA Auto)
Home
Index