---

Step * of Lemma select-as-reduce

∀[n:ℕ]. ∀[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
{ ((D 0 THENA Auto)
   THEN (Assert ∀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 n then inl ||L|| else inr L[||L|| - n + 1]  fi ) BY
               (InductionOnList
                THEN Reduce 0
                THEN ((SplitOnConclITE THENA Auto)
                      THEN Try (RWO "4" 0⋅)
                      THEN Try (Complete (Auto))
                      THEN Repeat (((SplitOnConclITE THENA Auto)
                                    THEN Reduce 0
                                    THEN Try (EqCD)
                                    THEN Try (Complete (Auto')))))⋅))
   ) }

1
1. n : ℕ
2. u : Top
3. v : Top List
4. 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;v) ~ if ||v|| ≤z n
then inl ||v||
else inr v[||v|| - n + 1] 
fi 
5. n < ||v|| + 1
6. ||v|| ≤ n
7. ||v|| = n ∈ ℤ
⊢ u ~ [u / v][(||v|| + 1) - n + 1]

2
1. n : ℕ
2. u : Top
3. v : Top List
4. 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;v) ~ if ||v|| ≤z n
then inl ||v||
else inr v[||v|| - n + 1] 
fi 
5. n < ||v|| + 1
6. n < ||v||
⊢ v[||v|| - n + 1] ~ [u / v][(||v|| + 1) - n + 1]

3
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||

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \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:
((D  0  THENA  Auto)
  THEN  (Assert  \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  )  BY
                          (InductionOnList
                            THEN  Reduce  0
                            THEN  ((SplitOnConclITE  THENA  Auto)
                                        THEN  Try  (RWO  "4"  0\mcdot{})
                                        THEN  Try  (Complete  (Auto))
                                        THEN  Repeat  (((SplitOnConclITE  THENA  Auto)
                                                                    THEN  Reduce  0
                                                                    THEN  Try  (EqCD)
                                                                    THEN  Try  (Complete  (Auto')))))\mcdot{}))
  )

---

Home Index