composite of a unary operation with itself

Johan G. F. Belinfante and Lee Martie
2006 June 27

SetDirectory["l:"]; << goedel82.22a; << tools.m

summary

If  x  is a unary operation, then so is  composite[x, x].  The derivation is a good illustration of the processes of eliminating and introducing variables.

derivation

The starting point is a result with variables:

SubstTest[implies, and[member[x, map[y, y]], member[z, map[y, y]]], 
      member[composite[x, z], map[y, y]], z -> x]

or[member[composite[x_, x_], map[y_, y_]], 
        not[member[x_, map[y_, y_]]]] := True

The variable x is eliminated first.

Map[equal[V, #] &, 
        SubstTest[class, x, 
          or[member[composite[x, x], z], not[member[x, z]]], 
          z -> map[y, y]]] // Reverse

(% /. y -> y_) /. Equal -> SetDelayed

One of the map[y,y] sets is easily replaced by the larger class UNOPS.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
      subclass[u, w], 
{u -> map[y, y], 
        v -> fix[image[inverse[COMPOSE], map[y, y]]], 
        w -> fix[image[inverse[COMPOSE], UNOPS]]}]

(% /. y -> y_) /. Equal -> SetDelayed

The remaining y variable is eliminated using reify.

Map[equal[0, range[#]] &, 
        SubstTest[reify, y, dif[map[y, y], fix[image[inverse[z], UNOPS]]], 
          z -> COMPOSE]] // Reverse

subclass[UNOPS, fix[image[inverse[COMPOSE], UNOPS]]] := True

The variable x is reintroduced to help make the final result more understandable.

SubstTest[implies, and[member[u, v], subclass[v, w]], 
      member[u, w], 
{u -> pair[x, x], 
        v -> id[UNOPS], 
        w -> image[inverse[COMPOSE], UNOPS]}]

or[member[composite[x_, x_], UNOPS], not[member[x_, UNOPS]]] := 
      True

invariance under composite[COMPOSE, DUP]

A related result is derived in this section.  Again reify is used to remove the variable y.

Map[equal[0, #] &, 
        SubstTest[reify, y, 
          dif[map[y, y], fix[image[inverse[z], map[y, y]]]], 
          z -> COMPOSE]] // Reverse

subclass[image[MAP, Id], invar[composite[COMPOSE, DUP]]] := 
      True

The union of a collection of invariant subsets is itself invariant.

SubstTest[implies, subclass[u, invar[v]], 
      invariant[v, U[u]], {u -> image[MAP, Id], 
        v -> composite[COMPOSE, DUP]}]

subclass[image[COMPOSE, id[UNOPS]], UNOPS] := True

This result is equivalent to the variable-free statement subclass[UNOPS, fix[image[inverse[COMPOSE], UNOPS]]] derived in the preceding section, but using direct images in place of inverse images.