2
私は"\<forall>x. \<exists>y.\<forall>(z::real). P x y z"
のような目標を持っています。すぐに私が"\<forall>x. \<exists>y.\<forall>(z::real). P x y (z-2)"
と結論づけることができるルールはありますか?もしそうでなければ、私はこのタイプの目標をどのように証明するかについての一般的な助言に感謝します。普遍的な定量化された変数(Isabelle)の置換を可能にする補題/規則
は私がallI
、exI
、allE
、exE
の多くを使用することによってそれを証明することができます知っているが、迅速かつ簡単な方法がなければならないように思えます。
これは役に立ちます。残念ながら、私が実際に証明したいことは、やや複雑で、これを使って動作しません。 –
自動化を支援するために、最小量の作業のみを実行して、もう一方の後に1つの量子をはがしてみることができます。 – larsrh