law same1_view

lawful-bytes@0.1.1.0 · LAWS.bend:313

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

313law same1_view:
314  for b: D.Bytes
315  for d: Nat
316  for i: U32
317  for j: U32
318  for n: U32
319  for h: {D.ok(b, d) == True{} : Bool}
320  for hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(b)) == True{} : Bool}
321  for hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(b)) == True{} : Bool}
322  {Pair.snd(D.Bytes, Bool, B.same1(b, i, j, n)) == D.list_eq(D.slice(D.view(b), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(b), U32.to_nat(j), U32.to_nat(n))) : Bool}