WhoCites Definitions IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Associativity of a function

Who Cites is assoc sep?
is_assoc_sepDef  is_assoc_sep(Af) == is_assoc(Ax,y.(f(x,y)))
Thm*  f:(AAA). is_assoc_sep(Af Prop
is_assocDef  is_assoc(Ax,z.f(x;z)) == x,y,z:Af(x;f(y;z)) = f(f(x;y);z A
Thm*  A:Type, f:(AAA). is_assoc(Ax,z.f(x,z))  Prop

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

WhoCites Definitions IteratedBinops Sections DiscrMathExt Doc