Skip to content
  1. CLRS-Lean
  2. Chapters 1–35 · CLRS Fourth Edition
  3. Chapter 19. Data Structures for Disjoint Sets
  4. 19.2. Linked-List Representation of Disjoint Sets
Browse chapters
Imports
import CLRSLean.FourthEdition.Chapter_19.Section_19_1_Disjoint_Set_Operations

19.2. Linked-List Representation of Disjoint Sets

The CLRS linked-list representation stores, for every element, the head of its set and stores a set size at each head. The executable model below makes that table-level behavior explicit. A weighted union redirects every head pointer in the class with the smaller recorded size. The returned cost uses that size; it equals actual changed pointers only when recorded sizes equal the cardinality of the represented classes. The WeightedExecution companion proves this invariant from singleton initialization and derives the whole-trace rewrite bound from the actual changed representatives.

Main results:

  • Theorem LinkedList.weightedUnion_sameSet_iff: weighted union has the exact abstract merge semantics.

  • Theorem LinkedList.weightedUnion_preserves_headInvariant: every head remains a representative.

  • Theorem LinkedList.weightedUnion_changed_doubles: whenever an element's representative pointer is rewritten, its recorded set size at least doubles.

  • Theorems LinkedList.move_count_le_log2 and LinkedList.total_rewrites_le_n_mul_log2: the standard CLRS aggregate conditional arithmetic bound extracted from supplied doubling events.

  • The WeightedExecution companion constructs those move counts from a mixed UNION/FIND execution, maintains class-size cardinality, and proves the initialized total-rewrite and query-output contracts.

namespace CLRSnamespace Chapter21namespace LinkedListopen Finset

Table-level model of the linked-list disjoint-set representation.

structure State (n : Nat) where head : Fin n → Fin n size : Fin n → Nat
namespace Statevariable {n : Nat}

Two elements are in the same represented list exactly when their heads agree.

def sameSet (s : State n) (x y : Fin n) : Prop := s.head x = s.head y

The size recorded at the representative of x.

def setSize (s : State n) (x : Fin n) : Nat := s.size (s.head x)

Every stored head is itself a representative.

def HeadInvariant (s : State n) : Prop := ∀ x, s.head (s.head x) = s.head x

The represented abstract partition.

def partition (s : State n) : Partition (Fin n) where sameSet := s.sameSet refl := fun _ => rfl symm := fun h => h.symm trans := fun hab hbc => hab.trans hbc

The initial state containing n singleton lists.

def singleton (n : Nat) : State n where head := id size := fun _ => 1
@[simp] theorem singleton_head (x : Fin n) : (singleton n).head x = x := rfl@[simp] theorem singleton_size (x : Fin n) : (singleton n).setSize x = 1 := rfltheorem singleton_headInvariant (n : Nat) : (singleton n).HeadInvariant := by intro x rfltheorem singleton_sameSet_iff (x y : Fin n) : (singleton n).sameSet x y ↔ x = y := Iff.rfl

Redirect the class of src to the head of dst.

def mergeToward (s : State n) (src dst : Fin n) : State n where head z := if s.head z = s.head src then s.head dst else s.head z size z := if z = s.head dst then s.setSize src + s.setSize dst else if z = s.head src then 0 else s.size z

Weighted union redirects the class with the smaller recorded size. The second component is that recorded-size charge; equality with actual pointer changes requires the companion's WeightedExecution.Sized invariant and is proved by WeightedExecution.union_changes_cost. Arbitrary malformed size fields do not have this interpretation.

def weightedUnion (s : State n) (x y : Fin n) : State n × Nat := if s.head x = s.head y then (s, 0) else if s.setSize x ≤ s.setSize y then (s.mergeToward x y, s.setSize x) else (s.mergeToward y x, s.setSize y)

Redirecting one distinct class to another has the exact merge relation.

