[tlaplus] Conjoining Specifications lemma1.2

[Apostolis Xekoukoulotakis <apostolis.xekoukoulotakis@xxxxxxxxx>]

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 .

1 . https://lamport.azurewebsites.net/pubs/pubs.html#abadi-conjoining

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.