---

Step * of Lemma firstn-append

∀[L1,L2:Top List]. ∀[n:ℕ].  (firstn(n;L1 @ L2) ~ if n ≤z ||L1|| then firstn(n;L1) else L1 @ firstn(n - ||L1||;L2) fi )
BY
{ (InductionOnList THEN RecUnfold `firstn` 0 THEN Reduce 0) }

1
∀[L2:Top List]. ∀[n:ℕ].
  (case L2 of [] => [] | a::as' => if 0 <z n then [a / firstn(n - 1;as')] else [] fi  esac ~ if n ≤z 0
  then []
  else case L2 of [] => [] | a::as' => if 0 <z n - 0 then [a / firstn(n - 0 - 1;as')] else [] fi  esac
  fi )

2
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 )

---

Latex:

---

Latex:
\mforall{}[L1,L2:Top  List].  \mforall{}[n:\mBbbN{}].
    (firstn(n;L1  @  L2)  \msim{}  if  n  \mleq{}z  ||L1||  then  firstn(n;L1)  else  L1  @  firstn(n  -  ||L1||;L2)  fi  )


By

---

Latex:
(InductionOnList  THEN  RecUnfold  `firstn`  0  THEN  Reduce  0)

---

Home Index