KernelGatherCertificate.finish: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/kernel_gather_certificate.bend as KernelGatherCertificate
Lines 31-35 of stelliferous@0.0.2.0/proofs/kernel_gather_certificate.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/kernel_gather_certificate.bend&start_line=31&end_line=35

import Base
import stelliferous@0.0.2.0/kernel_gather.bend as Gather
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

def finish(-depth: Nat,-input: Array<F32>,-owners: Array<F32> & Array<F32>,evidence: TraversalWitness.ResultEvidence<Array<F32>,F32,input,depth,owners>) ->
  Witness.Witness(F32,depth,Gather.gathered_output(owners)):
  TraversalWitness.ResultEvidence{output,equation,balanced} = evidence
  %Equal.sym(Array<F32> & Array<F32>,owners,(input,output),equation) : Witness.Witness(F32,depth,Gather.gathered_output(_))
  balanced

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gather.bend&name=gathered_output
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=Witness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=ResultEvidence