[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[]