Fibonacci Heap: Static-Array Word-RAM Program and State Representation

This file defines the uniform Basis.exact Word-RAM implementation (code : PQCode .exact rFib) of a static-array Fibonacci heap on n handles (space n = 9 * n + 1 words at [base, base + 9 * n + 1)), together with its concrete state projection (RawState.ofData), representation invariant (FibInv), potential function (potential), per-operation amortized time bounds, and memory/register framing lemmas.

Memory layout ([base, base + 9 * n + 1))

• [base + 0 * n, base + 1 * n): key[0..n-1]
• [base + 1 * n, base + 2 * n): par[0..n-1] (0 = root, p + 1 = parent p)
• [base + 2 * n, base + 3 * n): child[0..n-1] (0 = leaf, c + 1 = head child c)
• [base + 3 * n, base + 4 * n): left[0..n-1] (circular sibling list predecessor)
• [base + 4 * n, base + 5 * n): right[0..n-1] (circular sibling list successor)
• [base + 5 * n, base + 6 * n): deg[0..n-1] (number of children)
• [base + 6 * n, base + 7 * n): mark[0..n-1] (0 or 1, child-loss mark)
• [base + 7 * n, base + 8 * n): inHeap[0..n-1] (0 = absent, 1 = present)
• [base + 8 * n, base + 9 * n + 1): cons[0..n] (degree-consolidation table, 0 = empty)

Main definitions

• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.rFib, space, potential, charge: register count (42), memory footprint (9 * n + 1), integer potential, and per-operation amortized charges.
• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.code, dispatchCode: structured PQCode .exact rFib bundle and unified operation dispatcher.
• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FibInv: full machine-state invariant over Data rFib.

Main results

• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FibInv.supported, potential_supported: register and memory framing for SubroutineDS.

References

• M. L. Fredman and R. E. Tarjan, Fibonacci heaps and their uses in improved network optimization algorithms
• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Chapter 19

Register file (rFib = 42) and footprint size

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.rFib : ℕ

Total register count of the standalone/subroutine Fibonacci heap machine.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.nReg : Fin rFib

Persistent register holding handle-universe size n.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.frontierReg : Fin rFib

Persistent frontier register (base before allocSpan, base + space n after).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.baseReg : Fin rFib

Persistent base address of key[0..n-1] (base).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.parBase : Fin rFib

Persistent base address of par[0..n-1] (base + n).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.childBase : Fin rFib

Persistent base address of child[0..n-1] (base + 2 * n).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.leftBase : Fin rFib

Persistent base address of left[0..n-1] (base + 3 * n).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.rightBase : Fin rFib

Persistent base address of right[0..n-1] (base + 4 * n).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.degBase : Fin rFib

Persistent base address of deg[0..n-1] (base + 5 * n).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.markBase : Fin rFib

Persistent base address of mark[0..n-1] (base + 6 * n).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.inBase : Fin rFib

Persistent base address of inHeap[0..n-1] (base + 7 * n).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.consBase : Fin rFib

Persistent base address of cons[0..n] (base + 8 * n).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.zeroP : Fin rFib

Persistent constant register 0.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.oneP : Fin rFib

Persistent constant register 1.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.minRootReg : Fin rFib

Persistent nullable minimum-root pointer (0 = empty, m + 1 = some m).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.numRootsReg : Fin rFib

Persistent root-list length counter (numRoots).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.numMarkedReg : Fin rFib

Persistent marked-node counter (numMarked).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.szReg : Fin rFib

Persistent live-element count (sz).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.tag2 : Fin rFib

Caller high tag bit (≠ 0 selects extractMin).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.tag1 : Fin rFib

Caller middle tag bit.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.tag0 : Fin rFib

Caller low tag bit.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.argV : Fin rFib

Caller handle argument register (v.val).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.argK : Fin rFib

Caller key argument register (k).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.outFlag : Fin rFib

Output flag register (output = outFlag).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.outV : Fin rFib

Output handle register (u.val for non-empty extractMin).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.outK : Fin rFib

Output key register (k for present getKey and non-empty extractMin).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.curReg : Fin rFib

Scratch pointer register for generic SubroutineCode.zeroFillCode.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.zeroReg : Fin rFib

Scratch zero register for generic SubroutineCode.zeroFillCode.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.oneReg : Fin rFib

Scratch one register for generic SubroutineCode.zeroFillCode.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.zReg : Fin rFib

Outer scratch register: extracted vertex z or cascading-cut target cur.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.pReg : Fin rFib

Outer scratch register: parent p in decreaseKey or rStart in extractMin.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.remReg : Fin rFib

