Step * of Lemma omral_action_inj

g:OCMon. ∀r:CDRng. ∀k:|g|. ∀v,v':|r|.  ((v ⋅⋅ inj(k,v')) inj(k,v v') ∈ |omral(g;r)|)
BY
((RepD THENM BLemma `omral_lookups_same_a` 
THENM 
THENM RWW "lookup_omral_action lookup_omral_inj" 0) THENA Auto) }

1
1. OCMon
2. CDRng
3. |g|
4. |r|
5. v' |r|
6. |g|
⊢ (v (when =b u. v')) (when =b u. (v v')) ∈ |r|


Latex:


Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}k:|g|.  \mforall{}v,v':|r|.    ((v  \mcdot{}\mcdot{}  inj(k,v'))  =  inj(k,v  *  v'))


By


Latex:
((RepD  THENM  BLemma  `omral\_lookups\_same\_a` 
THENM  D  0 
THENM  RWW  "lookup\_omral\_action  lookup\_omral\_inj"  0)  THENA  Auto)




Home Index