ProofFastAppend.avc: law of lawful-bytes@0.1.1.0 Import: import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppend Lines 1469-1488 of lawful-bytes@0.1.1.0/proof_fast_append.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&start_line=1469&end_line=1488 import Base import lawful-bytes@0.1.1.0/defs.bend as D import lawful-bytes@0.1.1.0/proof_core.bend as C import lawful-arrays@0.1.0.0/proof_tree.bend as P # What the word loop leaves: the bytes in use after the prefix, then src from q. law avc: for +b0: Bool for +ld: U32 for +td: P.Tree for +ls: U32 for +ts: P.Tree for +d: Nat for +e: Nat for +s: U32 for +n: U32 for +l1: U32 for +t1: P.Tree for +hb0: {Nat.is_lt(U32.to_nat(H0(ld)), U32.to_nat(n)) == b0 : Bool} for +e1: {C.BT(l1, t1) == D1(ld, td, ls, ts, s, n) : D.Bytes} for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool} for +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool} for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(C.BT(ls, ts))) == True{} : Bool} for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool} {List.take(&2, U32, US(TF(ld, ts, s, n, l1, t1)), Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n)))) == List.append(&2, U32, D.view(C.BT(l1, t1)), List.take(&2, U32, List.drop(&2, U32, US(ts), U32.to_nat(QQ(ld, s, n))), U32.to_nat(NPw(ld, n)))) : List<&2, U32>} Uses (79): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool 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.append 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.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.div 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.min 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.and https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shrn 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=Bytes https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=cap 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=size 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_append.bend&name=append_nil 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=WD https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=add_fits https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=he32 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_full 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_fast_append.bend&name=AWT https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=D1 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=H0 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=HH https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=NPw https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=NW https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=QQ https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=SH https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=TF https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=US https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=align https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=and3_lt https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=av https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=cnt1 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=cnt2 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=el1 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=enp https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=esum_n https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=exk https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=hh_le https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=hlen0 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=min_l https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=min_r https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=ok1 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=shq https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=x3_lt_e https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_seq.bend&name=take_zero https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_shift.bend&name=sub_self https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=add_zero https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=div_lt https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_add_l https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_add_mono_l https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_add_r https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_trans https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_zero_l https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=lt_add_l 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_u32.bend&name=to_nat_add_fits_p https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=to_nat_inj https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=to_nat_min https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=to_nat_shrn