cleanF_sp (KFUU §8e: clearing registers and lists)

The following holds (Lean statement, in the scope of module Solutions.KFUUClean):

theorem NLogN.KFUU.cleanF_sp (s : IState HS) (F : Fin HS → List ℤ) (d B : ℕ) (L1 L2 L3 L4 : List ℤ)
    (h1 : F pSR = L1) (h2 : F pSK = L2) (h3 : F pTK = L3) (h4 : F pTR = L4)
    (l1 : L1.length = d + 1) (l2 : L2.length = d + 1) (l3 : L3.length = d + 1)
    (l4 : L4.length = d + 1) (b1 : Bnd B L1) (b2 : Bnd B L2) (b3 : Bnd B L3) (b4 : Bnd B L4)
    (hD : F oD = [(d : ℤ)]) (hC : F NLogN.KFUU.cL = []) (a b : ℤ) (hN : F nR = [a, b]) (za : zsz a ≤ B)
    (zb : zsz b ≤ B) (hB : zsz ((d + 1 : ℕ) : ℤ) ≤ B) (hB1 : 1 ≤ B)
    (hP : ∀ i ∈ [rW, NLogN.KFUU.rU, oPi, rU2, rCZ, oI, oBv], ∃ a, F i = [a] ∧ zsz a ≤ B) :
    Sp cleanF (NLogN.KIL.encK s F) (NLogN.KIL.encK s (clrF (Function.update (Function.update (Function.update
      (Function.update (Function.update F pSR []) pSK []) pTK []) pTR []) nR [b]) NLogN.KFUU.Lp))
      (cClean d B)

Context. The lemma belongs to the part KFUU §8e: clearing registers and lists.

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.