def AliveHandwritten.alive_DivRemOfSelect_src (w : ℕ) : Com InstCombine.LLVM ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy <$> ((Ctxt.snoc [] (InstCombine.MTy.bitvec 1)).snoc (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩))).snoc (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩))) EffectKind.pure ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩)))

Equations

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

def AliveHandwritten.alive_DivRemOfSelect_tgt (w : ℕ) : Com InstCombine.LLVM ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy <$> ((Ctxt.snoc [] (InstCombine.MTy.bitvec 1)).snoc (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩))).snoc (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩))) EffectKind.pure ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩)))

Equations

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

@[simp]

theorem AliveHandwritten.BitVec.ofNat_toNat_zero {w : ℕ} : (BitVec.ofInt w 0).toNat = 0

theorem AliveHandwritten.alive_DivRemOfSelect (w : ℕ) : (AliveHandwritten.alive_DivRemOfSelect_src w ⊑ AliveHandwritten.alive_DivRemOfSelect_tgt w) ⋯