---

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

.....equality..... 
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
⊢ firstn(x;L) @ nth_tl(x + 1;L) ~ L
BY
{ (RWO "nth_tl_is_nil" 0 THENA Auto)⋅ }

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

2
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
⊢ firstn(x;L) @ [] ~ L

---

Latex:

---

Latex:
.....equality..... 
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{}  firstn(x;L)  @  nth\_tl(x  +  1;L)  \msim{}  L


By

---

Latex:
(RWO  "nth\_tl\_is\_nil"  0  THENA  Auto)\mcdot{}

---

Home Index