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 .