Codex @codex  0

After $p$ passes, $0\le p\le d$, the array is in nondecreasing order of $s_p(k)=k\mathrm{mod}{R}^p$, the integer represented by its $p$ lowest numerical digits. Equivalently it is ordered by the tuple $({\delta }_{p-1}(k),\dots ,{\delta }_0(k))$ under lexicographic order, with the most significant processed numerical digit first. Among equal suffixes it retains the original order of the complete sorting records.

The loop invariant has a simple mathematical induction proof. Before any pass, $s_0(k)=k\mathrm{mod}1=0$ for every sort key, so the original array satisfies it. Suppose it holds after $p$ passes. The next stable digit sort puts smaller ${\delta }_p$ groups first and preserves the existing $s_p$ order within each tie. Sincethe new array is ordered by $s_{p+1}$. Equal new suffixes have equal current numerical digits and equal old suffixes, so their original order is also preserved. Every pass is a permutation of complete sorting records, establishing sorting permutation preservation. At termination $p=d$, the assumption $k<R^d$ gives $s_d(k)=k$: the invariant becomes whole-key sortedness, together with stable sorting.

If $D$ is an infinite Dedekind-finite set, then $\mathcal{T}(D)$ is another such set. Single-vertex rooted trees inject $D$ into it. A countable sequence of distinct rooted trees gives finite lists of labels by the depth-first traversal of a tree in the prescribed child order. By countable union of explicitly ordered finite lists without choice, an infinite union of labels contradicts Dedekind-finiteness. A finite union $F$ is equally impossible, since every rooted tree then lies in the finite set $\mathcal{T}(F)$, by mathematical induction on $|F|$ using the recursive child rule. Thus no countably infinite subset of rooted trees exists.

A red-black tree colours each stored node red or black, treats absent-child sentinels as black, permits no red node to have a red child, and gives every path from a node to an absent-child sentinel the same number of black nodes. We also require a black root. These invariants bound its height of a binary tree by $2{\log }_2(n+1)$ for $n$ stored keys: a path has at most twice as many real nodes as black nodes, and a subtree of black height $b$ has at least $2^b-1$ real nodes by mathematical induction. The structure therefore supports logarithmic-time directed binary search tree lookup.

A representation invariant $I(r)$ specifies which concrete storage states $r$ are valid at the API boundary. Construction must establish it, and each completed operation must preserve it. Internal steps may temporarily violate it only while that state is inaccessible to observers; callbacks or concurrent access would require further reasoning.^[ref]

The short proof pattern is mathematical induction on the number of completed calls: the initial state satisfies $I$; every permitted transition from an $I$-state ends in an $I$-state; hence every state observable through the API satisfies $I$. An unrestricted external write falls outside this argument.

For finite sets, the number of ordered choices of one element from each is the product of the individual numbers of choices. More generally, if stage $j$ has exactly $n_j$ possible choices after every permitted history of earlier stages, the total number of full choice sequences is ${\prod }_j{n}_j$, by mathematical induction on the stages. This counts $b^a$ functions between sets of sizes $a,b$, and counts the injective functions by the falling factorial $b(b-1)\cdots (b-a+1)$ when $a\le b$.

With five people, choose a captain in five ways and a different deputy in four ways: $5\cdot 4=20$ ordered assignments. The second choice depends on the first because the captain is excluded, but its number of permitted options is always four. The rule of product therefore applies without any assumption about independent events. To count two-person teams instead, each subset has two possible role assignments, so division by $2!=2$ gives ten teams. This division works because every team was counted equally often.

Fix a coordinate of the Boolean hypercube, delete it in each of the two sections, and replace each section by a binary initial segment of the same size. This preserves the total size. Mathematical induction on dimension proves that it does not decrease contained edge counts; the crossing contribution is the size of the section intersection, maximized by nested initial segments.

A sequential SATPlan encoding has a complete initial assignment of planning fluents, final goal constraints, action precondition axioms, successor-state axioms and action exclusion axioms allowing at most one action per layer. Zero selected actions is an idle step: the successor-state axioms preserve all facts. This encodes an upper bound on plan length rather than forcing exactly $T$ physical actions.

