MatmulPROOF.logical_dot_original: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend as MatmulPROOF
Lines 100-124 of bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&start_line=100&end_line=124

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/matmul_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend as DotFold

def logical_dot_original(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>,
  -ra: Core.Tensor<left>, -rb: Core.Tensor<right>, +row: U32, +column: U32, +cursor: Nat, values: List<&2, DotFold.Factors>,
  logical: Laws.LogicalDot(fuel, left, right, ra, rb, row, column, cursor, values),
  -left_kept: @+other: U32 -> {Core.checked_observe(left, ra, other) == Core.checked_observe(left, a, other) : Maybe<&2, F32>},
  -right_kept: @+other: U32 -> {Core.checked_observe(right, rb, other) == Core.checked_observe(right, b, other) : Maybe<&2, F32>}) ->
  Laws.LogicalDot(fuel, left, right, a, b, row, column, cursor, values):
  match fuel values:
    case 0n Nil{}:
      Unit{}
    case 1n+tail DotFold.Factors{+lv, +rv} <> rest:
      Laws.DotStep{exact, lo, ro, remaining} = logical
      Laws.DotStep{exact,
        Equal.trans(Maybe<&2, F32>, Laws.coordinate_observe(left, a, [row, U32.from_nat(cursor)]),
          Laws.coordinate_observe(left, ra, [row, U32.from_nat(cursor)]), Some{lv},
          Equal.sym(Maybe<&2, F32>, Laws.coordinate_observe(left, ra, [row, U32.from_nat(cursor)]),
            Laws.coordinate_observe(left, a, [row, U32.from_nat(cursor)]), coordinate_keeps(left, a, ra, [row, U32.from_nat(cursor)], left_kept)), lo),
        Equal.trans(Maybe<&2, F32>, Laws.coordinate_observe(right, b, [U32.from_nat(cursor), column]),
          Laws.coordinate_observe(right, rb, [U32.from_nat(cursor), column]), Some{rv},
          Equal.sym(Maybe<&2, F32>, Laws.coordinate_observe(right, rb, [U32.from_nat(cursor), column]),
            Laws.coordinate_observe(right, b, [U32.from_nat(cursor), column]), coordinate_keeps(right, b, rb, [U32.from_nat(cursor), column], right_kept)), ro),
        logical_dot_original(tail, left, right, a, b, ra, rb, row, column, 1n+cursor, rest, remaining, left_kept, right_kept)}
    case 0n DotFold.Factors{lv, rv} <> rest:
      Empty.absurd(Laws.LogicalDot(0n, left, right, a, b, row, column, cursor, DotFold.Factors{lv, rv} <> rest), logical)
    case 1n+tail Nil{}:
      Empty.absurd(Laws.LogicalDot(1n+tail, left, right, a, b, row, column, cursor, Nil{}), logical)

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=List
  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=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=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=checked_observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend&name=Factors
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_LAWS.bend&name=DotStep
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_LAWS.bend&name=LogicalDot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_LAWS.bend&name=coordinate_observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&name=coordinate_keeps