Outer loop counter (rem) in extractMin Phase A.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.iterCur : Fin rFib

Outer current-node register (iterCur) or cascading-cut loop guard.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.iterNxt : Fin rFib

Outer saved-next-node register (iterNxt) in extractMin Phase A.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.maxDegReg : Fin rFib

Maximum degree tracker (maxDeg / limit) in extractMin.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.curDReg : Fin rFib

Degree index (d / curD) in scatterRootCode and extractMin Phase B.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.s0 : Fin rFib

Inner helper scratch register 0 (addresses).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.s1 : Fin rFib

Inner helper scratch register 1.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.s2 : Fin rFib

Inner helper scratch register 2.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.s3 : Fin rFib

Inner helper scratch register 3.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.s4 : Fin rFib

Inner helper scratch register 4.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.s5 : Fin rFib

Inner helper scratch register 5.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.s6 : Fin rFib

Inner helper scratch register 6.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.inputReg (i : Fin rFib) : Bool

Persistent registers are 0..16 (false); caller/scratch registers are 17..41 (true).

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.space (n : ℕ) : ℕ

Static memory footprint on n handles: 9 * n + 1 words.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.space_lower (n : ℕ) : n + 1 ≤ space n

Structured Basis.exact Fibonacci-heap subprograms

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.allocSpan : WordRAM.Code WordRAM.Basis.exact rFib

Advance frontierReg from base to base + 9 * n + 1 using only + nReg and + #1, avoiding constants > 1 so small word widths (w ≥ 1 when n = 0) never fault.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.initSetup : WordRAM.Code WordRAM.Basis.exact rFib

Initialize array-base pointers and zero scalar heap counters (O(1) steps).

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.prioLTFlag (uReg kuReg vReg kvReg flagReg : Fin rFib) : WordRAM.Code WordRAM.Basis.exact rFib

Set flagReg ← 1 if (uReg, kuReg) strictly precedes (vReg, kvReg) lexicographically (ku < kv ∨ (ku = kv ∧ u < v)), and flagReg ← 0 otherwise. Writes only flagReg.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.insertIntoNonEmptyList (hReg uReg : Fin rFib) : WordRAM.Code WordRAM.Basis.exact rFib

Splice fresh vertex uReg immediately after hReg in a non-empty circular doubly-linked list (left[u] := h; left[right[h]] := u; right[u] := right[h]; right[h] := u). Writes only s0, s2.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.addRootAndUpdateMin (uReg : Fin rFib) : WordRAM.Code WordRAM.Basis.exact rFib

Insert root uReg into the root circular list, update minRootReg under IndexedMinPQ.PrioLT, and increment numRootsReg. Writes only s0..s5, minRootReg, numRootsReg.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.isEmptyCode : WordRAM.Code WordRAM.Basis.exact rFib

isEmpty: sets outFlag ← 1 if minRootReg = 0, else 0.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.getKeyCode : WordRAM.Code WordRAM.Basis.exact rFib

getKey v: loads outFlag ← inHeap[argV] and, if present, outK ← key[argV].

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.insertCode : WordRAM.Code WordRAM.Basis.exact rFib

insert v k: initializes singleton root argV with key argK, splices into root list, and increments szReg.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.cutNodeCode : WordRAM.Code WordRAM.Basis.exact rFib

Cut child zReg from parent pReg (par[zReg] = pReg + 1, minRootReg ≥ 1), splicing zReg into the root circular list, clearing par[zReg] and mark[zReg] (updating numMarkedReg if needed), and incrementing numRootsReg. Writes only s0..s4, numMarkedReg, numRootsReg.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.evalCascGuard : WordRAM.Code WordRAM.Basis.exact rFib

Evaluate cascading-cut guard iterCur ← 1 iff par[zReg] ≠ 0 ∧ mark[zReg] ≠ 0, else 0.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.decreaseKeyCode : WordRAM.Code WordRAM.Basis.exact rFib

decreaseKey v k: lowers key[argV] ← argK, cuts argV and runs cascading cuts if parent order under IndexedMinPQ.PrioLT is violated, and updates minRootReg.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.scatterRootCode : WordRAM.Code WordRAM.Basis.exact rFib

Scatter root iterCur into cons, linking equal-degree roots under IndexedMinPQ.PrioLT until reaching an empty slot and updating maxDegReg. Writes only s0..s6, curDReg, maxDegReg.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.extractMinCode : WordRAM.Code WordRAM.Basis.exact rFib

