Okay, I think I understand: He’s exploring Q under n := n+1 in the case k = 0 , to derive the update to s.0 .
By the invariant Q , he is entitled to use s.0 = (min p : 0 ≤ p ≤ n /\ N.p.n ≤ 0 : p) , where N.p.n gives the number of zeros in the range [p..n) .
So to calculate (min p : 0 ≤ p ≤ n /\ N.p.(n+1) ≤ 0 : p) , we need to check if X.n = 0 or not. If X.n ≠ 0 , then the minimum is still s.0 (there are no zeros in the range [s.0..n+1) , so no update to s.0 is needed. Otherwise X.n = 0 , so the smallest p such that N.p.(n+1) ≤ 0 is n+1 (that is, an empty range) , so we let s.0 := n+1 .