law sv_write

lawful-bytes@0.1.1.0 · proof_shift.bend:267

import Base

267# Writing that value at j moves the boundary to j + 1.
268law sv_write:
269  for +xs: List<&2, U32>
270  for +jj: Nat
271  for +kk: Nat
272  for +x: U32
273  for +hj: {Nat.is_le(jj, List.length(&2, U32, List.drop(&2, U32, xs, kk))) == True{} : Bool}
274  for +hjl: {Nat.is_lt(jj, List.length(&2, U32, xs)) == True{} : Bool}
275  for +hx: {List.get(&2, U32, List.drop(&2, U32, xs, kk), jj) == Some{x} : Maybe<&2, U32>}
276  {List.set(&2, U32, SV(xs, kk, jj), jj, x) == SV(xs, kk, Nat.add(jj, 1n)) : List<&2, U32>}