---

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


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∈v2.(∀b∈v3.(λx,y. fst(x) < fst(y)) a b))
⊢ v3 ∈ ({(fst(last(v2))) + 1...} × M) List
BY
{ ((Reduce (-1) THEN (RWO "l_all_iff" (-1) THENA Auto))
   THEN (InstHyp [⌈last(v2)⌉] (-1)⋅ THENA Auto)
   THEN (RWO "l_all_iff" (-1) THENA Auto)
   THEN UseListSubtype
   THEN Auto) }

1
.....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

---

Latex:

---

Latex:

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\mmember{}v2.(\mforall{}b\mmember{}v3.(\mlambda{}x,y.  fst(x)  <  fst(y))  a  b))
\mvdash{}  v3  \mmember{}  (\{(fst(last(v2)))  +  1...\}  \mtimes{}  M)  List


By

---

Latex:
((Reduce  (-1)  THEN  (RWO  "l\_all\_iff"  (-1)  THENA  Auto))
  THEN  (InstHyp  [\mkleeneopen{}last(v2)\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (RWO  "l\_all\_iff"  (-1)  THENA  Auto)
  THEN  UseListSubtype
  THEN  Auto)

---

Home Index