---

Step * 1 3 of Lemma insert-ordered-message_wf

.....antecedent..... 
1. M : Type
2. n : ℕ
3. L : ({n + 1...} × M) List
4. sorted-by(λx,y. fst(x) < fst(y);L)
5. x : {n + 1...} × M
⊢ sorted-by(λx,y. 0 < int-minus-comparison-inc(λp.(fst(p))) x y;L)
BY
{ (RepeatFor 2 (ParallelOp -2) THEN ParallelLast THEN All Reduce THEN RepUR ``int-minus-comparison-inc`` 0 THEN Auto') }

---

Latex:

---

Latex:
.....antecedent..... 
1.  M  :  Type
2.  n  :  \mBbbN{}
3.  L  :  (\{n  +  1...\}  \mtimes{}  M)  List
4.  sorted-by(\mlambda{}x,y.  fst(x)  <  fst(y);L)
5.  x  :  \{n  +  1...\}  \mtimes{}  M
\mvdash{}  sorted-by(\mlambda{}x,y.  0  <  int-minus-comparison-inc(\mlambda{}p.(fst(p)))  x  y;L)


By

---

Latex:
(RepeatFor  2  (ParallelOp  -2)
  THEN  ParallelLast
  THEN  All  Reduce
  THEN  RepUR  ``int-minus-comparison-inc``  0
  THEN  Auto')

---

Home Index