Nuprl - Proof: iteration terminates 1 2 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 2 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:

. m(f^n(x))

m(x)-n

f(f^n(x)) = f^n(x)
7. m(f^m(x)+1(x))

m(x)-(m(x)+1)

f(f^m(x)+1(x)) = f^m(x)+1(x)

By:	Subst (m(x)-(m(x)+1) = 0-1) -1

Generated subgoals:

1   m(x)-(m(x)+1) = 0-1
Auto

2 1. T : Type{i}
2. f : TT
3. m : T
4. x:T. m(f(x))m(x) & (m(f(x)) = m(x)  f(x) = x)
5. x : T
6. n:. m(f^n(x))m(x)-n  f(f^n(x)) = f^n(x)
7. m(f^m(x)+1(x))m(x)-(m(x)+1)
8. z :
  (m(f^m(x)+1(x))z)  Prop{1}
Auto

3 7. m(f^m(x)+1(x))0-1
  f(f^m(x)+1(x)) = f^m(x)+1(x)
6 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