---

Step * 2 2 2 2 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
⊢ let L1,L2 = split-maximal-consecutive(λp.(fst(p));[<u1, u2> / v]) 
  in eval n' = fst(last(L1)) in
     <[<n, k2> / L1], n', L2> ∈ {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 + 1...}\000C × M) List)))
                                 ∧ (n < n ⇒ ((↑null(out)) ∧ (L' = [<u1, u2> / v] ∈ (({n + 1...} × M) List))))} 
BY
{ (GenConclAtAddr [2;1]
   THEN (D -2 THEN D -3)
   THEN All Reduce
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (Assert sorted-by(λx,y. fst(x) < fst(y);v2 @ v3) BY
               Auto)
   THEN (RWO "sorted-by-append" (-1) THENA Auto)
   THEN SplitAndHyps) }

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))
⊢ <[<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))))} 

---

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
\mvdash{}  let  L1,L2  =  split-maximal-consecutive(\mlambda{}p.(fst(p));[<u1,  u2>  /  v]) 
    in  eval  n'  =  fst(last(L1))  in
          <[<n,  k2>  /  L1],  n',  L2>  \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>)  =  (out  \000C@  L')))
                                                                  \mwedge{}  (n  <  n  {}\mRightarrow{}  ((\muparrow{}null(out))  \mwedge{}  (L'  =  [<u1,  u2>  /  v])))\} 


By

---

Latex:
(GenConclAtAddr  [2;1]
  THEN  (D  -2  THEN  D  -3)
  THEN  All  Reduce
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (Assert  sorted-by(\mlambda{}x,y.  fst(x)  <  fst(y);v2  @  v3)  BY
                          Auto)
  THEN  (RWO  "sorted-by-append"  (-1)  THENA  Auto)
  THEN  SplitAndHyps)

---

Home Index