% https://doi.org/10.1007/978-3-030-85165-1_18
% 4.4 n-site Phosphorylation

off rlabout;



rlset r;


{}


algebraic procedure varietyStarIsNotEmpty(xl, sfl, theo);
   rlsimpl(ex(xl, notzero xl and zero sfl), theo);


varietystarisnotempty


algebraic procedure varietyStarIsCosetInv(xl, sfl, theo);
   % all({g, x}, g<>0 and x<>0 and y<>0 and F(g)=0 and F(g*x)=0 impl F(g/x)=0);
   begin
      scalar il, gl, gxl, u1in;
      scalar x_in_variety, g_in_variety, gx_in_variety, g_over_x_in_variety;
      x_in_variety := zero sfl;
      il := for each x in xl collect getIndex(x, 'x);
      gl := for each i in il collect mkid(g, i);
      gxl := append(gl, xl);
      g_in_variety := sub(
         for each i in il collect mkid(x, i) = mkid(g, i),
         x_in_variety);
      gx_in_variety := sub(
         for each i in il collect mkid(x, i) = mkid(g, i) * mkid(x, i),
         x_in_variety);
      g_over_x_in_variety := sub(
         for each i in il collect mkid(x, i) = mkid(g, i) / mkid(x, i),
         x_in_variety);
      % Inverse:
      u1in := all(gxl, notzero gxl and g_in_variety and gx_in_variety
         impl g_over_x_in_variety);
      return u1in
   end;


varietystariscosetinv


algebraic procedure varietyStarIsCosetMult(xl, sfl, theo);
   % all({g, x, y}, g<>0 and x<>0 and y<>0 and F(g)=0 and F(g*x)=0 and F(g*y)=0 impl F(g*x*y)=0);
   begin
      scalar il, yl, gl, gxl, gxyl, u1, u2, g_in_variety, u1in, u2in;
      scalar x_in_variety, gx_in_variety, gy_in_variety, gxy_in_variety, g_over_x_in_variety;
      x_in_variety := zero sfl;
      il := for each x in xl collect getIndex(x, 'x);
      gl := for each i in il collect mkid(g, i);
      yl := for each i in il collect mkid(y, i);
      gxl := append(gl, xl);
      gxyl := append(gxl, yl);
      g_in_variety := sub(
         for each i in il collect mkid(x, i) = mkid(g, i),
         x_in_variety);
      gx_in_variety := sub(
         for each i in il collect mkid(x, i) = mkid(g, i) * mkid(x, i),
         x_in_variety);
      gy_in_variety := sub(
         for each i in il collect mkid(x, i) = mkid(g, i) * mkid(y, i),
         x_in_variety);
      gxy_in_variety := sub(
         for each i in il collect
            mkid(x, i) = mkid(g, i) * mkid(x, i) * mkid(y, i),
         x_in_variety);
      u2in := all(gxyl, notzero gxyl and g_in_variety and gx_in_variety and
         gy_in_variety impl gxy_in_variety);
      return u2in
   end;


varietystariscosetmult


symbolic operator getIndex;



symbolic procedure getIndex(v, base);
   begin scalar w;
      w := explode v;
      for i := 1:length explode base do
         w := cdr w;
      return compress w
   end;


getindex


algebraic procedure notzero(vl);
   rlsimpl for each v in vl  mkand v <> 0;


notzero


algebraic procedure zero(vl);
   rlsimpl for each v in vl  mkand v = 0;


zero


algebraic procedure rename(vl, fl);
   begin
      integer j;
      scalar sb, xj, xl;
      j := 0;
      xl := sb := {};
      for each v in vl do <<
         j := j + 1;
         xj := mkid(x, j);
         xl := cons(xj, xl);
         sb := cons(v = xj, sb)
      >>;
      return {reverse xl, sub(sb, fl), reverse sb}
   end;


rename


off allfac;


on rlnzden;


on rlqeaprecise;


off rlqedfs;


off rlqefbmma;


off rlqefbqepcad;


off rlqefbslfq;


on rlsiexpl;


on rlsiexpla;



procedure npho_vectorfield(n);
   begin scalar res, w;
      res := {-k_on0 * s0 * e + k_off0 * c0 + l_cat0 * d1};
      w := for i := 1:n-1 collect <<
         - mkid(k_on, i) * mkid(s, i) * e
         + mkid(k_off, i) * mkid(c, i)
         + mkid(k_cat, i-1) * mkid(c, i-1)
         - mkid(l_on, i-1) * mkid(s, i) * f
         + mkid(l_off, i-1) * mkid(d, i)
         + mkid(l_cat, i) * mkid(d, i+1)
      >>;
      res := append(res, w);
      w := for i := 0:n-1 collect <<
         mkid(k_on, i) * mkid(s, i) * e
         - (mkid(k_off, i) + mkid(k_cat, i)) * mkid(c, i)
      >>;
      res := append(res, w);
      w := for i := 1:n collect <<
         mkid(l_on, i-1) * mkid(s, i) * f
         - (mkid(l_off, i-1) + mkid(l_cat, i-1)) * mkid(d, i)
      >>;
      res := append(res, w);
      return res
   end;


npho_vectorfield


procedure npho_parameters(n);
   begin scalar res, w;
      res := for i := 0:n-1 collect
         mkid(k_on, i);
      w := for i := 0:n-1 collect
         mkid(k_off, i);
      res := append(res, w);
      w := for i := 0:n-1 collect
         mkid(k_cat, i);
      res := append(res, w);
      w := for i := 0:n-1 collect
         mkid(l_on, i);
      res := append(res, w);
      w := for i := 0:n-1 collect
         mkid(l_off, i);
      res := append(res, w);
      w := for i := 0:n-1 collect
         mkid(l_cat, i);
      res := append(res, w);
      return res
   end;


npho_parameters


procedure npho_variables(n);
   begin scalar res, w;
      res := for i := 0:n collect
         mkid(s, i);
      w := for i := 0:n-1 collect
         mkid(c, i);
      res := append(res, w);
      w := for i := 1:n collect
         mkid(d, i);
      res := append(res, w);
      res := append(res, {e, f});
      return res
   end;


npho_variables


n := 4;


n := 4


kl := npho_parameters n;


kl := {k_on0,

       k_on1,

       k_on2,

       k_on3,

       k_off0,

       k_off1,

       k_off2,

       k_off3,

       k_cat0,

       k_cat1,

       k_cat2,

       k_cat3,

       l_on0,

       l_on1,

       l_on2,

       l_on3,

       l_off0,

       l_off1,

       l_off2,

       l_off3,

       l_cat0,

       l_cat1,

       l_cat2,

       l_cat3}

vl := npho_variables n;


vl := {s0,

       s1,

       s2,

       s3,

       s4,

       c0,

       c1,

       c2,

       c3,

       d1,

       d2,

       d3,

       d4,

       e,

       f}

ofl := npho_vectorfield n;


ofl := {c0*k_off0 + d1*l_cat0 - e*k_on0*s0,

        c0*k_cat0 + c1*k_off1 + d1*l_off0 + d2*l_cat1 - e*k_on1*s1 - f*l_on0*s1,

        c1*k_cat1 + c2*k_off2 + d2*l_off1 + d3*l_cat2 - e*k_on2*s2 - f*l_on1*s2,

        c2*k_cat2 + c3*k_off3 + d3*l_off2 + d4*l_cat3 - e*k_on3*s3 - f*l_on2*s3,

         - c0*k_cat0 - c0*k_off0 + e*k_on0*s0,

         - c1*k_cat1 - c1*k_off1 + e*k_on1*s1,

         - c2*k_cat2 - c2*k_off2 + e*k_on2*s2,

         - c3*k_cat3 - c3*k_off3 + e*k_on3*s3,

         - d1*l_cat0 - d1*l_off0 + f*l_on0*s1,

         - d2*l_cat1 - d2*l_off1 + f*l_on1*s2,

         - d3*l_cat2 - d3*l_off2 + f*l_on2*s3,

         - d4*l_cat3 - d4*l_off3 + f*l_on3*s4}


w := rename(vl, ofl)$


xl := first w;


xl := {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15}

fl := second w;


fl := {k_off0*x6 - k_on0*x1*x14 + l_cat0*x10,

       k_cat0*x6 + k_off1*x7 - k_on1*x14*x2 + l_cat1*x11 + l_off0*x10

        - l_on0*x15*x2,

       k_cat1*x7 + k_off2*x8 - k_on2*x14*x3 + l_cat2*x12 + l_off1*x11

        - l_on1*x15*x3,

       k_cat2*x8 + k_off3*x9 - k_on3*x14*x4 + l_cat3*x13 + l_off2*x12

        - l_on2*x15*x4,

        - k_cat0*x6 - k_off0*x6 + k_on0*x1*x14,

        - k_cat1*x7 - k_off1*x7 + k_on1*x14*x2,

        - k_cat2*x8 - k_off2*x8 + k_on2*x14*x3,

        - k_cat3*x9 - k_off3*x9 + k_on3*x14*x4,

        - l_cat0*x10 - l_off0*x10 + l_on0*x15*x2,

        - l_cat1*x11 - l_off1*x11 + l_on1*x15*x3,

        - l_cat2*x12 - l_off2*x12 + l_on2*x15*x4,

        - l_cat3*x13 - l_off3*x13 + l_on3*x15*x5}

third w;


{s0 = x1,

 s1 = x2,

 s2 = x3,

 s3 = x4,

 s4 = x5,

 c0 = x6,

 c1 = x7,

 c2 = x8,

 c3 = x9,

 d1 = x10,

 d2 = x11,

 d3 = x12,

 d4 = x13,

 e = x14,

 f = x15}


pos := for each k in kl collect k > 0$



% Non-emptyness of V_k^*:
phi1 := varietyStarIsNotEmpty(xl, fl, pos);


phi1 := ex x1 ex x2 ex x3 ex x4 ex x5 ex x6 ex x7 ex x8 ex x9 ex x10 ex x11 ex 

x12 ex x13 ex x14 ex x15 (x9 <> 0 and x8 <> 0 and x7 <> 0 and x6 <> 0

 and x5 <> 0 and x4 <> 0 and x3 <> 0 and x2 <> 0 and x15 <> 0 and x14 <> 0

 and x13 <> 0 and x12 <> 0 and x11 <> 0 and x10 <> 0 and x1 <> 0

 and l_cat3*x13 + l_off3*x13 - l_on3*x15*x5 = 0

 and l_cat2*x12 + l_off2*x12 - l_on2*x15*x4 = 0

 and l_cat1*x11 + l_off1*x11 - l_on1*x15*x3 = 0

 and l_cat0*x10 + l_off0*x10 - l_on0*x15*x2 = 0

 and k_off0*x6 - k_on0*x1*x14 + l_cat0*x10 = 0

 and k_cat3*x9 + k_off3*x9 - k_on3*x14*x4 = 0 and 

k_cat2*x8 + k_off3*x9 - k_on3*x14*x4 + l_cat3*x13 + l_off2*x12 - l_on2*x15*x4

 = 0 and k_cat2*x8 + k_off2*x8 - k_on2*x14*x3 = 0 and 

k_cat1*x7 + k_off2*x8 - k_on2*x14*x3 + l_cat2*x12 + l_off1*x11 - l_on1*x15*x3

 = 0 and k_cat1*x7 + k_off1*x7 - k_on1*x14*x2 = 0 and 

k_cat0*x6 + k_off1*x7 - k_on1*x14*x2 + l_cat1*x11 + l_off0*x10 - l_on0*x15*x2

 = 0 and k_cat0*x6 + k_off0*x6 - k_on0*x1*x14 = 0)

w := rlqea(phi1, pos);


w := {{true,

       {x1 = -1,

               k_cat0
        x10 = --------,
               l_cat0

                - k_cat0*k_cat1*k_on1 - k_cat1*k_off0*k_on1
        x11 = ----------------------------------------------,
                k_cat1*k_on0*l_cat1 + k_off1*k_on0*l_cat1

                     2
        x12 = (k_cat0 *k_cat1*k_cat2*k_on1*k_on2*l_cat0*l_cat1*l_on0

                        2
                + k_cat0 *k_cat1*k_cat2*k_on1*k_on2*l_cat0*l_off1*l_on0

                + 2*k_cat0*k_cat1*k_cat2*k_off0*k_on1*k_on2*l_cat0*l_cat1*l_on0

                + 2*k_cat0*k_cat1*k_cat2*k_off0*k_on1*k_on2*l_cat0*l_off1*l_on0

                                      2
                + k_cat1*k_cat2*k_off0 *k_on1*k_on2*l_cat0*l_cat1*l_on0

                                      2
                + k_cat1*k_cat2*k_off0 *k_on1*k_on2*l_cat0*l_off1*l_on0)/(

                                     2
           k_cat0*k_cat1*k_cat2*k_on0 *l_cat0*l_cat1*l_cat2*l_on1

                                        2
            + k_cat0*k_cat1*k_cat2*k_on0 *l_cat1*l_cat2*l_off0*l_on1

                                        2
            + k_cat0*k_cat1*k_off2*k_on0 *l_cat0*l_cat1*l_cat2*l_on1

                                        2
            + k_cat0*k_cat1*k_off2*k_on0 *l_cat1*l_cat2*l_off0*l_on1

                                        2
            + k_cat0*k_cat2*k_off1*k_on0 *l_cat0*l_cat1*l_cat2*l_on1

                                        2
            + k_cat0*k_cat2*k_off1*k_on0 *l_cat1*l_cat2*l_off0*l_on1

                                        2
            + k_cat0*k_off1*k_off2*k_on0 *l_cat0*l_cat1*l_cat2*l_on1

                                        2
            + k_cat0*k_off1*k_off2*k_on0 *l_cat1*l_cat2*l_off0*l_on1),

                        3                                              2
        x13 = ( - k_cat0 *k_cat1*k_cat2*k_cat3*k_on1*k_on2*k_on3*l_cat0 *l_cat1

                            2         3
               *l_cat2*l_on0  - k_cat0 *k_cat1*k_cat2*k_cat3*k_on1*k_on2*k_on3

                      2                    2         3
               *l_cat0 *l_cat1*l_off2*l_on0  - k_cat0 *k_cat1*k_cat2*k_cat3

                                        2                    2         3
               *k_on1*k_on2*k_on3*l_cat0 *l_cat2*l_off1*l_on0  - k_cat0 *k_cat1

                                                      2                    2
               *k_cat2*k_cat3*k_on1*k_on2*k_on3*l_cat0 *l_off1*l_off2*l_on0  - 3

                      2                                                     2
               *k_cat0 *k_cat1*k_cat2*k_cat3*k_off0*k_on1*k_on2*k_on3*l_cat0

                                   2           2
               *l_cat1*l_cat2*l_on0  - 3*k_cat0 *k_cat1*k_cat2*k_cat3*k_off0

                                        2                    2           2
               *k_on1*k_on2*k_on3*l_cat0 *l_cat1*l_off2*l_on0  - 3*k_cat0

                                                                    2
               *k_cat1*k_cat2*k_cat3*k_off0*k_on1*k_on2*k_on3*l_cat0 *l_cat2

                            2           2
               *l_off1*l_on0  - 3*k_cat0 *k_cat1*k_cat2*k_cat3*k_off0*k_on1

                                  2                    2
               *k_on2*k_on3*l_cat0 *l_off1*l_off2*l_on0  - 3*k_cat0*k_cat1

                                    2                         2
               *k_cat2*k_cat3*k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_cat1*l_cat2

                     2                                       2
               *l_on0  - 3*k_cat0*k_cat1*k_cat2*k_cat3*k_off0 *k_on1*k_on2*k_on3

                      2                    2
               *l_cat0 *l_cat1*l_off2*l_on0  - 3*k_cat0*k_cat1*k_cat2*k_cat3

                      2                         2                    2
               *k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_cat2*l_off1*l_on0  - 3

                                                  2                         2
               *k_cat0*k_cat1*k_cat2*k_cat3*k_off0 *k_on1*k_on2*k_on3*l_cat0

                                   2                              3
               *l_off1*l_off2*l_on0  - k_cat1*k_cat2*k_cat3*k_off0 *k_on1*k_on2

                            2                    2
               *k_on3*l_cat0 *l_cat1*l_cat2*l_on0  - k_cat1*k_cat2*k_cat3

                      3                         2                    2
               *k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_cat1*l_off2*l_on0  - k_cat1

                                    3                         2
               *k_cat2*k_cat3*k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_cat2*l_off1

                     2                              3                         2
               *l_on0  - k_cat1*k_cat2*k_cat3*k_off0 *k_on1*k_on2*k_on3*l_cat0

                                   2         2                           3
               *l_off1*l_off2*l_on0 )/(k_cat0 *k_cat1*k_cat2*k_cat3*k_on0

                  2                                            2
           *l_cat0 *l_cat1*l_cat2*l_cat3*l_on1*l_on2 + 2*k_cat0 *k_cat1*k_cat2

                        3
           *k_cat3*k_on0 *l_cat0*l_cat1*l_cat2*l_cat3*l_off0*l_on1*l_on2 + 

                 2                           3                            2
           k_cat0 *k_cat1*k_cat2*k_cat3*k_on0 *l_cat1*l_cat2*l_cat3*l_off0

                                2                           3       2
           *l_on1*l_on2 + k_cat0 *k_cat1*k_cat2*k_off3*k_on0 *l_cat0 *l_cat1

                                                2                           3
           *l_cat2*l_cat3*l_on1*l_on2 + 2*k_cat0 *k_cat1*k_cat2*k_off3*k_on0

                                                                   2
           *l_cat0*l_cat1*l_cat2*l_cat3*l_off0*l_on1*l_on2 + k_cat0 *k_cat1

                               3                            2
           *k_cat2*k_off3*k_on0 *l_cat1*l_cat2*l_cat3*l_off0 *l_on1*l_on2 + 

                 2                           3       2
           k_cat0 *k_cat1*k_cat3*k_off2*k_on0 *l_cat0 *l_cat1*l_cat2*l_cat3

                                  2                           3
           *l_on1*l_on2 + 2*k_cat0 *k_cat1*k_cat3*k_off2*k_on0 *l_cat0*l_cat1

                                                     2
           *l_cat2*l_cat3*l_off0*l_on1*l_on2 + k_cat0 *k_cat1*k_cat3*k_off2

                 3                            2                     2
           *k_on0 *l_cat1*l_cat2*l_cat3*l_off0 *l_on1*l_on2 + k_cat0 *k_cat1

                               3       2
           *k_off2*k_off3*k_on0 *l_cat0 *l_cat1*l_cat2*l_cat3*l_on1*l_on2 + 2

                  2                           3
           *k_cat0 *k_cat1*k_off2*k_off3*k_on0 *l_cat0*l_cat1*l_cat2*l_cat3

                                       2                           3
           *l_off0*l_on1*l_on2 + k_cat0 *k_cat1*k_off2*k_off3*k_on0 *l_cat1

                                2                     2
           *l_cat2*l_cat3*l_off0 *l_on1*l_on2 + k_cat0 *k_cat2*k_cat3*k_off1

                 3       2                                            2
           *k_on0 *l_cat0 *l_cat1*l_cat2*l_cat3*l_on1*l_on2 + 2*k_cat0 *k_cat2

                               3
           *k_cat3*k_off1*k_on0 *l_cat0*l_cat1*l_cat2*l_cat3*l_off0*l_on1*l_on2 

                   2                           3                            2
           + k_cat0 *k_cat2*k_cat3*k_off1*k_on0 *l_cat1*l_cat2*l_cat3*l_off0

                                2                           3       2
           *l_on1*l_on2 + k_cat0 *k_cat2*k_off1*k_off3*k_on0 *l_cat0 *l_cat1

                                                2                           3
           *l_cat2*l_cat3*l_on1*l_on2 + 2*k_cat0 *k_cat2*k_off1*k_off3*k_on0

                                                                   2
           *l_cat0*l_cat1*l_cat2*l_cat3*l_off0*l_on1*l_on2 + k_cat0 *k_cat2

                               3                            2
           *k_off1*k_off3*k_on0 *l_cat1*l_cat2*l_cat3*l_off0 *l_on1*l_on2 + 

                 2                           3       2
           k_cat0 *k_cat3*k_off1*k_off2*k_on0 *l_cat0 *l_cat1*l_cat2*l_cat3

                                  2                           3
           *l_on1*l_on2 + 2*k_cat0 *k_cat3*k_off1*k_off2*k_on0 *l_cat0*l_cat1

                                                     2
           *l_cat2*l_cat3*l_off0*l_on1*l_on2 + k_cat0 *k_cat3*k_off1*k_off2

                 3                            2                     2
           *k_on0 *l_cat1*l_cat2*l_cat3*l_off0 *l_on1*l_on2 + k_cat0 *k_off1

                               3       2
           *k_off2*k_off3*k_on0 *l_cat0 *l_cat1*l_cat2*l_cat3*l_on1*l_on2 + 2

                  2                           3
           *k_cat0 *k_off1*k_off2*k_off3*k_on0 *l_cat0*l_cat1*l_cat2*l_cat3

                                       2                           3
           *l_off0*l_on1*l_on2 + k_cat0 *k_off1*k_off2*k_off3*k_on0 *l_cat1

                                2
           *l_cat2*l_cat3*l_off0 *l_on1*l_on2),

                - k_cat0 - k_off0
        x14 = --------------------,
                     k_on0

               k_cat0*l_cat0 + k_cat0*l_off0
        x15 = -------------------------------,
                       l_cat0*l_on0

        x2 = 1,

        x3 = ( - k_cat0*k_cat1*k_on1*l_cat0*l_cat1*l_on0

               - k_cat0*k_cat1*k_on1*l_cat0*l_off1*l_on0

               - k_cat1*k_off0*k_on1*l_cat0*l_cat1*l_on0

               - k_cat1*k_off0*k_on1*l_cat0*l_off1*l_on0)/(

           k_cat0*k_cat1*k_on0*l_cat0*l_cat1*l_on1

            + k_cat0*k_cat1*k_on0*l_cat1*l_off0*l_on1

            + k_cat0*k_off1*k_on0*l_cat0*l_cat1*l_on1

            + k_cat0*k_off1*k_on0*l_cat1*l_off0*l_on1),

                    2                                 2                    2
        x4 = (k_cat0 *k_cat1*k_cat2*k_on1*k_on2*l_cat0 *l_cat1*l_cat2*l_on0

                       2                                 2                    2
               + k_cat0 *k_cat1*k_cat2*k_on1*k_on2*l_cat0 *l_cat1*l_off2*l_on0

                       2                                 2                    2
               + k_cat0 *k_cat1*k_cat2*k_on1*k_on2*l_cat0 *l_cat2*l_off1*l_on0

                       2                                 2                    2
               + k_cat0 *k_cat1*k_cat2*k_on1*k_on2*l_cat0 *l_off1*l_off2*l_on0  

                                                                2
              + 2*k_cat0*k_cat1*k_cat2*k_off0*k_on1*k_on2*l_cat0 *l_cat1*l_cat2

                    2                                                   2
              *l_on0  + 2*k_cat0*k_cat1*k_cat2*k_off0*k_on1*k_on2*l_cat0 *l_cat1

                           2                                                   2
              *l_off2*l_on0  + 2*k_cat0*k_cat1*k_cat2*k_off0*k_on1*k_on2*l_cat0

                                  2
              *l_cat2*l_off1*l_on0  + 2*k_cat0*k_cat1*k_cat2*k_off0*k_on1*k_on2

                     2                    2
              *l_cat0 *l_off1*l_off2*l_on0

                                     2                   2                    2
               + k_cat1*k_cat2*k_off0 *k_on1*k_on2*l_cat0 *l_cat1*l_cat2*l_on0

                                     2                   2                    2
               + k_cat1*k_cat2*k_off0 *k_on1*k_on2*l_cat0 *l_cat1*l_off2*l_on0

                                     2                   2                    2
               + k_cat1*k_cat2*k_off0 *k_on1*k_on2*l_cat0 *l_cat2*l_off1*l_on0

                                     2                   2                    2
               + k_cat1*k_cat2*k_off0 *k_on1*k_on2*l_cat0 *l_off1*l_off2*l_on0 )

                2                    2       2
        /(k_cat0 *k_cat1*k_cat2*k_on0 *l_cat0 *l_cat1*l_cat2*l_on1*l_on2 + 2

                 2                    2
          *k_cat0 *k_cat1*k_cat2*k_on0 *l_cat0*l_cat1*l_cat2*l_off0*l_on1*l_on2

                   2                    2                     2
           + k_cat0 *k_cat1*k_cat2*k_on0 *l_cat1*l_cat2*l_off0 *l_on1*l_on2

                   2                    2       2
           + k_cat0 *k_cat1*k_off2*k_on0 *l_cat0 *l_cat1*l_cat2*l_on1*l_on2 + 2

                 2                    2
          *k_cat0 *k_cat1*k_off2*k_on0 *l_cat0*l_cat1*l_cat2*l_off0*l_on1*l_on2

                   2                    2                     2
           + k_cat0 *k_cat1*k_off2*k_on0 *l_cat1*l_cat2*l_off0 *l_on1*l_on2

                   2                    2       2
           + k_cat0 *k_cat2*k_off1*k_on0 *l_cat0 *l_cat1*l_cat2*l_on1*l_on2 + 2

                 2                    2
          *k_cat0 *k_cat2*k_off1*k_on0 *l_cat0*l_cat1*l_cat2*l_off0*l_on1*l_on2

                   2                    2                     2
           + k_cat0 *k_cat2*k_off1*k_on0 *l_cat1*l_cat2*l_off0 *l_on1*l_on2

                   2                    2       2
           + k_cat0 *k_off1*k_off2*k_on0 *l_cat0 *l_cat1*l_cat2*l_on1*l_on2 + 2

                 2                    2
          *k_cat0 *k_off1*k_off2*k_on0 *l_cat0*l_cat1*l_cat2*l_off0*l_on1*l_on2

                   2                    2                     2
           + k_cat0 *k_off1*k_off2*k_on0 *l_cat1*l_cat2*l_off0 *l_on1*l_on2),

                       3                                              3
        x5 = ( - k_cat0 *k_cat1*k_cat2*k_cat3*k_on1*k_on2*k_on3*l_cat0 *l_cat1

                                  3         3
              *l_cat2*l_cat3*l_on0  - k_cat0 *k_cat1*k_cat2*k_cat3*k_on1*k_on2

                           3                           3         3
              *k_on3*l_cat0 *l_cat1*l_cat2*l_off3*l_on0  - k_cat0 *k_cat1*k_cat2

                                              3                           3
              *k_cat3*k_on1*k_on2*k_on3*l_cat0 *l_cat1*l_cat3*l_off2*l_on0  - 

                    3                                              3
              k_cat0 *k_cat1*k_cat2*k_cat3*k_on1*k_on2*k_on3*l_cat0 *l_cat1

                                  3         3
              *l_off2*l_off3*l_on0  - k_cat0 *k_cat1*k_cat2*k_cat3*k_on1*k_on2

                           3                           3         3
              *k_on3*l_cat0 *l_cat2*l_cat3*l_off1*l_on0  - k_cat0 *k_cat1*k_cat2

                                              3                           3
              *k_cat3*k_on1*k_on2*k_on3*l_cat0 *l_cat2*l_off1*l_off3*l_on0  - 

                    3                                              3
              k_cat0 *k_cat1*k_cat2*k_cat3*k_on1*k_on2*k_on3*l_cat0 *l_cat3

                                  3         3
              *l_off1*l_off2*l_on0  - k_cat0 *k_cat1*k_cat2*k_cat3*k_on1*k_on2

                           3                           3           2
              *k_on3*l_cat0 *l_off1*l_off2*l_off3*l_on0  - 3*k_cat0 *k_cat1

                                                            3
              *k_cat2*k_cat3*k_off0*k_on1*k_on2*k_on3*l_cat0 *l_cat1*l_cat2

                           3           2
              *l_cat3*l_on0  - 3*k_cat0 *k_cat1*k_cat2*k_cat3*k_off0*k_on1*k_on2

                           3                           3           2
              *k_on3*l_cat0 *l_cat1*l_cat2*l_off3*l_on0  - 3*k_cat0 *k_cat1

                                                            3
              *k_cat2*k_cat3*k_off0*k_on1*k_on2*k_on3*l_cat0 *l_cat1*l_cat3

                           3           2
              *l_off2*l_on0  - 3*k_cat0 *k_cat1*k_cat2*k_cat3*k_off0*k_on1*k_on2

                           3                           3           2
              *k_on3*l_cat0 *l_cat1*l_off2*l_off3*l_on0  - 3*k_cat0 *k_cat1

                                                            3
              *k_cat2*k_cat3*k_off0*k_on1*k_on2*k_on3*l_cat0 *l_cat2*l_cat3

                           3           2
              *l_off1*l_on0  - 3*k_cat0 *k_cat1*k_cat2*k_cat3*k_off0*k_on1*k_on2

                           3                           3           2
              *k_on3*l_cat0 *l_cat2*l_off1*l_off3*l_on0  - 3*k_cat0 *k_cat1

                                                            3
              *k_cat2*k_cat3*k_off0*k_on1*k_on2*k_on3*l_cat0 *l_cat3*l_off1

                           3           2
              *l_off2*l_on0  - 3*k_cat0 *k_cat1*k_cat2*k_cat3*k_off0*k_on1*k_on2

                           3                           3
              *k_on3*l_cat0 *l_off1*l_off2*l_off3*l_on0  - 3*k_cat0*k_cat1

                                   2                         3
              *k_cat2*k_cat3*k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_cat1*l_cat2

                           3                                       2
              *l_cat3*l_on0  - 3*k_cat0*k_cat1*k_cat2*k_cat3*k_off0 *k_on1*k_on2

                           3                           3
              *k_on3*l_cat0 *l_cat1*l_cat2*l_off3*l_on0  - 3*k_cat0*k_cat1

                                   2                         3
              *k_cat2*k_cat3*k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_cat1*l_cat3

                           3                                       2
              *l_off2*l_on0  - 3*k_cat0*k_cat1*k_cat2*k_cat3*k_off0 *k_on1*k_on2

                           3                           3
              *k_on3*l_cat0 *l_cat1*l_off2*l_off3*l_on0  - 3*k_cat0*k_cat1

                                   2                         3
              *k_cat2*k_cat3*k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_cat2*l_cat3

                           3                                       2
              *l_off1*l_on0  - 3*k_cat0*k_cat1*k_cat2*k_cat3*k_off0 *k_on1*k_on2

                           3                           3
              *k_on3*l_cat0 *l_cat2*l_off1*l_off3*l_on0  - 3*k_cat0*k_cat1

                                   2                         3
              *k_cat2*k_cat3*k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_cat3*l_off1

                           3                                       2
              *l_off2*l_on0  - 3*k_cat0*k_cat1*k_cat2*k_cat3*k_off0 *k_on1*k_on2

                           3                           3
              *k_on3*l_cat0 *l_off1*l_off2*l_off3*l_on0  - k_cat1*k_cat2*k_cat3

                     3                         3                           3
              *k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_cat1*l_cat2*l_cat3*l_on0  - 

                                         3                         3
              k_cat1*k_cat2*k_cat3*k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_cat1

                                  3                              3
              *l_cat2*l_off3*l_on0  - k_cat1*k_cat2*k_cat3*k_off0 *k_on1*k_on2

                           3                           3
              *k_on3*l_cat0 *l_cat1*l_cat3*l_off2*l_on0  - k_cat1*k_cat2*k_cat3

                     3                         3                           3
              *k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_cat1*l_off2*l_off3*l_on0  - 

                                         3                         3
              k_cat1*k_cat2*k_cat3*k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_cat2

                                  3                              3
              *l_cat3*l_off1*l_on0  - k_cat1*k_cat2*k_cat3*k_off0 *k_on1*k_on2

                           3                           3
              *k_on3*l_cat0 *l_cat2*l_off1*l_off3*l_on0  - k_cat1*k_cat2*k_cat3

                     3                         3                           3
              *k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_cat3*l_off1*l_off2*l_on0  - 

                                         3                         3
              k_cat1*k_cat2*k_cat3*k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_off1

                                  3         3                           3
              *l_off2*l_off3*l_on0 )/(k_cat0 *k_cat1*k_cat2*k_cat3*k_on0

                  3                                                  3
           *l_cat0 *l_cat1*l_cat2*l_cat3*l_on1*l_on2*l_on3 + 3*k_cat0 *k_cat1

                               3       2
           *k_cat2*k_cat3*k_on0 *l_cat0 *l_cat1*l_cat2*l_cat3*l_off0*l_on1*l_on2

                            3                           3
           *l_on3 + 3*k_cat0 *k_cat1*k_cat2*k_cat3*k_on0 *l_cat0*l_cat1*l_cat2

                         2                           3
           *l_cat3*l_off0 *l_on1*l_on2*l_on3 + k_cat0 *k_cat1*k_cat2*k_cat3

                 3                            3                           3
           *k_on0 *l_cat1*l_cat2*l_cat3*l_off0 *l_on1*l_on2*l_on3 + k_cat0

                                      3       3
           *k_cat1*k_cat2*k_off3*k_on0 *l_cat0 *l_cat1*l_cat2*l_cat3*l_on1*l_on2

                            3                           3       2
           *l_on3 + 3*k_cat0 *k_cat1*k_cat2*k_off3*k_on0 *l_cat0 *l_cat1*l_cat2

                                                      3
           *l_cat3*l_off0*l_on1*l_on2*l_on3 + 3*k_cat0 *k_cat1*k_cat2*k_off3

                 3                                   2
           *k_on0 *l_cat0*l_cat1*l_cat2*l_cat3*l_off0 *l_on1*l_on2*l_on3 + 

                 3                           3                            3
           k_cat0 *k_cat1*k_cat2*k_off3*k_on0 *l_cat1*l_cat2*l_cat3*l_off0

                                      3                           3       3
           *l_on1*l_on2*l_on3 + k_cat0 *k_cat1*k_cat3*k_off2*k_on0 *l_cat0

                                                             3
           *l_cat1*l_cat2*l_cat3*l_on1*l_on2*l_on3 + 3*k_cat0 *k_cat1*k_cat3

                        3       2
           *k_off2*k_on0 *l_cat0 *l_cat1*l_cat2*l_cat3*l_off0*l_on1*l_on2*l_on3 

                     3                           3
           + 3*k_cat0 *k_cat1*k_cat3*k_off2*k_on0 *l_cat0*l_cat1*l_cat2*l_cat3

                  2                           3                           3
           *l_off0 *l_on1*l_on2*l_on3 + k_cat0 *k_cat1*k_cat3*k_off2*k_on0

                                       3                           3
           *l_cat1*l_cat2*l_cat3*l_off0 *l_on1*l_on2*l_on3 + k_cat0 *k_cat1

                               3       3
           *k_off2*k_off3*k_on0 *l_cat0 *l_cat1*l_cat2*l_cat3*l_on1*l_on2*l_on3 

                     3                           3       2
           + 3*k_cat0 *k_cat1*k_off2*k_off3*k_on0 *l_cat0 *l_cat1*l_cat2*l_cat3

                                               3                           3
           *l_off0*l_on1*l_on2*l_on3 + 3*k_cat0 *k_cat1*k_off2*k_off3*k_on0

                                              2                           3
           *l_cat0*l_cat1*l_cat2*l_cat3*l_off0 *l_on1*l_on2*l_on3 + k_cat0

                                      3                            3
           *k_cat1*k_off2*k_off3*k_on0 *l_cat1*l_cat2*l_cat3*l_off0 *l_on1*l_on2

                          3                           3       3
           *l_on3 + k_cat0 *k_cat2*k_cat3*k_off1*k_on0 *l_cat0 *l_cat1*l_cat2

                                               3                           3
           *l_cat3*l_on1*l_on2*l_on3 + 3*k_cat0 *k_cat2*k_cat3*k_off1*k_on0

                  2                                                         3
           *l_cat0 *l_cat1*l_cat2*l_cat3*l_off0*l_on1*l_on2*l_on3 + 3*k_cat0

                                      3                                   2
           *k_cat2*k_cat3*k_off1*k_on0 *l_cat0*l_cat1*l_cat2*l_cat3*l_off0

                                      3                           3
           *l_on1*l_on2*l_on3 + k_cat0 *k_cat2*k_cat3*k_off1*k_on0 *l_cat1

                                3                           3
           *l_cat2*l_cat3*l_off0 *l_on1*l_on2*l_on3 + k_cat0 *k_cat2*k_off1

                        3       3
           *k_off3*k_on0 *l_cat0 *l_cat1*l_cat2*l_cat3*l_on1*l_on2*l_on3 + 3

                  3                           3       2
           *k_cat0 *k_cat2*k_off1*k_off3*k_on0 *l_cat0 *l_cat1*l_cat2*l_cat3

                                               3                           3
           *l_off0*l_on1*l_on2*l_on3 + 3*k_cat0 *k_cat2*k_off1*k_off3*k_on0

                                              2                           3
           *l_cat0*l_cat1*l_cat2*l_cat3*l_off0 *l_on1*l_on2*l_on3 + k_cat0

                                      3                            3
           *k_cat2*k_off1*k_off3*k_on0 *l_cat1*l_cat2*l_cat3*l_off0 *l_on1*l_on2

                          3                           3       3
           *l_on3 + k_cat0 *k_cat3*k_off1*k_off2*k_on0 *l_cat0 *l_cat1*l_cat2

                                               3                           3
           *l_cat3*l_on1*l_on2*l_on3 + 3*k_cat0 *k_cat3*k_off1*k_off2*k_on0

                  2                                                         3
           *l_cat0 *l_cat1*l_cat2*l_cat3*l_off0*l_on1*l_on2*l_on3 + 3*k_cat0

                                      3                                   2
           *k_cat3*k_off1*k_off2*k_on0 *l_cat0*l_cat1*l_cat2*l_cat3*l_off0

                                      3                           3
           *l_on1*l_on2*l_on3 + k_cat0 *k_cat3*k_off1*k_off2*k_on0 *l_cat1

                                3                           3
           *l_cat2*l_cat3*l_off0 *l_on1*l_on2*l_on3 + k_cat0 *k_off1*k_off2

                        3       3
           *k_off3*k_on0 *l_cat0 *l_cat1*l_cat2*l_cat3*l_on1*l_on2*l_on3 + 3

                  3                           3       2
           *k_cat0 *k_off1*k_off2*k_off3*k_on0 *l_cat0 *l_cat1*l_cat2*l_cat3

                                               3                           3
           *l_off0*l_on1*l_on2*l_on3 + 3*k_cat0 *k_off1*k_off2*k_off3*k_on0

                                              2                           3
           *l_cat0*l_cat1*l_cat2*l_cat3*l_off0 *l_on1*l_on2*l_on3 + k_cat0

                                      3                            3
           *k_off1*k_off2*k_off3*k_on0 *l_cat1*l_cat2*l_cat3*l_off0 *l_on1*l_on2

           *l_on3),

        x6 = 1,

               - k_cat0*k_on1 - k_off0*k_on1
        x7 = --------------------------------,
               k_cat1*k_on0 + k_off1*k_on0

                    2
        x8 = (k_cat0 *k_cat1*k_on1*k_on2*l_cat0*l_cat1*l_on0

                       2
               + k_cat0 *k_cat1*k_on1*k_on2*l_cat0*l_off1*l_on0

               + 2*k_cat0*k_cat1*k_off0*k_on1*k_on2*l_cat0*l_cat1*l_on0

               + 2*k_cat0*k_cat1*k_off0*k_on1*k_on2*l_cat0*l_off1*l_on0

                              2
               + k_cat1*k_off0 *k_on1*k_on2*l_cat0*l_cat1*l_on0

                              2
               + k_cat1*k_off0 *k_on1*k_on2*l_cat0*l_off1*l_on0)/(

                                     2
           k_cat0*k_cat1*k_cat2*k_on0 *l_cat0*l_cat1*l_on1

                                        2
            + k_cat0*k_cat1*k_cat2*k_on0 *l_cat1*l_off0*l_on1

                                        2
            + k_cat0*k_cat1*k_off2*k_on0 *l_cat0*l_cat1*l_on1

                                        2
            + k_cat0*k_cat1*k_off2*k_on0 *l_cat1*l_off0*l_on1

                                        2
            + k_cat0*k_cat2*k_off1*k_on0 *l_cat0*l_cat1*l_on1

                                        2
            + k_cat0*k_cat2*k_off1*k_on0 *l_cat1*l_off0*l_on1

                                        2
            + k_cat0*k_off1*k_off2*k_on0 *l_cat0*l_cat1*l_on1

                                        2
            + k_cat0*k_off1*k_off2*k_on0 *l_cat1*l_off0*l_on1),

                       3                                       2
        x9 = ( - k_cat0 *k_cat1*k_cat2*k_on1*k_on2*k_on3*l_cat0 *l_cat1*l_cat2

                    2         3                                       2
              *l_on0  - k_cat0 *k_cat1*k_cat2*k_on1*k_on2*k_on3*l_cat0 *l_cat1

                           2         3                                       2
              *l_off2*l_on0  - k_cat0 *k_cat1*k_cat2*k_on1*k_on2*k_on3*l_cat0

                                  2         3
              *l_cat2*l_off1*l_on0  - k_cat0 *k_cat1*k_cat2*k_on1*k_on2*k_on3

                     2                    2           2
              *l_cat0 *l_off1*l_off2*l_on0  - 3*k_cat0 *k_cat1*k_cat2*k_off0

                                       2                    2           2
              *k_on1*k_on2*k_on3*l_cat0 *l_cat1*l_cat2*l_on0  - 3*k_cat0 *k_cat1

                                                     2                    2
              *k_cat2*k_off0*k_on1*k_on2*k_on3*l_cat0 *l_cat1*l_off2*l_on0  - 3

                     2                                              2
              *k_cat0 *k_cat1*k_cat2*k_off0*k_on1*k_on2*k_on3*l_cat0 *l_cat2

                           2           2
              *l_off1*l_on0  - 3*k_cat0 *k_cat1*k_cat2*k_off0*k_on1*k_on2*k_on3

                     2                    2                                2
              *l_cat0 *l_off1*l_off2*l_on0  - 3*k_cat0*k_cat1*k_cat2*k_off0

                                       2                    2
              *k_on1*k_on2*k_on3*l_cat0 *l_cat1*l_cat2*l_on0  - 3*k_cat0*k_cat1

                            2                         2                    2
              *k_cat2*k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_cat1*l_off2*l_on0  - 3

                                          2                         2
              *k_cat0*k_cat1*k_cat2*k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_cat2

                           2                                2
              *l_off1*l_on0  - 3*k_cat0*k_cat1*k_cat2*k_off0 *k_on1*k_on2*k_on3

                     2                    2                       3
              *l_cat0 *l_off1*l_off2*l_on0  - k_cat1*k_cat2*k_off0 *k_on1*k_on2

                           2                    2                       3
              *k_on3*l_cat0 *l_cat1*l_cat2*l_on0  - k_cat1*k_cat2*k_off0 *k_on1

                                 2                    2                       3
              *k_on2*k_on3*l_cat0 *l_cat1*l_off2*l_on0  - k_cat1*k_cat2*k_off0

                                       2                    2
              *k_on1*k_on2*k_on3*l_cat0 *l_cat2*l_off1*l_on0  - k_cat1*k_cat2

                     3                         2                    2
              *k_off0 *k_on1*k_on2*k_on3*l_cat0 *l_off1*l_off2*l_on0 )/(

                 2                           3       2
           k_cat0 *k_cat1*k_cat2*k_cat3*k_on0 *l_cat0 *l_cat1*l_cat2*l_on1*l_on2

                      2                           3
            + 2*k_cat0 *k_cat1*k_cat2*k_cat3*k_on0 *l_cat0*l_cat1*l_cat2*l_off0

                                2                           3
           *l_on1*l_on2 + k_cat0 *k_cat1*k_cat2*k_cat3*k_on0 *l_cat1*l_cat2

                  2                     2                           3       2
           *l_off0 *l_on1*l_on2 + k_cat0 *k_cat1*k_cat2*k_off3*k_on0 *l_cat0

                                                2                           3
           *l_cat1*l_cat2*l_on1*l_on2 + 2*k_cat0 *k_cat1*k_cat2*k_off3*k_on0

                                                            2
           *l_cat0*l_cat1*l_cat2*l_off0*l_on1*l_on2 + k_cat0 *k_cat1*k_cat2

                        3                     2                     2
           *k_off3*k_on0 *l_cat1*l_cat2*l_off0 *l_on1*l_on2 + k_cat0 *k_cat1

                               3       2                                     2
           *k_cat3*k_off2*k_on0 *l_cat0 *l_cat1*l_cat2*l_on1*l_on2 + 2*k_cat0

                                      3
           *k_cat1*k_cat3*k_off2*k_on0 *l_cat0*l_cat1*l_cat2*l_off0*l_on1*l_on2 

                   2                           3                     2
           + k_cat0 *k_cat1*k_cat3*k_off2*k_on0 *l_cat1*l_cat2*l_off0 *l_on1

                          2                           3       2
           *l_on2 + k_cat0 *k_cat1*k_off2*k_off3*k_on0 *l_cat0 *l_cat1*l_cat2

                                  2                           3
           *l_on1*l_on2 + 2*k_cat0 *k_cat1*k_off2*k_off3*k_on0 *l_cat0*l_cat1

                                              2                           3
           *l_cat2*l_off0*l_on1*l_on2 + k_cat0 *k_cat1*k_off2*k_off3*k_on0

                                2                     2
           *l_cat1*l_cat2*l_off0 *l_on1*l_on2 + k_cat0 *k_cat2*k_cat3*k_off1

                 3       2                                     2
           *k_on0 *l_cat0 *l_cat1*l_cat2*l_on1*l_on2 + 2*k_cat0 *k_cat2*k_cat3

                        3                                                 2
           *k_off1*k_on0 *l_cat0*l_cat1*l_cat2*l_off0*l_on1*l_on2 + k_cat0

                                      3                     2
           *k_cat2*k_cat3*k_off1*k_on0 *l_cat1*l_cat2*l_off0 *l_on1*l_on2 + 

                 2                           3       2
           k_cat0 *k_cat2*k_off1*k_off3*k_on0 *l_cat0 *l_cat1*l_cat2*l_on1*l_on2

                      2                           3
            + 2*k_cat0 *k_cat2*k_off1*k_off3*k_on0 *l_cat0*l_cat1*l_cat2*l_off0

                                2                           3
           *l_on1*l_on2 + k_cat0 *k_cat2*k_off1*k_off3*k_on0 *l_cat1*l_cat2

                  2                     2                           3       2
           *l_off0 *l_on1*l_on2 + k_cat0 *k_cat3*k_off1*k_off2*k_on0 *l_cat0

                                                2                           3
           *l_cat1*l_cat2*l_on1*l_on2 + 2*k_cat0 *k_cat3*k_off1*k_off2*k_on0

                                                            2
           *l_cat0*l_cat1*l_cat2*l_off0*l_on1*l_on2 + k_cat0 *k_cat3*k_off1

                        3                     2                     2
           *k_off2*k_on0 *l_cat1*l_cat2*l_off0 *l_on1*l_on2 + k_cat0 *k_off1

                               3       2                                     2
           *k_off2*k_off3*k_on0 *l_cat0 *l_cat1*l_cat2*l_on1*l_on2 + 2*k_cat0

                                      3
           *k_off1*k_off2*k_off3*k_on0 *l_cat0*l_cat1*l_cat2*l_off0*l_on1*l_on2 

                   2                           3                     2
           + k_cat0 *k_off1*k_off2*k_off3*k_on0 *l_cat1*l_cat2*l_off0 *l_on1

           *l_on2)}}}

phi1_ := rlsimpl(for each case in w mkor first case, pos);


phi1_ := true


% Shifted completeness under inverses:
phi2 := varietyStarIsCosetInv(xl, fl, pos);


phi2 := all g1 all g2 all g3 all g4 all g5 all g6 all g7 all g8 all g9 all g10 

all g11 all g12 all g13 all g14 all g15 all x1 all x2 all x3 all x4 all x5 all 

x6 all x7 all x8 all x9 all x10 all x11 all x12 all x13 all x14 all x15 (((

x9 <> 0 and x8 <> 0 and x7 <> 0 and x6 <> 0 and x5 <> 0 and x4 <> 0 and x3 <> 0

 and x2 <> 0 and x15 <> 0 and x14 <> 0 and x13 <> 0 and x12 <> 0 and x11 <> 0

 and x10 <> 0 and x1 <> 0 and g9 <> 0 and g8 <> 0 and g7 <> 0 and g6 <> 0

 and g5 <> 0 and g4 <> 0 and g3 <> 0 and g2 <> 0 and g15 <> 0 and g14 <> 0

 and g13 <> 0 and g12 <> 0 and g11 <> 0 and g10 <> 0 and g1 <> 0) and (

g13*l_cat3 + g13*l_off3 - g15*g5*l_on3 = 0

 and g12*l_cat2 + g12*l_off2 - g15*g4*l_on2 = 0

 and g11*l_cat1 + g11*l_off1 - g15*g3*l_on1 = 0

 and g10*l_cat0 + g10*l_off0 - g15*g2*l_on0 = 0

 and  - g1*g14*k_on0 + g10*l_cat0 + g6*k_off0 = 0

 and  - g14*g4*k_on3 + g9*k_cat3 + g9*k_off3 = 0 and 

g12*l_off2 + g13*l_cat3 - g14*g4*k_on3 - g15*g4*l_on2 + g8*k_cat2 + g9*k_off3

 = 0 and  - g14*g3*k_on2 + g8*k_cat2 + g8*k_off2 = 0 and 

g11*l_off1 + g12*l_cat2 - g14*g3*k_on2 - g15*g3*l_on1 + g7*k_cat1 + g8*k_off2

 = 0 and  - g14*g2*k_on1 + g7*k_cat1 + g7*k_off1 = 0 and 

g10*l_off0 + g11*l_cat1 - g14*g2*k_on1 - g15*g2*l_on0 + g6*k_cat0 + g7*k_off1

 = 0 and  - g1*g14*k_on0 + g6*k_cat0 + g6*k_off0 = 0) and (

g13*l_cat3*x13 + g13*l_off3*x13 - g15*g5*l_on3*x15*x5 = 0

 and g12*l_cat2*x12 + g12*l_off2*x12 - g15*g4*l_on2*x15*x4 = 0

 and g11*l_cat1*x11 + g11*l_off1*x11 - g15*g3*l_on1*x15*x3 = 0

 and g10*l_cat0*x10 + g10*l_off0*x10 - g15*g2*l_on0*x15*x2 = 0

 and  - g1*g14*k_on0*x1*x14 + g10*l_cat0*x10 + g6*k_off0*x6 = 0

 and  - g14*g4*k_on3*x14*x4 + g9*k_cat3*x9 + g9*k_off3*x9 = 0 and g12*l_off2*x12

 + g13*l_cat3*x13 - g14*g4*k_on3*x14*x4 - g15*g4*l_on2*x15*x4 + g8*k_cat2*x8

 + g9*k_off3*x9 = 0 and  - g14*g3*k_on2*x14*x3 + g8*k_cat2*x8 + g8*k_off2*x8 = 0

 and g11*l_off1*x11 + g12*l_cat2*x12 - g14*g3*k_on2*x14*x3 - g15*g3*l_on1*x15*x3

 + g7*k_cat1*x7 + g8*k_off2*x8 = 0

 and  - g14*g2*k_on1*x14*x2 + g7*k_cat1*x7 + g7*k_off1*x7 = 0 and g10*l_off0*x10

 + g11*l_cat1*x11 - g14*g2*k_on1*x14*x2 - g15*g2*l_on0*x15*x2 + g6*k_cat0*x6

 + g7*k_off1*x7 = 0 and  - g1*g14*k_on0*x1*x14 + g6*k_cat0*x6 + g6*k_off0*x6 = 0

)) impl (g13*l_cat3*x15*x5 + g13*l_off3*x15*x5 - g15*g5*l_on3*x13 = 0

 and g12*l_cat2*x15*x4 + g12*l_off2*x15*x4 - g15*g4*l_on2*x12 = 0

 and g11*l_cat1*x15*x3 + g11*l_off1*x15*x3 - g15*g3*l_on1*x11 = 0

 and g10*l_cat0*x15*x2 + g10*l_off0*x15*x2 - g15*g2*l_on0*x10 = 0

 and  - g1*g14*k_on0*x10*x6 + g10*l_cat0*x1*x14*x6 + g6*k_off0*x1*x10*x14 = 0

 and  - g14*g4*k_on3*x9 + g9*k_cat3*x14*x4 + g9*k_off3*x14*x4 = 0 and 

g12*l_off2*x13*x14*x15*x4*x8*x9 + g13*l_cat3*x12*x14*x15*x4*x8*x9

 - g14*g4*k_on3*x12*x13*x15*x8*x9 - g15*g4*l_on2*x12*x13*x14*x8*x9

 + g8*k_cat2*x12*x13*x14*x15*x4*x9 + g9*k_off3*x12*x13*x14*x15*x4*x8 = 0

 and  - g14*g3*k_on2*x8 + g8*k_cat2*x14*x3 + g8*k_off2*x14*x3 = 0 and 

g11*l_off1*x12*x14*x15*x3*x7*x8 + g12*l_cat2*x11*x14*x15*x3*x7*x8

 - g14*g3*k_on2*x11*x12*x15*x7*x8 - g15*g3*l_on1*x11*x12*x14*x7*x8

 + g7*k_cat1*x11*x12*x14*x15*x3*x8 + g8*k_off2*x11*x12*x14*x15*x3*x7 = 0

 and  - g14*g2*k_on1*x7 + g7*k_cat1*x14*x2 + g7*k_off1*x14*x2 = 0 and 

g10*l_off0*x11*x14*x15*x2*x6*x7 + g11*l_cat1*x10*x14*x15*x2*x6*x7

 - g14*g2*k_on1*x10*x11*x15*x6*x7 - g15*g2*l_on0*x10*x11*x14*x6*x7

 + g6*k_cat0*x10*x11*x14*x15*x2*x7 + g7*k_off1*x10*x11*x14*x15*x2*x6 = 0

 and  - g1*g14*k_on0*x6 + g6*k_cat0*x1*x14 + g6*k_off0*x1*x14 = 0))

phi2_ := rlqe(phi2, pos);


phi2_ := true


% Shifted completeness under multiplication:
phi3 := varietyStarIsCosetMult(xl, fl, pos);


phi3 := all g1 all g2 all g3 all g4 all g5 all g6 all g7 all g8 all g9 all g10 

all g11 all g12 all g13 all g14 all g15 all x1 all x2 all x3 all x4 all x5 all 

x6 all x7 all x8 all x9 all x10 all x11 all x12 all x13 all x14 all x15 all y1 

all y2 all y3 all y4 all y5 all y6 all y7 all y8 all y9 all y10 all y11 all y12 

all y13 all y14 all y15 (((y9 <> 0 and y8 <> 0 and y7 <> 0 and y6 <> 0

 and y5 <> 0 and y4 <> 0 and y3 <> 0 and y2 <> 0 and y15 <> 0 and y14 <> 0

 and y13 <> 0 and y12 <> 0 and y11 <> 0 and y10 <> 0 and y1 <> 0 and x9 <> 0

 and x8 <> 0 and x7 <> 0 and x6 <> 0 and x5 <> 0 and x4 <> 0 and x3 <> 0

 and x2 <> 0 and x15 <> 0 and x14 <> 0 and x13 <> 0 and x12 <> 0 and x11 <> 0

 and x10 <> 0 and x1 <> 0 and g9 <> 0 and g8 <> 0 and g7 <> 0 and g6 <> 0

 and g5 <> 0 and g4 <> 0 and g3 <> 0 and g2 <> 0 and g15 <> 0 and g14 <> 0

 and g13 <> 0 and g12 <> 0 and g11 <> 0 and g10 <> 0 and g1 <> 0) and (

g13*l_cat3 + g13*l_off3 - g15*g5*l_on3 = 0

 and g12*l_cat2 + g12*l_off2 - g15*g4*l_on2 = 0

 and g11*l_cat1 + g11*l_off1 - g15*g3*l_on1 = 0

 and g10*l_cat0 + g10*l_off0 - g15*g2*l_on0 = 0

 and  - g1*g14*k_on0 + g10*l_cat0 + g6*k_off0 = 0

 and  - g14*g4*k_on3 + g9*k_cat3 + g9*k_off3 = 0 and 

g12*l_off2 + g13*l_cat3 - g14*g4*k_on3 - g15*g4*l_on2 + g8*k_cat2 + g9*k_off3

 = 0 and  - g14*g3*k_on2 + g8*k_cat2 + g8*k_off2 = 0 and 

g11*l_off1 + g12*l_cat2 - g14*g3*k_on2 - g15*g3*l_on1 + g7*k_cat1 + g8*k_off2

 = 0 and  - g14*g2*k_on1 + g7*k_cat1 + g7*k_off1 = 0 and 

g10*l_off0 + g11*l_cat1 - g14*g2*k_on1 - g15*g2*l_on0 + g6*k_cat0 + g7*k_off1

 = 0 and  - g1*g14*k_on0 + g6*k_cat0 + g6*k_off0 = 0) and (

g13*l_cat3*x13 + g13*l_off3*x13 - g15*g5*l_on3*x15*x5 = 0

 and g12*l_cat2*x12 + g12*l_off2*x12 - g15*g4*l_on2*x15*x4 = 0

 and g11*l_cat1*x11 + g11*l_off1*x11 - g15*g3*l_on1*x15*x3 = 0

 and g10*l_cat0*x10 + g10*l_off0*x10 - g15*g2*l_on0*x15*x2 = 0

 and  - g1*g14*k_on0*x1*x14 + g10*l_cat0*x10 + g6*k_off0*x6 = 0

 and  - g14*g4*k_on3*x14*x4 + g9*k_cat3*x9 + g9*k_off3*x9 = 0 and g12*l_off2*x12

 + g13*l_cat3*x13 - g14*g4*k_on3*x14*x4 - g15*g4*l_on2*x15*x4 + g8*k_cat2*x8

 + g9*k_off3*x9 = 0 and  - g14*g3*k_on2*x14*x3 + g8*k_cat2*x8 + g8*k_off2*x8 = 0

 and g11*l_off1*x11 + g12*l_cat2*x12 - g14*g3*k_on2*x14*x3 - g15*g3*l_on1*x15*x3

 + g7*k_cat1*x7 + g8*k_off2*x8 = 0

 and  - g14*g2*k_on1*x14*x2 + g7*k_cat1*x7 + g7*k_off1*x7 = 0 and g10*l_off0*x10

 + g11*l_cat1*x11 - g14*g2*k_on1*x14*x2 - g15*g2*l_on0*x15*x2 + g6*k_cat0*x6

 + g7*k_off1*x7 = 0 and  - g1*g14*k_on0*x1*x14 + g6*k_cat0*x6 + g6*k_off0*x6 = 0

) and (g13*l_cat3*y13 + g13*l_off3*y13 - g15*g5*l_on3*y15*y5 = 0

 and g12*l_cat2*y12 + g12*l_off2*y12 - g15*g4*l_on2*y15*y4 = 0

 and g11*l_cat1*y11 + g11*l_off1*y11 - g15*g3*l_on1*y15*y3 = 0

 and g10*l_cat0*y10 + g10*l_off0*y10 - g15*g2*l_on0*y15*y2 = 0

 and  - g1*g14*k_on0*y1*y14 + g10*l_cat0*y10 + g6*k_off0*y6 = 0

 and  - g14*g4*k_on3*y14*y4 + g9*k_cat3*y9 + g9*k_off3*y9 = 0 and g12*l_off2*y12

 + g13*l_cat3*y13 - g14*g4*k_on3*y14*y4 - g15*g4*l_on2*y15*y4 + g8*k_cat2*y8

 + g9*k_off3*y9 = 0 and  - g14*g3*k_on2*y14*y3 + g8*k_cat2*y8 + g8*k_off2*y8 = 0

 and g11*l_off1*y11 + g12*l_cat2*y12 - g14*g3*k_on2*y14*y3 - g15*g3*l_on1*y15*y3

 + g7*k_cat1*y7 + g8*k_off2*y8 = 0

 and  - g14*g2*k_on1*y14*y2 + g7*k_cat1*y7 + g7*k_off1*y7 = 0 and g10*l_off0*y10

 + g11*l_cat1*y11 - g14*g2*k_on1*y14*y2 - g15*g2*l_on0*y15*y2 + g6*k_cat0*y6

 + g7*k_off1*y7 = 0 and  - g1*g14*k_on0*y1*y14 + g6*k_cat0*y6 + g6*k_off0*y6 = 0

)) impl (

g13*l_cat3*x13*y13 + g13*l_off3*x13*y13 - g15*g5*l_on3*x15*x5*y15*y5 = 0

 and g12*l_cat2*x12*y12 + g12*l_off2*x12*y12 - g15*g4*l_on2*x15*x4*y15*y4 = 0

 and g11*l_cat1*x11*y11 + g11*l_off1*x11*y11 - g15*g3*l_on1*x15*x3*y15*y3 = 0

 and g10*l_cat0*x10*y10 + g10*l_off0*x10*y10 - g15*g2*l_on0*x15*x2*y15*y2 = 0

 and  - g1*g14*k_on0*x1*x14*y1*y14 + g10*l_cat0*x10*y10 + g6*k_off0*x6*y6 = 0

 and  - g14*g4*k_on3*x14*x4*y14*y4 + g9*k_cat3*x9*y9 + g9*k_off3*x9*y9 = 0 and 

g12*l_off2*x12*y12 + g13*l_cat3*x13*y13 - g14*g4*k_on3*x14*x4*y14*y4

 - g15*g4*l_on2*x15*x4*y15*y4 + g8*k_cat2*x8*y8 + g9*k_off3*x9*y9 = 0

 and  - g14*g3*k_on2*x14*x3*y14*y3 + g8*k_cat2*x8*y8 + g8*k_off2*x8*y8 = 0 and 

g11*l_off1*x11*y11 + g12*l_cat2*x12*y12 - g14*g3*k_on2*x14*x3*y14*y3

 - g15*g3*l_on1*x15*x3*y15*y3 + g7*k_cat1*x7*y7 + g8*k_off2*x8*y8 = 0

 and  - g14*g2*k_on1*x14*x2*y14*y2 + g7*k_cat1*x7*y7 + g7*k_off1*x7*y7 = 0 and 

g10*l_off0*x10*y10 + g11*l_cat1*x11*y11 - g14*g2*k_on1*x14*x2*y14*y2

 - g15*g2*l_on0*x15*x2*y15*y2 + g6*k_cat0*x6*y6 + g7*k_off1*x7*y7 = 0

 and  - g1*g14*k_on0*x1*x14*y1*y14 + g6*k_cat0*x6*y6 + g6*k_off0*x6*y6 = 0))

phi3_ := rlqe(phi3, pos);


phi3_ := true


coset := rlgsn(phi1_ and phi2_ and phi3_, form=dnf);


coset := true


phi4 := rlsimpl(sub(for each x in xl collect x=1, zero fl), pos);


phi4 := l_cat3 + l_off3 - l_on3 = 0 and l_cat2 + l_off2 - l_on2 = 0

 and l_cat1 + l_off1 - l_on1 = 0 and l_cat0 + l_off0 - l_on0 = 0

 and k_off0 - k_on0 + l_cat0 = 0 and k_cat3 + k_off3 - k_on3 = 0

 and k_cat2 + k_off3 - k_on3 + l_cat3 + l_off2 - l_on2 = 0

 and k_cat2 + k_off2 - k_on2 = 0

 and k_cat1 + k_off2 - k_on2 + l_cat2 + l_off1 - l_on1 = 0

 and k_cat1 + k_off1 - k_on1 = 0

 and k_cat0 + k_off1 - k_on1 + l_cat1 + l_off0 - l_on0 = 0

 and k_cat0 + k_off0 - k_on0 = 0


group := rlgsn(coset and phi4, form=dnf);


group := k_off0 - k_on0 - l_off0 + l_on0 = 0 and k_off0 - k_on0 + l_cat0 = 0

 and k_cat3 + l_off3 - l_on3 = 0 and k_cat3 - l_cat3 = 0

 and k_cat3 + k_off3 - k_on3 = 0 and k_cat2 + l_off2 - l_on2 = 0

 and k_cat2 - l_cat2 = 0 and k_cat2 + k_off2 - k_on2 = 0

 and k_cat1 + l_off1 - l_on1 = 0 and k_cat1 - l_cat1 = 0

 and k_cat1 + k_off1 - k_on1 = 0 and k_cat0 + k_off0 - k_on0 = 0


end;

