Figure 3: Axiom DS is incorrect as stated, because it does not ensure that the existentially quantified t does not affect the game c. DS should have been any of the following axioms instead
DS <x'=f>p(x,x') <-> \exists t>=0 <x:=x+f*t><x':=f>p(x,x')
DS <x'=f><t:=0><c>T <-> \exists t>=0 <x:=x+f*t><x':=f><t:=0><c>T
DS <x'=f><t:=*><c>T <-> \exists t>=0 <x:=x+f*t><x':=f><t:=*><c>T

In the latter version t:=* is the nondeterministic assignment that for a fresh variable t is definable via an ODE t'=1;t'=-1.