def transport_balanced
bendtorch-core@0.1.0.0 · src/tensor/elementwise_parallel_proof.bend:43
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as ElementwiseParallelProof
import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
43def transport_balanced(-d: Nat, -a: Array<F32>, -b: Array<F32>, -same: {a == b : Array<F32>}, -valid: Model.Balanced(F32, d, b)) ->
44 Fact<Model.Balanced(F32, d, a)>:
45 Fact{
46 %Equal.sym(Array<F32>, a, b, same) : Model.Balanced(F32, d, _)
47 valid}