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[]:=
RowFormatLemma/@DeleteCasesCasesValuesNormalProofObject["ProofDataset"][All,"Statement"],HoldForm[_==_],HoldForm[x_==x_],▮
Out[]=
In[]:=
TextTraditionalFormGridWithpg=ProofGraph2ProofObject,"Events"->False,{#,VertexOutDegree[pg,#]}&/@TakeLargestBy[VertexList[pg],VertexOutDegree[pg,#]&,6],Frame->All
Out[]=
a.·b.b.·a. | 43 |
a.((b.·c.)·a.)·(b.·((b.·a.)·b.)) | 34 |
a.·b.a.·((a.·b.)·a.) | 23 |
a.·(a.·(a.·b.))a.·b. | 10 |
(a.·b.)·c.c.·(b.·a.) | 10 |
a.(b.·a.)·((c.·b.)·(((c.·b.)·a.)·(c.·b.))) | 9 |
In[]:=
First/@Withpg=ProofGraph2ProofObject,"Events"->False,{#,VertexOutDegree[pg,#]}&/@TakeLargestBy[VertexList[pg],VertexOutDegree[pg,#]&,6]
Out[]=
{a.·b.b.·a.,a.((b.·c.)·a.)·(b.·((b.·a.)·b.)),a.·b.a.·((a.·b.)·a.),a.·(a.·(a.·b.))a.·b.,(a.·b.)·c.c.·(b.·a.),a.(b.·a.)·((c.·b.)·(((c.·b.)·a.)·(c.·b.)))}
In[]:=
ResourceFunction["UnformalizeSymbols"]/@%268
Out[]=
{a·bb·a,a((b·c)·a)·(b·((b·a)·b)),a·ba·((a·b)·a),a·(a·(a·b))a·b,(a·b)·cc·(b·a),a(b·a)·((c·b)·(((c·b)·a)·(c·b)))}
In[]:=
FEPp·q==q·p,((a.·b.)·c.)·(a.·((a.·c.)·a.))c.
∀
{a.,b.,c.}
Out[]=
ProofObject
In[]:=
SelectProofObject["ProofDataset"][All,"Statement"],LeafCount[#]<20&
Out[]=
In[]:=
NeighborhoodGraphProofGraph2ProofObject,a.·a.a.·((a.·a.)·a.),3,VertexLabels->Automatic
Out[]=
In[]:=
ProofGraph2ProofObject
Out[]=
Sizes of Input & Output Lemmas
Sizes of Input & Output Lemmas
Unrolling to Axioms
Unrolling to Axioms
[[ lemmas in priority queue ... ]]
Showing updating locations
Showing updating locations
The Full Unrolling
The Full Unrolling
Foliations
Foliations
Full Unrolling
Full Unrolling