HvdH machine lemma GL.loop12 (Generic element-stream loops (Gaussian list primitives, part 1))

The following holds (Lean statement, in the scope of module NLogN.HGl1):

theorem NLogN.GL.loop12 (M : MulSpec) (b : RM) (A B1 B2 c dA : Fin HS) (e : α → List Item)
    (d1 : β → List Item) (d2 : β2 → List Item) (f1 : α → β) (f2 : α → β2) (s : IState HS)
    (L : List α) (R : List Item) (C N Bc : ℕ) (n : Ex HS)
    (hd : [A, dA, B1, B2, c].Nodup) (h1 : s.G A = L.flatMap e ++ R) (hl : L.length = N)
    (hn : n.eval s = N) (hw : c ∉ b.writes)
    (hb : ∀ x ∈ L, ∀ (t : IState HS) (r o1 o2 : List Item),
      (∀ j, j ∉ [A, dA, B1, B2, c] → t.G j = s.G j) →
      t.G A = e x ++ r → t.G B1 = o1 ++ s.G B1 → t.G B2 = o2 ++ s.G B2 →
      b.run t = ((t.upd A r).upd B1 ((d1 (f1 x)).reverse ++ t.G B1)).upd B2
        ((d2 (f2 x)).reverse ++ t.G B2) ∧ b.ok M t ∧ b.cost M t ≤ C)
    (hc56 : c.val < 56) (hnc : n.Clean) (hno : n.ok s) (hnl : n.Lin) (hnB : n.Bnd s Bc) :
    (RM.rep c n b).run s = ((s.upd A R).upd B1 (((L.map f1).flatMap d1).reverse ++ s.G B1)).upd
      B2 (((L.map f2).flatMap d2).reverse ++ s.G B2) ∧
    (RM.rep c n b).ok M s ∧
    (RM.rep c n b).cost M s ≤ (n.size + 1) * 2000 * (Bc + 2) +
      N * (C + 8000 * (Bc + 2) + 30) + 32

Context. The lemma belongs to the part Generic element-stream loops (Gaussian list primitives, part 1): RM.rep c n b where the body b pops one element from each of the input stacks A1, A2 and pushes the (reversed) encodings of two results onto B1, B2. After N rounds the outputs are the reversed flattened encodings of the zipWith lists. The wrappers loop11, loop21, loop12 are the one/two-input, one/two-output special cases.

Formalization Note. This is a lemma of the Lean development NLogN, a multitape-Turing-machine implementation of the Harvey–van der Hoeven $O(n\log n)$ integer multiplication algorithm, used in the proof of NLogN.FIN.theorem_1_1_nlogn : IntMul.MulTimeBound fun n => n * Real.log n. All names refer to the definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8 (namespace NLogN), built on the platform model Def_IntMul_MultitapeModel and the published reference Def_IntMul_HvdH_MachineRef. The machine layer: IState HS is a state of 64 item stacks; RM programs have a semantics p.run s, a definedness predicate p.ok M s and a cost p.cost M s relative to a multiplication spec M : MulSpec; zsz z is the bit length of $|z|$.