In[]:=
2+2
Out[]=
4
In[]:=
s36path=ResourceFunction["FindEquationalPath"]ProofObject
Logic: EquationalLogic
Steps: 104
Theorem: p·qq·p
,{"SubstitutionLemma",36},All;
In[]:=
ByteCount[s36path["Path"]]
Out[]=
3150396392
In[]:=
ByteCount[s36path["Justification"]]
Out[]=
11716072
In[]:=
MapThread[{expr,justification,i}|->With[{​​pos=LexicographicSort@Position[expr,_,Heads->False],​​subPos=Join[justification[[3]],#]&/@LexicographicSort[Position[Extract[expr,justification[[3]]],_,Heads->False]][[{1,-1}]]​​},​​{Length[pos],{Replace[justification[[2]],{Right->Blue,Left->Red}],Tooltip[Rectangle@@Thread[{{i+-1,i+1},{-.5,.5}+Catenate@Lookup[PositionIndex[pos],subPos[[{1,-1}]]]}],Extract[expr,justification[[3]]]]}}​​],{Most@#["Path"],#["Justification"],Range[Length[#["Justification"]]]}]&[s36path];
In[]:=
ByteCount[%5]
Out[]=
474480408
In[]:=
ListStepPlot[#[[All,1]],Center,PlotRange->All,Filling->Axis,Epilog->#[[All,2]],PlotStyle->Opacity[.4],Frame->True,FrameLabel->{"step","expression size"},AspectRatio->.3]&
5

Out[]=
In[]:=
ListStepPlot[#[[All,1]],Center,PlotRange->All,Filling->Axis,Epilog->#[[All,2]],PlotStyle->Opacity[.4],Frame->True,FrameLabel->{"step","expression size"},AspectRatio->.3,ScalingFunctions->"Log"]&
5

Out[]=
In[]:=
LeafCount/@s36path["Path"]
Out[]=
{7,79,743,483,423,363,303,223,455,535,595,655,715,975,311,1379,1051,871,691,511,431,795,691,639,587,535,231,495,799,851,903,955,1059,695,775,955,1135,1315,1643,575,1239,979,919,859,799,719,487,851,747,695,643,591,651,711,771,1031,343,647,699,751,803,907,543,623,
⋯26977⋯
,883,803,695,767,839,911,671,743,815,887,647,443,787,671,639,607,575,167,383,415,447,479,595,251,323,167,631,491,459,427,395,635,563,491,419,311,239,1111,755,675,595,515,407,479,551,623,383,455,527,599,359,155,227,335,407,479,551,311,343,375,407,547,83,15}
Full expression not available
(
original memory size:
0.7 MB)
In[]:=
Max[%]
Out[]=
40215
:
In[]:=
Histogram[%10,100,{"Log","Count"},PlotRange->All,Frame->True,FrameLabel->{"expression size","count"},AspectRatio->.4]
Out[]=
In[]:=
%5[[3,2]]
Out[]=

,
Rectangle[{2,4.5},{4,279.5}]

KeyTake[s36path,{"Path","Justification"}]