Nuprl - Proof: factorial tail via iter step 1

(5steps total) PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: factorial tail via iter step 1

1. m :

2. k :

3. 1

m
4. m

k
5. k' :

6. m' :

7. k' = k-1
8. m' = m-1

(

i:{k-m..k

}. i+1) = k

k'!m'

By:	Rewrite by Thm* f:(AAA), u:A, a,b:, e:({a..b}A). Thm* a<b Thm* Thm* (Iter(f;u) i:{a..b}. e(i)) Thm* = Thm* f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1)) ...a THEN Reduce Concl

Generated subgoal:

1 ( i:{k-m..k-1}. i+1)(k-1+1) = kk'!m'
3 steps

About:

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

(5steps total) PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc