T(S)

=

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

= [expand I]
   
   { <1,i,0,0> | i in N_0 }

   U { s | exists s' in S: s' --> s }

= [expand -->]

   { <1,i,0,0> | i in N_0 }

   U 

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

       (... and for y and z)

   U 

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

       (... and for y and z)

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


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

       (... and for y and z)

= [write as join]

   { <1,i,0,0> | i in N_0 }

   U 

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

       (... and for y and z)

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

       (... and 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

       (... and for y and z)

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

alpha(S) = \pc.{ <xv,yv,zy> | <pc,xv,yv,zy> in S }

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

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

alpha o T(S)

= [expand T] --------------------------------------------------

alpha(

   { <1,i,0,0> | i in N_0 }

   U 

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

       (... and for y and z)

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

       (... and 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

       (... and for y and z)
  )

= [alpha is CJM] --------------------------------------------------

alpha( { <1,i,0,0> | i in N_0 } )

   U. 

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

       (... and 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

       (... and 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

       (... and for y and z)
  )

= [alpha is CJM] --------------------------------------------------

alpha( { <1,i,0,0> | i in N_0 } )

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

       (... and 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

       (... and 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

       (... and for y and z)

= [alpha def] --------------------------------------------------

alpha( { <1,i,0,0> | i in N_0 } )

   U. 
             U.           Ø. [ pc+1 ->  { <xv+1, yv, zv> } ]
   <pc, xv, yv, zv> in S
        P_pc = inc x

       (... and for y and z)

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

       (... and 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

       (... and for y and z)


= [Galois insertion] --------------------------------------------------

alpha( { <1,i,0,0> | i in N_0 } )

   U. 
             U.           Ø. [ pc+1 ->  { <xv+1, yv, zv> } ]
   <pc, xv, yv, zv> in gamma o alpha(S)
        P_pc = inc x

       (... and for y and z)

   U.
             U.           Ø. [ pc+1 -> { <xv-1, yv, zv> } ]
    <pc, xv, yv, zv> in gamma o alpha(S)
        P_pc = dec x
            xv>0

       (... and for y and z)

   U.
             U.           Ø. [ pc' -> { <xv, yv, zv> } ]
  <pc, xv, yv, zv> in gamma o alpha(S)
 P_pc = zero x pc' else pc''
           xv=0

   U.
             U.           Ø. [ pc'' -> { <xv, yv, zv> } ]
  <pc, xv, yv, zv> in gamma o alpha(S)
 P_pc = zero x pc' else pc''
           xv<>0

       (... and for y and z)


= [write as inclusion] --------------------------------------------------

alpha( { <1,i,0,0> | i in N_0 } )

   U. 
             U.           Ø. [ pc+1 ->  { <xv+1, yv, zv> } ]
   {<pc, xv, yv, zv>} C gamma o alpha(S)
        P_pc = inc x

       (... and for y and z)

   U.
             U.           Ø. [ pc+1 -> { <xv-1, yv, zv> } ]
    {<pc, xv, yv, zv>} C gamma o alpha(S)
        P_pc = dec x
            xv>0

       (... and for y and z)

   U.
             U.           Ø. [ pc' -> { <xv, yv, zv> } ]
  {<pc, xv, yv, zv>} C gamma o alpha(S)
 P_pc = zero x pc' else pc''
           xv=0

   U.
             U.           Ø. [ pc'' -> { <xv, yv, zv> } ]
  {<pc, xv, yv, zv>} C gamma o alpha(S)
 P_pc = zero x pc' else pc''
           xv<>0

       (... and for y and z)


= [write as inclusion] --------------------------------------------------

alpha( { <1,i,0,0> | i in N_0 } )

   U. 
             U.           Ø. [ pc+1 ->  { <xv+1, yv, zv> } ]
   alpha({<pc, xv, yv, zv>}) C. alpha(S)
        P_pc = inc x

       (... and 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

       (... and 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

       (... and for y and z)

= [def alpha] --------------------------------------------------

   Ø. [ 1 -> { <i,0,0> | i in N_0 } ]

   U. 
             U.           Ø. [ pc+1 ->  { <xv+1, yv, zv> } ]
   Ø. [ pc -> {<xv, yv, zv>}] C. alpha(S)
        P_pc = inc x

       (... and 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

       (... and 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

       (... and for y and z)


= [def C.] --------------------------------------------------

   Ø. [ 1 -> { <i,0,0> | i in N_0 } ]

   U. 
             U.           Ø. [ pc+1 ->  { <xv+1, yv, zv> } ]
   {<xv, yv, zv>} C alpha(S)(pc)
        P_pc = inc x

       (... and 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

       (... and 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

       (... and for y and z)

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

Hurrah! Now we can read off T#

T#(S#) =

   Ø. [ 1 -> { <i,0,0> | i in N_0 } ]

   U. 
             U.           Ø. [ pc+1 ->  { <xv+1, yv, zv> } ]
   {<xv, yv, zv>} C S#(pc)
        P_pc = inc x

       (... and for y and z)

   U.
             U.           Ø. [ pc+1 -> { <xv-1, yv, zv> } ]
   {<xv, yv, zv>} C S#(pc)
        P_pc = dec x
            xv>0

       (... and 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

       (... and for y and z)