simp[run_denoteOp]
n : ℕ
r : Region scf
⊢ run
      (denoteOp scf
        (Op.mk "scf.for'" [] [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
          (AttrDict.mk [])))
      (INPUT n) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (INPUT n)
n : ℕ
r : Region scf
⊢ run
      (do
        let args ← denoteOpArgs scf [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)]
        OpM.toTopM (TopM.mapDenoteRegion scf [r])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] args (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
      (INPUT n) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (INPUT n)