---

Step * 2 of Lemma select-front-as-reduce


1. n : ℕ
2. u : Top
3. v : Top List
4. reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];v) ~ rev(firstn(n + 1;v))
⊢ if ||reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];v)|| <z n + 1
then reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];v) @ [u]
else tl(reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];v)) @ [u]
fi  ~ rev(firstn(n + 1;[u / v]))
BY
{ RWO "4" 0
THEN AutoBoolCase ⌜||v|| ≤z n + 1⌝
⋅
THEN (RWO "length-reverse" 0 THENA Auto)
THEN (SplitOnConclITE THENA Auto) }

1
.....truecase..... 
1. n : ℕ
2. u : Top
3. v : Top List
4. reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];v) ~ rev(firstn(n + 1;v))
5. ||v|| ≤ (n + 1)
6. ||firstn(n + 1;v)|| < n + 1
⊢ rev(firstn(n + 1;v)) @ [u] ~ rev(firstn(n + 1;[u / v]))

2
.....falsecase..... 
1. n : ℕ
2. u : Top
3. v : Top List
4. reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];v) ~ rev(firstn(n + 1;v))
5. ||v|| ≤ (n + 1)
6. (n + 1) ≤ ||firstn(n + 1;v)||
⊢ tl(rev(firstn(n + 1;v))) @ [u] ~ rev(firstn(n + 1;[u / v]))

3
.....truecase..... 
1. n : ℕ
2. u : Top
3. v : Top List
4. ¬(||v|| ≤ (n + 1))
5. reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];v) ~ rev(firstn(n + 1;v))
6. ||firstn(n + 1;v)|| < n + 1
⊢ rev(firstn(n + 1;v)) @ [u] ~ rev(firstn(n + 1;[u / v]))

4
.....falsecase..... 
1. n : ℕ
2. u : Top
3. v : Top List
4. ¬(||v|| ≤ (n + 1))
5. reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];v) ~ rev(firstn(n + 1;v))
6. (n + 1) ≤ ||firstn(n + 1;v)||
⊢ tl(rev(firstn(n + 1;v))) @ [u] ~ rev(firstn(n + 1;[u / v]))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  u  :  Top
3.  v  :  Top  List
4.  reduce(\mlambda{}u,x.  if  ||x||  <z  n  +  1  then  x  @  [u]  else  tl(x)  @  [u]  fi  ;[];v)  \msim{}  rev(firstn(n  +  1;v))
\mvdash{}  if  ||reduce(\mlambda{}u,x.  if  ||x||  <z  n  +  1  then  x  @  [u]  else  tl(x)  @  [u]  fi  ;[];v)||  <z  n  +  1
then  reduce(\mlambda{}u,x.  if  ||x||  <z  n  +  1  then  x  @  [u]  else  tl(x)  @  [u]  fi  ;[];v)  @  [u]
else  tl(reduce(\mlambda{}u,x.  if  ||x||  <z  n  +  1  then  x  @  [u]  else  tl(x)  @  [u]  fi  ;[];v))  @  [u]
fi    \msim{}  rev(firstn(n  +  1;[u  /  v]))


By

---

Latex:
RWO  "4"  0
THEN  AutoBoolCase  \mkleeneopen{}||v||  \mleq{}z  n  +  1\mkleeneclose{}
\mcdot{}
THEN  (RWO  "length-reverse"  0  THENA  Auto)
THEN  (SplitOnConclITE  THENA  Auto)

---

Home Index