T#(S#) = [unfold definition] Ø. [1 -> { | i in N_0 }] U. U. Ø. [pc+1 -> { }] { } C S#(pc) P_pc = inc x (...and for y and z) U. U. Ø. [pc+1 -> { }] { } C S#(pc) P_pc = dec x xv>0 (...and for y and z) U. U. Ø. [pc' -> { }] { } C S#(pc) P_pc = zero x pc' else pc'' xv=0 (...and for y and z) U. U. Ø. [pc'' -> { }] { } C S#(pc) P_pc = zero x pc' else pc'' xv<>0 (...and for y and z) = [unfold definition] Ø. [1 -> { | i in N_0 }] U. U. U. Ø. [pc+1 -> { }] pc \in Dom(S#) { } C S#(pc) P_pc = inc x (...and for y and z) U. U. U. Ø. [pc+1 -> { }] pc \in Dom(S#) { } C S#(pc) P_pc = dec x xv>0 (...and for y and z) U. U. U. Ø. [pc' -> { }] pc \in Dom(S#) { } C S#(pc) P_pc = zero x pc' else pc'' xv=0 (...and for y and z) U. U. U. Ø. [pc'' -> { }] pc \in Dom(S#) { } C S#(pc) P_pc = zero x pc' else pc'' xv<>0 (...and for y and z) = [def of U.] Ø. [1 -> { | i in N_0 }] U. U. Ø. [pc+1 -> U { }] pc \in Dom(S#) { } C S#(pc) P_pc = inc x (...and for y and z) U. U. Ø. [pc+1 -> U { }] pc \in Dom(S#) { } C S#(pc) P_pc = dec x xv>0 (...and for y and z) U. U. Ø. [pc' -> U { }] pc \in Dom(S#) { } C S#(pc) P_pc = zero x pc' else pc'' xv=0 (...and for y and z) U. U. Ø. [pc'' -> U { }] pc \in Dom(S#) { } C S#(pc) P_pc = zero x pc' else pc'' xv<>0 (...and for y and z) = [def of U.] Ø. [1 -> { | i in N_0 }] U. U. Ø. [pc+1 -> { | \in S#(pc)}] pc \in Dom(S#) P_pc = inc x (...and for y and z) U. U. Ø. [pc+1 -> { | \in S#(pc) /\ xv>0}] pc \in Dom(S#) P_pc = dec x (...and for y and z) U. U. Ø. [pc' -> { | \in S#(pc) /\ xv=0}] pc \in Dom(S#) P_pc = zero x pc' else pc'' (...and for y and z) U. U. Ø. [pc'' -> { | \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 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) = { | \in S } [x--](S) = { | \in S /\ xv>0} [x==0](S) = { | \in S /\ xv=0} [x<>0](S) = { | \in S /\ xv<>0} Let's recall the abstr/conc functions: alpha_x(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 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 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 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 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 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 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#. ( . [1 -> ] ) 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) = [merge the last two joins] \S#. ( . [1 -> ] ) 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#) U. ( . [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] = [Galois surj] = [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] = [Galois surj] = [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] = [Galois surj] = [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] 0](gamma(xp))), alpha(gamma(yp)), alpha(gamma(zp))> = [Galois surj] 0](gamma(xp))),yp,zp> = [your calculations!] <[<>0]#(xp),yp,zp>