Nuprl - Proof: iteration terminates 1 1 1 1

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: iteration terminates 1 1 1 1

1. T : Type
2. f : T

T
3. m : T

4.

x:T. m(f(x))

m(x) & (m(f(x)) = m(x)

f(x) = x)
5. x : T
6. n :

7. 0<n
8. m(f^n-1(x))

m(x)-(n-1)

m(f^n(x))

m(x)-n

f(f^n(x)) = f^n(x)

By:	InstHyp [f^n-1(x)] 4 THEN Subst (f(f^n-1(x)) = f^n(x)) -1 THEN ExRepD

Generated subgoals:

1 9. m(f(f^n-1(x)))m(f^n-1(x))
10. m(f(f^n-1(x))) = m(f^n-1(x))  f(f^n-1(x)) = f^n-1(x)
  f(f^n-1(x)) = f^n(x)
1 step

2 9. m(f^n(x))m(f^n-1(x))
10. m(f^n(x)) = m(f^n-1(x))  f^n(x) = f^n-1(x)
  m(f^n(x))m(x)-n  f(f^n(x)) = f^n(x)
5 steps

About:

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

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