ProofFastAppend.fav.go: def of lawful-bytes@0.1.1.0 Import: import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppend Lines 1576-1607 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=1576&end_line=1607 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-bytes@0.1.1.0/proof_append.bend as X import lawful-words@0.1.0.0/proof_nat.bend as N 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 fav.go(+ld: U32, +td: P.Tree, +ls: U32, +ts: P.Tree, +d: Nat, +e: Nat, +s: U32, +n: U32, +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}, +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool}, +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(C.BT(ls, ts))) == 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.view(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n))) == List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}: (+l1, m2) = m (+t1, +e1) = m2 +sn = U32.to_nat(s) +nn = U32.to_nat(n) +hhn = U32.to_nat(HH(ld, n)) +L1 = U32.to_nat(l1) +NP = U32.to_nat(NPw(ld, n)) +RHS = List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), sn, nn)) +el = el1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc) +hl0 = hlen0(ld, td, l1, d, n, el, hd, hc) +hss = N.le_trans(Nat.add(sn, hhn), Nat.add(sn, nn), U32.to_nat(ls), N.le_add_mono_l(sn, hhn, nn, hh_le(ld, n)), hs) +vd1 = AB.subst(D.Bytes, y => {D.view(y) == List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), sn, hhn)) : List<&2, U32>}, D1(ld, td, ls, ts, s, n), C.BT(l1, t1), Equal.sym(D.Bytes, C.BT(l1, t1), D1(ld, td, ls, ts, s, n), e1), X.append_view_t(ld, td, ls, ts, d, e, s, HH(ld, n), hd, he, hss, hc_h(ld, td, n, hc))) +eq = C.add_fits(s, HH(ld, n), e, C.ok_d(ls, ts, e, he), N.le_trans(Nat.add(sn, hhn), U32.to_nat(ls), Nat.mul(4n, Nat.pow(2n, e)), hss, C.ok_len(ls, ts, e, he))) %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.view(Pair.fst(D.Bytes, D.Bytes, _)) == RHS : List<&2, U32>} %Equal.sym(Nat, U32.to_nat(U32.add(l1, NPw(ld, n))), Nat.add(L1, NP), C.add_fits(l1, NPw(ld, n), d, C.ok_d(ld, td, d, hd), hl0)) : {List.take(&2, U32, US(TF(ld, ts, s, n, l1, t1)), _) == RHS : List<&2, U32>} Equal.trans(List<&2, U32>, List.take(&2, U32, US(TF(ld, ts, s, n, l1, t1)), Nat.add(L1, NP)), 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))), NP)), RHS, avc(Nat.is_lt(U32.to_nat(H0(ld)), nn), ld, td, ls, ts, d, e, s, n, l1, t1, {==}, e1, hd, he, hs, hc), fin_eq(D.view(C.BT(l1, t1)), D.view(C.BT(ld, td)), US(ts), U32.to_nat(ls), sn, hhn, U32.to_nat(QQ(ld, s, n)), NP, nn, vd1, eq, enp(ld, n), hh_le(ld, n), hs)) Uses (51): 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=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.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=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.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=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/fast.bend&name=append https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_append.bend&name=append_view_t 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=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_len 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=QQ 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=avc 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=fa_eq https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=fin_eq https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=hc_h 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-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