Q(x;tr) Q(x';tr') P(x';tr'))
x,x':M.state, tr:M.action List, a:M.action.
(M -tr- > x) M.trans(x,a,x') R(x;x';tr;tr @ [a])
is mentioned by
|
Def (M |= x,tr.P(x;tr) while Q(x;tr))
== (M |= x,x',tr,tr'.P(x;tr) Q(x;tr) Q(x';tr') P(x';tr')) | [while] |
Try larger context: GenAutomata