Nuprl - Proof: primrec add 2 1 1 1

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

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)

T
8. b' : T
9. primrec(m;b;c) = b'
10. primrec(n-1+m;b;c) = primrec(n-1;b';

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

n+m = 0
12.

n = 0

c(n+m-1,primrec(n+m-1;b;c)) = c(n-1+m,primrec(n-1;b';

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

By:	Subst' (n+m-1 = n-1+m) 0

Generated subgoal:

1 c(n-1+m,primrec(n-1+m;b;c)) = c(n-1+m,primrec(n-1;b';i,t. c(i+m,t)))
1 step

About:

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