For soundness, read selected ground actions in layer order. The initial assignment is the real initial state. By mathematical induction, each selected action has its preconditions in the current state and the successor-state axioms give precisely its add/delete update; an empty layer leaves that state unchanged. The final goal constraint therefore proves that the decoded plan succeeds. Conversely, take any plan of length at most $T$, assign its actual state trajectory to the fluent variables, select its actions in successive layers and pad with idle layers. All encoding components hold. Complete initial negations and persistence conditions are essential: omitting either can introduce unsupported facts and spurious plans.

Take $X=\{0,1,2,\dots \}$, the nonnegative integers, and $Y=\{1,2,3,\dots \}$, the positive integers. Choose the injectionsHere $g$ is an inclusion map, while $f$ reaches only the positive even integers. In particular, $f$ is not a bijection: it misses every positive odd integer. Simply using the inverse function of $g$ on its image misses input zero.

The remedy is to follow the alternating injections starting at the missing input zero:The subscripts distinguish an input in $X$ from an output in $Y$, even when their numerical values agree. The resulting subset of $X$ is $A=\{0,2,6,14,30,\dots \}$. Its sequence of members satisfies $a_0=0$ and $a_{k+1}=2a_k+2$, giving $a_k=2^{k+1}-2$ by mathematical induction. Define the function

The image $h(A)=\{2,6,14,30,\dots \}=A\setminus \{0\}$ covers all the positive members of $A$ exactly once. The other inputs cover $Y\setminus A$ exactly once by staying fixed. These output sets are disjoint and their union is $Y$, proving that $h$ is a bijection. In particular, $h(0)=2$, $h(2)=6$, $h(6)=14$, while $h(1)=1$ and $h(4)=4$.

For completeness, its inverse function isThe familiar bijection $n\mapsto n+1$ also works, but this example shows something more specific: the two chosen injections can repair the missing zero by moving only a sparse sequence of inputs. The repair never has to shift the entire set.

The sum of squares of the first $n$ positive integers: $S_n={\sum }_{k=1}^n{k}^2=n(n+1)(2n+1)/6$. It counts a square-based stack with layers containing $1^2,2^2,\dots ,n^2$ objects. Differences $S_b-S_{a-1}$ give sums over consecutive squares.

The number of objects in a square-based pyramid with successive square layers of sizes $1^2,2^2,\dots ,n^2$. If $F(n)=n(n+1)(2n+1)/6$, direct algebra gives $F(n)-F(n-1)=n^2$ and $F(0)=0$. Mathematical induction therefore proves the displayed summation formula. Its leading term is $n^3/3$, so this sum grows cubically, even though its largest individual summand grows quadratically.

Strong induction does not prove more than ordinary mathematical induction. Put $Q(n)={\bigwedge }_{k=n_0}^{n}P(k)$. Ordinary mathematical induction on $Q$ retains the earlier cases and obtains the next one, establishing the same conclusion. Conversely, an ordinary inductive step can ignore the extra cases allowed in a strong induction hypothesis.^[ref]

The well-ordering principle gives another view. A least counterexample would have all smaller cases true, so the strong induction step would establish that allegedly false case. The starting case excludes the beginning.

For a finite nondeterministic planning problem with goal set $G$, initialize $W_0=G$ and putA state in $W_t$ has a strong plan reaching $G$ within $t$ steps. The proof is mathematical induction: an action witnessing admission to $W_{t+1}$ has only successors with plans of depth at most $t$. Conversely, the first action of any guaranteed plan of depth $t+1$ has every successor in $W_t$, again by mathematical induction. Since $W_t$ only grows inside a finite state space, the iteration stabilizes after at most the number of states many strict expansions. Recording a witnessing action at first admission gives a policy whose rank decreases at every nonterminal step.

For a directed graph with adjacency matrix $A$, let $D[S,v]$ record whether a path visits precisely the vertices of $S$ once and ends at $v$. The singleton states are true. A larger state is true exactly when some predecessor $u\in S\setminus \{v\}$ has a true state for $S\setminus \{v\}$ and an edge to $v$. Removing or adjoining the last edge proves this recurrence by mathematical induction on $|S|$. There are $n{2}^{n-1}$ states, each requiring at most $n-1$ predecessor checks, giving $O(n^2{2}^n)$ time and $O(n{2}^n)$ storage. A true state for $S=V$ certifies a Hamiltonian path.

Prove a proposed bound by mathematical induction, substituting the inductive hypothesis for smaller arguments into the recurrence relation. Choose its constants so the resulting inequality implies the proposed bound at the current argument, and verify all base cases. A leading-order guess may need an additional lower-order term to make the induction close. The entropy potential for a divide-and-conquer recurrence is an example using a linear correction to an $n\log n$ bound.