theorem mergeToward_sameSet_iff (s : State n) {x y : Fin n} (_hxy : ¬s.sameSet x y) (a b : Fin n) : (s.mergeToward x y).sameSet a b ↔ s.sameSet a b ∨ (s.sameSet a x ∧ s.sameSet y b) ∨ (s.sameSet a y ∧ s.sameSet x b) := by unfold sameSet at ⊢ by_cases ha : s.head a = s.head x · by_cases hb : s.head b = s.head x · simp [mergeToward, ha, hb] · constructor · intro h simp [mergeToward, ha, hb] at h exact Or.inr (Or.inl ⟨ha, h⟩) · intro h rcases h with hab | ⟨⟨_, hyb⟩ | ⟨_, hxb⟩⟩ · exact (hb (hab.symm.trans ha)).elim · simpa [mergeToward, ha, hb] using hyb · exact (hb hxb.symm).elim · by_cases hb : s.head b = s.head x · constructor · intro h simp [mergeToward, ha, hb] at h exact Or.inr (Or.inr ⟨h, hb.symm⟩) · intro h rcases h with hab | ⟨⟨hax, _⟩ | ⟨hay, _⟩⟩ · exact (ha (hab.trans hb)).elim · exact (ha hax).elim · simpa [mergeToward, ha, hb] using hay · constructor · intro h exact Or.inl (by simpa [mergeToward, ha, hb] using h) · intro h rcases h with hab | ⟨⟨hax, _⟩ | ⟨_, hxb⟩⟩ · simpa [mergeToward, ha, hb] using hab · exact (ha hax).elim · exact (hb hxb.symm).elim

Weighted union implements the Section 19.1 abstract union operation.

theorem weightedUnion_sameSet_iff (s : State n) (x y a b : Fin n) : (s.weightedUnion x y).1.sameSet a b ↔ s.sameSet a b ∨ (s.sameSet a x ∧ s.sameSet y b) ∨ (s.sameSet a y ∧ s.sameSet x b) := by by_cases hxy : s.sameSet x y · change s.head x = s.head y at hxy rw [show s.weightedUnion x y = (s, 0) by simp [weightedUnion, hxy]] change s.sameSet a b ↔ _ constructor · exact Or.inl · intro h rcases h with hab | ⟨⟨hax, hyb⟩ | ⟨hay, hxb⟩⟩ · exact hab · exact (s.partition.trans (s.partition.trans hax hxy) hyb) · exact (s.partition.trans (s.partition.trans hay (s.partition.symm hxy)) hxb) · by_cases hle : s.setSize x ≤ s.setSize y · change ¬s.head x = s.head y at hxy rw [show s.weightedUnion x y = (s.mergeToward x y, s.setSize x) by simp [weightedUnion, hxy, hle]] exact s.mergeToward_sameSet_iff hxy a b · have hyx : ¬s.sameSet y x := by intro h exact hxy h.symm change ¬s.head x = s.head y at hxy change ¬s.head y = s.head x at hyx rw [show s.weightedUnion x y = (s.mergeToward y x, s.setSize y) by simp [weightedUnion, hxy, hle]] rw [s.mergeToward_sameSet_iff hyx] aesop

Weighted union refines the abstract partition merge.

theorem weightedUnion_refines_merge (s : State n) (x y a b : Fin n) : ((s.weightedUnion x y).1.partition).sameSet a b ↔ ((s.partition).merge x y).sameSet a b := by rw [Partition.merge_sameSet_iff] exact s.weightedUnion_sameSet_iff x y a b

Redirecting a class preserves idempotent representative pointers.

theorem mergeToward_preserves_headInvariant (s : State n) {x y : Fin n} (hinv : s.HeadInvariant) (hxy : ¬s.sameSet x y) : (s.mergeToward x y).HeadInvariant := by intro z unfold sameSet at hxy by_cases hz : s.head z = s.head x · have hyx : ¬s.head (s.head y) = s.head x := by rw [hinv y] exact Ne.symm hxy simpa [mergeToward, hz, hyx] using hinv y · have hzx : ¬s.head (s.head z) = s.head x := by rw [hinv z] exact hz simpa [mergeToward, hz, hzx] using hinv z

