(14steps total) PrintForm Definitions hol prim rec Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hsimp rec wd 1 1 1

1. 'a : S
2. x : 'a
3. f : 'a  'a
4. n : 
5. fun : 'a
6. simp_rec_rel(fun,x,f,n+1)
  ncompose(f;n;x) = fun(n)


By: Unab [`hsimp_rec_rel`] THEN Simp THEN StrongAuto


Generated subgoal:

1 6. fun(0) = x
7. m:m<n+1  fun(m+1) = f(fun(m))
  ncompose(f;n;x) = fun(n)

8 steps

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

(14steps total) PrintForm Definitions hol prim rec Sections HOLlib Doc