A
B and
x
A as achieving the goal
of reaching a contradiction, even though they contradict each other.
However, it would recognize xA and xA as achieving the goal of reaching a contradiction.
Proof Designer does not automatically recognize when you have proven a statement you are trying to prove. You must tell it that you have reached your goal by using the Finish command.
If your goal is to prove some statement, then you cannot use the Finish
command unless the statement you are trying to prove is in your givens
list. If it is, select it in the givens list and give the Finish command.
If your goal is to prove a contradiction, then you cannot use the Finish
command unless there are two statements in your givens list, one of which
is the negation of the other. If there are two such statements in your
givens list, select both of them and give the Finish command. Note that it
is not sufficient to choose two statements that contradict each other; one
must actually be the negation of the other. For example, Proof Designer
would not recognize the givens xAB and
xA as achieving the goal
of reaching a contradiction, even though they contradict each other.
However, it would recognize xA and xA as achieving the goal of reaching a contradiction.
When you finish the last gap in a proof, Proof Designer will congratulate you on completing the proof.