KernelTileWitness.pair: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/kernel_tile_witness.bend as KernelTileWitness
Lines 6-19 of stelliferous@0.0.2.0/proofs/kernel_tile_witness.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/kernel_tile_witness.bend&start_line=6&end_line=19

import Base
import stelliferous@0.0.2.0/kernel_block.bend as Block
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

# Pair composition consumes already established observations. Context and
# values may be erased, so a cached head need not become a live proof field.
def pair(~State: Type,~Context: Data,~Element: Data,~read: State -> Context -> Nat -> State & Element,~stride: Nat,
  -state: State,-context: Context,+index: Nat,
  first: TraversalWitness.Sample<State,Element,state,read(state,context,index)>,
  second: TraversalWitness.Sample<State,Element,state,read(state,context,Nat.add(index,stride))>) ->
  TraversalWitness.Sample<State,Block.Twin<Element>,state,Block.read_pair(~State,~Context,~Element,~read,~stride,state,context,index)>:
  TraversalWitness.Sample{left,left_equation} = first
  TraversalWitness.Sample{right,right_equation} = second
  %Equal.sym(State & Element,read(state,context,index),(state,left),left_equation) :
    TraversalWitness.Sample<State,Block.Twin<Element>,state,Block.read_second(~State,~Context,~Element,~Nat,~read,_,context,Nat.add(index,stride))>
  %Equal.sym(State & Element,read(state,context,Nat.add(index,stride)),(state,right),right_equation) :
    TraversalWitness.Sample<State,Block.Twin<Element>,state,Block.finish_pair(~State,~Element,left,_)>
  TraversalWitness.Sample{Block.Twin{left,right},{==}}

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=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_block.bend&name=Twin
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_block.bend&name=finish_pair
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_block.bend&name=read_pair
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_block.bend&name=read_second
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=Sample