law sv_jd

lawful-bytes@0.1.1.0 · proof_shift.bend:334

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

334# j <= L - k from j + k < L.
335law sv_jd:
336  for +len: U32
337  for +t: P.Tree<U32>
338  for +d: Nat
339  for +jj: Nat
340  for +kk: Nat
341  for +h0: {D.ok(C.BT(len, t), d) == True{} : Bool}
342  for +hlt: {Nat.is_lt(Nat.add(jj, kk), U32.to_nat(len)) == True{} : Bool}
343  {Nat.is_le(jj, List.length(&2, U32, List.drop(&2, U32, D.view(C.BT(len, t)), kk))) == True{} : Bool}