# ProveDetails Command

From GeoGebra Manual

- ProveDetails[ <Boolean Expression> ]
- Returns some details of the result of the automated proof.

Normally, GeoGebra decides whether a boolean expression is true or not by using numerical computations. However, the ProveDetails command uses symbolic methods to determine whether a statement is true or false in general. This command works like the Prove command, but also returns some details of the result as a list:

- An empty list
**{}**if GeoGebra cannot determine the answer. - A list with one element:
**{false}**, if the statement is not true in general. - A list with one element:
**{true}**, if the statement is always true (in all cases when the diagram can be constructed). - A list with more elements, containing the boolean value
*true*and another list for some so-called*non-degeneracy conditions*, if the statement is true under certain conditions, e.g. {true, {"AreCollinear[A,B,C],AreEqual[C,D]"}}. This means that if none of the conditions are true (and the diagram can be constructed), then the statement will be true. - A list
**{true,{"..."}}**, if the statement is true under certain conditions, but these conditions cannot be translated to human readable form for some reasons.

**Example:**Let us define a triangle with vertices*A*,*B*and*C*, and define`D=MidPoint[B,C]`

,`E=MidPoint[A,C]`

,`p=Line[A,B]`

,`q=Line[D,E]`

. Now`ProveDetails[p∥q]`

returns {true}, which means that if the diagram can be constructed, then the midline*DE*of the triangle is parallel to the side*AB*.

**Example:**Let*AB*be the segment*a*, and define`C=MidPoint[A,B]`

,`b=PerpendicularBisector[A,B]`

,`D=Intersect[a,b]`

. Now`ProveDetails[C==D]`

returns {true,{"AreEqual[A,B]"}}: it means that if the points*A*and*B*differ, then the points*C*and*D*will coincide.

**Example:**Let*AB*be the segment*a*, and define`l=Line[A,B]`

. Let*C*be an arbitrary point on line*l*, moreover let`b=Segment[B,C]`

,`c=Segment[A,C]`

. Now`ProveDetails[a==b+c]`

returns {true,{"a+b==c", "b==a+c"}}: it means that if neither , nor , then .

It is possible that the list of the non-degeneracy conditions is not the simplest possible set. For the above example, the simplest set would be the empty set.

**Note:**See also Prove command, Boolean values, GeoGebra Automated Reasoning Tools: A Tutorial and technical details of the algorithms.