---

Step * 1 2 1 1 1 of Lemma lg-remove-noop


1. T : Type
2. x : ℕ
3. v : ℕ@i
4. L : (T × ℕv List × (ℕv List)) List@i
5. v ≤ x@i
6. ||L|| ≤ x@i
⊢ ||L|| ≤ (x + 1)
BY
{ Auto' }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  \mBbbN{}
3.  v  :  \mBbbN{}@i
4.  L  :  (T  \mtimes{}  \mBbbN{}v  List  \mtimes{}  (\mBbbN{}v  List))  List@i
5.  v  \mleq{}  x@i
6.  ||L||  \mleq{}  x@i
\mvdash{}  ||L||  \mleq{}  (x  +  1)


By

---

Latex:
Auto'

---

Home Index