ProofFastAppend.fao.go: def of lawful-bytes@0.1.1.0 Import: import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppend Lines 1419-1438 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=1419&end_line=1438 import Base import lawful-bytes@0.1.1.0/defs.bend as D import lawful-bytes@0.1.1.0/fast.bend as FA import lawful-bytes@0.1.1.0/proof_core.bend as C import lawful-arrays@0.1.0.0/proof_base.bend as AB import lawful-arrays@0.1.0.0/proof_tree.bend as P def fao.go(+ld: U32, +td: P.Tree, +ls: U32, +ts: P.Tree, +d: Nat, +s: U32, +n: U32, +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}, +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}, m: C.BMirror(D1(ld, td, ls, ts, s, n))) -> {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n)), d) == True{} : Bool}: (+l1, m2) = m (+t1, +e1) = m2 +q = QQ(ld, s, n) +hk1 = ok1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc) +el = el1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc) +hdd = C.ok_d(ld, td, d, hd) +hl0 = hlen0(ld, td, l1, d, n, el, hd, hc) %Equal.sym(D.Bytes & D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n), (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)), fa_eq(ld, td, ls, ts, s, n, l1, t1, e1)) : {D.ok(Pair.fst(D.Bytes, D.Bytes, _), d) == True{} : Bool} C.ok_mk(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1), d, aw_full(NW(ld, n), ts, U32.add(U32.shrn(q, 2n), 1), C.WD(ts, U32.shrn(q, 2n)), t1, U32.shrn(q, 2n), U32.shrn(l1, 2n), SH(q), d, C.ok_full(l1, t1, d, hk1)), hdd, AB.subst(Nat, y => {Nat.is_le(y, Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}, Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))), U32.to_nat(U32.add(l1, NPw(ld, n))), Equal.sym(Nat, U32.to_nat(U32.add(l1, NPw(ld, n))), Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))), C.add_fits(l1, NPw(ld, n), d, hdd, hl0)), hl0)) Uses (39): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym 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.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=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma 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.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/fast.bend&name=append https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=BMirror 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=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_mk 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=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=aw_full 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=fa_eq 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=ok1