PROOF.fast_append_view.go: def of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/PROOF.bend as PROOF
Lines 508-520 of lawful-bytes@0.1.1.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&start_line=508&end_line=520

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_fast_append.bend as FX

def fast_append_view.go(-dst: D.Bytes, -src: D.Bytes, +d: Nat, +e: Nat, +s: U32, +n: U32, hd: {D.ok(dst, d) == True{} : Bool}, he: {D.ok(src, e) == True{} : Bool}, hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(src)) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}, m_dst: C.BMirror(dst), m_src: C.BMirror(src)) ->
  {D.view(Pair.fst(D.Bytes, D.Bytes, FA.append(dst, src, s, n))) == List.append(&2, U32, D.view(dst), D.slice(D.view(src), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}:
  (+l_dst, m2_dst) = m_dst
  (+t_dst, +e_dst) = m2_dst
  (+l_src, m2_src) = m_src
  (+t_src, +e_src) = m2_src
  %e_dst : {D.view(Pair.fst(D.Bytes, D.Bytes, FA.append(_, src, s, n))) == List.append(&2, U32, D.view(_), D.slice(D.view(src), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}
  %e_src : {D.view(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(l_dst, t_dst), _, s, n))) == List.append(&2, U32, D.view(C.BT(l_dst, t_dst)), D.slice(D.view(_), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}
  +hd_t = C.tr(x => {D.ok(x, d) == True{} : Bool}, dst, l_dst, t_dst, e_dst, hd)
  +he_t = C.tr(x => {D.ok(x, e) == True{} : Bool}, src, l_src, t_src, e_src, he)
  +hs_t = C.tr(x => {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(x)) == True{} : Bool}, src, l_src, t_src, e_src, hs)
  +hc_t = C.tr(x => {Nat.is_le(Nat.add(D.size(x), U32.to_nat(n)), D.cap(x)) == True{} : Bool}, dst, l_dst, t_dst, e_dst, hc)
  FX.fast_append_view_t(l_dst, t_dst, l_src, t_src, d, e, s, n, hd_t, he_t, hs_t, hc_t)

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=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=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.to_nat
  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_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=tr
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=fast_append_view_t