KeYmaera のこと（４）

KeYmaera が非線形方程式を解かずに結論を得る仕組みは

\problem{ini->\[{ode}\]f>=g}

に対して，まず，時刻 0 における成立

ini->f>=g

を示し，さらに任意の非負の時刻における

f'>=g'

の成立を正規型の ode を用いてこの結果から導関数を消去，証明する素朴なものです．

例えば

\problem{x^3+y^3>=1->\[{x'=x^2-y^2,y'=x^2+y^2}\]x^3+y^3>=1}

なら

に帰着されます．