Step * of Lemma firstn-append

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

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

2
1. Top
2. Top List
3. ∀[L2:Top List]. ∀[n:ℕ].  (firstn(n;v L2) if n ≤||v|| then firstn(n;v) else firstn(n ||v||;L2) fi )
⊢ ∀[L2:Top List]. ∀[n:ℕ].
    (if 0 <then [u firstn(n 1;v L2)] else [] fi  if n ≤||v|| 1
    then if 0 <then [u firstn(n 1;v)] else [] fi 
    else [u 
          (v
          case L2 of 
              [] => [] 
              a::as' =>
               if 0 <||v|| then [a firstn(n ||v|| 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