Below we show the first target term, extracted from the current conjecture. Below it we show the associativity rule.
The variables of the rewrite rule are instantiated so that the left-hand side of the rule matches the target:
variable term from target
a x1
b x2
c (app x3 x4)
Then the target is replaced by the instantiated right-hand side of the rule.
Sometimes rules have hypotheses. To make a long story short, if the rule has hypotheses, then after matching the left-hand side, the rewriter instantiates the hypotheses and rewrites them recursively. This is called backchaining. If they all rewrite to true, then the target is replaced as above.
We discuss the rewriter in more detail in the extended introduction to how to use the theorem prover, see introduction-to-the-theorem-prover, which we will recommend you work through after you have finished the two tours.
