---

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


1. M : Type
2. n : ℕ
3. u1 : {n + 1...}
4. u2 : M
5. v : ({n + 1...} × M) List
6. sorted-by(λx,y. fst(x) < fst(y);[<u1, u2> / v])
7. k2 : M
8. n + 1 < u1
⊢ <[<n, k2>], n + 1, [<u1, u2> / v]> ∈ {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 + \000C1...} × M) List)))
                                      ∧ (n < n ⇒ ((↑null(out)) ∧ (L' = [<u1, u2> / v] ∈ (({n + 1...} × M) List))))} 
BY
{ (DupHyp 6
   THEN (RWO "sorted-by-cons" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN (Assert v ∈ ({n + 2...} × M) List BY
               ((UseListSubtype THENA Auto)
                THEN D -1
                THEN Auto
                THEN With ⌈i⌉ (D (-6))⋅
                THEN Auto
                THEN D -2
                THEN RevHypSubst (-2) (-1)
                THEN Auto
                THEN Reduce (-1)
                THEN Auto'))
   THEN At ⌈Type⌉ MemTypeCD⋅
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  M  :  Type
2.  n  :  \mBbbN{}
3.  u1  :  \{n  +  1...\}
4.  u2  :  M
5.  v  :  (\{n  +  1...\}  \mtimes{}  M)  List
6.  sorted-by(\mlambda{}x,y.  fst(x)  <  fst(y);[<u1,  u2>  /  v])
7.  k2  :  M
8.  n  +  1  <  u1
\mvdash{}  <[<n,  k2>],  n  +  1,  [<u1,  u2>  /  v]>  \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:
(DupHyp  6
  THEN  (RWO  "sorted-by-cons"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  (Assert  v  \mmember{}  (\{n  +  2...\}  \mtimes{}  M)  List  BY
                          ((UseListSubtype  THENA  Auto)
                            THEN  D  -1
                            THEN  Auto
                            THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  (-6))\mcdot{}
                            THEN  Auto
                            THEN  D  -2
                            THEN  RevHypSubst  (-2)  (-1)
                            THEN  Auto
                            THEN  Reduce  (-1)
                            THEN  Auto'))
  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  MemTypeCD\mcdot{}
  THEN  Reduce  0
  THEN  Auto)

---

Home Index