def Sim.decidableRobddHSimilar {n m m' : ℕ} (O : OBdd n m) (hO : O.Reduced) (U : OBdd n m') (hU : U.Reduced) : Decidable (O.HSimilar U)

Equations

• Sim.decidableRobddHSimilar O hO U hU = (Sim.sim_helper✝ O hO U hU (↑O).root ⋯ (↑U).root ⋯ { lr := Std.HashMap.emptyWithCapacity 0, rl := Std.HashMap.emptyWithCapacity 0, hl := ⋯, hr := ⋯ }).1