(12steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: compose iter inverses 1 1 2 2

1. A : Type
2. f : AA
3. g : AA
4. InvFuns(A;A;f;g)
5. x : A
6. i : 
7. 0<i
8. g{i-1}(f{i-1}(x)) = x
  g{i-1}(g(f(f{i-1}(x)))) = x


By: Analyze4 THEN Rewrite by x:Ag(f(x)) = x


Generated subgoals:

None

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

(12steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc