law sp1c

lawful-fields@0.1.1.0 · proof_cut.bend:239

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

239law sp1c:
240  for +x: U32
241  for +t: List<&2, U32>
242  for +sep: U32
243  for +b: Bool
244  for +hb: {U32.is_eq(x, sep) == b : Bool}
245  for +h: {Nat.is_lt(D.run_len(x <> t, sep), List.length(&2, U32, x <> t)) == True{} : Bool}
246  for ih: {Nat.is_lt(D.run_len(t, sep), List.length(&2, U32, t)) == True{} : Bool} -> {F.split(t, sep) == List.take(&2, U32, t, D.run_len(t, sep)) <> F.split(List.drop(&2, U32, t, Nat.add(D.run_len(t, sep), 1n)), sep) : List<&2, List<&2, U32>>}
247  {F.split(x <> t, sep) == List.take(&2, U32, x <> t, D.run_len(x <> t, sep)) <> F.split(List.drop(&2, U32, x <> t, Nat.add(D.run_len(x <> t, sep), 1n)), sep) : List<&2, List<&2, U32>>}