Nuprl - Proof: fun exp add

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

T:Type, n,m:

, f:(T

T). f^n+m = f^n o f^m

By:	(Auto THEN RWO Thm* n:, h,f:(TT). f^n o h = primrec(n;h;i,g. f o g) 0 (THEN (Unfold `fun_exp` 0 (THEN (Inst (Thm* n,m:, b:T, c:((n+m)TT). (Thm* primrec(n+m;b;c) = primrec(n;primrec(m;b;c);i,t. c(i+m,t)) ([TT;n;m;x.x;i,g. f o g]) THEN (Reduce -1)

Generated subgoals:

None

About:

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