In[]:=
twoWayRuleFix/@FindAccumulativeProof[{a_<->b_∘a_},2,a_∘(b_∘(c_∘d_))<->e_∘d_,10,"B","TokenLabeling"->True]
Out[]=

,
,
,
,
,
,
,
,
,

In[]:=
twoWayRuleFix/@FindAccumulativeProof[{a_<->b_∘a_},2,a_∘(b_∘(c_∘d_))<->e_∘d_,10,"B","TokenLabeling"->True,"EventDeduplication"->True]
Out[]=


In[]:=
Subgraph[%16,%23]
Out[]=
In[]:=
HighlightGraph[%16,Style[Subgraph[%16,First[%23]],Thick,Red]]
Out[]=
In[]:=
po=ProofObjectToTokenEventGraph[FindEquationalProof[a∘(b∘(c∘d))e∘d,ForAll[{a,b},a==b∘a]]]
Out[]=
In[]:=
EdgeList[po,Except[(ab∘a)_]]
Out[]=
{(e∘da∘(b∘(c∘d))){Event,Substitution Lemma 1},{Event,Substitution Lemma 1}(e∘da∘(b∘d)),(e∘da∘(b∘d)){Event,Substitution Lemma 2},{Event,Substitution Lemma 2}(da∘(b∘d)),(da∘(b∘d)){Event,Substitution Lemma 3},{Event,Substitution Lemma 3}(da∘d),(da∘d){Event,Conclusion 1},{Event,Conclusion 1}(dd)}
In[]:=
With[{u=EdgeList[po,Except[(ab∘a)_]]},EdgeAdd[EdgeDelete[po,u],Reverse/@u,VertexLabels->{_->None}]]
Out[]=
ProofObjectToTokenEventGraph[FindEquationalProof[a∘(b∘(c∘d))e∘d,ForAll[{a,b},a==b∘a]]]

Map:

Example of entailment cone where we can fish out a proof that is the same as ATP, probably using only substitution

Turning the proof around to make it more like entailment

More complicated case where bisubstitution is needed

critical pair lemmas

Much greater efficiency of finding a proof when one knows where one’s going

Cut elimination

[Confluence is automatic in accumulative systems]

Signature of confluence in a token-event graph

Completion

Derivation of new rule from existing rules
[Easier to use because there is a definite “objective function”: to reduce the size of the expression ??]
Ordering of statements

Search

Search for a theorem that cannot be found from the entailment cone

SW axiom

Another Axiom

Another axiom

Cut Elimination