def offset_pair

bendtorch-core@0.1.0.0 · src/tensor/matrix_index_proof.bend:178

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

178def offset_pair(+a: Nat, +b: Nat, +first: Nat, +second: Nat) ->
179  {Shape.offset([first, second], [a, b]) == Nat.add(Nat.mul(a, second), b) : Nat}:
180  %Equal.sym(Nat, Nat.mul(second, 1n), second, Nats.mul_one_right(second)) :
181    {Nat.add(Nat.mul(a, _), Nat.add(Nat.mul(b, 1n), 0n)) == Nat.add(Nat.mul(a, second), b) : Nat}
182  %Equal.sym(Nat, Nat.mul(b, 1n), b, Nats.mul_one_right(b)) :
183    {Nat.add(Nat.mul(a, second), Nat.add(_, 0n)) == Nat.add(Nat.mul(a, second), b) : Nat}
184  %Equal.sym(Nat, Nat.add(b, 0n), b, Conversion.add_zero(b)) :
185    {Nat.add(Nat.mul(a, second), _) == Nat.add(Nat.mul(a, second), b) : Nat}
186  {==}