---

Step * 2 of Lemma omralist_cases


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]})
BY
{ % This is too fiddly. Need better way of doing this % 
AbReduceIf (\e t.not is_term `oalist` (subterm t 1)) (-1) 
THEN Unfold `omralist` 0 THEN Trivial }

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  \mforall{}Q:|oal(g\mdownarrow{}oset;r\mdownarrow{}+gp)|  {}\mrightarrow{}  \mBbbP{}
          (Q[[]]
          {}\mRightarrow{}  (\mforall{}ws:|oal(g\mdownarrow{}oset;r\mdownarrow{}+gp)|.  \mforall{}x:|(g\mdownarrow{}oset)|.  \mforall{}y:|r\mdownarrow{}+gp|.
                      ((\muparrow{}before(x;map(\mlambda{}x.(fst(x));ws)))  {}\mRightarrow{}  (\mneg{}(y  =  e))  {}\mRightarrow{}  Q[[<x,  y>  /  ws]]))
          {}\mRightarrow{}  \{\mforall{}ws:|oal(g\mdownarrow{}oset;r\mdownarrow{}+gp)|.  Q[ws]\})
\mvdash{}  \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:
\%  This  is  too  fiddly.  Need  better  way  of  doing  this  \% 
AbReduceIf  (\mbackslash{}e  t.not  is\_term  `oalist`  (subterm  t  1))  (-1) 
THEN  Unfold  `omralist`  0  THEN  Trivial

---

Home Index