def nth0_upd_other

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/words32.bend:77

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

77def nth0_upd_other(+xs: List<&2, U32>, +i: Nat, +j: Nat, +v: U32, +h: {Nat.is_eq(i, j) == False{} : Bool}) -> {nth0(SC.update(U32, xs, i, v), j) == nth0(xs, j) : U32}:
78  match xs i j:
79    case Nil{} _ _:
80      {==}
81    case Con{x, r} 0n 0n:
82      Empty.absurd({nth0(SC.update(U32, Con{x, r}, 0n, v), 0n) == nth0(Con{x, r}, 0n) : U32}, L.true_false(h))
83    case Con{x, r} 0n 1n+q:
84      {==}
85    case Con{x, r} 1n+p 0n:
86      {==}
87    case Con{x, r} 1n+p 1n+q:
88      nth0_upd_other(r, p, q, v, h)