GenAutomata Sections NuprlLIB Doc

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'))

is mentioned

In prior sections: mb state machine


GenAutomata Sections NuprlLIB Doc