def drop_append_add

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/memory.bend:354

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/nat.bend as N

354def drop_append_add(+xs: List<&2, U32>, +ys: List<&2, U32>, +n: Nat, +k: Nat, +h: {SC.length(U32, xs) == n : Nat}) -> {SC.drop(U32, SC.append(U32, xs, ys), Nat.add(n, k)) == SC.drop(U32, ys, k) : List<&2, U32>}:
355  match xs n:
356    case Nil{} 0n:
357      {==}
358    case Nil{} 1n+p:
359      Empty.absurd({SC.drop(U32, ys, Nat.add(1n+p, k)) == SC.drop(U32, ys, k) : List<&2, U32>}, N.zero_succ(p, h))
360    case Con{x, t} 0n:
361      Empty.absurd({SC.drop(U32, SC.append(U32, Con{x, t}, ys), k) == SC.drop(U32, ys, k) : List<&2, U32>}, N.succ_zero(SC.length(U32, t), h))
362    case Con{x, +t} 1n+ +p:
363      drop_append_add(t, ys, p, k, N.succ_inj(SC.length(U32, t), p, h))