Local model checking with implication [Exam 31.08.2021]

Question

Which rule do we need in local model checking if there is an implication in the formula? 

S1|/- (c | b -> [] x)) can be rewritten to  S1|/- (!c & !b | [] x1)), but the solution splits it into S1|/- (!c & b)) and S1|/- ([]x1). Why is that done this way?

Answer 1

Thanks for pointing this out. Some years ago, there was a but in the pretty printer that did not respect the priorities of the operators in the correct way. In state s1, the formula is actually !(c|b) and not !c|b, so that the correct proof tree is as follows:

It has been fixed in the exam paper meanwhile.