**********************************************************************
**  The [x=0] operator (and friends)                                ** 
**********************************************************************

Calculating an abstract version of [x=0]:

[x=0]' : P(N) x P(N) x P(N)

 \S. alpha o [x=0] o gamma(S)
= [def of [x=0]]
 \S. alpha ( { <xv, yv, zv> | {<xv, yv, zv>} C gamma(S) /\ xv=0 } )
= [write S as triple]
 \<XV,YV,ZV>. alpha ( { <xv, yv, zv> | {<xv, yv, zv>} C gamma(<XV,YV,ZV>)
                                                          /\ xv=0 } )
= [def of gamma]
 \<XV,YV,ZV>. alpha ( { <xv, yv, zv> | {<xv, yv, zv>} C XV x YV x ZV
                                                          /\ xv=0 } )
= [def of Cartesian product]
 \<XV,YV,ZV>. alpha ( { <xv, yv, zv> | xv \in XV /\ yv in YV /\ zv in ZV
                                                          /\ xv=0 } )
= [def of Cartesian product]
 \<XV,YV,ZV>. alpha ( { <xv | xv \in XV /\ xv=0 } x YV x ZV )
= [def of alpha]
 \<XV,YV,ZV>. <{ <xv | xv \in XV /\ xv=0 }, YV, ZV>

Hence:

 [x=0]' = \<XV,YV,ZV>. <{ <xv | xv \in XV /\ xv=0 }, YV, ZV>

Similarly we get:

 [y=0]' = \<XV,YV,ZV>. <XV, { <yv | yv \in YV /\ yv=0 }, ZV>
 [z=0]' = \<XV,YV,ZV>. <XV, YV, { <zv | zv \in ZV /\ zv=0 }>

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

Calculating an abstract version [x=0] over Parity triples:

[x=0]'' : Parity x Parity x Parity


 \<XV,YV,ZV>. alpha o [x=0]' o gamma(<XV,YV,ZV>)
