CorePROOF.same_path_offset: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF
Lines 179-203 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=179&end_line=203

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

def same_path_offset(+depth: Nat, +left: Model.Path(depth), +right: Model.Path(depth),
  equal: {Model.same(depth, left, right) == True{} : Bool}) -> {Model.offset(depth, left) == Model.offset(depth, right) : Nat}:
  match depth:
    case 0n:
      {==}
    case 1n++p:
      Model.Step{+lb, +lt} = left
      match lb:
        case False{}:
          Model.Step{+rb, +rt} = right
          match rb:
            case False{}:
              same_path_offset(p, lt, rt, equal)
            case True{}:
              Empty.absurd({Model.offset(p, lt) == Nat.add(Model.capacity(p), Model.offset(p, rt)) : Nat},
                Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, equal)))
        case True{}:
          Model.Step{+rb, +rt} = right
          match rb:
            case False{}:
              Empty.absurd({Nat.add(Model.capacity(p), Model.offset(p, lt)) == Model.offset(p, rt) : Nat},
                Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, equal)))
            case True{}:
              Equal.cong(Nat, Nat, n => Nat.add(Model.capacity(p), n), Model.offset(p, lt), Model.offset(p, rt),
                same_path_offset(p, lt, rt, equal))

Uses (12):
  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.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Path
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=capacity
  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/tensor/lifecycle.bend&name=false_true