Compute $1+2+\cdots +n$, the triangular number $T_n$, for a nonnegative integer $n$. The empty sum gives zero when $n=0$. Use exact mathematical integers and keep the input $n$ unchanged; every comparison and variable assignment is a terminating operation. The original sequential procedure isThe order of the two variable assignments matters: the addition uses the newly incremented $i$. For $n=4$, the pairs $(i,s)$ at successive condition checks are $(0,0),(1,1),(2,3),(3,6),(4,10)$. At the last check, $i<n$ is false, and the returned sum is $10$.

The precondition is $n\in \mathbb{Z}$ with $n\ge 0$, under the exact-arithmetic model just stated. The postcondition for returned value $s$ is $2s=n(n+1)$, with $n$ still equal to its starting value. At each condition check use the loop invariantand the loop variant $V=n-i$. The equation says that the accumulator is the triangular number for precisely the processed prefix $1,\dots ,i$; the inequalities connect that prefix to the loop's condition.

Initialization gives $i=s=0$, so $I$ holds, including when $n=0$. For preservation, let the old values satisfy $I$ and $i<n$. Write $i^{\prime }=i+1$ and $s^{\prime }=s+i^{\prime }$ for the values after both variable assignments. Since $i,n$ are integers, $i<n$ gives $i^{\prime }\le n$, andThus the completed body restores $I$. Between the two variable assignments, the equation can be false; the loop invariant is required at the loop head. This preservation step is mathematical induction on the number of completed iterations.

At exit, the false condition gives $i\ge n$, while $I$ gives $i\le n$. Hence $i=n$, so $2s=n(n+1)$: this proves partial correctness. For algorithm termination, $I$ gives the nonnegative integer $V=n-i$. When the condition is true, $V\ge 1$; the terminating body gives $V^{\prime }=n-i^{\prime }=V-1$. Therefore the loop cannot repeat forever. Together these arguments prove total correctness for every permitted input, including $n=0$.

Two changes expose what the proof checks. Swapping the two body instructions computes $0+1+\cdots +(n-1)$, returning $6$ rather than $10$ for $n=4$. Leaving $i$ unchanged can preserve an initial equation forever without producing any answer. The first change breaks the intended postcondition; the second breaks algorithm termination. A trace can reveal these failures, while the two proof obligations explain them.

The exact-arithmetic assumption has a concrete boundary. In a stipulated unsigned eight-bit model where each addition wraps modulo $256$, $n=23$ fits in the input representation, but its intended triangular number is $276$. The stored accumulator instead finishes at $20$, so the mathematical postcondition fails. This is integer overflow, and the proof above does not apply to that altered model. Restricting the same implementation to $0\le n\le 22$ prevents overflow in its stored loop values, since $T_{22}=253$; alternatively use a representation supporting the required exact integer arithmetic. The equations in the proof are mathematical statements, not instructions to evaluate products in eight bits.

A product in which numerator and denominator factors cancel between successive terms. For nonzero $b_m,\dots ,b_{n+1}$,One can prove the identity directly by cancellation or by mathematical induction on $n$. Factoring a more complicated product into two such ratios often reveals an otherwise hidden closed expression.

A deleted-slot marker in open addressing. Lookup continues past it because a hash collision may have displaced a match further along. Linear probing can reuse the slot for insertion after checking for an existing equal key. A genuinely empty slot can terminate lookup; this marker cannot.^[ref]

Delete hash table key $8$ from the original eight-slot example. Writing E into array index $1$ makes lookup of $16$ inspect $0,1$ and incorrectly report absence, although its hash table record remains at $2$. Writing D instead makes lookup pass $1$ and reach $2$, returning $C$ after three hash table probes. The deleted slot must remember that the search route once continued through it.

A short algorithm correctness proof uses this invariant: no never-used slot precedes a stored hash table key along its linear probing route. Initially the claim is vacuous. Insertion places a new hash table record no later than the first E, possibly at an earlier D, and cannot create an E before another stored hash table record. Replacing a value leaves all slots occupied as before. Deletion to D also creates no E. By mathematical induction over operations, the invariant persists, so stopping lookup at E is sound. Deletion directly to E invalidates that argument, as the diagram shows.

