GatherPROOF.looked_value: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend as GatherPROOF
Lines 278-294 of bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&start_line=278&end_line=294

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic

# ... and gives the input word at the entry it read.
def looked_value(+plan: Gather.Plan, +at: Nat, +da: Nat, -A: Array<F32>, pair: Array<U32> & U32, +j: U32,
  -seen: {Refinement.second(U32, pair) == j : U32}, -valid: Model.Balanced(F32, da, A)) ->
  Generic.Fact<{Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.looked(plan, at, A, pair))} ==
    Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(Gather.source(plan, at, U32.to_nat(j))))) : Maybe<&2, F32>}>:
  (index, +found) = pair
  Generic.Fact{
    %seen : {Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.take(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found))))))} ==
      Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(Gather.source(plan, at, U32.to_nat(_))))) : Maybe<&2, F32>}
    Equal.trans(Maybe<&2, F32>, Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.take(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found))))))},
      Some{Refinement.second(F32, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found)))))},
      Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(Gather.source(plan, at, U32.to_nat(found))))),
      Equal.cong(F32, Maybe<&2, F32>, x => Some{x},
        Pair.fst(F32, Array<F32> & Array<U32>, Gather.take(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found)))))),
        Refinement.second(F32, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found))))),
        take_fst(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found)))))),
      Refinement.law_get_refines(F32, da, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found))), valid))}

Uses (24):
  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.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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=Pair.fst
  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.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=law_get_refines
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=route
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=second
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=Plan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=looked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=source
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=take
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=take_fst
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact