Pensieve header: The trace in α-calculus.

dir=SetDirectory["C:/drorbn/AcademicPensieve/Projects/MetaCalculi/"];
<< KnotTheory`
<< MetaCalculi-Program.m

n=3; γ0=Γ[ω, (∑_(a=0)^n)(Subscript[h, a])(Subscript[σ, a]), (∑_(a=1)^n)(∑_(b=1)^n)(Subscript[t, a])(Subscript[h, b])(Subscript[α, 10a+b])]

α0=A[ω, {t[a],t[b],t[S]}.(({{α, β, θ}, {γ, δ, ϵ}, {ϕ, ψ, Ξ}})).{h[a],h[b],h[S]}]

α0 // tha[a,b]

α0 // hm[a,b,c]

α0 // tm[a,b,c]

αSimplify[expr_]:=expr // Simplify;

α0 // dm[a,b,c] // αSimplify

α1=A[ω, {t[a],t[S]}.(({{α, θ}, {ϕ, Ξ}})).{h[a],h[S]}]

(α1 // Γ // tr[a] // A) /. Log[(E^(x_))] :> x

{α0 //dσ[S->c],
(α0 //dσ[S->c]// Γ // tr[c] // A) /. Log[(E^(x_))] :> x}

{α0 //dσ[S->c],
(α0 //dσ[S->c]// tr[c])}

{α0 // dm[a,b,c] // tr[c], α0 // dm[b,a,c] // tr[c]}