Weighted union preserves the representative invariant.

theorem weightedUnion_preserves_headInvariant (s : State n) (x y : Fin n) (hinv : s.HeadInvariant) : (s.weightedUnion x y).1.HeadInvariant := by by_cases hxy : s.sameSet x y · change s.head x = s.head y at hxy simpa [weightedUnion, hxy] using hinv · by_cases hle : s.setSize x ≤ s.setSize y · change ¬s.head x = s.head y at hxy simpa [weightedUnion, hxy, hle] using s.mergeToward_preserves_headInvariant hinv hxy · have hyx : ¬s.sameSet y x := fun h => hxy h.symm change ¬s.head x = s.head y at hxy change ¬s.head y = s.head x at hyx simpa [weightedUnion, hxy, hle] using s.mergeToward_preserves_headInvariant hinv hyx

A weighted union never charges more rewrites than either input set size.

theorem weightedUnion_cost_le_left (s : State n) (x y : Fin n) : (s.weightedUnion x y).2 ≤ s.setSize x := by simp only [weightedUnion] split <;> rename_i hxy · exact Nat.zero_le _ · split <;> rename_i hle · exact Nat.le_refl _ · exact Nat.le_of_lt (Nat.lt_of_not_ge hle)

Symmetric rewrite-cost bound for weighted union.

theorem weightedUnion_cost_le_right (s : State n) (x y : Fin n) : (s.weightedUnion x y).2 ≤ s.setSize y := by simp only [weightedUnion] split <;> rename_i hxy · exact Nat.zero_le _ · split <;> rename_i hle · exact hle · exact Nat.le_refl _

If an element's representative pointer changes, the size recorded at its new representative is at least twice the old represented-set size.

theorem weightedUnion_changed_doubles (s : State n) (x y z : Fin n) (hchanged : (s.weightedUnion x y).1.head z ≠ s.head z) : 2 * s.setSize z ≤ (s.weightedUnion x y).1.setSize z := by by_cases hxy : s.sameSet x y · change s.head x = s.head y at hxy rw [show s.weightedUnion x y = (s, 0) by simp [weightedUnion, hxy]] at hchanged exact (hchanged rfl).elim · by_cases hle : s.setSize x ≤ s.setSize y · change ¬s.head x = s.head y at hxy rw [show s.weightedUnion x y = (s.mergeToward x y, s.setSize x) by simp [weightedUnion, hxy, hle]] at hchanged ⊢ have hz : s.head z = s.head x := by by_contra hz apply hchanged simp [mergeToward, hz] unfold setSize at hle ⊢ simp [mergeToward, setSize, hz] omega · change ¬s.head x = s.head y at hxy rw [show s.weightedUnion x y = (s.mergeToward y x, s.setSize y) by simp [weightedUnion, hxy, hle]] at hchanged ⊢ have hz : s.head z = s.head y := by by_contra hz apply hchanged simp [mergeToward, hz] have hyx : s.head y ≠ s.head x := by exact fun h => hxy h.symm unfold setSize at hle ⊢ simp [mergeToward, setSize, hz] omega

Repeated size doublings give an exponential lower bound.

theorem pow_le_of_repeated_doubling (sizeAt : Nat → Nat) (k : Nat) (hzero : 1 ≤ sizeAt 0) (hstep : ∀ i, i < k → 2 * sizeAt i ≤ sizeAt (i + 1)) : 2 ^ k ≤ sizeAt k := by induction k with | zero => simpa using hzero | succ k ih => have ih' : 2 ^ k ≤ sizeAt k := ih (fun i hi => hstep i (Nat.lt_trans hi (Nat.lt_succ_self k))) calc 2 ^ (k + 1) = 2 * 2 ^ k := by rw [Nat.pow_succ] omega _ ≤ 2 * sizeAt k := Nat.mul_le_mul_left 2 ih' _ ≤ sizeAt (k + 1) := hstep k (Nat.lt_succ_self k)

