---

Step * of Lemma omralist_cases

∀g:OCMon. ∀r:CDRng. ∀Q:|omral(g;r)| ⟶ ℙ.
  (Q[[]]
  ⇒ (∀ws:|omral(g;r)|. ∀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
{ ((D 0 THENM D 0) THENA Auto) 
THEN AssertLemma `oalist_cases_a` [] 
THEN ((With g↓oset (D (-1)) THENM With r↓+gp (D (-1))) THENA Auto) 
 }

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

2
1. g : OCMon
2. r : CDRng
3. ∀Q:|oal(g↓oset;r↓+gp)| ⟶ ℙ
     (Q[[]]
     ⇒ (∀ws:|oal(g↓oset;r↓+gp)|. ∀x:|(g↓oset)|. ∀y:|r↓+gp|.
           ((↑before(x;map(λx.(fst(x));ws))) ⇒ (¬(y = e ∈ |r↓+gp|)) ⇒ Q[[<x, y> / ws]]))
     ⇒ {∀ws:|oal(g↓oset;r↓+gp)|. Q[ws]})
⊢ ∀Q:|omral(g;r)| ⟶ ℙ
    (Q[[]]
    ⇒ (∀ws:|omral(g;r)|. ∀x:|g|. ∀y:|r|.  ((↑before(x;map(λx.(fst(x));ws))) ⇒ (¬(y = 0 ∈ |r|)) ⇒ Q[[<x, y> / ws]]))
    ⇒ {∀ws:|omral(g;r)|. Q[ws]})

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}Q:|omral(g;r)|  {}\mrightarrow{}  \mBbbP{}.
    (Q[[]]
    {}\mRightarrow{}  (\mforall{}ws:|omral(g;r)|.  \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:
((D  0  THENM  D  0)  THENA  Auto) 
THEN  AssertLemma  `oalist\_cases\_a`  [] 
THEN  ((With  g\mdownarrow{}oset  (D  (-1))  THENM  With  r\mdownarrow{}+gp  (D  (-1)))  THENA  Auto) 

---

Home Index