---

Step * 3 of Lemma select-as-reduce


1. n : ℕ
2. ∀L:Top List
     (reduce(λu,x. case x of inl(i) => if (i =z n) then inr u  else inl (i + 1) fi  | inr(u) => x;inl 0;L) ~ if ||L|| ≤z\000C n
     then inl ||L||
     else inr L[||L|| - n + 1] 
     fi )
⊢ ∀[L:Top List]
    L[||L|| - n + 1] 
    ~ outr(reduce(λu,x. case x of inl(i) => if (i =z n) then inr u  else inl (i + 1) fi  | inr(u) => x;inl 0;L)) 
    supposing n < ||L||
BY
{ xxx((UnivCD THENA Auto) THEN (RWO "2" 0 THENA Auto) THEN (SplitOnConclITE THENA Auto) THEN Reduce 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  \mforall{}L:Top  List
          (reduce(\mlambda{}u,x.  case  x
                                      of  inl(i)  =>
                                      if  (i  =\msubz{}  n)  then  inr  u    else  inl  (i  +  1)  fi 
                                      |  inr(u)  =>
                                      x;inl  0;L)  \msim{}  if  ||L||  \mleq{}z  n  then  inl  ||L||  else  inr  L[||L||  -  n  +  1]    fi  )
\mvdash{}  \mforall{}[L:Top  List]
        L[||L||  -  n  +  1]  \msim{}  outr(reduce(\mlambda{}u,x.  case  x
                                                                                  of  inl(i)  =>
                                                                                  if  (i  =\msubz{}  n)  then  inr  u    else  inl  (i  +  1)  fi 
                                                                                  |  inr(u)  =>
                                                                                  x;inl  0;L)) 
        supposing  n  <  ||L||


By

---

Latex:
xxx((UnivCD  THENA  Auto)
        THEN  (RWO  "2"  0  THENA  Auto)
        THEN  (SplitOnConclITE  THENA  Auto)
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index