---

Step * 2 of Lemma firstn-append


1. u : Top
2. v : Top List
3. ∀[L2:Top List]. ∀[n:ℕ].  (firstn(n;v @ L2) ~ if n ≤z ||v|| then firstn(n;v) else v @ firstn(n - ||v||;L2) fi )
⊢ ∀[L2:Top List]. ∀[n:ℕ].
    (if 0 <z n then [u / firstn(n - 1;v @ L2)] else [] fi  ~ if n ≤z ||v|| + 1
    then if 0 <z n then [u / firstn(n - 1;v)] else [] fi 
    else [u / 
          (v
          @ case L2 of 
              [] => [] 
              a::as' =>
               if 0 <z n - ||v|| + 1 then [a / firstn(n - ||v|| + 1 - 1;as')] else [] fi  
            esac)]
    fi )
BY
{ ((UnivCD THENA Auto)
   THEN RepeatFor 2 ((SplitOnConclITE THENA Auto))
   THEN Try (Complete (Auto'))
   THEN (RWO "3" 0 THENA Auto)
   THEN (SplitOnConclITE THENA Auto)
   THEN Try (Complete (Auto'))
   THEN RepeatFor 2 ((EqCD THEN Try (Trivial)))
   THEN RW (AddrC [1] RecUnfoldTopAbC) 0
   THEN Subst' n - 1 - ||v|| ~ n - ||v|| + 1 0
   THEN Auto') }

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}[L2:Top  List].  \mforall{}[n:\mBbbN{}].
          (firstn(n;v  @  L2)  \msim{}  if  n  \mleq{}z  ||v||  then  firstn(n;v)  else  v  @  firstn(n  -  ||v||;L2)  fi  )
\mvdash{}  \mforall{}[L2:Top  List].  \mforall{}[n:\mBbbN{}].
        (if  0  <z  n  then  [u  /  firstn(n  -  1;v  @  L2)]  else  []  fi    \msim{}  if  n  \mleq{}z  ||v||  +  1
        then  if  0  <z  n  then  [u  /  firstn(n  -  1;v)]  else  []  fi 
        else  [u  / 
                    (v
                    @  case  L2  of 
                            []  =>  [] 
                            a::as'  =>
                              if  0  <z  n  -  ||v||  +  1  then  [a  /  firstn(n  -  ||v||  +  1  -  1;as')]  else  []  fi   
                        esac)]
        fi  )


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepeatFor  2  ((SplitOnConclITE  THENA  Auto))
  THEN  Try  (Complete  (Auto'))
  THEN  (RWO  "3"  0  THENA  Auto)
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  (Complete  (Auto'))
  THEN  RepeatFor  2  ((EqCD  THEN  Try  (Trivial)))
  THEN  RW  (AddrC  [1]  RecUnfoldTopAbC)  0
  THEN  Subst'  n  -  1  -  ||v||  \msim{}  n  -  ||v||  +  1  0
  THEN  Auto')

---

Home Index