TraversalLanesWitness.gathered: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend as TraversalLanesWitness
Lines 15-42 of stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend&start_line=15&end_line=42

import Base
import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes
import stelliferous@0.0.2.0/kernel_tile.bend as Tile
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness

def gathered(~Context: Data,~map: Context -> F32 -> F32,-values: Array<F32>,+position: U32,+context: Context,
  r0: Witness.Read<F32,values,Array.get(F32,values,position)>,
  r1: Witness.Read<F32,values,Array.get(F32,values,(position + 1 : U32))>,
  r2: Witness.Read<F32,values,Array.get(F32,values,((position + 1 : U32) + 1 : U32))>,
  r3: Witness.Read<F32,values,Array.get(F32,values,(((position + 1 : U32) + 1 : U32) + 1 : U32))>,
  r4: Witness.Read<F32,values,Array.get(F32,values,((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))>,
  r5: Witness.Read<F32,values,Array.get(F32,values,(((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))>,
  r6: Witness.Read<F32,values,Array.get(F32,values,((((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))>,
  r7: Witness.Read<F32,values,Array.get(F32,values,(((((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))>) ->
  Gathered<values,Lanes.gather(~Context,~map,values,position,context)>:
  match r0 r1 r2 r3 r4 r5 r6 r7:
    case Witness.Read{a,ea} Witness.Read{b,eb} Witness.Read{c,ec} Witness.Read{d,ed} Witness.Read{e,ee} Witness.Read{f,ef} Witness.Read{g,eg} Witness.Read{h,eh}:
      +p1 = (position + 1 : U32)
      +p2 = (p1 + 1 : U32)
      +p3 = (p2 + 1 : U32)
      +p4 = (p3 + 1 : U32)
      +p5 = (p4 + 1 : U32)
      +p6 = (p5 + 1 : U32)
      +p7 = (p6 + 1 : U32)
      %Equal.sym(Array<F32> & F32,Array.get(F32,values,position),(values,a),ea) : Gathered<values,Lanes.gather1(~Context,~map,position,context,_)>
      %Equal.sym(Array<F32> & F32,Array.get(F32,values,p1),(values,b),eb) : Gathered<values,Lanes.gather2(~Context,~map,p1,context,a,_)>
      %Equal.sym(Array<F32> & F32,Array.get(F32,values,p2),(values,c),ec) : Gathered<values,Lanes.gather3(~Context,~map,p2,context,a,b,_)>
      %Equal.sym(Array<F32> & F32,Array.get(F32,values,p3),(values,d),ed) : Gathered<values,Lanes.gather4(~Context,~map,p3,context,a,b,c,_)>
      %Equal.sym(Array<F32> & F32,Array.get(F32,values,p4),(values,e),ee) : Gathered<values,Lanes.gather5(~Context,~map,p4,context,a,b,c,d,_)>
      %Equal.sym(Array<F32> & F32,Array.get(F32,values,p5),(values,f),ef) : Gathered<values,Lanes.gather6(~Context,~map,p5,context,a,b,c,d,e,_)>
      %Equal.sym(Array<F32> & F32,Array.get(F32,values,p6),(values,g),eg) : Gathered<values,Lanes.gather7(~Context,~map,p6,context,a,b,c,d,e,f,_)>
      %Equal.sym(Array<F32> & F32,Array.get(F32,values,p7),(values,h),eh) : Gathered<values,Lanes.gathered(~Context,~map,context,a,b,c,d,e,f,g,_)>
      Gathered{Tile.Tile{map(context,a),map(context,b),map(context,c),map(context,d),map(context,e),map(context,f),map(context,g),map(context,h)},{==}}

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  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=Pair
  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=stelliferous@0.0.2.0/kernel_tile.bend&name=Tile8
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=Read
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend&name=Gathered
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather1
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather2
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather3
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather4
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather5
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather6
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather7
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gathered