<>x : it means atleast one successor

[]x : it means all successors or {}

suppose if x has some states like {s0,s1,s2,s3}

s0 has successors (s0,s1,s2)

s1 has successors ( s1,s2)

s2 has successors (s3)

s3 has successors {}

now if we have x = { s0,s1,s2,s3}

then following queries I have:

1. <>x = {s0,s1,s2} OR {s0,s2} // because s0 already has succssor s0,s1,s2 , so can we exclude s1 in <>x ?

2. []x = {s0,s1,s2,s3} OR {s3} // []x means all successors or {} , so should we exclude s0,s1,s2 because they don't contain all successors mentioned in x?