Selected Objects

def	ho	o == f:'a'b. g:'a'b. f o g
def	hk	k == x:'a. y:'b. x
def	hs	s == f:'a  'b  'c. g:'a  'b. x:'a. f(x,g(x))
def	hi	i == x:'a. x
THM	ho_def	'c,'b,'a:S. all(f:'b  'c. all(g:'a  'b. equal(o(f,g),x:'a. f(g(x)))))
THM	hk_def	'a,'b:S. equal(k,x:'a. y:'b. x)
THM	hs_def	'c,'b,'a:S. equal(s,f:'a  'b  'c. g:'a  'b. x:'a. f(x,g(x)))
THM	hi_def	'a:S. equal(i,s(k,k))
THM	ho_thm	'b,'c,'a:S. all(f:'b  'c. all(g:'a  'b. all(x:'a. equal(o(f,g,x),f(g(x))))))
THM	ho_assoc	'a,'c,'d,'b:S. all (f:'c  'd. all (f:'c  'd. (g:'b  'c. all(h:'a  'b. equal(o(f,o(g,h)),o(o(f,g),h)))))
THM	hk_thm	'a,'b:S. all(x:'a. all(y:'b. equal(k(x,y),x)))
THM	hs_thm	'a,'b,'c:S. all(f:'a  'b  'c. all(g:'a  'b. all(x:'a. equal(s(f,g,x),f(x,g(x))))))
THM	hi_thm	'a:S. all(x:'a. equal(i(x),x))
THM	hi_o_id	'b,'a:S. all(f:'a  'b. and(equal(o(i,f),f),equal(o(f,i),f)))
THM	o_thm	'b,'c,'a:S, x:('b  'c), x@0:('a  'b), x@1:'a. (x o x@0)(x@1) = x(x@0(x@1))
THM	o_assoc	'a,'c,'d,'b:S, x:('c  'd), x@0:('b  'c), x@1:('a  'b). x o (x@0 o x@1) = (x o x@0) o x@1  ('a  'd)
THM	k_thm	'a,'b:S, x:'a, x@0:'b. x = x
THM	s_thm	'a,'b,'c:S, x:('a  'b  'c), x@0:('a  'b), x@1:'a. x(x@1,x@0(x@1)) = x(x@1,x@0(x@1))
THM	i_thm	'a:S, x:'a. x = x
THM	i_o_id	'b,'a:S, x:('a  'b). (x:'b. x) o x = x  ('a  'b) & x o (x:'a. x) = x  ('a  'b)

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