[Earlier Version]

[[ Earlier version is in ARCHIVES ]]
FindReplacePath[{f[x_,y_]f[y,x],f[f[x_,y_],z_]f[x,f[y,z]],f[x_,f[y_,z_]]f[f[x,y],z]},f[f[b,a],f[b,a]],f[f[f[a,b],b],a],"MultiwayFragment"]
This is a basic function of multicomputation
FindReplacePath[rules,init,dest]
FindReplacePath[rules,init,FixedPoint]
where FixedPoint is a “meta pattern”
Or I could get multiple destinations....

Nik’s Version

In[]:=
AxiomaticTheory["BooleanAxioms"]
Out[]=

∀
a.,b.
a.⊗b.b.⊗a.,
∀
a.,b.,c.
a.⊗b.⊕c.a.⊗b.⊕a.⊗c.,
∀
a.,b.
a.⊕b.⊗
b.
a.,
∀
a.,b.
a.⊗b.⊕
b.
a.,
∀
a.,b.
a.⊕b.b.⊕a.,
∀
a.,b.,c.
a.⊕b.⊗c.a.⊕b.⊗a.⊕c.
In[]:=
AxiomaticTheory["BooleanAxioms","NotableTheorems"]
Out[]=
Absorption
∀
a.,b.
a.a.⊗a.⊕b.,AbsorptionOrAnd
∀
a.,b.
a.a.⊕a.⊗b.,AndAssociativity
∀
a.,b.,c.
a.⊗b.⊗c.a.⊗b.⊗c.,AndCommutativity
∀
a.,b.
a.⊗b.b.⊗a.,AndDistributivity
∀
a.,b.,c.
a.⊗b.⊕c.a.⊗b.⊕a.⊗c.,AndIdempotence
∀
a.
a.a.⊗a.,AndPreAssociativity
∀
a.,b.
a.⊗b.a.⊗a.⊗b.,DeMorgan
∀
a.,b.
a.⊕b.

a.
⊗
b.
,
∀
a.,b.
a.⊗b.

a.
⊕
b.
,DoubleNegation
∀
a.
a.
a.,DroppingAlwaysFalse
∀
a.,b.
a.a.⊕b.⊗
b.
,DroppingAlwaysTrue
∀
a.,b.
a.a.⊗b.⊕
b.
,ExcludedMiddle
∀
a.,b.
a.
⊕a.
b.
⊕b.,ImpliesHuntingtonAxioms
∀
a.,b.
a.⊕b.b.⊕a.,
∀
a.,b.,c.
a.⊕b.⊕c.a.⊕b.⊕c.,
∀
a.,b.
a.
⊕b.
⊕
a.
⊕
b.
a.,ImpliesRobbinsAxioms
∀
a.,b.
a.⊕b.b.⊕a.,
∀
a.,b.,c.
a.⊕b.⊕c.a.⊕b.⊕c.,
∀
a.,b.
a.⊕b.
⊕
a.⊕
b.
a.,NegationRedundancy
∀
a.,b.
a.⊕b.a.⊕
a.
⊗b.,Noncontradiction
∀
a.,b.
a.
⊗a.
b.
⊗b.,OrAssociativity
∀
a.,b.,c.
a.⊕b.⊕c.a.⊕b.⊕c.,OrCommutativity
∀
a.,b.
a.⊕b.b.⊕a.,OrDistributivity
∀
a.,b.,c.
a.⊕b.⊗c.a.⊕b.⊗a.⊕c.,OrIdempotence
∀
a.
a.a.⊕a.,Transposition
∀
a.,b.
a.
⊕b.
b.
⊕
a.

In[]:=
FindReplacePath["Absorption","BooleanAxioms"]
Out[]=
In[]:=
FindReplacePath["Absorption","BooleanAxioms","Path"]
Out[]=
a._⊗a._⊕b._,a._⊗a._⊕a._⊗b._,a._⊗a._⊕a._⊗
a._
⊕a._⊗b._,a._⊗a._⊕
a._
⊕a._⊗b._,a._⊕a._⊗b._,a._⊕b._⊗a._,a._⊕b._⊗a._⊕b._⊗
b._
,a._⊕b._⊗a._⊕
b._
,a._⊕b._⊗a._⊕a._⊕
b._
,a._⊕b._⊗a._⊕a._⊕
b._
⊗a._⊕
a._
,a._⊕b._⊗a._⊕
a._
⊗a._⊕a._⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗a._⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗a._⊕
a._
⊗
a._
⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗a._⊕
a._
⊗a._⊕
a._
⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗a._⊕
a._
⊗a._⊕
a._
⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗a._⊕
a._
⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗
a._
⊕a._⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗
a._
⊕a._⊗
a._
⊕
a._
⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗
a._
⊕a._⊗
a._
⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗
a._
⊕a._⊗
a._
⊕a._⊗
a._
⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗
a._
⊕a._⊗
a._
⊕a._⊗
a._
⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗
a._
⊕a._⊗
a._
⊕
a._
⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗
a._
⊕a._⊗
a._
⊕
a._
⊗
a._
⊕
a._
⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗
a._
⊕a._⊗
a._
⊕
a._
⊗
a._
⊕
a._
⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗
a._
⊕a._⊗
a._
⊕
a._
⊗
a._
⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗
a._
⊕a._⊗
a._
⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗
a._
⊕
b._
,a._⊕b._⊗a._⊕
a._
⊗
a._
⊕
a._
⊗
b._
,a._⊕b._⊗a._⊕
a._
⊗
b._
⊕
a._
⊗
a._
,a._⊕b._⊗a._⊕
a._
⊗
b._
,a._⊕b._⊗a._⊕
a._
⊗a._⊕
b._
,a._⊕b._⊗a._⊕
b._
⊗a._⊕
a._
,a._⊕b._⊗a._⊕
b._
,a._⊕b._⊗
b._
,a._
In[]:=
FindReplacePath[p∘(p∘p)q∘(q∘p),ForAll[{a,b},a==b∘a]]
Out[]=
Statementq∘(q∘p)p∘(p∘p),PathTestSuccess
✓
Message: Path sides match the original statement
Tag: Path
,RewriteTestSuccess
✓
Message: Running rewrite sequence reproduced the path.
Tag: Rewrite
,Justification{{{Axiom,1},Left,{}},{{Axiom,1},Left,{}},{{Axiom,1},Right,{}},{{Axiom,1},Right,{}}},Rewrites{Replace[b_∘a_a],Replace[b_∘a_a],Replace[a_b$1_∘a]/*ReplaceAll[b$1_p],Replace[a_b$2_∘a]/*ReplaceAll[b$2_p]},Path{q∘(q∘p),q∘p,p,p∘p,p∘(p∘p)}
In[]:=
FindReplacePath[p∘(p∘p)q∘(q∘p),ForAll[{a,b},a==b∘a],"Path"]
Out[]=
{q∘(q∘p),q∘p,p,p∘p,p∘(p∘p)}
In[]:=
FindReplacePath[p·q==q·p,"WolframAxioms","Path"]
justifyLemma
::wrongPosition
:Wrong substitution position {1,1,2,1,2} for lemma {SubstitutionLemma,1}. Found position {2,2,1,1} instead.
​
justifyLemma
::wrongPosition
:Wrong substitution position {1,1,2,1,2} for lemma {SubstitutionLemma,2}. Found position {2,2,2} instead.
​
justifyLemma
::wrongPosition
:Wrong substitution position {2} for lemma {SubstitutionLemma,40}. Found position {} instead.
​
General
:Further output of justifyLemma::wrongPosition will be suppressed during this calculation.
Out[]=
$Aborted[]