structure Sim.State {n m m' : ℕ} (O : OBdd n m) (U : OBdd n m') : Type

• lr : Std.HashMap (Fin m) (Fin m')
• rl : Std.HashMap (Fin m') (Fin m)
• hl (j : Fin m) (j' : Fin m') : self.lr[j]? = some j' → self.rl[j']? = some j ∧ Pointer.Reachable (↑O).heap (↑O).root (Pointer.node j) ∧ ∃ (hj : { heap := (↑O).heap, root := Pointer.node j }.Ordered) (hj' : { heap := (↑U).heap, root := Pointer.node j' }.Ordered), OBdd.HSimilar ⟨{ heap := (↑O).heap, root := Pointer.node j }, ⋯⟩ ⟨{ heap := (↑U).heap, root := Pointer.node j' }, ⋯⟩
• hr (j : Fin m) (j' : Fin m') : self.rl[j']? = some j → self.lr[j]? = some j' ∧ Pointer.Reachable (↑U).heap (↑U).root (Pointer.node j') ∧ ∃ (hj : { heap := (↑O).heap, root := Pointer.node j }.Ordered) (hj' : { heap := (↑U).heap, root := Pointer.node j' }.Ordered), OBdd.HSimilar ⟨{ heap := (↑O).heap, root := Pointer.node j }, ⋯⟩ ⟨{ heap := (↑U).heap, root := Pointer.node j' }, ⋯⟩

@[irreducible]

def Sim.sim_helper {n m m' : ℕ} (O : OBdd n m) (hO : O.Reduced) (U : OBdd n m') (hU : U.Reduced) (p : Pointer m) (hpr : Pointer.Reachable (↑O).heap (↑O).root p) (q : Pointer m') (hqr : Pointer.Reachable (↑U).heap (↑U).root q) : StateM (State O U) (Decidable (OBdd.HSimilar ⟨{ heap := (↑O).heap, root := p }, ⋯⟩ ⟨{ heap := (↑U).heap, root := q }, ⋯⟩))

Equations

• One or more equations did not get rendered due to their size.
• Sim.sim_helper O hO U hU (Pointer.terminal b') hqr_2 (Pointer.terminal b'_1) hqr_4 = if hb : b' = b'_1 then pure (isTrue ⋯) else pure (isFalse ⋯)
• Sim.sim_helper O hO U hU (Pointer.terminal b') hqr_2 (Pointer.node j') hqr_4 = pure (isFalse ⋯)
• Sim.sim_helper O hO U hU (Pointer.node j') hqr_2 (Pointer.terminal b') hqr_4 = pure (isFalse ⋯)

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

Equations

• One or more equations did not get rendered due to their size.