law ylen

lawful-fields@0.1.1.0 · proof_cut.bend:731

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-bytes@0.1.1.0/proof_core.bend as C
import lawful-arrays@0.1.0.0/proof_tree.bend as P

731# The slice from s to T has T - s bytes.
732law ylen:
733  for +len: U32
734  for +t: P.Tree<U32>
735  for +d: Nat
736  for +s: Nat
737  for +tt: Nat
738  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
739  for +hT: {Nat.is_le(tt, U32.to_nat(len)) == True{} : Bool}
740  {List.length(&2, U32, D.slice(D.view(C.BT(len, t)), s, Nat.sub(tt, s))) == Nat.sub(tt, s) : Nat}