def position_step

bendtorch-core@0.1.0.0 · src/tensor/contracts/matmul_parallel_proof.bend:210

import Base
import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats

210def position_step(+capacity: Nat, +offset: Nat, +base: Nat) ->
211  {Nat.add(offset, Nat.add(capacity, base)) == Nat.add(Nat.add(capacity, offset), base) : Nat}:
212  Equal.trans(Nat, Nat.add(offset, Nat.add(capacity, base)), Nat.add(capacity, Nat.add(offset, base)), Nat.add(Nat.add(capacity, offset), base),
213    Nats.add_swap(offset, capacity, base), Index.add_assoc(capacity, offset, base))