def add_after_subtract

stelliferous@0.0.2.0 · proofs/bounded_u32_arithmetic.bend:74

import Base

74def add_after_subtract(+value: U32,+padding: U32,+offset: U32) ->
75  {((value - padding : U32) + offset : U32) == ((value + offset : U32) - padding : U32) : U32}:
76  %Equal.sym(U32,((value - padding : U32) + offset : U32),(offset + (value - padding : U32) : U32),add_commutative((value - padding : U32),offset)) :
77    {_ == ((value + offset : U32) - padding : U32) : U32}
78  %add_commutative(offset,value) : {(offset + (value - padding : U32) : U32) == (_ - padding : U32) : U32}
79  Equal.sym(U32,((offset + value : U32) - padding : U32),(offset + (value - padding : U32) : U32),subtract_from_sum(offset,value,padding))