Using the Checker
Here we show how the checker can be used in solving a mathematical problem. The task is to solve a rational equation.
The 4f Checker tries to prove each step of the solution separately. The structured derivation on the right has correct steps but it is incomplete. The answer to the problem is missing. The factorization of the denominator on the right hand side of the equation is written as a nested derivation, and the checker can prove it.
We add the answer to the derivation.
The checker cannot prove all the steps of the derivation on the right. We have to examine carefully the steps that cannot be proved. We see that there is an error at the second warning sign: the terms mentioned in the justification should be subtracted, not added. The step and all the consecutive steps have to be corrected.
Justifications and Assumptions
We correct the sign error.
There are still two steps that the checker cannot prove. The first one is the step where both sides of the equation are multiplied by the denominators. This cannot be proved, because there is no reason for the multipliers to be different from zero. In the second step with a warning, the justification tells that one of the equations cannot be true, because then the denominator would be zero. However, the checker sees no reason, why the denominator cannot be zero.