KeYmaera のこと（２）

KeYmaera（キメラ）の目玉の一つは

微分方程式系，微分不等式系で表された Continuous evolution を action に使えること

ですが，見ての通り \programVariab 以下で，ロジカルな変数が時間の関数なのか否かを明示していません．

例えば，先の２つ目の例の時間発展から a が定数である条件 a'=0 を除いても，同じ証明を返してきます．

よりシンプルな例でも


というように v は定数扱いです．

これについて http://symbolaris.com/pub/KeYmaera-tutorial.pdf に

KeYmaera follows the explicit change principle. That is, no variable changes unless the model explicitly
specifies how it changes.

なる断りがあり，この例の場合，「時間微分すれば関数，しなければ定数」なので，例えば

で正しく止まります．