def independent_binary_reasoning

bendtorch-core@0.1.0.0 · src/tensor/core_PROOF.bend:1116

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

1116def independent_binary_reasoning(+operation: Elementwise.Operation, -left: Core.Dynamic, -right: Core.Dynamic) ->
1117  Laws.IndependentBinaryModel<operation, left, right, Elementwise.binary(operation, left, right)>:
1118  Laws.IndependentBinaryModel{
1119    {\{Elementwise.BinaryModel: mapping =>
1120      {\{IndependentPlannedModel: independent => independent} :
1121        IndependentPlannedModel<operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right)> ->
1122          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))
1123    } : Elementwise.BinaryModel<operation, left, right, Elementwise.binary(operation, left, right)> ->
1124      Laws.IndependentPlanned(operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right))}(successful_binary_mapping(operation, left, right))}