Basically you need a set of implications.
looking only at the first worker:
work = [w0, w1, w2, w3, w4, w5, w6]
shift = [s0, s1, s2, s3, s4]
shift_list=[[1,1,1,0,0,0,0],
[0,1,1,1,0,0,0],
[0,0,1,1,1,0,0],
[0,0,0,1,1,1,0],
[0,0,0,0,1,1,1]]
so
w0 <=> s0
w1 <=> or(s0, s1)
w2 <=> or(s0, s1, s2)
w3 <=> or(s1, s2, s3)
w4 <=> or(s2, s3, s4)
w5 <=> or(s3, s4)
w6 <=> s4
where you encode l0 <=> or(l1, ..., ln)
by writing
# l0 implies or(l1, .., ln)
or(l0.Not(), l1, .., ln)
# or(l1, .., ln) implies l0
forall i in 1..n:
implication(li, l0)