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