Next: Semantics
Up: Basic Transition Rules
Previous: Basic Transition Rules
An update instruction R is an expression
f(![[t]](tbar.xbm)
) := 
where f is a non-static function name (the subject of the
instruction), is a tuple of terms whose length equals the arity
of f , and is another term; if f is a relation name then must be a Boolean term. (Update instructions are called local function
updates in the tutorial.)