law sp2c

lawful-fields@0.1.1.0 · proof_cut.bend:281

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

281law sp2c:
282  for +x: U32
283  for +t: List<&2, U32>
284  for +sep: U32
285  for +b: Bool
286  for +hb: {U32.is_eq(x, sep) == b : Bool}
287  for +h: {Nat.is_le(List.length(&2, U32, x <> t), D.run_len(x <> t, sep)) == True{} : Bool}
288  for ih: {Nat.is_le(List.length(&2, U32, t), D.run_len(t, sep)) == True{} : Bool} -> {F.split(t, sep) == [t] : List<&2, List<&2, U32>>}
289  {F.split(x <> t, sep) == [x <> t] : List<&2, List<&2, U32>>}