IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Continued from Closed Map Operations (merge)

- Folding.

Using a method for zipping much like in the Zipping Merge, we define a way of "folding" a closed map into itself by identifying (with each other) certain objects within it.

Assume f A  Text(A) and Z is a 2-place relation on A.

See Merging for definition of "matching" texts and IdPairs(t,s).
Let Z' be the smallest symmetric-transitive extension of Z such that if x(Z')y then f(x) and f(y) match and each pair of IdPairs(f(x),g(y)) satisfies Z'.
A procedure for generating Z' from Z is to iteratively compare contents of already identified pairs of objects, failing when the texts don't match, or identifying the IdPairs(?,?) if they do match, then (at each step) taking the symmetric-transitive closure.

To fold f along Z, determine Z' as above, then choose a function r A  A such that r(x) = r(y) if x(Z')y, and r(x) = x if x is related to nothing by Z'. (Thus, r picks a canonical representative for each partial-equivalence class.)
The folding of f A  Text(A) is r* o f X  Text(X), where X A is the range of r over inputs from A.

Observe that folding a closed map need not result in a submap (modulo equivalence).

+ Cloning.

Cloning a collection of objects is replicating them and replacing the references to originals within the clones by references to their clones. This is probably done for the purpose of subsequently modifying some of them. If A and B are originals with clones A' and B', and if B references A, then B' references A'.

Assume f A  Text(A) and X A. To clone X, first choose a class B disjoint with A, and a bijection r X  B with inverse r  B  X; let r' A  B agree with r on X and be identity outside X. Then extend f from A to r'*(f(r (b))) for b B.

+ Splitting.

Splitting a closed map is cloning some objects along with all objects that refer to them, causing the closed map to branch into two equivalent closed maps, probably for the purpose of subsequently modifying a branch into a variant.

Not only is the original closed map a submap of the split, but deleting the cloned objects (and leaving the clones) would leave a closed map equivalent to the original. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html