# Abstract computational model: truncating halt edges, computing reachability and separating halting, stuck and non-terminating runs in a seven-state model [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-computational-model/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-computational-model-01 · production-20261019-adopted-96 ## Goal and scope Given the finite model (S,Init,Step,Halt) with S={s0,s1,s2,s3,s4,s5,s6}, Init={s0}, Halt={s3} and raw edge data {(s0,s1),(s0,s2),(s1,s3),(s1,s5),(s2,s4),(s4,s2),(s3,s6)}: truncate edges out of halt states as the MKO requires, compute the reachable set by fixpoint iteration, identify halt states, stuck states and reachable cycles, exhibit legal halting, stuck and infinite executions, rule out three illegal traces, and explain why depth-bounded exploration that has not exhausted the reachable graph cannot certify termination of all maximal executions merely from the absence of an observed counterexample. Works inside the MKO's scope: S is an explicitly given finite set of states and Step is a directed relation that may be nondeterministic (assumption a1); reaching Halt stops execution, and edges out of halts are truncated before analysis (assumption a2). Effective encodings, fairness and the layering of deterministic and nondeterministic models are not treated, and the canonical MKO and its English edition are not changed. ## Givens and symbols - set_operations_def - cartesian_product_def - subset_def - nat_induction - finite_counting_basics - G1 — S={s0,s1,s2,s3,s4,s5,s6}, Init={s0}, Halt={s3} (MKO assumption a1: S is explicitly finite). - G2 — Raw edge data E_raw={(s0,s1),(s0,s2),(s1,s3),(s1,s5),(s2,s4),(s4,s2),(s3,s6)}. - G3 — Execution conventions (MKO assumption a2 and paragraph 2): before analysis, delete every edge leaving a Halt state to obtain Step. An execution is a sequence of states (t_i) indexed by an initial segment of ℕ (finite or all of ℕ), with t_0∈Init and (t_i,t_{i+1})∈Step for consecutive terms; it ends on entering Halt. A finite execution is maximal if its last state has no Step-successor; a finite maximal execution halts if its last state is in Halt and is stuck otherwise; infinite executions are also maximal. Extendible finite prefixes remain legal executions, but not having reached Halt yet does not make such a prefix a counterexample to universal termination. Universal termination below quantifies over maximal executions from Init. - S — the state set {s0,s1,s2,s3,s4,s5,s6} - \mathrm{Init},\ \mathrm{Halt} — the initial and halting state sets - E_{\mathrm{raw}} — the raw edge data - \mathrm{Step} — the transition relation after truncation - \mathrm{Post}(s) — the successor set Step[{s}] of s - R_k — the round-k reachable set (at most k steps) - \mathrm{Reach} — the set of states reachable from Init ## Rules and sources - set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A. - cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d. - subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B). - nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀. - finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x). - set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements. - exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x). - case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility. - quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x). - mko_computational_model_def · cited — The finite abstract model in this entry is (S,Init,Step,Halt), with Init,Halt⊆S and Step⊆S×S. Executions start in Init and follow Step; a stuck state without successors is not automatically a member of Halt. · mko-computational-model - mko_relation_def · cited — A binary relation R from A to B is a subset of A×B; its image of C is R[C]={y∈B: there exists x∈C with (x,y)∈R}. · mko-relation - reach_def · prerequisite — Reachability: a state s is reachable from Init if there are k≥0 and a finite path of states u_0, u_1 up to u_k with u_0∈Init, u_k=s and every consecutive pair in Step (k=0 means zero steps, i.e. s∈Init). Reach is the set of all reachable states. - L_fix · lemma — Let R_0=Init and R_{k+1}=R_k∪Step[R_k]. Then (i) for every k, R_k is exactly the set of states reachable in at most k steps; (ii) if R_{m+1}=R_m for some m, then Reach=R_m. ## Main derivation S01 · impliesBefore \mathrm{Init}=\{s_0\},\ \mathrm{Halt}=\{s_3\},\ E_{\mathrm{raw}} After \mathrm{Init},\mathrm{Halt}\subseteq S,\ E_{\mathrm{raw}}\subseteq S\times S Conditions: none Rule: subset_def · Uses: G1, G2 Leaf basis: subset_def + cartesian_product_def + mko_computational_model_def First check that the data form a model in the MKO's sense: s0 and s3 lie in S, so Init, Halt⊆S; each of the seven ordered pairs of E_raw has both components in S, so E_raw⊆S×S. Ordered pairs keep their direction; for example (s2,s4) and (s4,s2) are two different edges. S02 · impliesBefore E_{\mathrm{raw}} After \mathrm{Step}=E_{\mathrm{raw}}\setminus\{(s_3,s_6)\}=\{(s_0,s_1),(s_0,s_2),(s_1,s_3),(s_1,s_5),(s_2,s_4),(s_4,s_2)\} Conditions: \mathrm{Halt}=\{s_3\} Rule: set_operations_def · Uses: S01, G3 Leaf basis: set_operations_def + numeric_evaluation By MKO assumption a2, delete every edge whose source is a Halt state. Of the seven edges only (s3,s6) starts at s3∈Halt; deleting it leaves 6 edges. Although the data contain (s3,s6), the model says execution stops on reaching s3, so this edge is not part of the execution semantics. S03 · impliesBefore \mathrm{Post}(s)=\mathrm{Step}[\{s\}] After \mathrm{Post}:\ s_0\mapsto\{s_1,s_2\},\ s_1\mapsto\{s_3,s_5\},\ s_2\mapsto\{s_4\},\ s_4\mapsto\{s_2\},\ s_3,s_5,s_6\mapsto\varnothing Conditions: none Rule: mko_relation_def · Uses: S02, mko_relation_def Leaf basis: mko_relation_def + set_builder For each state collect the targets of the Step edges starting there. s0 and s1 each have two successors, so the model is nondeterministic; s3, s5 and s6 have no successors. This successor table underlies every later computation. S04 · theorem_applicationBefore R_0=\mathrm{Init},\ R_{k+1}=R_k\cup\mathrm{Step}[R_k] After R_{m+1}=R_m\ \Rightarrow\ \mathrm{Reach}=R_m Conditions: S\ \text{finite} Rule: L_fix · Uses: S03, reach_def Leaf basis: nat_induction + set_operations_def + reach_def Reachability is the closure under zero or more Step moves starting from Init (MKO paragraph 1). Apply Lemma L_fix (proved in S04.1 and S04.2): add successors round by round, and as soon as a round adds nothing, the current set is Reach. Since R_k is increasing inside the finite S, it must stop growing within |S|=7 rounds. S05 · impliesBefore R_0=\{s_0\} After R_1=\{s_0,s_1,s_2\},\ R_2=\{s_0,s_1,s_2,s_3,s_4,s_5\},\ R_3=R_2\ \Rightarrow\ \mathrm{Reach}=R_2 Conditions: none Rule: L_fix · Uses: S03, S04 Leaf basis: set_operations_def + mko_relation_def + numeric_evaluation R_1=R_0∪Post(s0)={s0,s1,s2}. R_2=R_1∪Post(s0)∪Post(s1)∪Post(s2)={s0,s1,s2}∪{s1,s2}∪{s3,s5}∪{s4}={s0,s1,s2,s3,s4,s5}. R_3 further adds Post(s3)=∅, Post(s4)={s2} and Post(s5)=∅, giving no new state, so R_3=R_2. By L_fix, Reach=R_2 with 6 states; s6 is unreachable. S06 · impliesBefore E_{\mathrm{raw}}[R_2] After s_6\in E_{\mathrm{raw}}[R_2]\ \text{but}\ s_6\notin\mathrm{Reach} Conditions: none Rule: set_operations_def · Uses: G2, S05 Leaf basis: set_operations_def + mko_relation_def Contrast: if truncation is forgotten and E_raw is used directly, round 3 adds s6 through (s3,s6), giving 'all 7 states reachable' and treating s3 as a state that can continue. That contradicts MKO assumption a2. In the correct analysis s6 is unreachable and s3 is an endpoint of execution. S07 · impliesBefore \mathrm{Reach}=\{s_0,s_1,s_2,s_3,s_4,s_5\} After \mathrm{Reach}\cap\mathrm{Halt}=\{s_3\},\ \{s\in\mathrm{Reach}\setminus\mathrm{Halt}\mid\mathrm{Post}(s)=\varnothing\}=\{s_5\} Conditions: none Rule: set_builder · Uses: S03, S05, G1 Leaf basis: set_builder + mko_computational_model_def Among the reachable states, only s3 is in Halt. The only state not in Halt and without successors is s5: it is a stuck state. s3 also has no successors, but it is in Halt, so it halts rather than gets stuck; conversely, having no successors does not make s5 a halt state (the MKO statement). s0, s1, s2 and s4 all have successors. S08 · impliesBefore (s_0,s_1,s_3) After \text{legal execution that halts at}\ s_3 Conditions: none Rule: mko_computational_model_def · Uses: G3, S02 Leaf basis: mko_computational_model_def + exists_intro Check the trace (s0,s1,s3): the first state s0∈Init; (s0,s1) and (s1,s3)∈Step; the last state s3∈Halt, where execution ends. This is a legal halting execution. S09 · impliesBefore (s_0,s_1,s_5) After \text{legal maximal execution, stuck at}\ s_5\notin\mathrm{Halt} Conditions: none Rule: mko_computational_model_def · Uses: G3, S02, S07 Leaf basis: mko_computational_model_def + exists_intro (s0,s1,s5): s0∈Init and (s0,s1), (s1,s5)∈Step, so it is legal; Post(s5)=∅, so it cannot continue and is maximal; s5∉Halt, so it is stuck rather than halted. S10 · case_splitBefore t_0=s_0,\ t_{2k+1}=s_2,\ t_{2k+2}=s_4\ (k\ge 0) After \forall n\ge 0,\ (t_n,t_{n+1})\in\mathrm{Step},\ t_n\notin\mathrm{Halt} Conditions: none Rule: case_analysis · Uses: G3, S02, G1 Leaf basis: case_analysis + nat_induction + mko_computational_model_def Define a sequence indexed by all of ℕ: t0=s0, odd positions t_{2k+1}=s2, positive even positions t_{2k+2}=s4. Check consecutive pairs for every n in three cases: for n=0, (s0,s2)∈Step; for n=2k+1, (t_n,t_{n+1})=(s2,s4)∈Step; for n=2k+2, n+1=2(k+1)+1, so t_{n+1}=s2 and (s4,s2)∈Step. The three cases cover every n≥0. All states of the sequence lie in {s0,s2,s4}, disjoint from Halt, so the execution never ends: it is a legal infinite execution, coming from the reachable non-halting cycle s2→s4→s2. S11 · impliesBefore (s_0,s_3),\ (s_1,s_3),\ (s_0,s_1,s_3,s_6) After \text{none is a legal execution} Conditions: none Rule: mko_computational_model_def · Uses: G3, S02, G1 Leaf basis: mko_computational_model_def + quantifier_negation Three illegal traces, each violating one condition: in (s0,s3), (s0,s3)∉Step; (s1,s3) starts at s1∉Init; (s0,s1,s3,s6) continues after entering s3∈Halt, and (s3,s6) has been truncated and is not in Step (MKO paragraph 2: entering Halt ends the execution). S12 · impliesBefore \text{stuck execution (S09)},\ \text{infinite execution (S10)} After \neg(\text{every maximal execution from Init halts}) Conditions: none Rule: quantifier_negation · Uses: S09, S10 Leaf basis: quantifier_negation + exists_intro 'Every maximal execution from Init halts' is a universal statement. S09 gives a stuck finite maximal execution and S10 an infinite maximal execution; either refutes it. Thus this model is not universally terminating, although S08 gives one halting run. An extendible finite prefix is not by itself a counterexample to this property. S13 · impliesBefore \text{prefixes of depth}\ 1:\ (s_0,s_1),\ (s_0,s_2) After \text{no cycle or stuck state visible at depth 1, yet termination fails} Conditions: none Rule: quantifier_negation · Uses: S03, S12 Leaf basis: quantifier_negation + mko_computational_model_def At depth 1 the observed prefixes are only (s0,s1) and (s0,s2), with no cycle or stuck state yet displayed. Inferring that every maximal execution halts merely from these observations would be wrong: S12 supplies counterexamples. The rejected inference uses observations that have not exhausted the reachable graph; it does not reject every finite exploration certificate. Exhaustively exploring a finite reachable graph and checking cycles and non-Halt dead ends can support the corresponding decision. The complete graph here (S05, S07, S10) reveals both risks. ## Substeps and lemmas S04.1 · induction_stepBefore R_k After R_k=\{s\mid s\ \text{reachable in at most}\ k\ \text{steps}\} Conditions: none Rule: nat_induction · Uses: reach_def, nat_induction, set_operations_def Leaf basis: nat_induction + set_operations_def + reach_def + mko_relation_def Induct on k. k=0: the states reachable in zero steps are exactly Init=R_0. Assume the claim for k. If s is reachable in at most k+1 steps, either it is reachable in at most k steps (so in R_k) or the last move of the path goes from some u reachable in at most k steps to s, i.e. s∈Step[R_k]. Conversely, elements of R_k are reachable in at most k steps, and elements of Step[R_k] are one move from some u∈R_k, hence reachable in at most k+1 steps. So R_{k+1} is exactly the set reachable in at most k+1 steps, proving (i). S04.2 · impliesBefore R_{m+1}=R_m After \forall k\ge m,\ R_k=R_m;\ \mathrm{Reach}=\textstyle\bigcup_k R_k=R_m Conditions: none Rule: nat_induction · Uses: S04.1, nat_induction Leaf basis: nat_induction + set_extensionality + set_operations_def If R_{m+1}=R_m then R_{m+2}=R_{m+1}∪Step[R_{m+1}]=R_m∪Step[R_m]=R_{m+1}=R_m, and by induction R_k=R_m for all k≥m. Every reachable state has a path of some length k, so by (i) it lies in R_k; since R_k is increasing, it lies in R_{max(k,m)}=R_m. Conversely every element of R_m is reachable. Hence Reach=R_m, proving (ii). ## Reverse audits - S13 · premise_audit · S03, S12 — This step rejects inferring termination of all maximal executions merely from the absence of counterexamples in a non-exhaustive depth-bounded observation. It neither rejects complete finite-graph certificates nor claims a general termination decision method for programs. - S12 · premise_audit · S09, S10, quantifier_negation — Refuting a universal statement needs one counterexample; here there are two of different kinds, matching the two termination risks in MKO paragraph 3. - S11 · premise_audit · G3, S02, G1 — Each trace is ruled out by naming one violated condition. - S10 · premise_audit · G3, S02, case_analysis — The case split must cover every n: 0, positive odd, positive even, which are mutually exclusive and exhaustive. The index identity (2k+2)+1=2(k+1)+1 is checked as a degree-one polynomial identity in N5. - S09 · premise_audit · G3, S02, S07 — Being stuck needs two facts: no successor, and not in Halt. - S08 · premise_audit · G3, S02 — The three legality conditions are checked one by one. One halting execution does not mean every execution halts (nondeterminism). - S07 · premise_audit · S03, S05, G1, mko_computational_model_def — The classification uses only the given list Halt and the successor table, never inferring membership in Halt from having no successors. - S06 · premise_audit · G2, S02, S05 — This step only shows that the result differs with and without truncation, to justify S02; the E_raw result is not taken as a conclusion about the model. - S05 · premise_audit · S03, L_fix — Each round uses the complete successor table; the stop test is the set equality R_3=R_2 (N3, N4 recompute the sizes). - S04.2 · premise_audit · S04.1, nat_induction, set_extensionality — The argument needs R_k to be increasing (R_{k+1}⊇R_k by definition) and (i). - S04.1 · premise_audit · reach_def, nat_induction, set_operations_def, mko_relation_def — Both inclusions are proved in the induction step; the base uses zero-step paths. - S04 · premise_audit · L_fix, reach_def — The stopping condition must be the set equality R_{m+1}=R_m, not an observation such as 'no new cycle seen in some round'. - S03 · premise_audit · S02, mko_relation_def — Each of the six edges is assigned to its source exactly once; 2+2+1+1=6 agrees with the edge count (N2). - S02 · premise_audit · G3, set_operations_def — Each edge's source must be checked against Halt; N1 recomputes the edge count 7−1=6. - S01 · premise_audit · G1, G2, subset_def, cartesian_product_def — Every element and every edge is checked; this step derives no execution property. ## Error controls and negative controls No outgoing edge does not mean haltingThe misconception identified in the MKO is calling a state without outgoing edges a halt automatically. s5 has no successors but is not in Halt, so (s0,s1,s5) is stuck, not halted (S07, S09). Halting is decided only by the given list Halt. Non-exhaustive finite prefixes do not certify terminationDepth-1 exploration displays neither the cycle s2→s4→s2 nor the stuck s5, yet non-halting maximal executions exist (S12, S13). If the reachable graph has not been exhausted, absence of an observed counterexample is not a termination proof. A complete finite reachable graph permits cycle and non-Halt dead-end checks; general programs still require suitable proof methods. Truncate edges out of halts firstThe raw data contain (s3,s6). Without truncation, s6 would be wrongly counted as reachable and (s0,s1,s3,s6) wrongly accepted as legal (S06, S11). MKO assumption a2 requires deleting such edges before analysis. - s5 has no successor, so s5 is a halt state → reject — Halt={s3}; s5 is a stuck state, not a halt state. - Every consecutive pair of (s0,s1,s3,s6) is in the raw data, so it is a legal execution → reject — Execution ends on entering s3∈Halt, and (s3,s6) has been truncated. - Exploring to depth 1 found no cycle, so every execution terminates → reject — The sequence that leaves s0 and then alternates between s2 and s4 forever is an infinite execution, and (s0,s1,s5) is a stuck execution. - s6 is reachable because (s3,s6) is in the data → reject — After truncation no edge enters s6, and Reach={s0,s1,s2,s3,s4,s5}. ## Result and limitations After truncation Step has 6 edges; Reach={s0,s1,s2,s3,s4,s5} and s6 is unreachable. s3 is the only reachable halt state, s5 is stuck (no successors but not in Halt), and {s2,s4} is a reachable non-halting cycle. (s0,s1,s3) halts, (s0,s1,s5) is stuck, and the sequence that goes from s0 and then alternates between s2 and s4 forever is an infinite execution; (s0,s3), (s1,s3) and (s0,s1,s3,s6) are illegal. So not every maximal execution from Init halts, and exploration to depth 1 cannot reveal this. - The layered treatment of deterministic and nondeterministic models, maximal executions, fairness and effective encodings (MKO formal next) is not built here; this guide handles one explicit finite model only. ## Verification and source binding 5 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 4e735eff3b7dce6a70f861ddcd8dc409e5a688e22cfd99ecfa7115e5ad0c3ebc - original source SHA-256: e947537df405a61ccf81d4f1a305ce5e409796bc956b63e5b8517923dab8e201 - Lean: NOT_RUN · independent AI: NOT_MEASURED [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-computational-model-01.json)