---

Step * of Lemma omralist_car_properties

∀g:OCMon. ∀r:CDRng. ∀ws:|omral(g;r)|.  ((↑sd_ordered(map(λx.(fst(x));ws))) ∧ (¬↑(0 ∈b map(λx.(snd(x));ws))))
BY
{ ProveSpecializedLemma `oalist_car_properties` 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{}ws:|omral(g;r)|.
    ((\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));ws)))  \mwedge{}  (\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ws))))


By

---

Latex:
ProveSpecializedLemma  `oalist\_car\_properties`  2  [parm\{i\};g\mdownarrow{}oset;r\mdownarrow{}+gp
...

---

Home Index