Main derivation
S01 · definition
Before
S=\{123,132,213,231,312,321\},\ \mathrm{Init}=\{321\},\ \mathrm{Halt}=\{123\}After
\mathrm{Init},\mathrm{Halt}\subseteq S,\ \mathrm{Step}\subseteq S\times S,\ |S|=3!=6Conditions: none
Rule: def_intro · Uses: G1
Leaf basis: def_intro + subset_def + cartesian_product_def + finite_counting_basics
Confirm that M is a finite model in the MKO's sense. 321 and 123 lie in S. Swapping two entries of a permutation gives another permutation of 1, 2, 3, so both ends of every edge lie in S, and Step⊆S×S. S has exactly 3!=6 elements. 123 has no adjacent inverted pair, so it has no outgoing edges anyway, consistent with Halt states being endpoints.
S02 · definition
Before
M,\ Q
After
\mathrm{PC}:\ \text{every halt reached satisfies}\ Q;\quad \mathrm{T}:\ \text{every maximal execution is finite and ends in Halt};\quad \mathrm{TC}=\mathrm{PC}\wedge\mathrm{T}Conditions: none
Rule: def_unfold · Uses: G2, G4, mko_algorithm_correctness_def
Leaf basis: def_unfold + mko_algorithm_correctness_def
Write out the partial/total-correctness obligations, quantifying termination precisely over maximal executions. PC: every execution from Init that reaches Halt ends in a state satisfying Q. T: every maximal execution from Init is finite and ends in Halt, equivalently there is no infinite execution and no finite maximal execution ending outside Halt. A finite nonmaximal prefix need not have reached Halt already. TC is PC together with T, and all nondeterministic choices must be covered (G4).
S03 · theorem_application
Before
s\in S\setminus\mathrm{Halt}After
x_1>x_2\ \vee\ x_2>x_3,\ \text{so}\ \mathrm{Post}(s)\ne\varnothingConditions: none
Rule: L_succ · Uses: G1
Leaf basis: contrapositive + order_basics
Apply Lemma L_succ (proved in S03.1 and S03.2): a state outside Halt always has an adjacent inverted pair and hence a successor, so it cannot be stuck. This is the part of the termination argument that rules out getting stuck.
S04 · definition
Before
s=(x_1,x_2,x_3)
After
\mathrm{inv}(s)=[x_1>x_2]+[x_1>x_3]+[x_2>x_3]\ge 0;\ \mathrm{inv}(321)=3,\ \mathrm{inv}(231)=\mathrm{inv}(312)=2,\ \mathrm{inv}(213)=\mathrm{inv}(132)=1,\ \mathrm{inv}(123)=0Conditions: none
Rule: def_intro · Uses: G1
Leaf basis: def_intro + numeric_evaluation
Define the ranking function inv(s): the number of position pairs (i,j) with i<j and x_i>x_j. It is a sum of three 0-or-1 terms, so it is a natural number between 0 and 3. Compute it for all six states (recomputable as N2 to N7).
S05 · theorem_application
Before
(s,s')\in\mathrm{Step}After
\mathrm{inv}(s')=\mathrm{inv}(s)-1Conditions: none
Rule: L_rank · Uses: S04, G1
Leaf basis: def_unfold + add_comm + numeric_evaluation
Apply Lemma L_rank (proved separately for the two kinds of swap in S05.1 and S05.2): every step lowers the inversion count by exactly 1. This is a proof for every kind of edge, not an observation at a few sample states.
S06 · induction_base
Before
(t_k)\ \text{an execution of}\ M,\ t_0\in\mathrm{Init}After
\mathrm{inv}(t_0)=\mathrm{inv}(321)=3Conditions: none
Rule: nat_induction · Uses: S04, G1
Leaf basis: nat_induction + numeric_evaluation
Consider any execution (t_k). t0∈Init={321}, so inv(t0)=3. This is the base case (k=0) of the invariant inv(t_k)=3−k.
S07 · induction_step
Before
\mathrm{inv}(t_k)=3-k,\ (t_k,t_{k+1})\in\mathrm{Step}After
\mathrm{inv}(t_{k+1})=(3-k)-1=3-(k+1)Conditions: none
Rule: nat_induction · Uses: S06, S05
Leaf basis: nat_induction + eq_replace + add_assoc
Assume inv(t_k)=3−k and that the execution has a next state t_{k+1}. By L_rank, inv(t_{k+1})=inv(t_k)−1=(3−k)−1=3−(k+1). So inv(t_k)=3−k for every index k of the execution. Preservation is proved for every step, whichever edge is chosen at a nondeterministic branch.
S08 · implies
Before
\mathrm{inv}(t_k)=3-k\ge 0After
k\le 3:\ \text{every execution has at most 3 steps; no infinite execution}Conditions: none
Rule: order_basics · Uses: S07, S04
Leaf basis: order_basics + nat_induction
inv is never below 0, so every index k of an execution satisfies 3−k≥0, i.e. k≤3. Hence every execution has at most 4 states and 3 steps, and no infinite execution exists. This is the ranking-function argument: a nonnegative integer that strictly decreases at every step cannot decrease forever.
S09 · implies
Before
\text{every execution is finite}After
\text{every maximal execution ends in Halt:}\ \mathrm{T}Conditions: none
Rule: contrapositive · Uses: S08, S03
Leaf basis: contrapositive + mko_computational_model_def
By S08 every execution is finite; it can be extended while its last state has a successor, at most up to 3 steps, so every execution extends to a maximal one whose last state has no successor. By the contrapositive of L_succ (S03), a state without successors lies in Halt. Thus every maximal execution from Init is finite and ends in Halt, and every finite prefix extends to such a halting execution. Termination T holds as defined in S02.
S10 · implies
Before
t_{\mathrm{last}}\in\mathrm{Halt}=\{123\}After
Q(123):\ 1<2<3\ \wedge\ \{1,2,3\}=\{1,2,3\}\ \Rightarrow\ \mathrm{PC}Conditions: none
Rule: mko_algorithm_correctness_def · Uses: S01, G1, G2
Leaf basis: mko_algorithm_correctness_def + order_basics
Every execution reaching Halt ends at 123. 123 is increasing, and its entries are a rearrangement of the entries of the input 321 (S01: every state is a permutation of 1, 2, 3, and swaps do not change the entries). So Q holds at every reachable halt state, and partial correctness PC holds.
S11 · implies
Before
\mathrm{PC},\ \mathrm{T}After
\mathrm{TC}=\mathrm{PC}\wedge\mathrm{T}\ \text{holds for}\ MConditions: none
Rule: and_intro_elim · Uses: S09, S10, S02
Leaf basis: and_intro_elim + mko_algorithm_correctness_def
Conjoin PC from S10 and T from S09; by the definition in S02 this is total correctness: every maximal execution from 321 terminates, and on termination outputs the increasing rearrangement 123.
S12 · implies
Before
\text{reachable graph from}\ 321After
321\to 231\to 213\to 123,\quad 321\to 312\to 132\to 123
Conditions: none
Rule: mko_computational_model_def · Uses: G1, S11
Leaf basis: mko_computational_model_def + case_analysis
A finite model can be cross-checked with its complete reachable graph. 321 has two successors: swapping the first pair gives 231, swapping the last pair gives 312. 231 has only its last pair inverted, giving 213; 312 has only its first pair inverted, giving 132; 213 gives 123; 132 gives 123. So there are exactly two maximal executions, each of 3 steps, equal to inv(321), both ending at 123. This agrees with S07 to S11; the general proof, however, comes from S05 to S10 and does not depend on this graph.
S13 · implies
Before
M':\ 321\to 231\to 213\to 123\ \text{exists}After
t_{2k}=321,\ t_{2k+1}=231\ \text{is infinite}\ \Rightarrow\ \neg\mathrm{T},\ \neg\mathrm{TC}\ \text{for}\ M'Conditions: none
Rule: quantifier_negation · Uses: G3, S02
Leaf basis: quantifier_negation + case_analysis + mko_algorithm_correctness_def
In M′ the successful path 321→231→213→123 still exists, and Halt is still {123}, so PC still holds. But M′ allows swapping non-inverted pairs: swapping the first pair of 321 gives 231, and swapping the first pair of 231 returns to 321, neither in Halt. The sequence t_{2k}=321, t_{2k+1}=231 is a legal infinite execution, so T fails and TC fails. Neither one successful path nor PC yields total correctness (the misconception identified in the MKO).
S14 · implies
Before
M'':\ \mathrm{Halt}''=\{s\mid x_1<x_2\}=\{123,132,231\}After
321\to 231\in\mathrm{Halt}'',\ \neg Q(231)\ \Rightarrow\ \neg\mathrm{PC},\ \neg\mathrm{TC}\ \text{for}\ M''Conditions: none
Rule: quantifier_negation · Uses: G3, G2, S02
Leaf basis: quantifier_negation + mko_algorithm_correctness_def
In M″ there are only two maximal executions from 321: 321→231 (231 has 2<3, so it is in Halt″ and stops) and 321→312→132 (132 is in Halt″ and stops). Both stop, so T holds; but the halt state 231 is not increasing (3>1), so Q(231) is false, PC fails, and TC fails too. Termination by itself does not guarantee correctness.
Substeps and lemmas
S03.1 · implies
Before
\neg(x_1>x_2)\ \wedge\ \neg(x_2>x_3)
After
x_1<x_2<x_3
Conditions: x_1,x_2,x_3\ \text{distinct}
Rule: order_basics · Uses: order_basics, contrapositive
Leaf basis: order_basics + contrapositive
Prove the contrapositive: if there is no adjacent inverted pair, then s∈Halt. The three entries of a permutation are distinct, so by trichotomy 'not x1>x2' with x1≠x2 gives x1<x2; likewise x2<x3. So x1<x2<x3.
S03.2 · implies
Before
x_1<x_2<x_3,\ \{x_1,x_2,x_3\}=\{1,2,3\}After
(x_1,x_2,x_3)=(1,2,3)\in\mathrm{Halt}Conditions: none
Rule: order_basics · Uses: S03.1, order_basics
Leaf basis: order_basics + contrapositive
x1 is smaller than the other two entries (x1<x2 and, by transitivity, x1<x3), so x1 is the least element 1 of {1,2,3}; x3 is larger than the other two, so x3=3; what remains is x2=2. Hence s=123∈Halt. S03.1 and S03.2 together prove L_succ by contraposition.
S05.1 · implies
Before
x_1>x_2,\ s'=(x_2,x_1,x_3)
After
\mathrm{inv}(s')=0+[x_2>x_3]+[x_1>x_3]=\mathrm{inv}(s)-1Conditions: x_1>x_2
Rule: def_unfold · Uses: S04, G1
Leaf basis: def_unfold + add_comm + order_basics
Swap the first two entries: inv(s′)=[x2>x1]+[x2>x3]+[x1>x3]. Since x1>x2, [x2>x1]=0. And inv(s)=[x1>x2]+[x1>x3]+[x2>x3]=1+[x1>x3]+[x2>x3]. The remaining two terms only change places (commutativity of addition), so inv(s′)=inv(s)−1.
S05.2 · implies
Before
x_2>x_3,\ s'=(x_1,x_3,x_2)
After
\mathrm{inv}(s')=[x_1>x_3]+[x_1>x_2]+0=\mathrm{inv}(s)-1Conditions: x_2>x_3
Rule: def_unfold · Uses: S04, G1
Leaf basis: def_unfold + add_comm + order_basics + case_analysis
Swap the last two entries: inv(s′)=[x1>x3]+[x1>x2]+[x3>x2]. Since x2>x3, [x3>x2]=0, while inv(s)=[x1>x2]+[x1>x3]+1. So inv(s′)=inv(s)−1. S05.1 and S05.2 cover both kinds of edge in M, proving L_rank.