Nuprl - Proof: primrec wf

(4steps 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 wf

T:Type, n:

, b:T, c:(

T). primrec(n;b;c)

By:	RepeatFor 2 (Analyze 0) THEN NatInd -1 THEN RecUnfold `primrec` 0 THEN Reduce 0

Generated subgoals:

1 1. T : Type
2. b : T
3. 0TT
  b  T
Auto

2 1. T : Type
2. n :
3. 0<n
4. b:T, c:((n-1)TT). primrec(n-1;b;c)  T
5. b : T
6. c : nTT
  if n=0 b else c(n-1,primrec(n-1;b;c)) fi  T
2 steps

About:

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

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

1	1. T : Type 2. b : T 3. 0TT b T	Auto
2	1. T : Type 2. n : 3. 0<n 4. b:T, c:((n-1)TT). primrec(n-1;b;c) T 5. b : T 6. c : nTT if n=0 b else c(n-1,primrec(n-1;b;c)) fi T	2 steps