def route_separation_decided

bendtorch-core@0.1.0.0 · src/tensor/core_PROOF.bend:227

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

227def route_separation_decided(+depth: Nat, +length: Nat, +index: U32, +other: U32,
228  index_checked: {Storage.index_matches(depth, length, index) == True{} : Bool},
229  other_checked: {Storage.index_matches(depth, length, other) == True{} : Bool},
230  different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool}, same: Bool,
231  decision: {same == Model.same(depth, Refinement.route(depth, index), Refinement.route(depth, other)) : Bool}) -> {same == False{} : Bool}:
232  match same:
233    case False{}:
234      {==}
235    case True{}:
236      Empty.absurd({True{} == False{} : Bool}, natural_clash(U32.to_nat(index), U32.to_nat(other),
237        Equal.trans(Nat, U32.to_nat(index), Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(other),
238          Equal.sym(Nat, Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index), checked_offset(depth, length, index, index_checked)),
239          Equal.trans(Nat, Model.offset(depth, Refinement.route(depth, index)), Model.offset(depth, Refinement.route(depth, other)), U32.to_nat(other),
240            same_path_offset(depth, Refinement.route(depth, index), Refinement.route(depth, other),
241              Equal.sym(Bool, True{}, Model.same(depth, Refinement.route(depth, index), Refinement.route(depth, other)), decision)),
242            checked_offset(depth, length, other, other_checked))), different))