Theorem: th1.equivalent (MLIR/Dialects/ArithSemantics.lean)

State before:
n m : FinInt 32
⊢ run ⟦ LHS ⟧
      (SSAEnv.One
        [(SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }),
          (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m })]) =
    run ⟦ RHS ⟧
      (SSAEnv.One
        [(SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }),
          (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m })])
Tactic:
simp [LHS, RHS,
      run, StateT.run,
      denoteOp, bind, List.mapM, StateT.bind, denoteOpArgs, List.mapM,
      List.mapM.loop, Except.bind, TopM.get, StateT.get, pure, Except.pure,
      StateT.pure, TopM.mapDenoteRegion, OpM.toTopM, TopM.set, StateT.set, MLIRType.eval,
      SSAEnv.get, SSAEnv.getT, cast]
State after:
n m : FinInt 32
⊢ FinInt.add n m = FinInt.add m n ∧
    [(SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }), (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m }),
        (SSAVal.SSAVal "r", { fst := MLIRType.int Signedness.Signless 32, snd := FinInt.add n m })] =
      [(SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }), (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m }),
        (SSAVal.SSAVal "r", { fst := MLIRType.int Signedness.Signless 32, snd := FinInt.add m n })]

State before:
n m : FinInt 32
⊢ FinInt.add n m = FinInt.add m n ∧
    [(SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }), (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m }),
        (SSAVal.SSAVal "r", { fst := MLIRType.int Signedness.Signless 32, snd := FinInt.add n m })] =
      [(SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }), (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m }),
        (SSAVal.SSAVal "r", { fst := MLIRType.int Signedness.Signless 32, snd := FinInt.add m n })]
Tactic:
simp [FinInt.add_comm']
State after:
no goals