CorePROOF.independent_binary_reasoning: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF
Lines 1116-1124 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=1116&end_line=1124

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_reasoning(+operation: Elementwise.Operation, -left: Core.Dynamic, -right: Core.Dynamic) ->
  Laws.IndependentBinaryModel<operation, left, right, Elementwise.binary(operation, left, right)>:
  Laws.IndependentBinaryModel{
    {\{Elementwise.BinaryModel: mapping =>
      {\{IndependentPlannedModel: independent => independent} :
        IndependentPlannedModel<operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right)> ->
          Laws.IndependentPlanned(operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right))}(independent_planned_pair(operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right), mapping))
    } : Elementwise.BinaryModel<operation, left, right, Elementwise.binary(operation, left, right)> ->
      Laws.IndependentPlanned(operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right))}(successful_binary_mapping(operation, left, right))}

Uses (10):
  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=IndependentPlannedModel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=independent_planned_pair
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=successful_binary_mapping
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=BinaryModel
  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