In this tutorial, we will prove a simple theorem to demonstrate the remove button in the suggestion box. We will prove that if a number A is less than (5), it is also less than (8). Put more succinctly (-> (< A (5)) (< A (8))).
We are now going to use the transitive property of inequality. That property is found in the lttr theorem.
The editor should now look like this:
and the suggestion box like this:
Select the left side of the expression by clicking on it. You will see the expression (/\ (< A (5)) (< (5) (8))) expand into (< A (5)) ∧ (< (5) (8)). The two statements are equivalent.
Since (< (5) (8)) is true, it will find a previously generated proof that (< (5) (8)) and add it to the editor. The statement (< (5) (8)) now appears on the proof stack. The suggestion box now looks like this:
The suggestion box has two rows. The first row contains our initial statement. The second contains the generated proof that (< (5) (8)). This is saying that we can use the second statement to simplify the first statment. We can remove the the term (< (5) (8)) from the conditional statement because we already know that it is always true.
This produces the desired outcome: (-> (< A (5)) (< A (8))).
This concludes the tutorial. If you having any questions please don't hesitate to contact us. Paul Merrell wrote the tutorial and is eager answer any questions you might have. His contact information can be found on his website. You can also ask questions on the the mailing list.