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

Equations

• Sim.decidableRobddHSimilar O hO U hU = ⋯ ▸ ⋯ ▸ (Sim.sim_helper✝ O hO U hU O.bdd.root ⋯ U.bdd.root ⋯ { lr := ∅, rl := ∅, hl := ⋯, hr := ⋯ }).1