Pensieve Header: The pentagon in β-calculus, ignoring the hexagon.

SetDirectory["C:\\drorbn\\AcademicPensieve\\2012-01"];
<< betaCalculus.m

(V=α ar[1,1] + β ar[1,2] + γ ar[2,1] + δ ar[2,2]) // βForm

({t1,t2} = {V**dΔ[1,1,2][R[1,3]], R[1,3]**R[2,3]**V} /. _W -> 0) // βForm

eqns=Simplify[Coefficient[(t1-t2 // βCollect) /. h[3]->1,t[#]] == 0]& /@ {1,2}

γsol=(Solve[eqns, {α, β, γ, δ}] /. {α|β|δ -> 0})[[1,1,2]] // FullSimplify

(V0=βCollect[V /. {γ -> γsol, α|β|δ -> 0}]) // βForm

V0**dΔ[1,1,2][R[1,3]] - R[1,3]**R[2,3]**V0 // βForm

(V0Inv= λ ar[2,1]) // βForm

(V0Inv**V0) // βForm

λsol = First@Solve[λ+((((E^(c[1])) ((-1+(E^(c[2]))) c[1]-c[2])+c[2]) (1+λ c[2]))/((-1+(E^(c[1]))) c[2] (c[1]+c[2])))==0, λ]

(V0Inv = V0Inv /. λsol) // βForm

(Φ = 
(V0Inv // dP[2->3] // dΔ[1,1,2]) ** V0Inv ** (V0 // dP[1->2, 2->3]) ** (V0 // dΔ[2,2,3])
) // βForm

(t1 = Φ ** (Φ // dP[3->4] // dΔ[2,2,3]) ** (Φ // dP[1->2, 2->3, 3->4])) // βForm

(t2 = (Φ // dP[2->3, 3->4] // dΔ[1,1,2]) ** (Φ // dΔ[3,3,4])) // βForm

t1==t2