We first write out T specific to the 3 counter machine:

   T(S)

 = (def T)

   I  U  { s | exist s' in S: s' --> s }

 = (def I)

   { <1,i,0,0> | i \in N0 }

   U
              U            { <pc+1, xv+1, yv, zv> }
     <pc, xv, yv, zv> in S
         P_pc = inc x

      (similar for y and z)

   U
              U            { <pc+1, xv-1, yv, zv> }
     <pc, xv, yv, zv> in S
         P_pc = dec x
             xv>0

      (similar for y and z)


   U
              U            { <pc', xv, yv, zv> }
     <pc, xv, yv, zv> in S
  P_pc = zero x pc' else pc''
             xv=0

   U
              U            { <pc'', xv, yv, zv> }
     <pc, xv, yv, zv> in S
  P_pc = zero x pc' else pc''
             xv<>0

      (similar for y and z)

-----

The alpha and gamma of the Galois connection read:

 alpha(R) = \pc.{ <xv,yv,zv> | <pc,xv,yv,zv> \in R }
 gamma(F) = { <pc,xv,yv,zv> | <xv,yv,zv> \in F(pc) }

-----

Finally we are all set for "pushing alpha" under T's definition.


Let S be given

   alpha(T(S))

 = (per above)

   alpha(

      { <1,i,0,0> | i \in N0 }
   
      U
                 U            { <pc+1, xv+1, yv, zv> }
        <pc, xv, yv, zv> in S
            P_pc = inc x
   
         (similar for y and z)
   
      U
                 U            { <pc+1, xv-1, yv, zv> }
        <pc, xv, yv, zv> in S
            P_pc = dec x
                xv>0
   
         (similar for y and z)
   
   
      U
                 U            { <pc', xv, yv, zv> }
        <pc, xv, yv, zv> in S
     P_pc = zero x pc' else pc''
                xv=0
   
      U
                 U            { <pc'', xv, yv, zv> }
        <pc, xv, yv, zv> in S
     P_pc = zero x pc' else pc''
                xv<>0
   
         (similar for y and z)
   )

 = (alpha CJM)

       alpha({ <1,i,0,0> | i \in N0 })
   
      U.
       alpha(    U            { <pc+1, xv+1, yv, zv> } )
        <pc, xv, yv, zv> in S
            P_pc = inc x
   
         (similar for y and z)
   
      U.
       alpha(    U            { <pc+1, xv-1, yv, zv> } )
        <pc, xv, yv, zv> in S
            P_pc = dec x
                xv>0
   
         (similar for y and z)
   
   
      U.
       alpha(    U            { <pc', xv, yv, zv> } )
        <pc, xv, yv, zv> in S
     P_pc = zero x pc' else pc''
                xv=0
   
      U.
       alpha(    U            { <pc'', xv, yv, zv> } )
        <pc, xv, yv, zv> in S
     P_pc = zero x pc' else pc''
                xv<>0
   
         (similar for y and z)

 = (alpha CJM)

       alpha({ <1,i,0,0> | i \in N0 })
   
      U.
                 U.           alpha( { <pc+1, xv+1, yv, zv> } )
        <pc, xv, yv, zv> in S
            P_pc = inc x
   
         (similar for y and z)
   
      U.
                 U.           alpha( { <pc+1, xv-1, yv, zv> } )
        <pc, xv, yv, zv> in S
            P_pc = dec x
                xv>0
   
         (similar for y and z)
   
         U.
                 U.           alpha( { <pc', xv, yv, zv> } )
        <pc, xv, yv, zv> in S
     P_pc = zero x pc' else pc''
                xv=0
   
      U.
                 U.           alpha( { <pc'', xv, yv, zv> } )
        <pc, xv, yv, zv> in S
     P_pc = zero x pc' else pc''
                xv<>0
   
         (similar for y and z)

 = (def alpha)

       Ø.[1 -> { <i,0,0> | i \in N0 }]
   
      U.
                 U.           Ø.[pc+1 -> { <xv+1, yv, zv> }]
        <pc, xv, yv, zv> in S
            P_pc = inc x
   
         (similar for y and z)
   
      U.
                 U.           Ø.[pc+1 -> { <xv-1, yv, zv> }]
        <pc, xv, yv, zv> in S
            P_pc = dec x
                xv>0
   
         (similar for y and z)
   
         U.
                 U.           Ø.[pc' -> { <xv, yv, zv> }]
        <pc, xv, yv, zv> in S
     P_pc = zero x pc' else pc''
                xv=0
   
      U.
                 U.           Ø.[pc'' -> { <xv, yv, zv> }]
        <pc, xv, yv, zv> in S
     P_pc = zero x pc' else pc''
                xv<>0
   
         (similar for y and z)

 = (Galois surjection/iso)

       Ø.[1 -> { <i,0,0> | i \in N0 }]
   
      U.
                 U.           Ø.[pc+1 -> { <xv+1, yv, zv> }]
        <pc, xv, yv, zv> in gamma(alpha(S))
            P_pc = inc x
   
         (similar for y and z)
   
      U.
                 U.           Ø.[pc+1 -> { <xv-1, yv, zv> }]
        <pc, xv, yv, zv> in gamma(alpha(S))
            P_pc = dec x
                xv>0
   
         (similar for y and z)
   
         U.
                 U.           Ø.[pc' -> { <xv, yv, zv> }]
        <pc, xv, yv, zv> in gamma(alpha(S))
     P_pc = zero x pc' else pc''
                xv=0
   
      U.
                 U.           Ø.[pc'' -> { <xv, yv, zv> }]
        <pc, xv, yv, zv> in gamma(alpha(S))
     P_pc = zero x pc' else pc''
                xv<>0
   
         (similar for y and z)

 = (membership as inclusion)

       Ø.[1 -> { <i,0,0> | i \in N0 }]
   
      U.
                 U.           Ø.[pc+1 -> { <xv+1, yv, zv> }]
   {<pc, xv, yv, zv>} C gamma(alpha(S))
            P_pc = inc x
   
         (similar for y and z)
   
      U.
                 U.           Ø.[pc+1 -> { <xv-1, yv, zv> }]
   {<pc, xv, yv, zv>} C gamma(alpha(S))
            P_pc = dec x
                xv>0
   
         (similar for y and z)
   
         U.
                 U.           Ø.[pc' -> { <xv, yv, zv> }]
   {<pc, xv, yv, zv>} C gamma(alpha(S))
     P_pc = zero x pc' else pc''
                xv=0
   
      U.
                 U.           Ø.[pc'' -> { <xv, yv, zv> }]
   {<pc, xv, yv, zv>} C gamma(alpha(S))
     P_pc = zero x pc' else pc''
                xv<>0
   
         (similar for y and z)

 = (Galois conn.)

       Ø.[1 -> { <i,0,0> | i \in N0 }]
   
      U.
                 U.           Ø.[pc+1 -> { <xv+1, yv, zv> }]
   alpha({<pc, xv, yv, zv>}) C. alpha(S)
            P_pc = inc x
   
         (similar for y and z)
   
      U.
                 U.           Ø.[pc+1 -> { <xv-1, yv, zv> }]
   alpha({<pc, xv, yv, zv>}) C. alpha(S)
            P_pc = dec x
                xv>0
   
         (similar for y and z)
   
         U.
                 U.           Ø.[pc' -> { <xv, yv, zv> }]
   alpha({<pc, xv, yv, zv>}) C. alpha(S)
     P_pc = zero x pc' else pc''
                xv=0
   
      U.
                 U.           Ø.[pc'' -> { <xv, yv, zv> }]
   alpha({<pc, xv, yv, zv>}) C. alpha(S)
     P_pc = zero x pc' else pc''
                xv<>0
   
         (similar for y and z)

 = (def alpha)

       Ø.[1 -> { <i,0,0> | i \in N0 }]
   
      U.
                 U.           Ø.[pc+1 -> { <xv+1, yv, zv> }]
   Ø.[pc -> {<xv, yv, zv>}] C. alpha(S)
            P_pc = inc x
   
         (similar for y and z)
   
      U.
                 U.           Ø.[pc+1 -> { <xv-1, yv, zv> }]
   Ø.[pc -> {<xv, yv, zv>}] C. alpha(S)
            P_pc = dec x
                xv>0
   
         (similar for y and z)
   
         U.
                 U.           Ø.[pc' -> { <xv, yv, zv> }]
   Ø.[pc -> {<xv, yv, zv>}] C. alpha(S)
     P_pc = zero x pc' else pc''
                xv=0
   
      U.
                 U.           Ø.[pc'' -> { <xv, yv, zv> }]
   Ø.[pc -> {<xv, yv, zv>}] C. alpha(S)
     P_pc = zero x pc' else pc''
                xv<>0
   
         (similar for y and z)

 = (def pointwise inclusion)

       Ø.[1 -> { <i,0,0> | i \in N0 }]
   
      U.
                 U.           Ø.[pc+1 -> { <xv+1, yv, zv> }]
    {<xv, yv, zv>} C alpha(S)(pc)
            P_pc = inc x
   
         (similar for y and z)
   
      U.
                 U.           Ø.[pc+1 -> { <xv-1, yv, zv> }]
    {<xv, yv, zv>} C alpha(S)(pc)
            P_pc = dec x
                xv>0
   
         (similar for y and z)
   
         U.
                 U.           Ø.[pc' -> { <xv, yv, zv> }]
    {<xv, yv, zv>} C alpha(S)(pc)
     P_pc = zero x pc' else pc''
                xv=0
   
      U.
                 U.           Ø.[pc'' -> { <xv, yv, zv> }]
    {<xv, yv, zv>} C alpha(S)(pc)
     P_pc = zero x pc' else pc''
                xv<>0
   
         (similar for y and z)


----------------------------------------------------------------------

Hurrah! Now we can read off T#:


T#(S#) =

       Ø.[1 -> { <i,0,0> | i \in N0 }]
   
      U.
                 U.           Ø.[pc+1 -> { <xv+1, yv, zv> }]
    {<xv, yv, zv>} C S#(pc)
            P_pc = inc x
   
         (similar for y and z)
   
      U.
                 U.           Ø.[pc+1 -> { <xv-1, yv, zv> }]
    {<xv, yv, zv>} C S#(pc)
            P_pc = dec x
                xv>0
   
         (similar for y and z)
   
         U.
                 U.           Ø.[pc' -> { <xv, yv, zv> }]
    {<xv, yv, zv>} C S#(pc)
     P_pc = zero x pc' else pc''
                xv=0
   
      U.
                 U.           Ø.[pc'' -> { <xv, yv, zv> }]
    {<xv, yv, zv>} C S#(pc)
     P_pc = zero x pc' else pc''
                xv<>0
   
         (similar for y and z)