---

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


1. T : Type
2. x : ℕ
3. v : ℕ@i
⊢ ∀L:(T × ℕv List × (ℕv List)) List. ((v ≤ x) ⇒ (||L|| ≤ x) ⇒ (lg-remove(L;x) ~ L))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``lg-remove`` 0 THEN Subst' firstn(x;L) @ nth_tl(x + 1;L) ~ L 0)⋅ }

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

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
⊢ map(λtr.let lbl,in,out = tr in 
          <lbl
          , map(λx@0.if x@0 ≤z x then x@0 else x@0 - 1 fi ;filter(λx@0.(¬b(x@0 =z x));in))
          , map(λx@0.if x@0 ≤z x then x@0 else x@0 - 1 fi ;filter(λx@0.(¬b(x@0 =z x));out))>;L) ~ L

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  \mBbbN{}
3.  v  :  \mBbbN{}@i
\mvdash{}  \mforall{}L:(T  \mtimes{}  \mBbbN{}v  List  \mtimes{}  (\mBbbN{}v  List))  List.  ((v  \mleq{}  x)  {}\mRightarrow{}  (||L||  \mleq{}  x)  {}\mRightarrow{}  (lg-remove(L;x)  \msim{}  L))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``lg-remove``  0  THEN  Subst'  firstn(x;L)  @  nth\_tl(x  +  1;L)  \msim{}  L  0)\mcdot{}

---

Home Index