---

Step * 1 1 1 3 1 of Lemma es-causl_weakening_p-locl


1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. causal-predecessor(es;p)@i
4. n : ℤ@i
5. 0 < n
⊢ ∀e,e':E.
    (((↑isl(primrec(n;λx.(inl x);λi,g,x. if isl(g x) then p outl(g x) else g x fi ) e'))
    c∧ (e = outl(primrec(n;λx.(inl x);λi,g,x. if isl(g x) then p outl(g x) else g x fi ) e') ∈ E))
    ⇒ (e < e')) ∈ ℙ
BY
{ Folds ``can-apply do-apply`` 0 }

1
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. causal-predecessor(es;p)@i
4. n : ℤ@i
5. 0 < n
⊢ ∀e,e':E.
    (((↑can-apply(primrec(n;λx.(inl x);λi,g,x. if can-apply(g;x) then p do-apply(g;x) else g x fi );e'))
    c∧ (e = do-apply(primrec(n;λx.(inl x);λi,g,x. if can-apply(g;x) then p do-apply(g;x) else g x fi );e') ∈ E))
    ⇒ (e < e')) ∈ ℙ

---

Latex:



1.  es  :  EO@i'
2.  p  :  E  {}\mrightarrow{}  (E  +  Top)@i
3.  causal-predecessor(es;p)@i
4.  n  :  \mBbbZ{}@i
5.  0  <  n
\mvdash{}  \mforall{}e,e':E.
        (((\muparrow{}isl(primrec(n;\mlambda{}x.(inl  x);\mlambda{}i,g,x.  if  isl(g  x)  then  p  outl(g  x)  else  g  x  fi  )  e'))
        c\mwedge{}  (e  =  outl(primrec(n;\mlambda{}x.(inl  x);\mlambda{}i,g,x.  if  isl(g  x)  then  p  outl(g  x)  else  g  x  fi  )  e')))
        {}\mRightarrow{}  (e  <  e'))  \mmember{}  \mBbbP{}


By

Folds  ``can-apply  do-apply``  0

---

Home Index