Theorem: SCF.FOR_PEELING.equivalent
Proof state before:
n : ℕ
r : Region scf
⊢ (match
      match
        match
          Except.ok
            (match
                SSAEnv.get (SSAVal.SSAVal "cn_plus_1") MLIRType.index
                  (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                    (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                      (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))) with
              | some v => v
              | none => default,
              SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, snd := a } :: a_1)) env'
          | Except.error e => Except.error e
        | Except.error e => Except.error e with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    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 [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
rw[SSAEnv.get_set_eq_val] <;> simp
Proof state after:
n : ℕ
r : Region scf
⊢ (match
      match
        match
          run (denoteOpArgs scf [])
            (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
              (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := ↑n + 1 } :: a)) env'
        | Except.error e => Except.error e with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    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 [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"