In[]:=
stat10=DeleteCases[Take[Union[Sort/@canonicalizePatterns/@(TwoWayRule@@@Tuples[(Flatten[Groupings[#,SmallCircle->2]&/@Table[Tuples[{a,b},n],{n,3}]]/.{a->a_,b->b_}),2])],10]/.{p_Pattern:>First[p],TwoWayRule->Equal},Except[_Equal]]
Out[]=
{ab,aa∘a,aa∘b,aa∘(a∘a),aa∘(a∘b),aa∘(b∘a),aa∘(b∘b),ab∘a,ab∘b}
In[]:=
Tuples[stat10,2]
Out[]=
In[]:=
ParallelMap[If[Head[#]===Failure,None,#["ProofLength"]]&[FindEquationalProof[ForAll[{a,b},#[[1]]],ForAll[{a,b},#[[2]]],TimeConstraint4]]&,Tuples[stat10,2]]
Out[]=
{3,None,None,None,None,None,None,None,4,3,3,3,None,4,None,None,3,3,3,None,3,None,None,None,None,None,4,3,4,3,3,3,3,3,4,4,3,None,3,None,3,None,None,None,4,3,None,3,None,None,3,None,4,4,3,None,3,None,None,None,3,None,4,3,None,None,None,None,None,None,3,4,3,None,None,None,None,None,None,None,3}
In[]:=
With[{axs=DeleteCases[Take[Union[Sort/@canonicalizePatterns/@(TwoWayRule@@@Tuples[(Flatten[Groupings[#,SmallCircle->2]&/@Table[Tuples[{a,b},n],{n,3}]]/.{a->a_,b->b_}),2])],20]/.{p_Pattern:>First[p],TwoWayRule->Equal},Except[_Equal]]},axs->Transpose[Partition[#,Sqrt[Length[#]]]&[ParallelMap[If[Head[#]===Failure,None,#["ProofLength"]]&[FindEquationalProof[ForAll[{a,b},#[[1]]],ForAll[{a,b},#[[2]]],TimeConstraint4]]&,Tuples[axs,2]]]]]
Out[]=
{ab,aa∘a,aa∘b,aa∘(a∘a),aa∘(a∘b),aa∘(b∘a),aa∘(b∘b),ab∘a,ab∘b,ab∘(a∘a),ab∘(a∘b),ab∘(b∘a),ab∘(b∘b),a(a∘a)∘a,a(a∘a)∘b,a(a∘b)∘a,a(a∘b)∘b,a(b∘a)∘a,a(b∘a)∘b}{{3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3},{None,3,None,4,None,None,None,None,None,None,None,None,None,4,None,None,None,None,None},{None,3,3,3,3,3,3,None,None,None,None,None,None,4,4,4,4,None,None},{None,None,None,3,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None},{None,4,None,3,3,None,None,None,None,None,None,None,None,5,None,None,None,None,None},{None,None,None,3,None,3,None,None,None,None,None,None,None,None,None,None,None,None,None},{None,None,None,3,None,None,3,None,None,None,None,None,None,None,None,None,None,None,None},{None,3,None,4,None,4,None,3,None,4,None,4,None,3,None,3,None,3,None},{4,3,4,4,4,4,4,4,3,4,4,4,4,4,4,4,4,4,4},{None,None,None,3,None,5,None,None,None,3,None,5,None,None,None,None,None,None,None},{None,None,None,3,None,None,None,None,None,None,3,None,None,4,None,None,None,None,4},{None,None,None,3,None,None,None,None,None,None,None,3,None,None,None,None,None,None,None},{4,4,4,3,4,4,4,4,4,4,4,4,3,4,4,4,4,4,4},{None,None,None,None,None,None,None,None,None,None,None,None,None,3,None,None,None,None,None},{None,None,None,None,None,None,None,None,None,None,None,None,None,3,3,5,5,None,None},{None,None,None,None,None,None,None,None,None,None,None,None,None,3,None,3,None,None,None},{None,None,None,None,None,None,None,None,None,None,None,None,None,3,None,None,3,None,None},{None,4,None,5,None,None,None,None,None,None,None,None,None,3,None,None,None,3,None},{None,None,None,4,None,None,None,None,None,None,4,None,None,3,None,None,None,None,3}}
In[]:=
PlotAx[axs_->mat_]:=MatrixPlot[mat,Mesh->True,FrameTicks->{MapIndexed[{First[#2],#1,0}&,axs],MapIndexed[{First[#2],Rotate[#1,Pi/2],0}&,axs]}]
In[]:=
PlotAx[%930]
Out[]=
In[]:=
TheoremArray23[axct_,thmct_]:=With[{axlist=DeleteCases[Union[Sort/@canonicalizePatterns/@(TwoWayRule@@@Tuples[(Flatten[Groupings[#,SmallCircle->2]&/@Table[Tuples[{a,b},n],{n,3}]]/.{a->a_,b->b_}),2])]/.{p_Pattern:>First[p],TwoWayRule->Equal},Except[_Equal]]},{Take[axlist,axct],Take[axlist,thmct]}->ParallelTable[If[Head[#]===Failure,None,#["ProofLength"]]&[FindEquationalProof[ForAll[{a,b},tx],ForAll[{a,b},ax],TimeConstraint4]],{ax,Take[axlist,axct]},{tx,Take[axlist,thmct]}]]
In[]:=
TheoremArray23[5,8]
Out[]=
{{ab,aa∘a,aa∘b,aa∘(a∘a),aa∘(a∘b)},{ab,aa∘a,aa∘b,aa∘(a∘a),aa∘(a∘b),aa∘(b∘a),aa∘(b∘b),ab∘a}}{{3,3,3,3,3,3,3,3},{None,3,None,4,None,None,None,None},{None,3,3,3,3,3,3,None},{None,None,None,3,None,None,None,None},{None,4,None,3,3,None,None,None}}
In[]:=
PlotAxX[{axs_,ths_}->mat_]:=MatrixPlot[mat,Mesh->True,FrameTicks->{{MapIndexed[{First[#2],#1,0}&,axs],None},{None,MapIndexed[{First[#2],Rotate[#1,Pi/2],0}&,ths]}}]
In[]:=
PlotAxX[%960]
Out[]=
In[]:=
TheoremArray23[20,40]
Out[]=
In[]:=
PlotAxX[%]
Out[]=
In[]:=
PlotAxX[%971]
Out[]=
Nasty bugs:
Nasty bugs:
More:
More:
Entailment Cone
Entailment Cone