v'
var'(x)= > false
opr(x)= > false
fvar(x)= > false
trace(x)= > false
end_ts_case
var'(p)= > ts_case(b)
var(x)= > false
var'(p')= > p = p'
opr(x)= > false
fvar(x)= > false
trace(x)= > false
end_ts_case
opr(op)= > ts_case(b)
var(x)= > false
var'(x)= > false
opr(op')= > op = op'
fvar(x)= > false
trace(x)= > false
end_ts_case
fvar(f)= > ts_case(b)
var(x)= > false
var'(x)= > false
opr(x)= > false
fvar(f')= > f = f'
trace(x)= > false
end_ts_case
trace(P)= > ts_case(b)
var(x)= > false
var'(x)= > false
opr(x)= > false
fvar(x)= > false
trace(P')= > P = P'
end_ts_case
end_ts_case
is mentioned
In prior sections: mb automata 1 mb automata 2
Try larger context: GenAutomata