Def 'a  'b == 'a'b

is mentioned by

Thm* 'b,'a:S, x:('a  'b). Thm* (x:'b. x) o x = x  ('a  'b) & x o (x:'a. x) = x  ('a  'b)	[i_o_id]
Thm* 'a,'b,'c:S, x:('a  'b  'c), x@0:('a  'b), x@1:'a. Thm* x(x@1,x@0(x@1)) = x(x@1,x@0(x@1))	[s_thm]
Thm* 'a,'c,'d,'b:S, x:('c  'd), x@0:('b  'c), x@1:('a  'b). Thm* x o (x@0 o x@1) = (x o x@0) o x@1  ('a  'd)	[o_assoc]
Thm* 'b,'c,'a:S, x:('b  'c), x@0:('a  'b), x@1:'a. Thm* (x o x@0)(x@1) = x(x@0(x@1))	[o_thm]
Thm* 'b,'a:S. all(f:'a  'b. and(equal(o(i,f),f),equal(o(f,i),f)))	[hi_o_id]
Thm* 'a,'b,'c:S. Thm* all Thm* (f:'a  'b  'c. all Thm* (f:'a  'b  'c. (g:'a  'b. all(x:'a. equal(s(f,g,x),f(x,g(x))))))	[hs_thm]
Thm* 'a,'c,'d,'b:S. Thm* all Thm* (f:'c  'd. all Thm* (f:'c  'd. (g:'b  'c. all Thm* (f:'c  'd. (g:'b  'c. (h:'a  'b. equal(o(f,o(g,h)),o(o(f,g),h)))))	[ho_assoc]
Thm* 'b,'c,'a:S. Thm* all(f:'b  'c. all(g:'a  'b. all(x:'a. equal(o(f,g,x),f(g(x))))))	[ho_thm]
Thm* 'a:S. equal(i,s(k,k))	[hi_def]
Thm* 'c,'b,'a:S. equal(s,f:'a  'b  'c. g:'a  'b. x:'a. f(x,g(x)))	[hs_def]
Thm* 'a,'b:S. equal(k,x:'a. y:'b. x)	[hk_def]
Thm* 'c,'b,'a:S. Thm* all(f:'b  'c. all(g:'a  'b. equal(o(f,g),x:'a. f(g(x)))))	[ho_def]
Def s == f:'a  'b  'c. g:'a  'b. x:'a. f(x,g(x))	[hs]

In prior sections: hol bool

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html