Memory.splice_self: 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 523-536 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=523&end_line=536

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

# Storing ws from word i over V, when V ends exactly there: the first i words of V, then ws.
def splice_self(+ws: List<&2, U32>, +i: Nat, +V: List<&2, U32>, +h: {SC.length(U32, V) == Nat.add(i, SC.length(U32, ws)) : Nat}) -> {splice(ws, i, V) == SC.append(U32, SC.take(U32, V, i), ws) : List<&2, U32>}:
  match ws:
    case Nil{}:
      +hv = Equal.trans(Nat, SC.length(U32, V), Nat.add(i, 0n), i, h, N.add_zero(i))
      Equal.trans(List<&2, U32>, V, SC.take(U32, V, i), SC.append(U32, SC.take(U32, V, i), Nil{}), Equal.sym(List<&2, U32>, SC.take(U32, V, i), V, take_all(V, i, hv)), Equal.sym(List<&2, U32>, SC.append(U32, SC.take(U32, V, i), Nil{}), SC.take(U32, V, i), LL.append_nil(U32, SC.take(U32, V, i))))
    case +w <> +rest:
      +V2 = SC.update(U32, V, i, w)
      +hi = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, Nat.add(i, 1n+SC.length(U32, rest)), SC.length(U32, V), Equal.sym(Nat, SC.length(U32, V), Nat.add(i, 1n+SC.length(U32, rest)), h), lt_add_succ(i, SC.length(U32, rest)))
      +h2 = Equal.trans(Nat, SC.length(U32, V2), SC.length(U32, V), Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), LL.length_update(U32, V, i, w), Equal.trans(Nat, SC.length(U32, V), Nat.add(i, 1n+SC.length(U32, rest)), Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), h, Equal.sym(Nat, Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), Nat.add(i, 1n+SC.length(U32, rest)), add_one_assoc(i, SC.length(U32, rest)))))
      %Equal.sym(List<&2, U32>, splice(rest, Nat.add(i, 1n), V2), SC.append(U32, SC.take(U32, V2, Nat.add(i, 1n)), rest), splice_self(rest, Nat.add(i, 1n), V2, h2)) : {_ == SC.append(U32, SC.take(U32, V, i), Con{w, rest}) : List<&2, U32>}
      %Equal.sym(Nat, Nat.add(i, 1n), 1n+i, Equal.trans(Nat, Nat.add(i, 1n), 1n+Nat.add(i, 0n), 1n+i, N.add_succ(i, 0n), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(i, 0n), i, N.add_zero(i)))) : {SC.append(U32, SC.take(U32, V2, _), rest) == SC.append(U32, SC.take(U32, V, i), Con{w, rest}) : List<&2, U32>}
      %Equal.sym(List<&2, U32>, SC.take(U32, V2, 1n+i), SC.append(U32, SC.take(U32, V, i), Con{w, Nil{}}), take_upd(V, i, w, hi)) : {SC.append(U32, _, rest) == SC.append(U32, SC.take(U32, V, i), Con{w, rest}) : List<&2, U32>}
      LL.append_assoc(U32, SC.take(U32, V, i), Con{w, Nil{}}, rest)

Uses (24):
  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_lt
  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=add_one_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=lt_add_succ
  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/crypto/argon2/memory.bend&name=take_all
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=take_upd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend&name=append_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend&name=append_nil
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend&name=length_update
  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_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_zero
  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=take
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=update