---

Step * 1 1 1 5 1 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. ∀e,e':E.  ((p-graph(E;p^1) e' e) ⇒ (e < e'))
6. ∀n:ℕ+. ((∀e,e':E.  ((p-graph(E;p^n) e' e) ⇒ (e < e'))) ⇒ (∀e,e':E.  ((p-graph(E;p^n + 1) e' e) ⇒ (e < e'))))
⊢ λ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')) ∈ ℕ+ ─→ ℙ
BY
{ (RepeatFor 7 ((MemCD THENA Auto)) THEN Try (Complete (Auto))) }

1
.....subterm..... T:t
1:n
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. causal-predecessor(es;p)@i
4. n : ℕ+@i
5. ∀e,e':E.  ((p-graph(E;p^1) e' e) ⇒ (e < e'))
6. ∀n:ℕ+. ((∀e,e':E.  ((p-graph(E;p^n) e' e) ⇒ (e < e'))) ⇒ (∀e,e':E.  ((p-graph(E;p^n + 1) e' e) ⇒ (e < e'))))
7. n1 : ℕ+@i
8. e : E@i
9. e' : E@i
⊢ primrec(n1;λx.(inl x);λi,g,x. if can-apply(g;x) then p do-apply(g;x) else g x fi ) ∈ E ─→ (Top + Top)

---

Latex:



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


By

(RepeatFor  7  ((MemCD  THENA  Auto))  THEN  Try  (Complete  (Auto)))

---

Home Index