Nuprl - Proof: primrec add 2 1

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

By:	MoveToConcl -1 THEN GenConcl (primrec(m;b;c) = b') THEN Try (ExtWith [`z'] [(n+m)TT])

Generated subgoal:

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

About:

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