In this video we show you how to apply the abbreviate rule. This rule is helpful when your proof uses the same or equivalent expressions in more than one place. If the expression you are abbreviating has a lot of variables, it will simplify the computation done by the quantifier elimination algorithm. Or, if your expression causes branching, you can reduce the number of branches taken by the prover.
Let's look at an example. As humans, we can see that this property holds by transitivity. With the complexity of the formulas and the number of variables therein, quantifier elimination will eventually solve the problem, but it may take a very long time. We can help by showing the transitive structure of the problem through abbreviating equivalent terms to a single variable with the abbreviate rule.
Using abbreviate can allow you to give some high-level hints to KeYmaera to guide the proof in the right direction.