E:TaggedEventStruct, tr:|E| List, x,y:|E|.
Dec(R_ad_normal(tr)(x,y))
(is-send(E)(a)) 
(is-send(E)(b)) (a =msg=(E) b))
& ((is-send(E)(a))
(is-send(E)(b))
(
x,y:
||tr||.
x < y
& (is-send(E)(tr[x]))
& (is-send(E)(tr[y]))
& (tr[x] =msg=(E) b)
& (tr[y] =msg=(E) a))
loc(E)(a) = loc(E)(b))
is mentioned by
|
Thm* E:TaggedEventStruct, tr:|E| List, x,y:|E|.
Dec(R_ad_normal(tr)(x,y)) | [decidable__R_ad_normal] |
Try larger context: GenAutomata