def same_eq

bendtorch-core@0.1.0.0 · src/storage/api.bend:224

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

224def same_eq(+d: Nat, +p: Model.Path(d), +q: Model.Path(d)) ->
225  {Nat.is_eq(Model.offset(d, p), Model.offset(d, q)) == Model.same(d, p, q) : Bool}:
226  match d:
227    case 0n:
228      {==}
229    case 1n+r:
230      Model.Step{+pb, +pr} = p
231      match pb:
232        case False{}:
233          Model.Step{+qb, +qr} = q
234          match qb:
235            case False{}:
236              same_eq(r, pr, qr)
237            case True{}:
238              Equal.sym(Bool, False{}, Nat.is_eq(Model.offset(r, pr), Nat.add(Model.capacity(r), Model.offset(r, qr))),
239                ne_low(Model.offset(r, pr), Model.capacity(r), Model.offset(r, qr), offset_lt(r, pr)))
240        case True{}:
241          Model.Step{+qb, +qr} = q
242          match qb:
243            case False{}:
244              Equal.sym(Bool, False{}, Nat.is_eq(Nat.add(Model.capacity(r), Model.offset(r, pr)), Model.offset(r, qr)),
245                ne_high(Model.offset(r, qr), Model.capacity(r), Model.offset(r, pr), offset_lt(r, qr)))
246            case True{}:
247              %eq_add_cancel(Model.capacity(r), Model.offset(r, pr), Model.offset(r, qr)) : {_ == Model.same(r, pr, qr) : Bool}
248              same_eq(r, pr, qr)