---

Step * of Lemma insert-ordered-message_wf

∀[M:Type]. ∀[n:ℕ]. ∀[L:{L:({n + 1...} × M) List| sorted-by(λx,y. fst(x) < fst(y);L)} ]. ∀[x:{n + 1...} × M].
  (insert-ordered-message(L;x) ∈ {L:({n + 1...} × M) List| sorted-by(λx,y. fst(x) < fst(y);L)} )
BY
{ (ProveWfLemma THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
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. fst(x) < fst(y);insert-combine(int-minus-comparison-inc(λp.(fst(p)));λx,y. y;x;L))

---

Latex:

---

Latex:
\mforall{}[M:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[L:\{L:(\{n  +  1...\}  \mtimes{}  M)  List|  sorted-by(\mlambda{}x,y.  fst(x)  <  fst(y);L)\}  ].
\mforall{}[x:\{n  +  1...\}  \mtimes{}  M].
    (insert-ordered-message(L;x)  \mmember{}  \{L:(\{n  +  1...\}  \mtimes{}  M)  List|  sorted-by(\mlambda{}x,y.  fst(x)  <  fst(y);L)\}  )


By

---

Latex:
(ProveWfLemma  THEN  MemTypeCD  THEN  Auto)

---

Home Index