equations for ENUMS

Johan G. F. Belinfante
2011 September 15

SetDirectory["l:"]; << goedel.11sep12a

summary

Two equations for the class ENUMS of enumerators are derived.

derivation

Theorem.  A formula for the class  ENUMS.

SubstTest[class, x, member[x, y], 
      y -> intersection[FUNS, P[cart[OMEGA, OMEGA]], 
          image[inverse[IMAGE[SWAP]], subcommutant[inverse[E]]]]]

intersection[FUNS, 
        image[inverse[IMAGE[SWAP]], subcommutant[inverse[E]]], 
        P[cart[OMEGA, OMEGA]]] := ENUMS

Another formula for ENUMS will be derived in which  subcommutant[inverse[E]]  is replaced with monotone[E, E].

Theorem.  A connection between monotone[x, x] and subcommutant[x].

(Map[equal[V, #] &, 
          SubstTest[class, t, 
            or[not[subclass[P[t], z]], not[member[t, V]], 
              not[subclass[image[inverse[s], domain[t]], domain[t]]], 
              subclass[composite[t, s], composite[s, t]]], 
            z -> intersection[FUNS, monotone[s, s]]]]) /. 
      s -> inverse[x]

subclass[
        image[IMAGE[SWAP], 
          intersection[monotone[x_, x_], U[image[MAP, cart[invar[x_], V]]]]], 
        subcommutant[x_]] := True

Corollary.  A special case of the above theorem needed here.

SubstTest[subclass, 
        image[IMAGE[SWAP], 
          intersection[monotone[x, x], U[image[MAP, cart[invar[x], V]]]]], 
        subcommutant[x], x -> inverse[E]] // Reverse

subclass[
        image[IMAGE[SWAP], 
          intersection[monotone[E, E], U[image[MAP, cart[FULL, V]]]]], 
        subcommutant[inverse[E]]] := True

Lemma.

U[image[MAP, cart[x, P[y]]]] // Normality // Reverse

intersection[P[complement[cart[V, complement[y_]]]], 
        U[image[MAP, cart[x_, V]]]] := 
      U[image[MAP, cart[x, P[y]]]]

Theorem.

intersection[P[cart[V, y]], 
        U[image[MAP, cart[x, V]]]] // Normality

intersection[P[cart[V, y_]], U[image[MAP, cart[x_, V]]]] := 
      U[image[MAP, cart[x, P[y]]]]

Lemma.  An upper bound for  ENUMS.

SubstTest[subclass, ENUMS, 
        intersection[u, v, w], {u -> FUNS, v -> P[cart[V, OMEGA]], 
          w -> image[inverse[IMAGE[FIRST]], OMEGA]}] // Reverse

subclass[ENUMS, U[image[MAP, cart[OMEGA, P[OMEGA]]]]] := 
      True

An inclusion in the opposite direction will now be derived.

Lemma.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
        subclass[u, 
          w], {u -> intersection[monotone[E, E], 
              U[image[MAP, cart[OMEGA, P[OMEGA]]]]], 
          v -> U[image[MAP, cart[OMEGA, P[OMEGA]]]], 
          w -> P[cartsq[OMEGA]]}] // Reverse

% /. Equal -> SetDelayed

Lemma.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
        subclass[u, 
          w], {u -> intersection[monotone[E, E], 
              U[image[MAP, cart[OMEGA, P[OMEGA]]]]], 
          v -> intersection[monotone[E, E], U[image[MAP, cart[FULL, V]]]], 
          w -> image[inverse[IMAGE[SWAP]], subcommutant[inverse[E]]]}] // 
      Reverse

% /. Equal -> SetDelayed

Lemma.  A lower bound for  ENUMS.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
          subclass[u, 
            w], {u -> intersection[monotone[E, E], 
                U[image[MAP, 
                    cart[OMEGA, P[OMEGA]]]]], 
v -> 
              intersection[y, 
                image[inverse[IMAGE[SWAP]], subcommutant[inverse[E]]]], 
            w -> ENUMS}] /. y -> intersection[FUNS, P[cartsq[OMEGA]]] // 
      Reverse

% /. Equal -> SetDelayed

The two inclusions in opposite directions can be combined into an equation for  ENUMS.

Theorem.  Another formula for the class  ENUMS.

SubstTest[and, subclass[u, v], 
      subclass[v, 
        u], {u -> intersection[monotone[E, E], 
            U[image[MAP, cart[OMEGA, P[OMEGA]]]]], v -> ENUMS}]

intersection[monotone[E, E], U[image[MAP, cart[OMEGA, P[OMEGA]]]]] := 
      ENUMS