First, massage T# a bit:


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                  (...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                  (...and for y and z)


= [formulate as two pointwise joins] ------------------------------

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

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

          (...and for y and z)

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

          (...and for y and z)
  U.

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

          (...and for y and z)

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

          (...and for y and z)

= [pointwise join] --------------------------------------------------

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

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

          (...and for y and z)

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

          (...and for y and z)
  U.

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

          (...and for y and z)

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

          (...and for y and z)

= [write as set comprehension] --------------------------------------------------

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

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

          (...and for y and z)

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

          (...and for y and z)
  U.

            U.        Ø. [pc' -> { <xv, yv, zv> | { <xv, yv, zv> } C S#(pc)
       pc in Dom(S#)                                           /\ xv=0 } ]      
  P_pc = zero x pc' else pc''

          (...and for y and z)

  U.
            U.        Ø. [pc'' -> { <xv, yv, zv> | { <xv, yv, zv> } C S#(pc)
       pc in Dom(S#)                                           /\ xv<>0 } ]
  P_pc = zero x pc' else pc''

          (...and for y and z)

= [factor into four helper functions] ------------------------------

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

  U.
            U.        Ø. [pc+1 -> [x++] o S#(pc) ]
       pc in Dom(S#)               
       P_pc = inc x     

          (...and for y and z)

  U.
            U.        Ø. [pc+1 -> [x--] o S#(pc) ]
       pc in Dom(S#)
       P_pc = dec x

          (...and for y and z)
  U.

            U.        Ø. [pc' -> [x=0] o S#(pc) ]
       pc in Dom(S#)
  P_pc = zero x pc' else pc''

          (...and for y and z)

  U.
            U.        Ø. [pc'' -> [x<>0] o S#(pc) ]
       pc in Dom(S#)
  P_pc = zero x pc' else pc''

          (...and for y and z)


with the following factored helper definitions:

[x++] = \S. { <xv+1, yv, zv> | { <xv, yv, zv> } C S }
[x--] = \S. { <xv-1, yv, zv> | { <xv, yv, zv> } C S /\ xv>0 }
[x=0] = \S. { <xv, yv, zv> | { <xv, yv, zv> } C S /\ xv=0 }
[x<>0] = \S. { <xv, yv, zv> | { <xv, yv, zv> } C S /\ xv<>0 }


 (...and for y and z)

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

Sidestep:

Calculate optimal [x++] operation over P(N_0) x P(N_0) x P(N_0):


       : P(N_0) x P(N_0) x P(N_0)  -->  P(N_0) x P(N_0) x P(N_0):
[x++]' = alpha o [x++] o gamma
       = [eta expansion]
        \(XV,YV,ZV). alpha o [x++] o gamma(XV,YV,ZV)
       = [unfold [x++] def]
        \(XV,YV,ZV).
           alpha({ <xv+1, yv, zv> | { <xv, yv, zv> } C gamma(XV,YV,ZV) })
       = [def gamma]
        \(XV,YV,ZV).
           alpha({ <xv+1, yv, zv> | { <xv, yv, zv> } C XV x YV x ZV })
       = [pointwise inclusion]
        \(XV,YV,ZV).
           alpha({ <xv+1, yv, zv> | xv \in XV, yv in YV, zv in ZV })
       = [write as Cartesian product]
        \(XV,YV,ZV).
           alpha({ xv+1 | xv \in XV} x YV x ZV )
       = [def alpha]
        \(XV,YV,ZV). ({ xv+1 | xv \in XV},YV,ZV)
       = [factor [+1] operation]
        \(XV,YV,ZV). ([+1](XV),YV,ZV)

[+1] = \S.{ xv+1 | xv \in S}


Calculate optimal [x++] operation over Par x Par x Par:

        : Par x Par x Par  -->  Par x Par x Par:
[x++]'' = alpha o [x++]' o gamma
        = [eta expand]
         \(xv,yv,zv). alpha o [x++]' o gamma(xv,yv,zv)
        = [def [x++]']
         \(xv,yv,zv). alpha((\(XV,YV,ZV). ([+1](XV),YV,ZV)) gamma(xv,yv,zv))
        = [def gamma]
         \(xv,yv,zv).
           alpha((\(XV,YV,ZV). ([+1](XV),YV,ZV)) (gamma(xv),gamma(yv),gamma(zv)))
        = [apply lambda]
         \(xv,yv,zv).
           alpha([+1](gamma(xv),gamma(yv),gamma(zv)))
        = [pointwise alpha]
         \(xv,yv,zv).
           (alpha o [+1] o gamma(xv),alpha o gamma(yv), alpha o gamma(zv))
        =/C. [Galois surjection/connection]
         \(xv,yv,zv). (alpha o [+1] o gamma(xv),yv,zv)
        = [def [+1]' from handin]
         \(xv,yv,zv). ([+1]'(xv),yv,zv)

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

Back to where we came from:


\S#. alpha o T# o gamma(S#)

= [def massaged T#]

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

  U.
            U.        Ø. [pc+1 -> [x++] o gamma(S#)(pc) ]
       pc in Dom(gamma(S#))
       P_pc = inc x     

          (...and for y and z)

  U.
            U.        Ø. [pc+1 -> [x--] o gamma(S#)(pc) ]
       pc in Dom(gamma(S#))
       P_pc = dec x

          (...and for y and z)
  U.

            U.        Ø. [pc' -> [x=0] o gamma(S#)(pc) ]
       pc in Dom(gamma(S#))
  P_pc = zero x pc' else pc''

          (...and for y and z)

  U.
            U.        Ø. [pc'' -> [x<>0] o gamma(S#)(pc) ]
       pc in Dom(gamma(S#))
  P_pc = zero x pc' else pc''

          (...and for y and z)
)

= [alpha CJM x 2] --------------------------------------------------

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

  U.
            U.        alpha( Ø. [pc+1 -> [x++] o gamma(S#)(pc) ] )
       pc in Dom(gamma(S#))
       P_pc = inc x     

          (...and for y and z)

  U.
            U.        alpha( Ø. [pc+1 -> [x--] o gamma(S#)(pc) ] )
       pc in Dom(gamma(S#))
       P_pc = dec x

          (...and for y and z)
  U.

            U.        alpha( Ø. [pc' -> [x=0] o gamma(S#)(pc) ] )
       pc in Dom(gamma(S#))
  P_pc = zero x pc' else pc''

          (...and for y and z)

  U.
            U.        alpha( Ø. [pc'' -> [x<>0] o gamma(S#)(pc) ] )
       pc in Dom(gamma(S#))
  P_pc = zero x pc' else pc''

          (...and for y and z)

= [Dom is the same] --------------------------------------------------

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

  U.
            U.        alpha( Ø. [pc+1 -> [x++] o gamma(S#)(pc) ] )
       pc in Dom(S#)
       P_pc = inc x     

          (...and for y and z)

  U.
            U.        alpha( Ø. [pc+1 -> [x--] o gamma(S#)(pc) ] )
       pc in Dom(S#)
       P_pc = dec x

          (...and for y and z)
  U.

            U.        alpha( Ø. [pc' -> [x=0] o gamma(S#)(pc) ] )
       pc in Dom(S#)
  P_pc = zero x pc' else pc''

          (...and for y and z)

  U.
            U.        alpha( Ø. [pc'' -> [x<>0] o gamma(S#)(pc) ] )
       pc in Dom(S#)
  P_pc = zero x pc' else pc''

          (...and for y and z)

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

  \bot. [1 -> alpha({ <i,0,0> | i in N_0 })]

  U.
            U.        \bot. [pc+1 -> alpha( [x++] o gamma(S#)(pc) ) ]
       pc in Dom(S#)
       P_pc = inc x     

          (...and for y and z)

  U.
            U.         \bot. [pc+1 -> alpha( [x--] o gamma(S#)(pc) ) ]
       pc in Dom(S#)
       P_pc = dec x

          (...and for y and z)
  U.

            U.         \bot. [pc' -> alpha( [x=0] o gamma(S#)(pc) ) ]
       pc in Dom(S#)
  P_pc = zero x pc' else pc''

          (...and for y and z)

  U.
            U.         \bot. [pc'' -> alpha( [x<>0] o gamma(S#)(pc) ) ]
       pc in Dom(S#)
  P_pc = zero x pc' else pc''

          (...and for y and z)

= [def pointwise gamma] --------------------------------------------------

  \bot. [1 -> alpha({ <i,0,0> | i in N_0 })]

  U.
            U.        \bot. [pc+1 -> alpha( [x++] o gamma(S#(pc)) ) ]
       pc in Dom(S#)
       P_pc = inc x     

          (...and for y and z)

  U.
            U.         \bot. [pc+1 -> alpha( [x--] o gamma(S#(pc)) ) ]
       pc in Dom(S#)
       P_pc = dec x

          (...and for y and z)
  U.

            U.         \bot. [pc' -> alpha( [x=0] o gamma(S#(pc)) ) ]
       pc in Dom(S#)
  P_pc = zero x pc' else pc''

          (...and for y and z)

  U.
            U.         \bot. [pc'' -> alpha( [x<>0] o gamma(S#(pc)) ) ]
       pc in Dom(S#)
  P_pc = zero x pc' else pc''

          (...and for y and z)

= [def [x++]''] --------------------------------------------------

  \bot. [1 -> alpha({ <i,0,0> | i in N_0 })]

  U.
            U.        \bot. [pc+1 -> [x++]'' o S#(pc) ]
       pc in Dom(S#)
       P_pc = inc x     

          (...and for y and z)

  U.
            U.         \bot. [pc+1 -> [x--]'' o S#(pc) ]
       pc in Dom(S#)
       P_pc = dec x

          (...and for y and z)
  U.

            U.         \bot. [pc' -> [x=0]'' o S#(pc) ]
       pc in Dom(S#)
  P_pc = zero x pc' else pc''

          (...and for y and z)

  U.
            U.         \bot. [pc'' -> [x<>0]'' o S#(pc) ]
       pc in Dom(S#)
  P_pc = zero x pc' else pc''

          (...and for y and z)

= [pointwise join] --------------------------------------------------

  \bot. [1 -> alpha({ <i,0,0> | i in N_0 })]

  U.
            U.        \bot. [pc+1 -> [x++]'' o S#(pc) ]
       pc in Dom(S#)
       P_pc = inc x     

          (...and for y and z)

  U.
            U.         \bot. [pc+1 -> [x--]'' o S#(pc) ]
       pc in Dom(S#)
       P_pc = dec x

          (...and for y and z)
  U.

            U.         \bot. [pc' -> [x=0]'' o S#(pc) ]
       pc in Dom(S#)                 U. \bot. [pc'' -> [x<>0]'' o S#(pc) ]
  P_pc = zero x pc' else pc''

          (...and for y and z)

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

  \bot. [1 -> alpha(N_0,{0},{0})]

  U.
            U.        \bot. [pc+1 -> [x++]'' o S#(pc) ]
       pc in Dom(S#)
       P_pc = inc x     

          (...and for y and z)

  U.
            U.         \bot. [pc+1 -> [x--]'' o S#(pc) ]
       pc in Dom(S#)
       P_pc = dec x

          (...and for y and z)
  U.

            U.         \bot. [pc' -> [x=0]'' o S#(pc) ]
       pc in Dom(S#)                 U. \bot. [pc'' -> [x<>0]'' o S#(pc) ]
  P_pc = zero x pc' else pc''

          (...and for y and z)

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

  \bot. [1 -> (top,even,even)]

  U.
            U.        \bot. [pc+1 -> [x++]'' o S#(pc) ]
       pc in Dom(S#)
       P_pc = inc x     

          (...and for y and z)

  U.
            U.         \bot. [pc+1 -> [x--]'' o S#(pc) ]
       pc in Dom(S#)
       P_pc = dec x

          (...and for y and z)
  U.

            U.         \bot. [pc' -> [x=0]'' o S#(pc) ]
       pc in Dom(S#)                 U. \bot. [pc'' -> [x<>0]'' o S#(pc) ]
  P_pc = zero x pc' else pc''

          (...and for y and z)

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

Note: in the rush we missed the last two steps at the lecture. They
      just abstract the initial states from P(N_0 x N_0 x N_0) to
      P(N_0) x P(N_0) x P(N_0)  to  Par x Par x Par.