An element whose class doubles on every move is rewritten at most logarithmically often.

theorem move_count_le_log2 {sizeAt : Nat → Nat} {k total : Nat} (htotal : total ≠ 0) (hzero : 1 ≤ sizeAt 0) (hstep : ∀ i, i < k → 2 * sizeAt i ≤ sizeAt (i + 1)) (hfinal : sizeAt k ≤ total) : k ≤ Nat.log2 total := by apply (Nat.le_log2 htotal).2 exact Nat.le_trans (pow_le_of_repeated_doubling sizeAt k hzero hstep) hfinal

Summing the per-element logarithmic rewrite bound gives n log n.

theorem total_rewrites_le_n_mul_log2 (moves : Fin n → Nat) (hmoves : ∀ z, moves z ≤ Nat.log2 n) : ∑ z, moves z ≤ n * Nat.log2 n := by calc ∑ z, moves z ≤ ∑ _z : Fin n, Nat.log2 n := by exact Finset.sum_le_sum fun z _ => hmoves z _ = n * Nat.log2 n := by simp
end Stateend LinkedListend Chapter21end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_19.Section_19_2_Linked_List_Representation.WeightedExecution

Weighted-union traces and aggregate pointer rewrites

The execution starts from the native head-table state and runs arbitrary FIND and weighted UNION commands. Each union enumerates the representatives that actually changed, then derives both its rewrite total and per-element move counts from this list. No move events or doubling assumptions are supplied by a caller. The initialized invariant identifies every recorded class size with the cardinality of its actual head fiber.

The returned total is the sum of constructed per-element counts and is at most n * Nat.log2 n. Adding one abstract controller event per command gives m + n * Nat.log2 n. This is the head-pointer rewrite model: enumeration of audit events, persistent function evaluation, and linked-list allocation are outside the charged model. It is not a runtime bound for these instrumentation lists or an implementation of explicit linked-list cells.

namespace CLRS.Chapter21.LinkedList.WeightedExecutionopen Finset Statevariable {n : Nat}def classOf (s : State n) (x : Fin n) : Finset (Fin n) := univ.filter (fun z => s.head z = s.head x)

Recorded class sizes agree with the actual represented partition.

