law ol_rest

lawful-bytes@0.1.1.0 · proof_grow.bend:122

import Base

122# The rest still fits after the push.
123law ol_rest:
124  for +len: U32
125  for +d: Nat
126  for +r: Nat
127  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
128  for +hn: {Nat.is_le(Nat.add(U32.to_nat(len), 1n+r), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
129  {Nat.is_le(Nat.add(U32.to_nat((len + 1 : U32)), r), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}