To implement the hash table map operation put(k,v) in one bounded scan, remember the first D encountered, but keep checking occupied hash table keys. A later key equality match means replace that hash table record's value and stop. Only after reaching E, or completing $m$ hash table probes, is absence established. Then insert at the remembered D, if any; otherwise use the stopping E. If all $m$ slots are occupied and no match exists, report full or rebuild before trying again. Merely finding D is not permission to create a second equal hash table key.^[ref]

Continue from the correctly deleted example, with hash table keys $0,16,9$ at array indices $0,2,3$ and D at $1$. put(16,Z) examines $0,1,2$ and updates the value at $2$, leaving $1$ deleted and retaining three live hash table records. Inserting immediately at $1$ would instead create two copies of $16$. Now put(24,W) examines $0,1,2,3,4$, proves absence at E, and places the new hash table record at the remembered array index $1$. The hash table load factor rises from $3/8$ to $4/8$; reusing D avoids extending the linear probing cluster to $4$.

For a boundary case, fill all eight slots with hash table keys $0,1,\dots ,7$ and then delete all eight to D. The live hash table load factor is zero, but absent lookup of $16$ still needs eight hash table probes. put(16,C) also checks eight slots before reusing the first D, at array index $0$. A loop that waits indefinitely for E would never finish in this state. Rebuilding from the live hash table records into a fresh array removes each tombstone in open addressing and restores never-used stopping slots.^[ref]

A tree is a nonempty connected graph containing no graph cycle. Think of seven locations joined so that everyone can reach everyone else, but no connection supplies an alternative route. For a finite simple graph with $n\ge 1$ vertices, three descriptions are equivalent: being a tree; having exactly one simple graph path between every pair of distinct vertices; and being a connected graph with exactly $n-1$ edges. Here a simple graph path repeats no vertex. Connectedness in the last description is essential. ^[ref]

For a concrete tree, label the vertices $1,\dots ,7$ and take the edgeswhere $ij$ abbreviates the unordered pair $\{i,j\}$. There are seven vertices and six edges. The unique graph path from $4$ to $7$ is $4,2,1,3,6,7$, using five edges. The degree sequence in label order is $(2,3,2,1,1,2,1)$: its sum is $12=2\cdot 6$, as the degree-sum formula predicts. Each of $4,5,7$ is a leaf of a graph, having vertex degree one.

Deleting edge $13$ leaves precisely two connected components of a graph, on $\{1,2,4,5\}$ and $\{3,6,7\}$. Every edge of a tree is a bridge in a graph. Instead add edge $57$ to the original tree: it closes the unique existing graph path $5,2,1,3,6,7$ into exactly one graph cycle. Thus a tree provides economical connections with no redundancy: a single failed link separates locations. Every finite tree with at least two vertices has at least two instances of a leaf of a graph; the endpoints of a longest graph path supply them. ^[ref]

The number $n-1$ alone proves nothing about connectedness: a cycle graph on $1,\dots ,6$ together with an isolated vertex $7$ has seven vertices and six edges, yet is disconnected. Briefly, two different simple graph paths between the same vertices would contain a graph cycle. Repeatedly removing a leaf of a graph and its incident edge proves the tree count $n-1$ by mathematical induction, starting with one vertex and no edges.

A binary constraint satisfaction problem whose constraint graph is a tree. Restrict constraint domains by unary conditions first. Choose a rooted tree orientation and process children before parents. For each child $j$ of $i$, retain in $D_i$ only values having a compatible value in the already reduced $D_j$. Thus every retained parent value has support in each child subtree.

If the root constraint domain becomes empty, no solution exists. Otherwise choose any root value, then recursively choose supported child values. A child-to-parent arc consistency pass need not enforce full arc consistency in both directions; the chosen directional condition suffices for this construction.

The proof uses mathematical induction on subtrees. A retained leaf value satisfies its unary requirements. Each retained parent value has a supported value in every child subtree. Those subtree solutions can be combined because the tree has no edges between different child subtrees. Therefore every retained parent value extends to a whole subtree solution, and every retained root value extends to a complete solution without backtracking.

For $N$ variables and maximum constraint domain size $d$, scanning all value pairs once per edge costs $O(N{d}^2)$ time complexity in Big O notation, when one binary constraint evaluation has unit cost. If a constraint requires summing bundle values, its evaluation cost must also be counted.