law append_ok

lawful-bytes@0.1.1.0 · LAWS.bend:203

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

203law append_ok:
204  for dst: D.Bytes
205  for src: D.Bytes
206  for d: Nat
207  for s: U32
208  for n: U32
209  for hd: {D.ok(dst, d) == True{} : Bool}
210  for hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}
211  {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append(dst, src, s, n)), d) == True{} : Bool}