law sl_fin

lawful-fields@0.1.1.0 · proof_list.bend:55

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

55law sl_fin:
56  for +x: U32
57  for +r: List<&2, List<&2, U32>>
58  for +b: Bool
59  for +c: Nat
60  for +hr: {List.length(&2, List<&2, U32>, r) == Nat.add(c, 1n) : Nat}
61  {List.length(&2, List<&2, U32>, F.split.fin(x, r, b)) == Nat.add(F.count.if(b, c), 1n) : Nat}