Prooftoys basic examples – solutions
1. The repetitious number
Writing down a three-digit number and making it into a six-digit number by appending the same three digits has the same effect as multiplying by 1,001.
So we can ask whether it is true that
1001 * x / 7 / 11 / 13 = x.
This problem comes from the book “My Best Mathematical and Logic Puzzles” (page 10) by the legendary Martin Gardner, author of the Mathematical Games column in Scientific American magazine for 25 years and numerous books of entertaining and puzzling mathematics.
The steps. A proof consists of a sequence of steps connected by inference rules, each producing a new step, often with other steps as inputs. In this proof we have:
“Consider” – we start by “considering” the expression that computes the result that hopefully is equal to the input,
x. A Prooftoys step is always a true statement. You can “consider” an arbitrary term, which can have any kind of value, for example numeric as here, or boolean, or any other kind. The full content of the step is a statement that the term is equal to itself.
“Simplify” – Prooftoys automatically tries simplification after most steps, to shrink the result. Making a term (expression) smaller is the basic concept of simplification.
“Standard form” – There are a few different ways to get Prooftoys to look at the two occurrences of 1001 and cancel them out; and this is one of them.
“Display fully” – Prooftoys often just displays an ellipsis (” … “) if part of a step is the same as in the previous step. This forces it to show the whole of the solution step.