Loop.run_tree_go: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend as Loop
Lines 53-56 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&start_line=53&end_line=56

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend as K
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend as TR

def run_tree_go(+x: T.Out, +r: List<&2,T.Out>) -> {K.finish(TR.push_all(K.StkNil{},TR.cvs(init2(r,x))),last2(r,x)) == S.tree(1n+SC.length(T.Out,r),Con{x,r}) : T.Out}:
  %snoc2(r,x) : {K.finish(TR.push_all(K.StkNil{},TR.cvs(init2(r,x))),last2(r,x)) == S.tree(1n+SC.length(T.Out,r),_) : T.Out}
  %len_init2(r,x) : {K.finish(TR.push_all(K.StkNil{},TR.cvs(init2(r,x))),last2(r,x)) == S.tree(1n+_,SC.append(T.Out,init2(r,x),Con{last2(r,x),Nil{}})) : T.Out}
  TR.tree_stack(init2(r,x),last2(r,x))

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&name=init2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&name=last2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&name=len_init2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&name=snoc2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=cvs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=push_all
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=tree_stack
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=tree
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=length
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=Stack
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=finish
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend&name=Out