law wc

lawful-fields@0.1.1.0 · proof_cut.bend:577

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

577law wc:
578  for +x: U32
579  for +t: List<&2, U32>
580  for +s: Nat
581  for +sep: U32
582  for +b: Bool
583  for +hb: {U32.is_eq(x, sep) == b : Bool}
584  for +ih: {WN(F.ends(F.split(t, sep), Nat.add(s, 1n)), s, Nat.add(s, 1n+List.length(&2, U32, t))) == True{} : Bool}
585  {WN(F.ends(F.split(x <> t, sep), s), s, Nat.add(s, List.length(&2, U32, x <> t))) == True{} : Bool}