def balanced_as

bendtorch-core@0.1.0.0 · src/tensor/gather_PROOF.bend:232

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic

232def balanced_as(-T: Data, -d: Nat, -a: Array<T>, -b: Array<T>, -same: {a == b : Array<T>}, -valid: Model.Balanced(T, d, b)) ->
233  Generic.Fact<Model.Balanced(T, d, a)>:
234  Generic.Fact{
235    %Equal.sym(Array<T>, a, b, same) : Model.Balanced(T, d, _)
236    valid}