extractMin: returns 0 when empty, or removes z = minRootReg - 1, scatters z's children and the numRoots - 1 remaining roots into cons, and scans 0 .. maxDeg to rebuild the root circular list and minRootReg while restoring cons = 0 in O(log n) steps.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.dispatchCode : WordRAM.Code WordRAM.Basis.exact rFib

Unified dispatcher over 1-bit tags (tag2, tag1, tag0).

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.code : PQCode WordRAM.Basis.exact rFib

Uniform PQCode .exact rFib bundle for the static-array Fibonacci heap.

Concrete state projection, representation invariant, and amortized bounds

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.RawState.ofData (n base : ℕ) (x : WordRAM.Data rFib) : RawState n

Project Data rFib at (n, base) to a logical RawState n.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.BaseRegs (n base : ℕ) (x : WordRAM.Data rFib) : Prop

Persistent base-address and constant registers 0..12 hold their initialized values.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FibInv (n K_max w base : ℕ) (s : Lean.IndexedMinPQ.State n) (x : WordRAM.Data rFib) : Prop

Full Word-RAM representation invariant for FibonacciHeap at (n, K_max, w, base).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.unitCredit : ℕ

Amortized credit per root (80 instructions; marked nodes carry 2 * unitCredit = 160).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.slotCredit : ℕ

Internal consolidation-slot credit (50 instructions per occupied degree slot).

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.potential (x : WordRAM.Data rFib) : ℕ

Concrete integer potential 80 * (numRoots + 2 * numMarked).

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.tInit (_n : ℕ) : ℕ

Fresh-initialization instruction bound (allocSpan 12 + initSetup 14 = 26).

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.tEmpty (_n : ℕ) : ℕ

Instruction bound for isEmpty (including dispatch).

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.tGet (_n : ℕ) : ℕ

Instruction bound for getKey (including dispatch).

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.tIns (_n : ℕ) : ℕ

Amortized instruction bound for insert (including dispatch and +80 root potential).

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.tDec (_n : ℕ) : ℕ

Amortized instruction bound for decreaseKey (including dispatch and cascading cuts).

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.tExt (n : ℕ) : ℕ

Amortized instruction bound for extractMin (O(log n)).

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.charge (n : ℕ) (_s : Lean.IndexedMinPQ.State n) : Lean.IndexedMinPQ.Op n → ℕ

Per-operation amortized instruction charge for FibonacciHeap.

