IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Operations on Closed Maps

Here we describe some basic operations on closed maps. Recall that a closed map is a function of type DText(D) for some finite discrete type D. See Conservation and Destruction for connotations of + and - prefixes used below.

Let the function r* Text(D)Text(X), for rDX, replace each abstract id constituent i:abid (for iD) by r(i):abid throughout the text. A renaming of a whole closed map fDText(D) is a closed map r* o f o rXText(X) for inverse functions rDX and rXD. Two closed maps fDText(D) and gXText(X) are "equivalent" when they are renamings of each other.

If XD then "contracting" a closed map fDText(D) around X is restricting f to X together with objects referred to by objects in X (ie, the smallest AD such that XA and f(i) Text(A) for all iA). Hence the contraction is the smallest submap including X. So, contracting a closed map around some of its objects (indices) X is discarding all objects except those among or referred to by the objects of X.

If XD then "focusing" a closed map fDText(D) on X is "contracting" f around X together with objects that refer to members of X. So focusing a closed map on some of its objects X is restricting it to the objects relevant to X.

If XD then "deleting X" from a closed map fDText(D) is finding the largest submap of f excluding X from its indices. That is, the deletion of some objects (indices) X from a closed map is gotten by removing X along with all objects whose contents refer to any of X.