Nuprl - Proof: hsimp rec wd 1 1 1 1 1 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hsimp rec wd 1 1 1 1 1 1 2

1. 'a : S
2. x : 'a
3. f : 'a

'a
4. fun :

'a
5. fun(0) = x
6. n :

7. 0<n
8.

. m<n+1

fun(m+1) = f(fun(m))
9. fun(n-1+1) = f(fun(n-1))
10. ncompose(f;n-1;x) = fun(n-1)

f(ncompose(f;n-1;x)) = fun(n)

By:	On [0;9;10] ArithSimp THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoal:

1 9. fun(n) = f(fun(-1+n))
10. ncompose(f;-1+n;x) = fun(-1+n)
f(ncompose(f;-1+n;x)) = fun(n)
3 steps

About:

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