def indexed_successor

stelliferous@0.0.2.0 · proofs/loop_projection.bend:86

import Base
import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as Arithmetic
import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic

86def indexed_successor(+position: U32,+offset: Nat) ->
87  {(position + U32.from_nat(1n+offset) : U32) == ((position + 1 : U32) + U32.from_nat(offset) : U32) : U32}:
88  %WordArithmetic.native_add(1n,offset) :
89    {(position + _ : U32) == ((position + 1 : U32) + U32.from_nat(offset) : U32) : U32}
90  Equal.sym(U32,((position + 1 : U32) + U32.from_nat(offset) : U32),(position + (1 + U32.from_nat(offset) : U32) : U32),
91    Arithmetic.add_associative(position,1,U32.from_nat(offset)))