MatrixIndexProof.offset_pair: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndexProof
Lines 178-186 of bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&start_line=178&end_line=186

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion

def offset_pair(+a: Nat, +b: Nat, +first: Nat, +second: Nat) ->
  {Shape.offset([first, second], [a, b]) == Nat.add(Nat.mul(a, second), b) : Nat}:
  %Equal.sym(Nat, Nat.mul(second, 1n), second, Nats.mul_one_right(second)) :
    {Nat.add(Nat.mul(a, _), Nat.add(Nat.mul(b, 1n), 0n)) == Nat.add(Nat.mul(a, second), b) : Nat}
  %Equal.sym(Nat, Nat.mul(b, 1n), b, Nats.mul_one_right(b)) :
    {Nat.add(Nat.mul(a, second), Nat.add(_, 0n)) == Nat.add(Nat.mul(a, second), b) : Nat}
  %Equal.sym(Nat, Nat.add(b, 0n), b, Conversion.add_zero(b)) :
    {Nat.add(Nat.mul(a, second), _) == Nat.add(Nat.mul(a, second), b) : Nat}
  {==}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=mul_one_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=add_zero