---

Step * of Lemma omral_lookups_same_a

∀g:OCMon. ∀r:CDRng. ∀ps,qs:|omral(g;r)|.  ((∀u:|g|. ((ps[u]) = (qs[u]) ∈ |r|)) ⇒ (ps = qs ∈ |omral(g;r)|))
BY
{ ProveSpecializedLemma `lookups_same_a` 2 [parm{i};g↓oset;r↓+gp
... }

1
.....wf..... 
1. g : OCMon
2. r : CDRng
⊢ r↓+gp ∈ AbDMon

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}ps,qs:|omral(g;r)|.    ((\mforall{}u:|g|.  ((ps[u])  =  (qs[u])))  {}\mRightarrow{}  (ps  =  qs))


By

---

Latex:
ProveSpecializedLemma  `lookups\_same\_a`  2  [parm\{i\};g\mdownarrow{}oset;r\mdownarrow{}+gp
...

---

Home Index