law cgv

lawful-fields@0.1.1.0 · proof_cut.bend:787

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

787law cgv:
788  for +k: Nat
789  for +g: Bool
790  for +s: Nat
791  for +e: U32
792  for +len: U32
793  for +t: P.Tree<U32>
794  for +d: Nat
795  for +to: U32
796  for +sep: U32
797  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
798  for +hT: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
799  for +hs: {Nat.is_le(s, U32.to_nat(to)) == True{} : Bool}
800  for +hsep: {U32.is_lt(sep, 256) == True{} : Bool}
801  for +he: {U32.to_nat(e) == D.first(D.view(C.BT(len, t)), s, U32.to_nat(to), sep) : Nat}
802  for +hg: {U32.is_lt(e, to) == g : Bool}
803  {F.nats(CG(1n+k, True{}, e, len, t, to, sep)) == 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+k) : List<&2, Nat>}