TensorAccessCertificate.reduced: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend as TensorAccessCertificate
Lines 253-265 of stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend&start_line=253&end_line=265

import Base
import stelliferous@0.0.2.0/tensor_view.bend as Views
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/tensor_cursor.bend as Cursor
import stelliferous@0.0.2.0/proofs/tensor_cursor_witness.bend as CursorWitness
import stelliferous@0.0.2.0/proofs/traversal_visit_witness.bend as VisitWitness
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

def reduced(~Element: Data,~Accumulator: Data,~operation: Accumulator -> Element -> Accumulator,
  call: ReduceCall,-storage: Array<Element>,-initial: Accumulator,certificate: Certificate.Certificate<Element,storage>) ->
  {TraversalWitness.first(~Array<Element>,~Accumulator,reduce_operation(~Element,~Accumulator,~operation,call,storage,initial)) == storage : Array<Element>}:
  match call:
    case ReduceCall{True{},count,Views.View{axes,offset}}:
      TraversalWitness.fold(~Array<Element>,~Element,~Accumulator,~Traversal.Offsets,~TraversalWitness.array_evidence(~Element),~Traversal.source_offset(~Element),~operation,~TraversalWitness.offset_read(~Element),
        count,storage,0,Traversal.Offsets{offset,0},initial,Certificate.witness(Element,storage,certificate))
    case ReduceCall{False{},count,view}:
      TraversalWitness.fold_finished(~Array<Element>,~Accumulator,~Cursor.Cursor,storage,
        Traversal.visit_fold(~Array<Element>,~Element,~Accumulator,~Cursor.Cursor,~Cursor.read(~Element),~operation,count,Traversal.State{storage,initial,0,Cursor.prepare(view)}),
        VisitWitness.fold_run(~Array<Element>,~Element,~Accumulator,~Cursor.Cursor,~TraversalWitness.array_evidence(~Element),~Cursor.read(~Element),~operation,~CursorWitness.read(~Element),
          count,storage,Traversal.State{storage,initial,0,Cursor.prepare(view)},Certificate.witness(Element,storage,certificate),
          TraversalWitness.FoldEvidence{initial,0,Cursor.prepare(view),{==}}))

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_certificate.bend&name=Certificate
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_certificate.bend&name=witness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend&name=ReduceCall
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend&name=reduce_operation
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/tensor_cursor_witness.bend&name=read
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_visit_witness.bend&name=fold_run
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=FoldEvidence
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=array_evidence
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=first
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=fold
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=fold_finished
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=offset_read
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_cursor.bend&name=Cursor
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_cursor.bend&name=prepare
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_cursor.bend&name=read
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_view.bend&name=View
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=Offsets
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=source_offset
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=visit_fold