law ends_push

lawful-fields@0.1.1.0 · proof_cut.bend:468

import Base
import lawful-fields@0.1.1.0/defs.bend as F

468# Pushing a byte onto the first piece shifts every end by one.
469law ends_push:
470  for +x: U32
471  for +ps: List<&2, List<&2, U32>>
472  for +s: Nat
473  for +hnn: {nn(ps) == True{} : Bool}
474  {F.ends(F.split.push(x, ps), s) == F.ends(ps, Nat.add(s, 1n)) : List<&2, Nat>}