Memory.splice_app_right: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as Memory
Lines 501-512 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&start_line=501&end_line=512

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend as LL
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

def splice_app_right(+ws: List<&2, U32>, +n: Nat, +k: Nat, +X: List<&2, U32>, +Y: List<&2, U32>, +hX: {SC.length(U32, X) == n : Nat}) -> {splice(ws, Nat.add(n, k), SC.append(U32, X, Y)) == SC.append(U32, X, splice(ws, k, Y)) : List<&2, U32>}:
  match ws:
    case Nil{}:
      {==}
    case +w <> +rest:
      +hle = L.subst(Nat, z => {Nat.is_le(z, Nat.add(n, k)) == True{} : Bool}, n, SC.length(U32, X), Equal.sym(Nat, SC.length(U32, X), n, hX), N.le_add_right(n, k))
      +ek = Equal.trans(Nat, Nat.sub(Nat.add(n, k), SC.length(U32, X)), Nat.sub(Nat.add(n, k), n), k, Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(n, k), z), SC.length(U32, X), n, hX), N.add_sub_cancel(n, k))
      +Y2 = SC.update(U32, Y, k, w)
      %Equal.sym(List<&2, U32>, SC.update(U32, SC.append(U32, X, Y), Nat.add(n, k), w), SC.append(U32, X, SC.update(U32, Y, Nat.sub(Nat.add(n, k), SC.length(U32, X)), w)), LL.update_append_right(U32, X, Y, Nat.add(n, k), w, hle)) : {splice(rest, Nat.add(Nat.add(n, k), 1n), _) == SC.append(U32, X, splice(rest, Nat.add(k, 1n), Y2)) : List<&2, U32>}
      %Equal.sym(Nat, Nat.sub(Nat.add(n, k), SC.length(U32, X)), k, ek) : {splice(rest, Nat.add(Nat.add(n, k), 1n), SC.append(U32, X, SC.update(U32, Y, _, w))) == SC.append(U32, X, splice(rest, Nat.add(k, 1n), Y2)) : List<&2, U32>}
      %Equal.sym(Nat, Nat.add(Nat.add(n, k), 1n), Nat.add(n, Nat.add(k, 1n)), NA.add_assoc(n, k, 1n)) : {splice(rest, _, SC.append(U32, X, Y2)) == SC.append(U32, X, splice(rest, Nat.add(k, 1n), Y2)) : List<&2, U32>}
      splice_app_right(rest, n, Nat.add(k, 1n), X, Y2, hX)

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=splice
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend&name=update_append_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_sub_cancel
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_add_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=length
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=update