def Sized (s : State n) : Prop := ∀ z, s.setSize z = (classOf s z).card
theorem singleton_sized : Sized (singleton n) := by intro z simp [setSize, State.singleton, classOf, Finset.filter_eq']theorem class_disjoint (s : State n) {x y : Fin n} (h : s.head x ≠ s.head y) : Disjoint (classOf s x) (classOf s y) := by apply Finset.disjoint_left.mpr simp only [classOf, mem_filter, mem_univ, true_and] intro z hx hy exact h (hx.symm.trans hy)theorem merge_class_left (s : State n) (x y z : Fin n) (hz : s.head z = s.head x) : classOf (s.mergeToward x y) z = classOf s x ∪ classOf s y := by ext w by_cases hw : s.head w = s.head x <;> simp [classOf, mergeToward, hz, hw]theorem merge_class_right (s : State n) (x y z : Fin n) (hxy : s.head x ≠ s.head y) (hz : s.head z = s.head y) : classOf (s.mergeToward x y) z = classOf s x ∪ classOf s y := by ext w by_cases hw : s.head w = s.head x <;> simp [classOf, mergeToward, hz, hw, hxy] theorem merge_class_other (s : State n) (x y z : Fin n) (hzx : s.head z ≠ s.head x) (hzy : s.head z ≠ s.head y) : classOf (s.mergeToward x y) z = classOf s z := by ext w by_cases hw : s.head w = s.head x · have hwz : s.head w ≠ s.head z := by rw [hw]; exact Ne.symm hzx simp [classOf, mergeToward, hzx, Ne.symm hzy, hw, Ne.symm hzx] · simp [classOf, mergeToward, hzx, hw] theorem merge_sized (s : State n) (x y : Fin n) (hs : Sized s) (hxy : s.head x ≠ s.head y) : Sized (s.mergeToward x y) := by intro z by_cases hzx : s.head z = s.head x · rw [merge_class_left s x y z hzx, card_union_of_disjoint (class_disjoint s hxy)] simp [setSize, mergeToward, hzx, ← hs x, ← hs y] · by_cases hzy : s.head z = s.head y · rw [merge_class_right s x y z hxy hzy, card_union_of_disjoint (class_disjoint s hxy)] simp [setSize, mergeToward, hzy, ← hs x, ← hs y] · rw [merge_class_other s x y z hzx hzy] simpa [setSize, mergeToward, hzx, hzy] using hs ztheorem union_sized (s : State n) (x y : Fin n) (hs : Sized s) : Sized (s.weightedUnion x y).1 := by unfold weightedUnion split · exact hs · rename_i hxy split · exact merge_sized s x y hs hxy · exact merge_sized s y x hs (Ne.symm hxy)theorem merge_size_mono (s : State n) (x y z : Fin n) (_hxy : s.head x ≠ s.head y) : s.setSize z ≤ (s.mergeToward x y).setSize z := by by_cases hzx : s.head z = s.head x · simp [setSize, mergeToward, hzx] · by_cases hzy : s.head z = s.head y · simp [setSize, mergeToward, hzy] · simp [setSize, mergeToward, hzx, hzy]theorem union_size_mono (s : State n) (x y z : Fin n) : s.setSize z ≤ (s.weightedUnion x y).1.setSize z := by unfold weightedUnion split · exact Nat.le_refl _ · rename_i hxy split · exact merge_size_mono s x y z hxy · exact merge_size_mono s y x z (Ne.symm hxy)

Enumerate actual pre/post representative changes for the audit ledger.

def changes (s t : State n) : List (Fin n) := (List.finRange n).filter (fun z => decide (t.head z ≠ s.head z))
theorem changes_count (s t : State n) (z : Fin n) : (changes s t).count z = if t.head z ≠ s.head z then 1 else 0 := by by_cases h : t.head z ≠ s.head z · rw [if_pos h] exact List.count_eq_one_of_mem ((List.nodup_finRange n).filter _) (by simp [changes, h]) · rw [if_neg h] apply List.count_eq_zero.mpr simp [changes, h]theorem sum_counts (xs : List (Fin n)) : ∑ z, xs.count z = xs.length := by induction xs with | nil => simp | cons x xs ih => simp [List.count_cons, Finset.sum_add_distrib, ih, beq_iff_eq]theorem changes_length (s t : State n) : (changes s t).length = ∑ z, (changes s t).count z := by exact (sum_counts (changes s t)).symmtheorem merge_changes (s : State n) (x y : Fin n) (hxy : s.head x ≠ s.head y) : changes s (s.mergeToward x y) = (List.finRange n).filter (fun z => decide (s.head z = s.head x)) := by apply List.filter_congr intro z _ by_cases hz : s.head z = s.head x · simp [mergeToward, hz, Ne.symm hxy] · simp [mergeToward, hz] theorem merge_changes_length (s : State n) (x y : Fin n) (hxy : s.head x ≠ s.head y) : (changes s (s.mergeToward x y)).length = (classOf s x).card := by rw [merge_changes s x y hxy] rw [← List.toFinset_card_of_nodup ((List.nodup_finRange n).filter _)] congr 1 ext z simp [classOf]theorem union_changes_cost (s : State n) (x y : Fin n) (hs : Sized s) : (changes s (s.weightedUnion x y).1).length = (s.weightedUnion x y).2 := by unfold weightedUnion split · simp [changes] · rename_i hxy split · exact (merge_changes_length s x y hxy).trans (hs x).symm · exact (merge_changes_length s y x (Ne.symm hxy)).trans (hs y).symmstructure Step (n : Nat) where state : State n output : Option (Fin n) rewritten : List (Fin n)def step (s : State n) : Operation (Fin n) → Step n | .find x => ⟨s, some (s.head x), []⟩ | .union x y => let next := s.weightedUnion x y ⟨next.1, none, changes s next.1⟩theorem step_sized (s : State n) (op : Operation (Fin n)) (hs : Sized s) : Sized (step s op).state := by cases op with | find x => exact hs | union x y => exact union_sized s x y hstheorem step_headInvariant (s : State n) (op : Operation (Fin n)) (hs : s.HeadInvariant) : (step s op).state.HeadInvariant := by cases op with | find x => exact hs | union x y => exact s.weightedUnion_preserves_headInvariant x y hstheorem step_growth (s : State n) (op : Operation (Fin n)) (z : Fin n) : 2 ^ (step s op).rewritten.count z * s.setSize z ≤ (step s op).state.setSize z := by cases op with | find x => simp [step] | union x y => simp only [step, changes_count] split · simpa using s.weightedUnion_changed_doubles x y z ‹_› · simpa using union_size_mono s x y zstructure Run (n : Nat) where state : State n outputs : List (Option (Fin n)) moves : Fin n → Nat rewrites : Nat commands : Nat

Run native transitions, returning query outputs and the derived rewrite ledger.

def execute (s : State n) : List (Operation (Fin n)) → Run n | [] => ⟨s, [], fun _ => 0, 0, 0⟩ | op :: ops => let current := step s op let rest := execute current.state ops ⟨rest.state, current.output :: rest.outputs, fun z => current.rewritten.count z + rest.moves z, current.rewritten.length + rest.rewrites, rest.commands + 1⟩
theorem execute_sized (s : State n) (ops : List (Operation (Fin n))) (hs : Sized s) : Sized (execute s ops).state := by induction ops generalizing s with | nil => exact hs | cons op ops ih => exact ih _ (step_sized s op hs)theorem execute_headInvariant (s : State n) (ops : List (Operation (Fin n))) (hs : s.HeadInvariant) : (execute s ops).state.HeadInvariant := by induction ops generalizing s with | nil => exact hs | cons op ops ih => exact ih _ (step_headInvariant s op hs)

The returned rewrite total is exactly the sum of its per-element move counts.

theorem execute_rewrites_eq_sum (s : State n) (ops : List (Operation (Fin n))) : (execute s ops).rewrites = ∑ z, (execute s ops).moves z := by induction ops generalizing s with | nil => simp [execute] | cons op ops ih => simp only [execute, Finset.sum_add_distrib, ← ih] congr 1 exact (sum_counts (step s op).rewritten).symm
theorem execute_growth (s : State n) (ops : List (Operation (Fin n))) (z : Fin n) : 2 ^ (execute s ops).moves z * s.setSize z ≤ (execute s ops).state.setSize z := by induction ops generalizing s with | nil => simp [execute] | cons op ops ih => have hg := step_growth s op z have ht := ih (step s op).state simp only [execute, pow_add] calc _ = 2 ^ (execute (step s op).state ops).moves z * (2 ^ (step s op).rewritten.count z * s.setSize z) := by ring _ ≤ 2 ^ (execute (step s op).state ops).moves z * (step s op).state.setSize z := Nat.mul_le_mul_left _ hg _ ≤ _ := ht theorem execute_singleton_moves_le (ops : List (Operation (Fin n))) (z : Fin n) : (execute (State.singleton n) ops).moves z ≤ Nat.log2 n := by have hs := execute_sized (State.singleton n) ops singleton_sized have hg := execute_growth (State.singleton n) ops z rw [singleton_size, Nat.mul_one, hs z] at hg apply (Nat.le_log2 (by have h := z.isLt; omega)).2 exact hg.trans (by simpa [classOf] using Finset.card_le_card (Finset.filter_subset (fun w => (execute (State.singleton n) ops).state.head w = (execute (State.singleton n) ops).state.head z) (univ : Finset (Fin n))))

Aggregate doubling bound for arbitrary operations from singleton sets.

theorem execute_singleton_rewrites_le (ops : List (Operation (Fin n))) : (execute (State.singleton n) ops).rewrites ≤ n * Nat.log2 n := by rw [execute_rewrites_eq_sum] exact total_rewrites_le_n_mul_log2 _ (execute_singleton_moves_le ops)
private theorem partition_ext {P Q : Partition (Fin n)} (h : ∀ x y, P.sameSet x y ↔ Q.sameSet x y) : P = Q := by cases P cases Q congr funext x y exact propext (h x y)theorem step_refines_spec (s : State n) (op : Operation (Fin n)) : (step s op).state.partition = stepSpec s.partition op := by cases op with | find x => rfl | union x y => apply partition_ext intro a b exact s.weightedUnion_refines_merge x y a b theorem execute_refines_spec (s : State n) (ops : List (Operation (Fin n))) : (execute s ops).state.partition = runSpec s.partition ops := by induction ops generalizing s with | nil => rfl | cons op ops ih => change (execute (step s op).state ops).state.partition = runSpec (stepSpec s.partition op) ops rw [ih, step_refines_spec]theorem execute_commands (s : State n) (ops : List (Operation (Fin n))) : (execute s ops).commands = ops.length := by induction ops generalizing s with | nil => rfl | cons op ops ih => simp [execute, ih]theorem execute_outputs_length (s : State n) (ops : List (Operation (Fin n))) : (execute s ops).outputs.length = ops.length := by induction ops generalizing s with | nil => rfl | cons op ops ih => simp [execute, ih]theorem execute_append_state (s : State n) (xs ys : List (Operation (Fin n))) : (execute s (xs ++ ys)).state = (execute (execute s xs).state ys).state := by induction xs generalizing s with | nil => rfl | cons op xs ih => exact ih (step s op).statetheorem execute_append_outputs (s : State n) (xs ys : List (Operation (Fin n))) : (execute s (xs ++ ys)).outputs = (execute s xs).outputs ++ (execute (execute s xs).state ys).outputs := by induction xs generalizing s with | nil => rfl | cons op xs ih => simp [execute, ih]

A FIND returns the representative in the state reached by its preceding commands.

theorem execute_find_output (s : State n) (before suffix : List (Operation (Fin n))) (x : Fin n) : (execute s (before ++ .find x :: suffix)).outputs[before.length]? = some (some ((execute s before).state.head x)) := by rw [execute_append_outputs, List.getElem?_append_right (by rw [execute_outputs_length])] simp [execute_outputs_length, execute, step]

Returned FIND representatives are resident representatives of the queried class.

theorem execute_find_representative (s : State n) (before : List (Operation (Fin n))) (hs : s.HeadInvariant) (x : Fin n) : (execute s before).state.sameSet x ((execute s before).state.head x) ∧ (execute s before).state.head ((execute s before).state.head x) = (execute s before).state.head x := by have hi := execute_headInvariant s before hs x exact ⟨hi.symm, hi⟩

One abstract command event plus actual representative-pointer changes. This excludes scanning head tables to enumerate the audit events.

def Run.charged (run : Run n) : Nat := run.commands + run.rewrites
theorem execute_singleton_charged_le (ops : List (Operation (Fin n))) : (execute (State.singleton n) ops).charged ≤ ops.length + n * Nat.log2 n := by unfold Run.charged rw [execute_commands] exact Nat.add_le_add_left (execute_singleton_rewrites_le ops) _end CLRS.Chapter21.LinkedList.WeightedExecution