In[]:=
HistogramLeafCount/@
[◼]
PatternsToSymbols
VertexList
[◼]
TwoWayRuleTokenEventGraph

[◼]
AxiomaticTheoryTWP
["GroupAxioms"],2,"TokenLabeling"->False,_TwoWayRule,{1},AspectRatio->12,Frame->True,ChartStyleOrange
Out[]=
In[]:=
VertexCount
[◼]
TwoWayRuleTokenEventGraph

[◼]
AxiomaticTheoryTWP
["GroupAxioms"],2,"TokenLabeling"->False,_TwoWayRule
Out[]=
792
In[]:=
VertexCount
[◼]
TwoWayRuleTokenEventGraph

[◼]
AxiomaticTheoryTWP
["BooleanAxioms"],2,"B","Identity"True,"TokenLabeling"->False,"PatternTest"->LeafCount
[◼]
PatternsToSymbols
[#]<12&,GraphLayout->"SpringElectricalEmbedding",_TwoWayRule
Out[]=
593
In[]:=
VertexCount
[◼]
TwoWayRuleTokenEventGraph

[◼]
AxiomaticTheoryTWP
["BooleanAxioms"],2,"B","Identity"True,"TokenLabeling"->False,"PatternTest"->LeafCount
[◼]
PatternsToSymbols
[#]<14&,GraphLayout->"SpringElectricalEmbedding",_TwoWayRule
Out[]=
27953
In[]:=
Now
Out[]=
Sun 20 Feb 2022 19:54:16GMT-5
In[]:=
VertexCount
[◼]
TwoWayRuleTokenEventGraph

[◼]
AxiomaticTheoryTWP
["BooleanAxioms"],2,"B","Identity"True,"TokenLabeling"->False,GraphLayout->"SpringElectricalEmbedding",_TwoWayRule
Out[]=
$Aborted
Now
In[]:=
With{depGraph=ReverseGraph[VertexOutComponentGraph[euc,<|"Book"1,"Theorem"47|>]​​]},​​EdgeAdd​​VertexDelete[depGraph,Alternatives@@axioms],​​MapAt[{#,CreateUUID[]}&,EdgeList[depGraph,Alternatives@@axioms_],{All,1}],​​VertexLabels{v_,_}v_Placed[EuclidVertexName[v],Center],​​VertexStyle{u_,_}u_IfKeyExistsQ[u,"Book"],
[◼]
MetamathematicsStyleData
["TokenStyle"],
[◼]
MetamathematicsStyleData
["AxiomTokenStyle"],​​VertexSizeScaled[0.05],​​VertexLabelStyle8,​​EdgeStyleArrowheads[0.015],​​AspectRatio1,​​ImageSizeScaled[.8],​​PerformanceGoal"Quality",​​GraphLayout"LayeredDigraphEmbedding"​​​​
Out[]=
In[]:=
Table[RandomInteger[10000],4,6]
Out[]=
{{6811,5061,5935,9829,7433,6685},{7199,9797,7318,5826,5100,1818},{5778,8992,6011,9478,5353,7267},{9140,5923,4887,1118,1658,1783}}
{{2,5},#}->Lighter
[◼]
MetamathematicsStyleData
["TheoremColor"],.8&/@{3,5,7}
In[]:=
TextGridJoin[{Rotate[Style[#,GrayLevel[.4],Italic],-70Degree]&/@Flatten[Prepend[Table[{"expressions","theorems"},3],"variables"]],Prepend[Catenate[Table[{Row[{"≤",n}],},{n,3}]],Style["size",Italic]]},MapIndexed[Prepend[#,First[#2]]&,{{6811,5061,5935,9829,7433,6685},{7199,9797,7318,5826,5100,1818},{5778,8992,6011,9478,5353,7267},{9140,5923,4887,1118,1658,1783}}]],Frame->All,Dividers->{Table[n->Black,{n,2,10,2}]},FrameStyle->LightGray,Background->None,None,Flatten@{{3,6},{#,#}}->Lighter
[◼]
MetamathematicsStyleData
["TheoremColor"],.8&/@{3,5,7},{{1,1},{1,7}}->GrayLevel[.95],{{2,2},{1,7}}->GrayLevel[.9],Alignment->Right
Out[]=
variables
expressions
theorems
expressions
theorems
expressions
theorems
size
≤1
≤2
≤3
1
6811
5061
5935
9829
7433
6685
2
7199
9797
7318
5826
5100
1818
3
5778
8992
6011
9478
5353
7267
4
9140
5923
4887
1118
1658
1783
In[]:=
CloudGet["https://wolfr.am/PO7vasDF"];
In[]:=
data73=DepthLeafSort[Select[FindAONTheoremsList[7,3],LowestQ[#,{a,b,c}]&]];
In[]:=
data73
Out[]=
{aa⋀a,aa⋁a,a⋀aa⋁a,a⋀bb⋀a,a⋁bb⋁a,aa,a⋀aa,a⋁aa,a(a⋀a),a(a⋁a),a(a⋀a)⋀a,a(a⋁a)⋀a,aa⋀(a⋀a),aa⋀(a⋁a),aa⋀a⋁a,a(a⋁a)⋁a,
⋯261893⋯
,a⋀(b⋀c)⋁aa,a⋀(b⋁c)⋁aa,a⋁(b⋀c)⋀aa,a⋁(b⋁c)⋀aa,a⋁b⋀(c⋀a)a,((a⋁b)⋁c)⋀bb,(a⋁(b⋁c))⋀bb,(a⋀b)⋀c⋁bb,a⋀(b⋀c)⋁bb,(a⋀b⋁c)⋀cc,((a⋁b)⋁c)⋀cc,(a⋁(b⋁c))⋀cc,(a⋀b)⋀c⋁cc,(a⋁b)⋀c⋁cc,a⋀(b⋀c)⋁cc}
large output
show less
show more
show all
set size limit...
In[]:=
data73[[1;;180]]
In[]:=
data73[[799;;858]]
In[]:=
data73[[2803;;2826]]
In[]:=
640/7.
Out[]=
91.4286
In[]:=
799-180
Out[]=
619