---

Step * 1 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. e : E@i
5. e' : E@i
6. n : ℕ+@i
7. p-graph(E;p^n) e' e@i
⊢ (e < e')
BY
{ (((MoveToConcl (-3)) THEN MoveToConcl (-2)) THEN NatPlusInd (-1)) }

1
.....basecase..... 
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. causal-predecessor(es;p)@i
4. n : ℕ+@i
⊢ ∀e,e':E.  ((p-graph(E;p^1) e' e) ⇒ (e < e'))

2
.....upcase..... 
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. causal-predecessor(es;p)@i
4. n : ℤ@i
5. 0 < n
6. ∀e,e':E.  ((p-graph(E;p^n) e' e) ⇒ (e < e'))@i
⊢ ∀e,e':E.  ((p-graph(E;p^n + 1) e' e) ⇒ (e < e'))

3
.....wf..... 
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.  ((p-graph(E;p^n) e' e) ⇒ (e < e')) ∈ ℙ

4
.....wf..... 
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. causal-predecessor(es;p)@i
4. n : ℕ+@i
⊢ ℕ+ ∈ Type

5
.....wf..... 
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.  ((p-graph(E;p^n) e' e) ⇒ (e < e')) ∈ ℕ+ ─→ ℙ

---

Latex:



1.  es  :  EO@i'
2.  p  :  E  {}\mrightarrow{}  (E  +  Top)@i
3.  causal-predecessor(es;p)@i
4.  e  :  E@i
5.  e'  :  E@i
6.  n  :  \mBbbN{}\msupplus{}@i
7.  p-graph(E;p\^{}n)  e'  e@i
\mvdash{}  (e  <  e')


By

(((MoveToConcl  (-3))  THEN  MoveToConcl  (-2))  THEN  NatPlusInd  (-1))

---

Home Index