CorePROOF.independent_binary_mapping: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF
Lines 1126-1131 of bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&start_line=1126&end_line=1131

import Base
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/tensor/core_LAWS.bend as Laws

def independent_binary_mapping(+operation: Elementwise.Operation, left: Core.Dynamic, right: Core.Dynamic) ->
  Laws.IndependentBinaryModel<operation, left, right, Elementwise.binary(operation, left, right)>:
  Laws.IndependentBinaryModel{
    {\{Laws.IndependentBinaryModel: mapping => mapping} :
      Laws.IndependentBinaryModel<operation, left, right, Elementwise.binary(operation, left, right)> ->
        Laws.IndependentPlanned(operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right))}(independent_binary_reasoning(operation, left, right))}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_LAWS.bend&name=IndependentBinaryModel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_LAWS.bend&name=IndependentPlanned
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=independent_binary_reasoning
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Operation
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=binary
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=plan_for