I am unable to prove this direction :
If PA , PB , PC are safety properties , then
if ⊨ ((PC /\ PA) => PB) , then ⊨ (PC => (PA -▹ PB))
Consider closed sets
1 . PA : all sequences with prefix (2 , 4 , ....)
2 . PC : all sequences with prefix (2 , 5 , ...)
3 . PB : all sequences with prefix (3 , ....)
All sets are closed, aka they are safety properties, and the condition is true.
However , for sequence a = (2 , 5 , ...) , the result of the lemma is not true.
since a belongs at PC, and the finite prefix (2) belongs at PA, but the prefix (2) does not belong at PB, as it should.
Am I missing something? Maybe I made an error in the definitions .