Nuprl - Proof: primrec add

(8steps total) PrintForm Definitions mb nat Sections MarkB generic Doc

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

T:Type, n,m:

, b:T, c:(

(n+m)

T).

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

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

By:	RepeatFor 2 (Analyze 0) THEN NatInd -1

Generated subgoals:

1 1. T : Type
2. m :
3. b : T
4. c : (0+m)TT
primrec(0+m;b;c) = primrec(0;primrec(m;b;c);i,t. c(i+m,t))
2 steps

2 1. T : Type
2. n :
3. 0<n
4. m:, b:T, c:((n-1+m)TT).
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)TT
primrec(n+m;b;c) = primrec(n;primrec(m;b;c);i,t. c(i+m,t))
5 steps

About:

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

(8steps total) PrintForm Definitions mb nat Sections MarkB generic Doc

1	1. T : Type 2. m : 3. b : T 4. c : (0+m)TT primrec(0+m;b;c) = primrec(0;primrec(m;b;c);i,t. c(i+m,t))	2 steps
2	1. T : Type 2. n : 3. 0<n 4. m:, b:T, c:((n-1+m)TT). 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)TT primrec(n+m;b;c) = primrec(n;primrec(m;b;c);i,t. c(i+m,t))	5 steps