= [def [x=0]']
 \<XV,YV,ZV>. alpha o (\<XV,YV,ZV>. <{ <xv | xv \in XV /\ xv=0 }, YV, ZV>)
                                                         (gamma(<XV,YV,ZV>))
= [def gamma]
 \<XV,YV,ZV>. alpha (<{ <xv | xv \in gamma(XV) /\ xv=0}, gamma(YV), gamma(ZV)>)
= [def alpha]
 \<XV,YV,ZV>. (<alpha({ <xv | xv \in gamma(XV) /\ xv=0}), alpha(gamma(YV)), alpha(gamma(ZV))>)
=/C. [Galois surjection/connection]
 \<XV,YV,ZV>. (<alpha({ <xv | xv \in gamma(XV) /\ xv=0}), YV, ZV>)
= [factor [=0] operation]
 \<XV,YV,ZV>. (<alpha o [=0] o gamma(XV), YV, ZV>)
= [def [=0]' from handin]
 \<XV,YV,ZV>. (<[=0]'(XV), YV, ZV>)

Hence we define:

 [x=0]'' = \<XV,YV,ZV>. <[=0]'(XV), YV, ZV>

and similarly

 [y=0]'' = \<XV,YV,ZV>. <XV, [=0]'(YV), ZV>
 [z=0]'' = \<XV,YV,ZV>. <XV, YV, [=0]'(ZV)>

where
       : P(N_0) -> P(N_0)
  [=0] = \S. { <xv | xv \in S /\ xv=0 }

       : Parity -> Parity
 [=0]' = (from handin)



**********************************************************************
**  The [x<>0] operator (and friends)                               ** 
**********************************************************************

Calculating an abstract version of [x<>0]:

[x<>0]' : P(N) x P(N) x P(N)

 \S. alpha o [x<>0] o gamma(S)
= [def of [x<>0]]
 \S. alpha ( { <xv, yv, zv> | {<xv, yv, zv>} C gamma(S) /\ xv<>0 } )
= [write S as triple]
 \<XV,YV,ZV>. alpha ( { <xv, yv, zv> | {<xv, yv, zv>} C gamma(<XV,YV,ZV>)
                                                          /\ xv<>0 } )
= [def of gamma]
 \<XV,YV,ZV>. alpha ( { <xv, yv, zv> | {<xv, yv, zv>} C XV x YV x ZV
                                                          /\ xv<>0 } )
= [def of Cartesian product]
 \<XV,YV,ZV>. alpha ( { <xv, yv, zv> | xv \in XV /\ yv in YV /\ zv in ZV
                                                          /\ xv<>0 } )
= [def of Cartesian product]
 \<XV,YV,ZV>. alpha ( { <xv | xv \in XV /\ xv<>0 } x YV x ZV )
= [def of alpha]
 \<XV,YV,ZV>. <{ <xv | xv \in XV /\ xv<>0 }, YV, ZV>

Hence:

 [x<>0]' = \<XV,YV,ZV>. <{ <xv | xv \in XV /\ xv<>0 }, YV, ZV>

Similarly we get:

 [y<>0]' = \<XV,YV,ZV>. <XV, { <yv | yv \in YV /\ yv<>0 }, ZV>
 [z<>0]' = \<XV,YV,ZV>. <XV, YV, { <zv | zv \in ZV /\ zv<>0 }>

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

Calculating an abstract version [x<>0]'' over Parity triples:

[x<>0]'' : Parity x Parity x Parity


 \<XV,YV,ZV>. alpha o [x<>0]' o gamma(<XV,YV,ZV>)
= [def [x<>0]']
 \<XV,YV,ZV>. alpha o (\<XV,YV,ZV>. <{ <xv | xv \in XV /\ xv<>0 }, YV, ZV>)
                                                         (gamma(<XV,YV,ZV>))
= [def gamma]
 \<XV,YV,ZV>. alpha (<{ <xv | xv \in gamma(XV) /\ xv<>0}, gamma(YV), gamma(ZV)>)
= [def alpha]
 \<XV,YV,ZV>. (<alpha({ <xv | xv \in gamma(XV) /\ xv<>0}), alpha(gamma(YV)), alpha(gamma(ZV))>)
=/C. [Galois surjection/connection]
 \<XV,YV,ZV>. (<alpha({ <xv | xv \in gamma(XV) /\ xv<>0}), YV, ZV>)
= [factor [<>0] operation]
 \<XV,YV,ZV>. (<alpha o [<>0] o gamma(XV), YV, ZV>)
= [def [<>0]']
 \<XV,YV,ZV>. (<[<>0]'(XV), YV, ZV>)

Hence we define:

 [x<>0]'' = \<XV,YV,ZV>. <[<>0]'(XV), YV, ZV>

and similarly

 [y<>0]'' = \<XV,YV,ZV>. <XV, [<>0]'(YV), ZV>
 [z<>0]'' = \<XV,YV,ZV>. <XV, YV, [<>0]'(ZV)>

where
        : P(N) -> P(N)
  [<>0] = \S. { <xv | xv \in S /\ xv<>0 }

        : Parity -> Parity
 [<>0]' = (from handin)



**********************************************************************
**  The [x--] operator (and friends)                                ** 
**********************************************************************

Calculating an abstract version of [x--]:

[x--]' : P(N) x P(N) x P(N)

 \S. alpha o [x--] o gamma(S)
= [def of [x--]]
 \S. alpha ( { <xv-1, yv, zv> | {<xv, yv, zv>} C gamma(S) /\ xv>0 } )
= [write S as triple]
 \<XV,YV,ZV>. alpha ( { <xv-1, yv, zv> | {<xv, yv, zv>} C gamma(<XV,YV,ZV>)
                                                          /\ xv>0 } )
= [def of gamma]
 \<XV,YV,ZV>. alpha ( { <xv-1, yv, zv> | {<xv, yv, zv>} C XV x YV x ZV
                                                          /\ xv>0 } )
= [def of Cartesian product]
 \<XV,YV,ZV>. alpha ( { <xv-1, yv, zv> | xv \in XV /\ yv in YV /\ zv in ZV
                                                          /\ xv>0 } )
= [def of Cartesian product]
 \<XV,YV,ZV>. alpha ( { <xv-1 | xv \in XV /\ xv>0 } x YV x ZV )
= [def of alpha]
 \<XV,YV,ZV>. <{ <xv-1 | xv \in XV /\ xv>0 }, YV, ZV>

Hence:

 [x--]' = \<XV,YV,ZV>. <{ <xv-1 | xv \in XV /\ xv>0 }, YV, ZV>

Similarly we get:

 [y--]' = \<XV,YV,ZV>. <XV, { <yv-1 | yv \in YV /\ yv>0 }, ZV>
 [z--]' = \<XV,YV,ZV>. <XV, YV, { <zv-1 | zv \in ZV /\ zv>0 }>

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

Calculating an abstract version [x--]'' over Parity triples:

[x--]'' : Parity x Parity x Parity


 \<XV,YV,ZV>. alpha o [x--]' o gamma(<XV,YV,ZV>)
= [def [x--]']
 \<XV,YV,ZV>. alpha o (\<XV,YV,ZV>. <{ <xv-1 | xv \in XV /\ xv>0 }, YV, ZV>)
                                                         (gamma(<XV,YV,ZV>))
= [def gamma]
 \<XV,YV,ZV>. alpha (<{ <xv-1 | xv \in gamma(XV) /\ xv>0}, gamma(YV),gamma(ZV)>)
= [def alpha]
 \<XV,YV,ZV>. (<alpha({ <xv-1 | xv \in gamma(XV) /\ xv>0}), alpha(gamma(YV)), alpha(gamma(ZV))>)
=/C. [Galois surjection/connection]
 \<XV,YV,ZV>. (<alpha({ <xv-1 | xv \in gamma(XV) /\ xv>0}), YV, ZV>)
= [factor [-1] operation]
 \<XV,YV,ZV>. (<alpha o [-1] o gamma(XV), YV, ZV>)
= [def [-1]']
 \<XV,YV,ZV>. (<[-1]'(XV), YV, ZV>)

Hence we define:

 [x--]'' = \<XV,YV,ZV>. <[-1]'(XV), YV, ZV>

and similarly

 [y--]'' = \<XV,YV,ZV>. <XV, [-1]'(YV), ZV>
 [z--]'' = \<XV,YV,ZV>. <XV, YV, [-1]'(ZV)>

where
          : P(N) -> P(N)
     [-1] = \S. { <xv-1 | xv \in S /\ xv>0 }

          : Parity -> Parity
    [-1]' = (from handin)