law fast_append_ok

lawful-bytes@0.1.1.0 · LAWS.bend:475

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-bytes@0.1.1.0/fast.bend as FA

475law fast_append_ok:
476  for dst: D.Bytes
477  for src: D.Bytes
478  for d: Nat
479  for s: U32
480  for n: U32
481  for hd: {D.ok(dst, d) == True{} : Bool}
482  for hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}
483  {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(dst, src, s, n)), d) == True{} : Bool}