Exact-ALU step rules, footprint framing, and RawState.ofData update lemmas

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.execWithin_exactAdd {w : ℕ} {x : WordRAM.Data rFib} {d i j : Fin rFib} (hfit : WordRAM.Fits w (x.regs i + x.regs j)) : WordRAM.ExecWithin w (WordRAM.Code.op (WordRAM.Op.exactBin WordRAM.BinOp.add d i j)) x (x.set d (x.regs i + x.regs j)) 1

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.execWithin_exactSub {w : ℕ} {x : WordRAM.Data rFib} {d i j : Fin rFib} (hle : x.regs j ≤ x.regs i) (hfit : WordRAM.Fits w (x.regs i - x.regs j)) : WordRAM.ExecWithin w (WordRAM.Code.op (WordRAM.Op.exactBin WordRAM.BinOp.sub d i j)) x (x.set d (x.regs i - x.regs j)) 1

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.modifies_block_trans {b : WordRAM.Block} {m₁ m₂ m₃ : ℕ → ℕ} (h₁ : WordRAM.Modifies b.footprint m₁ m₂) (h₂ : WordRAM.Modifies b.footprint m₂ m₃) : WordRAM.Modifies b.footprint m₁ m₃

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.BaseRegs.fits_stop {n base w : ℕ} {x : WordRAM.Data rFib} (hb : WordRAM.Data.Bounded w x) (hbr : BaseRegs n base x) : WordRAM.Fits w (base + space n)

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.BaseRegs.set_non_base {n base : ℕ} {x : WordRAM.Data rFib} (hbr : BaseRegs n base x) {d : Fin rFib} (hd : 13 ≤ ↑d) (v : ℕ) : BaseRegs n base (x.set d v)

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.BaseRegs.write_eq {n base : ℕ} {x : WordRAM.Data rFib} (hbr : BaseRegs n base x) (a v : ℕ) : BaseRegs n base (x.write a v)

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.BaseRegs.preserved {n base w T : ℕ} {c : WordRAM.Code WordRAM.Basis.exact rFib} {x y : WordRAM.Data rFib} (he : WordRAM.ExecWithin w c x y T) (hbr : BaseRegs n base x) (hp0 : WordRAM.Code.Preserves nReg c) (hp1 : WordRAM.Code.Preserves frontierReg c) (hp2 : WordRAM.Code.Preserves baseReg c) (hp3 : WordRAM.Code.Preserves parBase c) (hp4 : WordRAM.Code.Preserves childBase c) (hp5 : WordRAM.Code.Preserves leftBase c) (hp6 : WordRAM.Code.Preserves rightBase c) (hp7 : WordRAM.Code.Preserves degBase c) (hp8 : WordRAM.Code.Preserves markBase c) (hp9 : WordRAM.Code.Preserves inBase c) (hp10 : WordRAM.Code.Preserves consBase c) (hp11 : WordRAM.Code.Preserves zeroP c) (hp12 : WordRAM.Code.Preserves oneP c) : BaseRegs n base y

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ofData_set_scratch {n base : ℕ} (x : WordRAM.Data rFib) {d : Fin rFib} (hd : 17 ≤ ↑d) (v : ℕ) : RawState.ofData n base (x.set d v) = RawState.ofData n base x

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ofData_set_minRoot {n base : ℕ} (x : WordRAM.Data rFib) (v : ℕ) : RawState.ofData n base (x.set minRootReg v) = have __src := RawState.ofData n base x; { key := __src.key, par := __src.par, child := __src.child, left := __src.left, right := __src.right, deg := __src.deg, mark := __src.mark, inHeap := __src.inHeap, cons := __src.cons, minRoot := v, numRoots := __src.numRoots, numMarked := __src.numMarked, sz := __src.sz }

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ofData_set_numRoots {n base : ℕ} (x : WordRAM.Data rFib) (v : ℕ) : RawState.ofData n base (x.set numRootsReg v) = have __src := RawState.ofData n base x; { key := __src.key, par := __src.par, child := __src.child, left := __src.left, right := __src.right, deg := __src.deg, mark := __src.mark, inHeap := __src.inHeap, cons := __src.cons, minRoot := __src.minRoot, numRoots := v, numMarked := __src.numMarked, sz := __src.sz }

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ofData_set_numMarked {n base : ℕ} (x : WordRAM.Data rFib) (v : ℕ) : RawState.ofData n base (x.set numMarkedReg v) = have __src := RawState.ofData n base x; { key := __src.key, par := __src.par, child := __src.child, left := __src.left, right := __src.right, deg := __src.deg, mark := __src.mark, inHeap := __src.inHeap, cons := __src.cons, minRoot := __src.minRoot, numRoots := __src.numRoots, numMarked := v, sz := __src.sz }

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ofData_set_sz {n base : ℕ} (x : WordRAM.Data rFib) (v : ℕ) : RawState.ofData n base (x.set szReg v) = have __src := RawState.ofData n base x; { key := __src.key, par := __src.par, child := __src.child, left := __src.left, right := __src.right, deg := __src.deg, mark := __src.mark, inHeap := __src.inHeap, cons := __src.cons, minRoot := __src.minRoot, numRoots := __src.numRoots, numMarked := __src.numMarked, sz := v }

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ofData_write_key {n base : ℕ} (x : WordRAM.Data rFib) (v : Fin n) (val : ℕ) : RawState.ofData n base (x.write (base + ↑v) val) = have __src := RawState.ofData n base x; { key := Function.update (RawState.ofData n base x).key v val, par := __src.par, child := __src.child, left := __src.left, right := __src.right, deg := __src.deg, mark := __src.mark, inHeap := __src.inHeap, cons := __src.cons, minRoot := __src.minRoot, numRoots := __src.numRoots, numMarked := __src.numMarked, sz := __src.sz }

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ofData_write_par {n base : ℕ} (x : WordRAM.Data rFib) (v : Fin n) (val : ℕ) : RawState.ofData n base (x.write (base + n + ↑v) val) = have __src := RawState.ofData n base x; { key := __src.key, par := Function.update (RawState.ofData n base x).par v val, child := __src.child, left := __src.left, right := __src.right, deg := __src.deg, mark := __src.mark, inHeap := __src.inHeap, cons := __src.cons, minRoot := __src.minRoot, numRoots := __src.numRoots, numMarked := __src.numMarked, sz := __src.sz }

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ofData_write_child {n base : ℕ} (x : WordRAM.Data rFib) (v : Fin n) (val : ℕ) : RawState.ofData n base (x.write (base + 2 * n + ↑v) val) = have __src := RawState.ofData n base x; { key := __src.key, par := __src.par, child := Function.update (RawState.ofData n base x).child v val, left := __src.left, right := __src.right, deg := __src.deg, mark := __src.mark, inHeap := __src.inHeap, cons := __src.cons, minRoot := __src.minRoot, numRoots := __src.numRoots, numMarked := __src.numMarked, sz := __src.sz }

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ofData_write_left {n base : ℕ} (x : WordRAM.Data rFib) (v : Fin n) (val : ℕ) : RawState.ofData n base (x.write (base + 3 * n + ↑v) val) = have __src := RawState.ofData n base x; { key := __src.key, par := __src.par, child := __src.child, left := Function.update (RawState.ofData n base x).left v val, right := __src.right, deg := __src.deg, mark := __src.mark, inHeap := __src.inHeap, cons := __src.cons, minRoot := __src.minRoot, numRoots := __src.numRoots, numMarked := __src.numMarked, sz := __src.sz }

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ofData_write_right {n base : ℕ} (x : WordRAM.Data rFib) (v : Fin n) (val : ℕ) : RawState.ofData n base (x.write (base + 4 * n + ↑v) val) = have __src := RawState.ofData n base x; { key := __src.key, par := __src.par, child := __src.child, left := __src.left, right := Function.update (RawState.ofData n base x).right v val, deg := __src.deg, mark := __src.mark, inHeap := __src.inHeap, cons := __src.cons, minRoot := __src.minRoot, numRoots := __src.numRoots, numMarked := __src.numMarked, sz := __src.sz }

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ofData_write_deg {n base : ℕ} (x : WordRAM.Data rFib) (v : Fin n) (val : ℕ) : RawState.ofData n base (x.write (base + 5 * n + ↑v) val) = have __src := RawState.ofData n base x; { key := __src.key, par := __src.par, child := __src.child, left := __src.left, right := __src.right, deg := Function.update (RawState.ofData n base x).deg v val, mark := __src.mark, inHeap := __src.inHeap, cons := __src.cons, minRoot := __src.minRoot, numRoots := __src.numRoots, numMarked := __src.numMarked, sz := __src.sz }

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ofData_write_mark {n base : ℕ} (x : WordRAM.Data rFib) (v : Fin n) (val : ℕ) : RawState.ofData n base (x.write (base + 6 * n + ↑v) val) = have __src := RawState.ofData n base x; { key := __src.key, par := __src.par, child := __src.child, left := __src.left, right := __src.right, deg := __src.deg, mark := Function.update (RawState.ofData n base x).mark v val, inHeap := __src.inHeap, cons := __src.cons, minRoot := __src.minRoot, numRoots := __src.numRoots, numMarked := __src.numMarked, sz := __src.sz }

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ofData_write_inHeap {n base : ℕ} (x : WordRAM.Data rFib) (v : Fin n) (val : ℕ) : RawState.ofData n base (x.write (base + 7 * n + ↑v) val) = have __src := RawState.ofData n base x; { key := __src.key, par := __src.par, child := __src.child, left := __src.left, right := __src.right, deg := __src.deg, mark := __src.mark, inHeap := Function.update (RawState.ofData n base x).inHeap v val, cons := __src.cons, minRoot := __src.minRoot, numRoots := __src.numRoots, numMarked := __src.numMarked, sz := __src.sz }

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ofData_write_cons {n base d : ℕ} (hd : d ≤ n) (x : WordRAM.Data rFib) (val : ℕ) : RawState.ofData n base (x.write (base + 8 * n + d) val) = have __src := RawState.ofData n base x; { key := __src.key, par := __src.par, child := __src.child, left := __src.left, right := __src.right, deg := __src.deg, mark := __src.mark, inHeap := __src.inHeap, cons := Function.update (RawState.ofData n base x).cons d val, minRoot := __src.minRoot, numRoots := __src.numRoots, numMarked := __src.numMarked, sz := __src.sz }

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ofData_supported {n base : ℕ} {x x' : WordRAM.Data rFib} (hreg : ∀ (i : Fin rFib), inputReg i = false → x'.regs i = x.regs i) (hmem : ∀ a ∈ { base := base, length := space n }.footprint, x'.mem a = x.mem a) : RawState.ofData n base x' = RawState.ofData n base x

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FibInv.supported {n K_max w base : ℕ} {s : Lean.IndexedMinPQ.State n} {x x' : WordRAM.Data rFib} (hreg : ∀ (i : Fin rFib), inputReg i = false → x'.regs i = x.regs i) (hmem : ∀ a ∈ { base := base, length := space n }.footprint, x'.mem a = x.mem a) (hb' : WordRAM.Data.Bounded w x') (h : FibInv n K_max w base s x) : FibInv n K_max w base s x'

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.potential_supported {x x' : WordRAM.Data rFib} (hreg : ∀ (i : Fin rFib), inputReg i = false → x'.regs i = x.regs i) : potential x' = potential x