def position_step

bendtorch-core@0.1.0.0 · src/tensor/parallel_proofs.bend:71

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

71def position_step(+capacity: Nat, +offset: Nat, +base: Nat) ->
72  {Nat.add(offset, Nat.add(capacity, base)) == Nat.add(Nat.add(capacity, offset), base) : Nat}:
73  Equal.trans(Nat, Nat.add(offset, Nat.add(capacity, base)), Nat.add(capacity, Nat.add(offset, base)), Nat.add(Nat.add(capacity, offset), base),
74    Nats.add_swap(offset, capacity, base), Index.add_assoc(capacity, offset, base))