T#(S#)

= [unfold definition]

  Ø. [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)


= [unfold definition]

  Ø. [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)

= [def of U.]

  Ø. [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)

= [def of U.]

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

  U.
        U.  Ø. [pc+1 -> { <xv+1, yv, zv> | <xv, yv, zv> \in 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> \in S#(pc) /\ xv>0}]
   pc \in Dom(S#)     
    P_pc = dec x                 
                              (...and for y and z)
  U.
        U.  Ø. [pc' -> { <xv, yv, zv> | <xv, yv, zv> \in S#(pc) /\ xv=0}]
   pc \in Dom(S#)
  P_pc = zero x pc' else pc''    
                              (...and for y and z)
  U.
        U. Ø. [pc'' -> { <xv, yv, zv> | <xv, yv, zv> \in S#(pc) /\ xv<>0}]
   pc \in Dom(S#)     
  P_pc = zero x pc' else pc''    
                              (...and for y and z)

= [factor helper operations]

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

  U.
        U.  Ø. [pc+1 -> [x++](S#(pc))]
   pc \in Dom(S#)     
    P_pc = inc x             
                              (...and for y and z)
  U.
        U.  Ø. [pc+1 -> [x--](S#(pc))]
   pc \in Dom(S#)     
    P_pc = dec x                 
                              (...and for y and z)
  U.
        U.  Ø. [pc' -> [x==0](S#(pc))]
   pc \in Dom(S#)
  P_pc = zero x pc' else pc''    
                              (...and for y and z)
  U.
        U. Ø. [pc'' -> [x<>0](S#(pc))]
   pc \in Dom(S#)     
  P_pc = zero x pc' else pc''    
                              (...and for y and z)



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


Let's recall the abstr/conc functions:

       alpha_x(S) = <alpha(proj1 S),alpha(proj2 S),alpha(proj3 S)>
gamma_x(xp,yp,zp) = gamma(xp) x gamma(yp) x gamma(zp)

alpha.(S#) = \pc.alpha_x(S#(pc))
gamma.(S#) = \pc.gamma_x(S#(pc))

Now we are all set for alpha-gamma composition


  alpha. o T# o gamma.

= [eta expansion]

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

= [unfold T# based on the above]

  \S#. 

   alpha. (
   
     Ø. [1 -> { <i,0,0> | i in N_0 }]
   
     U.
           U.  Ø. [pc+1 -> [x++](gamma.(S#)(pc))]
      pc \in Dom(gamma.(S#))     
       P_pc = inc x             
                                 (...and for y and z)
     U.
           U.  Ø. [pc+1 -> [x--](gamma.(S#)(pc))]
      pc \in Dom(gamma.(S#))     
       P_pc = dec x                 
                                 (...and for y and z)
     U.
           U.  Ø. [pc' -> [x==0](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](gamma.(S#)(pc))]
      pc \in Dom(gamma.(S#))     
     P_pc = zero x pc' else pc''    
                                 (...and for y and z)
    )

= [Domain is unchanged]

  \S#. 

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

= [alpha. is CJM]

  \S#. 

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


= [alpha. is CJM, again]

  \S#. 

     alpha.( Ø. [1 -> { <i,0,0> | i in N_0 }] )
   
     U.
           U.  alpha. ( Ø. [pc+1 -> [x++](gamma.(S#)(pc))] )
     pc \in Dom(S#)     
      P_pc = inc x             
                                 (...and for y and z)
     U.
           U.  alpha. ( Ø. [pc+1 -> [x--](gamma.(S#)(pc))] )
     pc \in Dom(S#)     
      P_pc = dec x                 
                                 (...and for y and z)
     U.
           U.  alpha. ( Ø. [pc' -> [x==0](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](gamma.(S#)(pc))] )
      pc \in Dom(S#)     
 P_pc = zero x pc' else pc''    
                                 (...and for y and z)


= [alpha. is CJM, again]

  \S#. 

     ( alpha_x(Ø). [1 -> alpha_x({ <i,0,0> | i in N_0 })] )
   
     U.
           U.  ( alpha_x(Ø). [pc+1 -> alpha_x([x++](gamma.(S#)(pc)))] )
     pc \in Dom(S#)     
      P_pc = inc x             
                                 (...and for y and z)
     U.
           U.  ( alpha_x(Ø). [pc+1 -> alpha_x([x--](gamma.(S#)(pc)))] )
     pc \in Dom(S#)     
      P_pc = dec x                 
                                 (...and for y and z)
     U.
           U.  ( alpha_x(Ø). [pc' -> alpha_x([x==0](gamma.(S#)(pc)))] )
     pc \in Dom(S#)
 P_pc = zero x pc' else pc''    
                                 (...and for y and z)
     U.
           U.  ( alpha_x(Ø). [pc'' -> alpha_x([x<>0](gamma.(S#)(pc)))] )
      pc \in Dom(S#)     
 P_pc = zero x pc' else pc''    
                                 (...and for y and z)

= [def gamma.]

  \S#. 

     ( alpha_x(Ø). [1 -> alpha_x({ <i,0,0> | i in N_0 })] )
   
     U.
           U.  ( alpha_x(Ø). [pc+1 -> [x++]#(S#(pc))] )
     pc \in Dom(S#)     
      P_pc = inc x             
                                 (...and for y and z)
     U.
           U.  ( alpha_x(Ø). [pc+1 -> [x--]#(S#(pc))] )
     pc \in Dom(S#)     
      P_pc = dec x                 
                                 (...and for y and z)
     U.
           U.  ( alpha_x(Ø). [pc' -> [x==0]#(S#(pc))] )
     pc \in Dom(S#)
 P_pc = zero x pc' else pc''    
                                 (...and for y and z)
     U.
           U.  ( alpha_x(Ø). [pc'' -> [x<>0]#(S#(pc))] )
      pc \in Dom(S#)     
 P_pc = zero x pc' else pc''    
                                 (...and for y and z)

where

 [x++]# = alpha_x o [x++] o gamma_x
 [x--]# = alpha_x o [x--] o gamma_x
[x==0]# = alpha_x o [x==0] o gamma_x
[x<>0]# = alpha_x o [x<>0] o gamma_x

             (...and similarly for y and z)

= [def alpha_x]

  \S#. 

     ( <bot,bot,bot>. [1 ->  <top,even,even>] )
   
     U.
           U.  ( <bot,bot,bot>. [pc+1 -> [x++]#(S#(pc))] )
     pc \in Dom(S#)     
      P_pc = inc x             
                                 (...and for y and z)
     U.
           U.  ( <bot,bot,bot>. [pc+1 -> [x--]#(S#(pc))] )
     pc \in Dom(S#)     
      P_pc = dec x                 
                                 (...and for y and z)
     U.
           U.  ( <bot,bot,bot>. [pc' -> [x==0]#(S#(pc))] )
     pc \in Dom(S#)
 P_pc = zero x pc' else pc''    
                                 (...and for y and z)
     U.
           U.  ( <bot,bot,bot>. [pc'' -> [x<>0]#(S#(pc))] )
      pc \in Dom(S#)     
 P_pc = zero x pc' else pc''    
                                 (...and for y and z)

= [merge the last two joins]

  \S#. 

     ( <bot,bot,bot>. [1 ->  <top,even,even>] )
   
     U.
           U.      ( <bot,bot,bot>. [pc+1 -> [x++]#(S#(pc))] )
     pc \in Dom(S#)     
      P_pc = inc x             
                                 (...and for y and z)
     U.
           U.      ( <bot,bot,bot>. [pc+1 -> [x--]#(S#(pc))] )
     pc \in Dom(S#)     
      P_pc = dec x                 
                                 (...and for y and z)
     U.
           U.      ( <bot,bot,bot>. [pc' -> [x==0]#(S#(pc))] )
     pc \in Dom(S#)          U. ( <bot,bot,bot>. [pc'' -> [x<>0]#(S#(pc))] )
 P_pc = zero x pc' else pc''    
                                 (...and for y and z)


This is almost an analysis!


We just need to calculate the locally optimal abstract operations:

* an abstract [x++]:

    [x++]#(xp,yp,zp)
 
  = [by spec]
 
    (alpha_x o [x++] o gamma_x)(xp,yp,zp)
 
  = [def of gamma_x]
 
    (alpha_x o [x++])(gamma(xp) x gamma(yp) x gamma(zp))
 
  = [def of [+1]]
 
    alpha_x([+1](gamma(xp)) x gamma(yp) x gamma(zp))
 
  = [def alpha_x]
 
    <alpha([+1](gamma(xp))), alpha(gamma(yp)), alpha(gamma(zp))>
 
  = [Galois surj]
 
    <alpha([+1](gamma(xp))),yp,zp>
 
  = [your calculations!]
 
    <[+1]#(xp),yp,zp>


* an abstract [x--]:

    [x--]#(xp,yp,zp)
 
  = [by spec]
 
    (alpha_x o [x--] o gamma_x)(xp,yp,zp)
 
  = [def of gamma_x]
 
    (alpha_x o [x--])(gamma(xp) x gamma(yp) x gamma(zp))
 
  = [def of [-1]]
 
    alpha_x([-1](gamma(xp)) x gamma(yp) x gamma(zp))
 
  = [def alpha_x]
 
    <alpha([-1](gamma(xp))), alpha(gamma(yp)), alpha(gamma(zp))>
 
  = [Galois surj]
 
    <alpha([-1](gamma(xp))),yp,zp>
 
  = [your calculations!]
 
    <[-1]#(xp),yp,zp>


* an abstract [x==0]:

    [x==0]#(xp,yp,zp)
 
  = [by spec]
 
    (alpha_x o [x==0] o gamma_x)(xp,yp,zp)
 
  = [def of gamma_x]
 
    (alpha_x o [x==0])(gamma(xp) x gamma(yp) x gamma(zp))
 
  = [def of [=0]]
 
    alpha_x([=0](gamma(xp)) x gamma(yp) x gamma(zp))
 
  = [def alpha_x]
 
    <alpha([=0](gamma(xp))), alpha(gamma(yp)), alpha(gamma(zp))>
 
  = [Galois surj]
 
    <alpha([=0](gamma(xp))),yp,zp>
 
  = [your calculations!]
 
    <[=0]#(xp),yp,zp>


* an abstract [x<>0]:

    [x<>0]#(xp,yp,zp)
 
  = [by spec]
 
    (alpha_x o [x<>0] o gamma_x)(xp,yp,zp)
 
  = [def of gamma_x]
 
    (alpha_x o [x<>0])(gamma(xp) x gamma(yp) x gamma(zp))
 
  = [def of [<>0]]
 
    alpha_x([<>0](gamma(xp)) x gamma(yp) x gamma(zp))
 
  = [def alpha_x]
 
    <alpha([<>0](gamma(xp))), alpha(gamma(yp)), alpha(gamma(zp))>
 
  = [Galois surj]
 
    <alpha([<>0](gamma(xp))),yp,zp>
 
  = [your calculations!]
 
    <[<>0]#(xp),yp,zp>