CorePROOF.route_separation_decided: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF
Lines 227-242 of bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&start_line=227&end_line=242

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

def route_separation_decided(+depth: Nat, +length: Nat, +index: U32, +other: U32,
  index_checked: {Storage.index_matches(depth, length, index) == True{} : Bool},
  other_checked: {Storage.index_matches(depth, length, other) == True{} : Bool},
  different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool}, same: Bool,
  decision: {same == Model.same(depth, Refinement.route(depth, index), Refinement.route(depth, other)) : Bool}) -> {same == False{} : Bool}:
  match same:
    case False{}:
      {==}
    case True{}:
      Empty.absurd({True{} == False{} : Bool}, natural_clash(U32.to_nat(index), U32.to_nat(other),
        Equal.trans(Nat, U32.to_nat(index), Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(other),
          Equal.sym(Nat, Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index), checked_offset(depth, length, index, index_checked)),
          Equal.trans(Nat, Model.offset(depth, Refinement.route(depth, index)), Model.offset(depth, Refinement.route(depth, other)), U32.to_nat(other),
            same_path_offset(depth, Refinement.route(depth, index), Refinement.route(depth, other),
              Equal.sym(Bool, True{}, Model.same(depth, Refinement.route(depth, index), Refinement.route(depth, other)), decision)),
            checked_offset(depth, length, other, other_checked))), different))

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=index_matches
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=same
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=route
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=checked_offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=natural_clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=same_path_offset