You are using a browser not supported by the Wolfram Cloud
Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.
I understand and wish to continue anyway »
WOLFRAM NOTEBOOK
In[]:=
2+2
Out[]=
4
In[]:=
s36path=ResourceFunction["FindEquationalPath"]ProofObject,{"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]&
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"]&
Out[]=
In[]:=
LeafCount/@s36path["Path"]
Out[]=
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"}]