# How to extract steps from FullSimplify? [duplicate]

The answer proposed to the original question doesn't solve it, I need to understand the results of TraceInternal when used on FullSimplify as a sequence of steps, which has not been resolved for me.

Original Question:

I'm trying to verify an identity:

Reduce[(2*n)! (2*n + 1)!/n!^2 == 16^(n) Pochhammer[1/2, n] Pochhammer[3/2, n] &&
n >= 1, {n}, Integers]


Neither Reduce nor Solve can prove it, they generated these methods:

Reduce::fexp: Warning: Reduce used FunctionExpand to transform the system. Since FunctionExpand transformation rules are only generically correct, the solution set might have been altered.

This system cannot be solved with the methods available to Solve.

I randomly decided to try yet another function:

FullSimplify[(2*n)! (2*n + 1)!/n!^2 == 16^(n) Pochhammer[1/2, n] Pochhammer[3/2, n], ForAll[{n}, n >= 1 && n \[Element] Integers]]


And I guess it worked, but how and why!? Here's my question:

1. Why did FullSimplify work and the others fail?

2. For "theorem proving" functions (e.g. Reduce and FullSimplify) - Is there any way to see the steps here or the sow the intermediate results or (i.e. individual transformation steps of FunctionExpand) that it uses/deduces so as to verify it by hand?

3. If not are what are viable packages (or 3rd party software) available that can illustrate human verifiable steps for identities?

• In a nutshell: when you have special functions like Pochhammer[] or Factorial[] involved, use FullSimplify[]. Aug 5, 2016 at 1:48

Can you do the following:

Trace[FullSimplify[expr], TraceInternal -> True]


or

FullSimplify[expr, TransformationFunctions -> {Sow, Automatic}] // Reap


References:

What are the default TransformationFunctions used in Simplify and FullSimplify?

Simplify with TransformationFunctions, Bug?

http://12000.org/my_notes/faq/mma_notes/MMA.htm#x1-1600015

http://forums.wolfram.com/mathgroup/archive/2006/Sep/msg00670.html

Information[TraceInternal] "TraceInternal is an option for Trace and related functions which, if True or False, specifies whether to trace evaluations of expressions generated internally by Mathematica. The intermediate Automatic setting traces a selected set of internal evaluations including Messages and sets or unsets of visible symbols."

Attributes[TraceInternal] = {Protected}

Trace of FullSimplify

• Thanks @Young, can you elaborate on how to read the output?
– M.R.
Aug 5, 2016 at 1:40
• It may be prudent to execute ClearSystemCache[] first to avoid earlier computations, if any, causing FullSimplify to omit important steps. Aug 5, 2016 at 13:09
• It looks as if you are just quoting from Simon Woods' earlier answer. If so, you should make a reference to it. Aug 5, 2016 at 15:24
• I still don't understand clearly how to read the output from this (what are the steps?)
– M.R.
Aug 5, 2016 at 15:25
• @m_goldberg I guess I found several places using these methods and really this was just to help M.R. on his way Aug 5, 2016 at 15:35