(4steps total) PrintForm Definitions mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: firstn append
  L1,L2:Top List, n:(||L1||+1). firstn(n;L1 @ L2) ~ firstn(n;L1)
By: InductionOnList THEN RecUnfold `firstn` 0 THEN Reduce 0

Generated subgoals:

1 1. Top List
  L2:Top List, n:1.
  (Case of L2
  (Canil  nil
  (Caa.as'  if 0<n [a / firstn(n-1;as')] else nil fi) ~ nil
1 step
2 1. Top List
2. u : Top
3. v : Top List
4. L2:Top List, n:(||v||+1). firstn(n;v @ L2) ~ firstn(n;v)
  L2:Top List, n:(||v||+1+1).
  if 0<n [u / firstn(n-1;v @ L2)] else nil fi ~ if 0<n [u / firstn(n-1;v)]
  if 0<n [u / firstn(n-1;v @ L2)] else nil fi ~ else nil fi
2 steps

About:
listconsnillist_ind
ifthenelsenatural_numberaddsubtractsqequaltopall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(4steps total) PrintForm Definitions mb event system 1 Sections EventSystems Doc