law of_list_view

lawful-bytes@0.1.1.0 · proof_grow.bend:206

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

206law of_list_view:
207  for +d: Nat
208  for +xs: List<&2, U32>
209  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
210  for +hn: {Nat.is_le(List.length(&2, U32, xs), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
211  for +hb: {D.all_bytes(xs) == True{} : Bool}
212  {D.view(B.of_list(d, xs)) == xs : List<&2, U32>}