law checked_route_separation

bendtorch-core@0.1.0.0 · src/tensor/core_LAWS.bend:183

import Base
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

183law checked_route_separation:
184  for +depth: Nat
185  for +length: Nat
186  for +index: U32
187  for +other: U32
188  for index_checked: {Storage.index_matches(depth, length, index) == True{} : Bool}
189  for other_checked: {Storage.index_matches(depth, length, other) == True{} : Bool}
190  for different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool}
191  {Model.same(depth, Refinement.route(depth, index), Refinement.route(depth, other)) == False{} : Bool}