---

Step * 2 2 2 2 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))
⊢ <[<n, k2> / v2], fst(last(v2)), v3> ∈ {tr:({n...} × M) List × n:{n...} × (({n + 1...} × M) List)| 
                                         let out,n',L' = tr in 
                                         sorted-by(λx,y. fst(x) < fst(y);L')
                                         ∧ (0 < ||out|| ⇒ ((n = n ∈ ℤ) ∧ (hd(out) = <n, k2> ∈ (ℕ × M))))
                                         ∧ ((n = n ∈ ℤ)
                                           ⇒ ([<n, k2>; [<u1, u2> / v]] = (out @ L') ∈ (({n...} × M) List)))
                                         ∧ (n < n ⇒ (insert-ordered-message([<u1, u2> / v];<n, k2>) = (out @ L') ∈ (({n\000C + 1...} × M) List)))
                                         ∧ (n < n ⇒ ((↑null(out)) ∧ (L' = [<u1, u2> / v] ∈ (({n + 1...} × M) List))))} 
BY
{ (At ⌈Type⌉ MemTypeCD⋅ THEN Reduce 0 THEN Auto) }

1
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

---

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{}  <[<n,  k2>  /  v2],  fst(last(v2)),  v3>  \mmember{}  \{tr:(\{n...\}  \mtimes{}  M)  List  \mtimes{}  n:\{n...\}  \mtimes{}  ((\{n  +  1...\}  \mtimes{}  M)  List)| 
                                                                                  let  out,n',L'  =  tr  in 
                                                                                  sorted-by(\mlambda{}x,y.  fst(x)  <  fst(y);L')
                                                                                  \mwedge{}  (0  <  ||out||  {}\mRightarrow{}  ((n  =  n)  \mwedge{}  (hd(out)  =  <n,  k2>)))
                                                                                  \mwedge{}  ((n  =  n)  {}\mRightarrow{}  ([<n,  k2>  [<u1,  u2>  /  v]]  =  (out  @  L')))
                                                                                  \mwedge{}  (n  <  n  {}\mRightarrow{}  (insert-ordered-message([<u1,  u2>  /  v];<n,  k2>)\000C  =  (out  @  L')))
                                                                                  \mwedge{}  (n  <  n  {}\mRightarrow{}  ((\muparrow{}null(out))  \mwedge{}  (L'  =  [<u1,  u2>  /  v])))\} 


By

---

Latex:
(At  \mkleeneopen{}Type\mkleeneclose{}  MemTypeCD\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index