NATMOD fixed point theorems

Johan G. F. Belinfante
2005 June 24

<< goedel70.24b; << 
      tools.m

summary

Some fixed point theorems concerning natmod are derived.

basic result

Recall that  natmod[x,y] = x  when  x < y.

implies[and[member[x, y], member[y, omega]], 
      equal[natmod[x, y], x]]

Combining this result with a converse result yields this logical equivalence:

equiv[equal[x, natmod[x, y]], 
          or[and[member[x, y], member[y, omega]], 
            and[member[x, omega], equal[0, y]], equal[x, V]]] // not // 
      not

This can be made into a rewrite rule.

equal[x_, natmod[x_, y_]] := 
      or[and[equal[0, y], member[x, omega]], 
        and[member[x, y], member[y, omega]], equal[V, x]]

variable-free formulation

The following variable-free statement holds:

fix[composite[inverse[FIRST], NATMOD]] // RelnNormality

fix[composite[inverse[FIRST], NATMOD]] := 
      union[cart[omega, set[0]], composite[id[omega], E]]

Companion result.

fix[composite[inverse[NATMOD], FIRST]] // InvertFixTest

fix[composite[inverse[NATMOD], FIRST]] := 
      union[cart[omega, set[0]], composite[id[omega], E]]

idempotence result

Corollary.

equal[natmod[natmod[x, y], y], natmod[x, y]]

natmod[natmod[x_, y_], y_] := natmod[x, y]

Lemma.

symdif[composite[NATMOD, RIGHT[x], NATMOD, RIGHT[x]], 
        composite[NATMOD, RIGHT[x]]] // VSNormality

(% /. x -> x_) /. Equal -> SetDelayed

SubstTest[equal, 0, 
      symdif[u, v], {u -> composite[NATMOD, RIGHT[x], NATMOD, RIGHT[x]], 
        v -> composite[NATMOD, RIGHT[x]]}]

composite[NATMOD, RIGHT[x_], NATMOD, RIGHT[x_]] := 
      composite[NATMOD, RIGHT[x]]

consequences of the idempotence result

The following temporary result will be subsumed by a more general corollary in a moment.

SubstTest[implies, and[FUNCTION[y], idempotent[y]], 
      equal[range[y], fix[y]], 
      y -> composite[NATMOD, RIGHT[x]]]

image[NATMOD, cart[V, set[x_]]] := 
      union[intersection[omega, complement[image[V, x]]], nat[x]]

The variable  x  can be eliminated.

SubstTest[reify, x, image[z, cart[V, set[x]]], z -> NATMOD] // 
      Reverse

composite[NATMOD, inverse[SECOND]] := 
      union[cart[set[0], omega], composite[inverse[E], id[omega]]]

The following image rule subsumes the temporary rule derived earlier.

ImageComp[NATMOD, inverse[SECOND], x] // Reverse

image[NATMOD, cart[V, x_]] := 
      union[intersection[omega, image[V, intersection[x, set[0]]]], 
        U[intersection[omega, x]]]

another variable-free rule

Lemma.

composite[
        rotate[composite[
            intersection[composite[rotate[x], SWAP, FIRST], 
              composite[rotate[y], SWAP, SECOND]], inverse[RIF], SWAP]], 
        SWAP] // VSTriNormality

composite[
        rotate[composite[
            intersection[composite[rotate[x_], SWAP, FIRST], 
              composite[rotate[y_], SWAP, SECOND]], inverse[RIF], SWAP]], 
        SWAP] := composite[x, 
        intersection[composite[inverse[FIRST], y], 
          composite[inverse[SECOND], SECOND]]]

This can be cleaned up:

Map[flip[rotate[inverse[#]]] &, 
        SubstTest[reify, x, composite[z, RIGHT[x], z, RIGHT[x]], 
          z -> NATMOD]] // Reverse

composite[NATMOD, 
        intersection[composite[inverse[FIRST], NATMOD], 
          composite[inverse[SECOND], SECOND]]] := NATMOD