Tactic for {{tactic.modelName}}

KeYmaera X provides automated proof search, as well as proof construction using tactics.

Automated Proof Search

Use tactic Auto after loading the model. The automated search will make progress, but may take a long time and remain incomplete on this model.

Proof Construction