ProofFastAppend.step: law of lawful-bytes@0.1.1.0 Import: import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppend Lines 755-788 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=755&end_line=788 import Base import lawful-bytes@0.1.1.0/proof_core.bend as C import lawful-arrays@0.1.0.0/defs.bend as A import lawful-arrays@0.1.0.0/proof_tree.bend as P import lawful-arrays@0.1.0.0/proof_index.bend as I law step: for +ts: P.Tree for +e: Nat for +td: P.Tree for +d: Nat for +p: U32 for +lo: U32 for +si: U32 for +di: U32 for +sh: Nat for +l1: Nat for +qn: Nat for +r: Nat for +o: Nat for +np: Nat for +v1: List<&2, U32> for +m: Nat for +hfs: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool} for +hes: {Nat.is_le(e, 29n) == True{} : Bool} for +hfd: {A.full(U32, P.fromT(U32, td), d) == True{} : Bool} for +hdd: {Nat.is_le(d, 29n) == True{} : Bool} for +hdi: {Nat.mul(U32.to_nat(di), 4n) == Nat.add(l1, o) : Nat} for +hsi: {Nat.add(Nat.mul(U32.to_nat(si), 4n), r) == Nat.add(qn, o) : Nat} for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat} for +hlo: {lo == C.WD(ts, si) : U32} for +hsh: {sh == Nat.mul(8n, r) : Nat} for +hr: {Nat.is_lt(r, 4n) == True{} : Bool} for +hq: {Nat.is_le(Nat.add(qn, np), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool} for +hl: {Nat.is_le(Nat.add(l1, np), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool} for +ho: {Nat.is_lt(o, np) == True{} : Bool} for +hm: {Nat.is_le(m, 4n) == True{} : Bool} for +hmv: {Nat.is_le(Nat.add(o, m), np) == True{} : Bool} for +hinv: {List.take(&2, U32, US(td), Nat.add(l1, o)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), o)) : List<&2, U32>} {List.take(&2, U32, US(I.set_tree(U32, td, di, U32.or(U32.shrn(lo, sh), U32.shln(C.WD(ts, p), Nat.sub(32n, sh))))), Nat.add(l1, Nat.add(o, m))) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), Nat.add(o, m))) : List<&2, U32>} Uses (47): 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.length https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.set 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_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.or https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shln 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/defs.bend&name=full 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_index.bend&name=set_tree 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-arrays@0.1.0.0/proof_tree.bend&name=fromT https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=view_length https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=unpack https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_append.bend&name=append_assoc https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=L4 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=WL https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=wl_set 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=drop_drop https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=lt_w0 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=mrg https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=take_split https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=us1 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=win https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/defs.bend&name=merge 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=le_add_mono_l 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=lt_add_l https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=lt_le_trans