law decs

lawful-fields@0.1.1.0 · proof_num.bend:575

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

575law decs:
576  for +xs: List<&2, U32>
577  for +i: Nat
578  for +k: Nat
579  for +x: U32
580  for +M: Nat
581  for +hx: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
582  {F.decb(D.slice(xs, i, 1n+k), M) == F.decb.of(F.dec.go(D.slice(xs, i, 1n+k), Some{0n}), M) : Maybe<&2, Nat>}