>>> symbolic n, over1, over2;
>>> 
>>> s0:= { [t1,t2,t3,t4,t5] : exists ( alpha,beta : t2 = 1+4beta && t4 = 1+4alpha && t1 = 1 && t3 = 1 && t5 = 0 && 0 <= over2 <= 3 && 0 <= over1 <= 3 && 1 <= t4 && 1 <= t2 && over1+t2 <= n && over2+t4 <= n) };
>>> s1:= { [t1] : 1+t1 = 0 && 0 <= over2 <= 3 && 0 <= over1 <= 3 && 1 <= n };
>>> s2:= { [t1,t2,t3,t4,t5] : t1 = 2 && t3 = 0 && t5 = 0 && 1 <= t2 <= n && 1 <= t4 <= n && 0 <= over2 <= 3 && over1 <= 3 && n < over1+t2 };
>>> s3:= { [t1,t2,t3,t4,t5] : exists ( alpha,beta : t2 = 1+4beta && t4 = 1+4alpha && t1 = 1 && t3 = 1 && t5 = 1 && 0 <= over2 <= 3 && 0 <= over1 <= 3 && 1 <= t4 && 1 <= t2 && over1+t2 <= n && over2+t4 <= n) };
>>> s4:= { [t1,t2,t3] : exists ( alpha : t2 = 1+4alpha && 1+t3 = 0 && t1 = 1 && 0 <= over1 <= 3 && 0 <= over2 <= 3 && over1+t2 <= n && 1 <= t2) };
>>> s5:= { [t1,t2,t3,t4,t5] : exists ( alpha : t2 = 1+4alpha && t5 = 0 && t1 = 1 && t3 = 2 && 0 <= over1 <= 3 && 1 <= t4 <= n && over2 <= 3 && 1 <= t2 && over1+t2 <= n && n < over2+t4) };
>>> s6:= { [t1,t2,t3,t4,t5] : exists ( alpha : t2 = 1+4alpha && t5 = 1 && t1 = 1 && t3 = 2 && 0 <= over1 <= 3 && 1 <= t4 <= n && over2 <= 3 && 1 <= t2 && over1+t2 <= n && n < over2+t4) };
>>> s7:= { [t1,t2,t3,t4,t5] : exists ( alpha,beta : t2 = 1+4beta && t4 = 1+4alpha && t5 = 2 && t1 = 1 && t3 = 1 && 0 <= over1 <= 3 && 0 <= over2 <= 3 && 1 <= t4 && 1 <= t2 && over1+t2 <= n && over2+t4 <= n) };
>>> 
>>> codegen s0,s1,s2,s3,s4,s5,s6,s7;
if (over2 >= 0 && over1 <= 3 && over2 <= 3) {
  if (over1 >= 0) {
    if (n >= 1) {
      s1(-1);
    }
    for(t2 = 1; t2 <= n-over1; t2 += 4) {
      s4(1,t2,-1);
      for(t4 = 1; t4 <= n-over2; t4 += 4) {
        s0(1,t2,1,t4,0);
        s3(1,t2,1,t4,1);
        s7(1,t2,1,t4,2);
      }
      for(t4 = max(1,n-over2+1); t4 <= n; t4++) {
        s5(1,t2,2,t4,0);
        s6(1,t2,2,t4,1);
      }
    }
  }
  for(t2 = max(1,n-over1+1); t2 <= n; t2++) {
    for(t4 = 1; t4 <= n; t4++) {
      s2(2,t2,0,t4,0);
    }
  }
}

>>> 
>>> 
>>>