---

Step * 2 2 2 2 1 1 1 of Lemma process-ordered-message_wf

.....set predicate..... 
1. M : Type
2. n : ℕ
3. u1 : {n + 1...}
4. ¬n + 1 < u1
5. u2 : M
6. v : ({n + 1...} × M) List
7. sorted-by(λx,y. fst(x) < fst(y);[<u1, u2> / v])
8. k2 : M
9. v2 : {n + 1...} × M List+@i
10. v3 : ({n + 1...} × M) List@i
11. [<u1, u2> / v] = (v2 @ v3) ∈ (({n + 1...} × M) List)@i
12. split-maximal-consecutive(λp.(fst(p));[<u1, u2> / v])
= <v2, v3>
∈ {p:{n + 1...} × M List+ × (({n + 1...} × M) List)| [<u1, u2> / v] = ((fst(p)) @ (snd(p))) ∈ (({n + 1...} × M) List)} @\000Ci
13. sorted-by(λx,y. fst(x) < fst(y);v2)
14. sorted-by(λx,y. fst(x) < fst(y);v3)
15. ∀a:{n + 1...} × M. ((a ∈ v2) ⇒ (∀b∈v3.fst(a) < fst(b)))
16. ∀b:{n + 1...} × M. ((b ∈ v3) ⇒ fst(last(v2)) < fst(b))
17. v3 = v3 ∈ ({x:{n + 1...} × M| (x ∈ v3)}  List)
18. x1 : {n + 1...}@i
19. x2 : M@i
20. (<x1, x2> ∈ v3)@i
⊢ ((fst(last(v2))) + 1) ≤ x1
BY
{ ((FHyp (-5) [-1] THENM Reduce (-1)) THEN Auto') }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  M  :  Type
2.  n  :  \mBbbN{}
3.  u1  :  \{n  +  1...\}
4.  \mneg{}n  +  1  <  u1
5.  u2  :  M
6.  v  :  (\{n  +  1...\}  \mtimes{}  M)  List
7.  sorted-by(\mlambda{}x,y.  fst(x)  <  fst(y);[<u1,  u2>  /  v])
8.  k2  :  M
9.  v2  :  \{n  +  1...\}  \mtimes{}  M  List\msupplus{}@i
10.  v3  :  (\{n  +  1...\}  \mtimes{}  M)  List@i
11.  [<u1,  u2>  /  v]  =  (v2  @  v3)@i
12.  split-maximal-consecutive(\mlambda{}p.(fst(p));[<u1,  u2>  /  v])  =  <v2,  v3>@i
13.  sorted-by(\mlambda{}x,y.  fst(x)  <  fst(y);v2)
14.  sorted-by(\mlambda{}x,y.  fst(x)  <  fst(y);v3)
15.  \mforall{}a:\{n  +  1...\}  \mtimes{}  M.  ((a  \mmember{}  v2)  {}\mRightarrow{}  (\mforall{}b\mmember{}v3.fst(a)  <  fst(b)))
16.  \mforall{}b:\{n  +  1...\}  \mtimes{}  M.  ((b  \mmember{}  v3)  {}\mRightarrow{}  fst(last(v2))  <  fst(b))
17.  v3  =  v3
18.  x1  :  \{n  +  1...\}@i
19.  x2  :  M@i
20.  (<x1,  x2>  \mmember{}  v3)@i
\mvdash{}  ((fst(last(v2)))  +  1)  \mleq{}  x1


By

---

Latex:
((FHyp  (-5)  [-1]  THENM  Reduce  (-1))  THEN  Auto')

---

Home Index