def position_step

bendtorch-core@0.1.0.0 · src/autograd/reduce_replayed_proof.bend:227

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

227def position_step(+capacity: Nat, +offset: Nat, +base: Nat) ->
228  {Nat.add(offset, Nat.add(capacity, base)) == Nat.add(Nat.add(capacity, offset), base) : Nat}:
229  Equal.trans(Nat, Nat.add(offset, Nat.add(capacity, base)), Nat.add(capacity, Nat.add(offset, base)), Nat.add(Nat.add(capacity, offset), base),
230    Nats.add_swap(offset, capacity, base), Index.add_assoc(capacity, offset, base))