Nuprl - Proof: primrec add 2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: primrec add 2 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))

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

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

By:	RecUnfold `primrec` 0 THEN Reduce 0 THEN Repeat (SplitOnConclITE THEN Try (Complete Auto))

Generated subgoal:

1 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)))
2 steps

About:

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