---

Step * 1 4 of Lemma insert-ordered-message_wf


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
6. sorted-by(λx,y. 0 < int-minus-comparison-inc(λp.(fst(p))) x 
                       y;insert-combine(int-minus-comparison-inc(λp.(fst(p)));λx,y. y;x;L))
⊢ sorted-by(λx,y. fst(x) < fst(y);insert-combine(int-minus-comparison-inc(λp.(fst(p)));λx,y. y;x;L))
BY
{ (MoveToConcl (-1) THEN (GenConclTerm ⌈insert-combine(int-minus-comparison-inc(λp.(fst(p)));λx,y. y;x;L)⌉ ⋅ THENA Auto)\000C) }

1
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
6. v : ({n + 1...} × M) List@i
7. insert-combine(int-minus-comparison-inc(λp.(fst(p)));λx,y. y;x;L) = v ∈ (({n + 1...} × M) List)@i
⊢ sorted-by(λx,y. 0 < int-minus-comparison-inc(λp.(fst(p))) x y;v) ⇒ sorted-by(λx,y. fst(x) < fst(y);v)

---

Latex:

---

Latex:

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
6.  sorted-by(\mlambda{}x,y.  0  <  int-minus-comparison-inc(\mlambda{}p.(fst(p)))  x 
                                              y;insert-combine(int-minus-comparison-inc(\mlambda{}p.(fst(p)));\mlambda{}x,y.  y;x;L))
\mvdash{}  sorted-by(\mlambda{}x,y.  fst(x)  <  fst(y);insert-combine(int-minus-comparison-inc(\mlambda{}p.(fst(p)));\mlambda{}x,y.  y;x;L))


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}insert-combine(int-minus-comparison-inc(\mlambda{}p.(fst(p)));\mlambda{}x,y.  y;x;L)\mkleeneclose{}  \mcdot{}  THENA  Auto\000C)
  )

---

Home Index