---

Step * 1 of Lemma insert-ordered-message_wf

.....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))
BY
{ (InstLemma `insert-combine-sorted-by` [⌈{n + 1...} × M⌉;⌈int-minus-comparison-inc(λp.(fst(p)))⌉;⌈λx,y. y⌉;⌈L⌉;⌈x⌉]⋅
   THENA Auto
   ) }

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. u : {n + 1...} × M@i
7. x1 : {n + 1...} × M@i
8. z : {n + 1...} × M@i
9. 0 < int-minus-comparison-inc(λp.(fst(p))) x1 u@i
10. 0 < int-minus-comparison-inc(λp.(fst(p))) u z@i
⊢ 0 < int-minus-comparison-inc(λp.(fst(p))) x1 z

2
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. u : {n + 1...} × M@i
7. x1 : {n + 1...} × M@i
8. (int-minus-comparison-inc(λp.(fst(p))) x1 u) = 0 ∈ ℤ@i
⊢ (int-minus-comparison-inc(λp.(fst(p))) u ((λx,y. y) x1 u)) = 0 ∈ ℤ

3
.....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)

4
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))

---

Latex:

---

Latex:
.....set  predicate..... 
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.  fst(x)  <  fst(y);insert-combine(int-minus-comparison-inc(\mlambda{}p.(fst(p)));\mlambda{}x,y.  y;x;L))


By

---

Latex:
(InstLemma  `insert-combine-sorted-by`  [\mkleeneopen{}\{n  +  1...\}  \mtimes{}  M\mkleeneclose{};\mkleeneopen{}int-minus-comparison-inc(\mlambda{}p.(fst(p)))\mkleeneclose{};
  \mkleeneopen{}\mlambda{}x,y.  y\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THENA  Auto
  )

---

Home Index