def route_allowed

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:356

import Base
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as Mapping

356def route_allowed(+depth: Nat, +length: Nat, +index: U32,
357  +matched: {Storage.index_matches(depth, length, index) == True{} : Bool}) ->
358  {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}:
359  +offset = Model.offset(depth, Refinement.route(depth, index))
360  %Lifecycle.natural_equal(offset, U32.to_nat(index),
361    Mapping.and_left(Nat.is_eq(offset, U32.to_nat(index)), Nat.is_lt(offset, length),
362      Equal.sym(Bool, Storage.index_matches(depth, length, index), True{}, matched))) :
363    {Nat.is_lt(_, length) == True{} : Bool}
364  Equal.sym(Bool, True{}, Nat.is_lt(offset, length),
365    Mapping.and_right(Nat.is_eq(offset, U32.to_nat(index)), Nat.is_lt(offset, length),
366      Equal.sym(Bool, Storage.index_matches(depth, length, index), True{}, matched)))