# 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.