s0: { Sym=[bm,an] [t1,t2,t3,t4,t5,t6,t7] : t1 = 0 && t3 = 0 && t5 = 0 && t7 = 0 && t6 = 0 && 0 <= t2 < an && 0 <= t4 < bm } s1: { Sym=[ambn,bm,an] [t1,t2,t3,t4,t5,t6,t7] : t1 = 0 && t3 = 0 && t5 = 0 && t7 = 0 && 0 <= t2 < an && 0 <= t6 < ambn && 0 <= t4 < bm }