---

Step * 1 2 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. 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 ∈ ℤ
BY
{ (All (RepUR ``int-minus-comparison-inc``) THEN Auto') }

---

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.  u  :  \{n  +  1...\}  \mtimes{}  M@i
7.  x1  :  \{n  +  1...\}  \mtimes{}  M@i
8.  (int-minus-comparison-inc(\mlambda{}p.(fst(p)))  x1  u)  =  0@i
\mvdash{}  (int-minus-comparison-inc(\mlambda{}p.(fst(p)))  u  ((\mlambda{}x,y.  y)  x1  u))  =  0


By

---

Latex:
(All  (RepUR  ``int-minus-comparison-inc``)  THEN  Auto')

---

Home Index