law cgf

lawful-fields@0.1.1.0 · proof_cut.bend:752

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-fields@0.1.1.0/defs.bend as F
import lawful-bytes@0.1.1.0/proof_core.bend as C
import lawful-arrays@0.1.0.0/proof_tree.bend as P

752# After the last piece (the end reached to): one more end, at to.
753law cgf:
754  for +s: Nat
755  for +e: U32
756  for +len: U32
757  for +t: P.Tree<U32>
758  for +d: Nat
759  for +to: U32
760  for +sep: U32
761  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
762  for +hT: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
763  for +he: {U32.to_nat(e) == D.first(D.view(C.BT(len, t)), s, U32.to_nat(to), sep) : Nat}
764  for +hg: {U32.is_lt(e, to) == False{} : Bool}
765  for +kk: Nat
766  {Con{U32.to_nat(e), Nil{}} == List.take(&2, Nat, F.ends(F.split(D.slice(D.view(C.BT(len, t)), s, Nat.sub(U32.to_nat(to), s)), sep), s), 1n+kk) : List<&2, Nat>}