Nuprl - Proof: primrec add 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: primrec add 2

1. T : Type
2. n :

3. 0<n
4.

, b:T, c:(

(n-1+m)

T).
4. primrec(n-1+m;b;c) = primrec(n-1;primrec(m;b;c);

i,t. c(i+m,t))
5. m :

6. b : T
7. c :

(n+m)

primrec(n+m;b;c) = primrec(n;primrec(m;b;c);

i,t. c(i+m,t))

By:	InstHyp [m;b;c] 4

Generated subgoal:

1 8. primrec(n-1+m;b;c) = primrec(n-1;primrec(m;b;c);i,t. c(i+m,t))
primrec(n+m;b;c) = primrec(n;primrec(m;b;c);i,t. c(i+m,t))
4 steps

About:

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