ProofCut.cgv: law of lawful-fields@0.1.1.0 Import: import lawful-fields@0.1.1.0/proof_cut.bend as ProofCut Lines 787-803 of lawful-fields@0.1.1.0/proof_cut.bend: https://jend.leeeet.dev/read.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&start_line=787&end_line=803 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 law cgv: for +k: Nat for +g: Bool for +s: Nat for +e: U32 for +len: U32 for +t: P.Tree for +d: Nat for +to: U32 for +sep: U32 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} for +hT: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool} for +hs: {Nat.is_le(s, U32.to_nat(to)) == True{} : Bool} for +hsep: {U32.is_lt(sep, 256) == True{} : Bool} for +he: {U32.to_nat(e) == D.first(D.view(C.BT(len, t)), s, U32.to_nat(to), sep) : Nat} for +hg: {U32.is_lt(e, to) == g : Bool} {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>} Uses (54): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.drop https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.take https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=subst https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=Tree https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=first https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=ok https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=run_len https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=slice https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=view https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=BT https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=inc_fits https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=ok_d https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=ok_len https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=succ_le https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_find.bend&name=find_view_t https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_seq.bend&name=take_length https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=ends https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=nats https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=split https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=CG https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=FV https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=NX https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=cgf https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=lt_sub_of https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=slice_drop https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=sp1 https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=tz https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_cut.bend&name=ylen https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=add_assoc https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=lt_le_trans https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=lt_to_le https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=is_le_to_nat https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=is_lt_to_nat