Remark: in node 4, it should be !(a|b) (as your remarked) instead of !a|b.
The local model checking procedure starts with arguments (s, phi) to check whether property phi holds on state s. When returning from the recursion, we know whether that is the case or not. Only then, we can state this, and finish the proof tree up to this call. Hence, whether a formula satisfies a state or not is because of the results of the child nodes.
In case of node 4, we ask (s6,!(a|b)) and because the child node 5 returns that s6 satisfies a|b, the state s6 cannot satisfy at the same time the negation !(a|b). The result of node 5 is obtained by its child 6, where we check that s6 satisfies "a", since s6 is labelled with "a".
Similar argumentations hold for node 7. You have to read the results bottom up from the leaf nodes.
