---

Step * of Lemma omralist_ind_a

∀g:OCMon. ∀r:CDRng. ∀Q:|omral(g;r)| ⟶ ℙ.
  (Q[[]]
  ⇒ (∀ws:|omral(g;r)|
        (Q[ws] ⇒ (∀x:|g|. ∀y:|r|.  ((↑before(x;map(λx.(fst(x));ws))) ⇒ (¬(y = 0 ∈ |r|)) ⇒ Q[[<x, y> / ws]]))))
  ⇒ {∀ws:|omral(g;r)|. Q[ws]})
BY
{ ProveSpecializedLemma `oalist_ind_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{}Q:|omral(g;r)|  {}\mrightarrow{}  \mBbbP{}.
    (Q[[]]
    {}\mRightarrow{}  (\mforall{}ws:|omral(g;r)|
                (Q[ws]
                {}\mRightarrow{}  (\mforall{}x:|g|.  \mforall{}y:|r|.    ((\muparrow{}before(x;map(\mlambda{}x.(fst(x));ws)))  {}\mRightarrow{}  (\mneg{}(y  =  0))  {}\mRightarrow{}  Q[[<x,  y>  /  ws]]))))
    {}\mRightarrow{}  \{\mforall{}ws:|omral(g;r)|.  Q[ws]\})


By

---

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

---

Home Index