Definition
Deterministic Program Transition
A deterministic program transition is a program transition relation in which every non-final program configuration has at most one successor configuration.
Formally, for every non-final configuration
, if then
.