GenAutomata Sections NuprlLIB Doc

Def (M |= initially x,tr.P(x;tr)) == x:M.state. M.init(x) P(x;nil)

is mentioned

In prior sections: mb state machine


GenAutomata Sections NuprlLIB Doc