def same_path_offset

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

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

179def same_path_offset(+depth: Nat, +left: Model.Path(depth), +right: Model.Path(depth),
180  equal: {Model.same(depth, left, right) == True{} : Bool}) -> {Model.offset(depth, left) == Model.offset(depth, right) : Nat}:
181  match depth:
182    case 0n:
183      {==}
184    case 1n++p:
185      Model.Step{+lb, +lt} = left
186      match lb:
187        case False{}:
188          Model.Step{+rb, +rt} = right
189          match rb:
190            case False{}:
191              same_path_offset(p, lt, rt, equal)
192            case True{}:
193              Empty.absurd({Model.offset(p, lt) == Nat.add(Model.capacity(p), Model.offset(p, rt)) : Nat},
194                Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, equal)))
195        case True{}:
196          Model.Step{+rb, +rt} = right
197          match rb:
198            case False{}:
199              Empty.absurd({Nat.add(Model.capacity(p), Model.offset(p, lt)) == Model.offset(p, rt) : Nat},
200                Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, equal)))
201            case True{}:
202              Equal.cong(Nat, Nat, n => Nat.add(Model.capacity(p), n), Model.offset(p, lt), Model.offset(p, rt),
203                same_path_offset(p, lt, rt, equal))