# Decision problem: proving that a trial-division procedure is a decider on an explicit finite input set

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-decision-problem/)

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-decision-problem-01 · production-20261019-adopted-96



## Goal and scope

Take the input set X={0,1,2,3,4,5,6,7,8,9}, the specification P(x): 'x is prime', and the yes-instance set Y={x∈X ∣ P(x)}. In the explicit while-program model W, prove that the trial-division procedure D1 terminates on every x∈X and that D1(x)=true exactly when x∈Y, so D1 is a decider for (X,Y); then show that D2, which halts only on yes-instances, and D3, which tests only parity, are not deciders.

Works inside the MKO's scope: a fixed finite input set X with Y⊆X (assumption a1) and an explicit computational model and input representation (assumption a2). The conclusion covers this X only; it draws no conclusion about computability or undecidability over all natural numbers, does not treat the general theory of semi-decision procedures, and does not change the canonical MKO or its English edition.





## Givens and symbols


- set_builder
- divides_def
- order_basics
- numeric_evaluation
- prime_def
- while_semantics


- G1 — The input set X={0,1,2,3,4,5,6,7,8,9} is an explicitly listed finite set; the specification P(x) is 'x is prime'; the yes-instance set is Y={x∈X ∣ P(x)}, so Y⊆X (MKO assumption a1).
- G2 — Computational model W: deterministic while-programs whose states are values of natural-number variables. The input x is given as a natural-number value (for example its binary numeral). The basic operations are comparing two numbers, adding 1, the remainder x mod d for d≥1, assignment and 'return v', each counted as one step. A program terminates on x if it executes a return after finitely many steps, and its output is the returned value; a run that never executes return does not terminate (MKO assumption a2).
- G3 — Candidate procedures. D1(x): line 1, if x<2 then return false; line 2, d:=2; line 3, while d<x do (if x mod d=0 then return false; d:=d+1); line 4, return true. D2(x): run the text of D1; if D1 would return true, return true; if D1 would return false, instead execute 'while true do skip' (never returns). D3(x): return (x mod 2=1).


- X — the input set {0,1,2,3,4,5,6,7,8,9}
- P(x) — the specification: x is prime
- Y — the yes-instance set {x∈X ∣ P(x)}
- W — the explicit while-program computational model
- D_1,D_2,D_3 — the three candidate procedures
- x \bmod d — the remainder of x on division by d (d≥1)
- d\mid x — d divides x





## Rules and sources


- set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
- divides_def · prerequisite — Divisibility: for integers a, b, a∣b means there is an integer k with b=ak.
- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- 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₀.
- 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.
- iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold.
- contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
- forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- 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_decision_problem_def · cited — A decision problem is an input set X with a yes-instance set Y⊆X, equivalently a proposition-valued specification P:X→Prop. Relative to an explicit computational model, a decider D must terminate on every x∈X and satisfy D(x)=true exactly when x∈Y. · mko-decision-problem
- prime_def · prerequisite — A natural number p is prime exactly when p≥2 and its only positive divisors are 1 and p. Since a positive divisor d of p≥1 satisfies d≤p (p=dk with k≥1), this is equivalent to: p≥2 and no integer d with 2≤d≤p−1 divides p. For natural x and d≥1, d∣x exactly when x mod d=0.
- while_semantics · prerequisite — Semantics of W: statements run in order; 'if B then S' runs S only when B is true; 'while B do S' tests B, runs S and tests again when B is true, and continues after the loop when B is false; 'return v' ends the run with output v; 'while true do skip' never ends.
- finite_exhaustion · prerequisite — For an explicitly listed finite set D, ∀x∈D, Q(x) is equivalent to the conjunction of Q(d) over the listed elements d; checking every element proves it, checking only some does not, and the conclusion covers D only.
- L_loop_term · lemma — For every natural number x≥2, the while loop of D1 on x completes at most x−2 passes, so D1 terminates on x.
- L_loop_inv · lemma — For every natural number x≥2, whenever D1 on x tests d<x, we have 2≤d≤x and no integer e with 2≤e<d divides x.





## Main derivation

S01 · definitionBefore

P(x):\ x\ \text{is prime},\quad x\in X

After

Y=\{x\in X\mid P(x)\}

Conditions: X=\{0,1,2,3,4,5,6,7,8,9\}

Rule: set_builder · Uses: G1

Leaf basis: set_builder + def_intro

Write the problem as a pair (X,Y): Y is defined from the specification P by set-builder notation, and x∈Y means x∈X and P(x). Y describes the correct answers and does not depend on any candidate program; D1, D2 and D3 are implementations to be compared with Y later (MKO paragraph 1: specification and implementation are separate).



S02 · impliesBefore

Y=\{x\in X\mid P(x)\}

After

Y=\{2,3,5,7\}

Conditions: X\ \text{finite and listed}

Rule: prime_def · Uses: S01, G1

Leaf basis: prime_def + divides_def + numeric_evaluation + finite_exhaustion

Decide P(x) for each of the ten elements of X. X is an explicitly listed finite set, so checking every element yields the complete list of Y; the details are in S02.1 to S02.3. The result is Y={2,3,5,7}.



S03 · equivalentBefore

D\ \text{decides}\ (X,Y)\ \text{in}\ W

After

(\forall x\in X,\ D\ \text{terminates on}\ x)\ \wedge\ (\forall x\in X,\ D(x)=\mathrm{true}\iff x\in Y)

Conditions: W\ \text{fixed (G2)}

Rule: def_unfold · Uses: G2, mko_decision_problem_def

Leaf basis: def_unfold + mko_decision_problem_def

Unfold the MKO's definition of a decider into two clauses: (T) termination on every x∈X; (C) the output is true exactly when x∈Y. Both clauses quantify over all of X and both are relative to the fixed model W. (T) and (C) are then proved separately for D1.



S04 · impliesBefore

x\in\{0,1\}

After

D_1\ \text{terminates on}\ x,\ D_1(x)=\mathrm{false},\ x\notin Y

Conditions: x<2

Rule: while_semantics · Uses: G3, S02.1

Leaf basis: while_semantics + prime_def

For x=0 or x=1 the test x<2 on line 1 is true, so D1 returns false immediately and terminates after finitely many steps. By S02.1 these two inputs are indeed not in Y, so the output agrees with the specification.



S05 · theorem_applicationBefore

x\in X,\ x\ge 2

After

D_1\ \text{terminates on}\ x\ \text{after at most}\ x-2\le 7\ \text{loop passes}

Conditions: x\ge 2

Rule: L_loop_term · Uses: G3, G1

Leaf basis: while_semantics + nat_induction + order_basics

Apply Lemma L_loop_term: for x≥2 the loop completes at most x−2 passes, after which the test d<x fails and line 4 returns true, unless some pass returns false earlier. The largest x in X is 9, so at most 7 passes. Together with S04, D1 terminates on every x∈X, so clause (T) holds.



S06 · theorem_applicationBefore

x\ge 2

After

\text{at every test of}\ d<x:\ 2\le d\le x\ \wedge\ \neg\exists e\,(2\le e<d\ \wedge\ e\mid x)

Conditions: x\ge 2

Rule: L_loop_inv · Uses: G3

Leaf basis: nat_induction + divides_def + while_semantics

Apply the loop invariant L_loop_inv: whenever d<x is tested, d lies between 2 and x and x has no divisor between 2 and d−1. The invariant records as a proposition what the loop has already checked, so that S07 and S08 can infer from the exit point whether x is prime.



S07 · impliesBefore

D_1(x)=\mathrm{true}

After

x\in Y

Conditions: none

Rule: prime_def · Uses: S04, S06, G3

Leaf basis: prime_def + order_basics + while_semantics

D1 outputs true only on line 4, and by S04 line 4 is not reached when x<2, so x≥2. Reaching line 4 means the test d<x failed; the invariant gives d≤x, so by trichotomy d=x. The invariant then says no e with 2≤e<x divides x, i.e. x has no divisor between 2 and x−1. By prime_def x is prime, so x∈Y.



S08 · impliesBefore

D_1(x)=\mathrm{false}

After

x\notin Y

Conditions: none

Rule: case_analysis · Uses: S04, S06, G3

Leaf basis: case_analysis + prime_def + divides_def + while_semantics

D1 outputs false in only two places. Case one: line 1, x<2, not prime (S04). Case two: in the loop with x mod d=0; the test d<x has just passed and the invariant gives d≥2, so d is a divisor with 2≤d≤x−1 and x is not prime. The two cases cover every 'return false' in the program, so x∉Y.



S09 · impliesBefore

D_1(x)=\mathrm{true}\Rightarrow x\in Y,\quad D_1(x)=\mathrm{false}\Rightarrow x\notin Y

After

\forall x\in X,\ D_1(x)=\mathrm{true}\iff x\in Y

Conditions: D_1\ \text{terminates on}\ x

Rule: iff_intro · Uses: S04, S05, S07, S08

Leaf basis: iff_intro + contrapositive + forall_intro

Take any x∈X. By S04 and S05, D1 terminates on x with output true or false. (⇒) is S07. (⇐) If x∈Y, the output cannot be false, for then S08 would give x∉Y, a contradiction; so the output is true. The two directions give ⇔; since x was arbitrary, generalization gives it for all x∈X, so clause (C) holds.



S10 · impliesBefore

(\forall x\in X,\ D_1\ \text{terminates})\ \wedge\ (\forall x\in X,\ D_1(x)=\mathrm{true}\iff x\in Y)

After

D_1\ \text{decides}\ (X,Y)\ \text{in}\ W

Conditions: none

Rule: and_intro_elim · Uses: S03, S04, S05, S09

Leaf basis: and_intro_elim + def_unfold + case_analysis

Clause (T) combines S04 (x<2) and S05 (x≥2), and these two cases cover every element of X; clause (C) is S09. Their conjunction folds back through the equivalence of S03: D1 is a decider for (X,Y) in W.



S11 · impliesBefore

x=0,1,2,3,4,5,6,7,8,9

After

D_1(x)=\mathrm{F},\mathrm{F},\mathrm{T},\mathrm{T},\mathrm{F},\mathrm{T},\mathrm{F},\mathrm{T},\mathrm{F},\mathrm{F}\ =\ [x\in Y]

Conditions: X\ \text{finite and listed}

Rule: finite_exhaustion · Uses: S02, S10, G3

Leaf basis: finite_exhaustion + numeric_evaluation + while_semantics

Cross-check: run D1 by hand on all ten inputs. For example x=9: at d=2, 9 mod 2=1; at d=3, 9 mod 3=0, return false; x=7: the remainders for d=2 to 6 are 1, 1, 3, 2, 1, then the test fails at d=7 and it returns true. The full table agrees entry by entry with membership in Y={2,3,5,7}. Because X is finite and fully listed, this table is by itself a complete check of clause (C) on X; but it covers X only (MKO assumption a2).



S12 · impliesBefore

x=4\in X:\ D_1\ \text{would return false}

After

D_2\ \text{does not terminate on}\ 4\ \Rightarrow\ \neg(\forall x\in X,\ D_2\ \text{terminates})

Conditions: none

Rule: quantifier_negation · Uses: S03, S02.2, G3

Leaf basis: quantifier_negation + while_semantics + divides_def

On x=4 the text of D1 finds 4 mod 2=0 at d=2 and would return false; D2 instead executes 'while true do skip' and never returns. So some x∈X makes D2 fail to terminate; by quantifier negation clause (T) fails and D2 is not a decider. D2 halts with true exactly on Y, so it is a semi-decision procedure for Y; this is the misconception the MKO names: accepting exactly the yes-instances alone does not ensure a total decider. D2 fails termination on no-instances, while D1 also accepts exactly the yes-instances but rejects and halts on the remaining inputs.



S13 · impliesBefore

D_3(x)=[x\bmod 2=1]

After

D_3(9)=\mathrm{true},\ 9\notin Y\ \Rightarrow\ \neg(\forall x\in X,\ D_3(x)=\mathrm{true}\iff x\in Y)

Conditions: none

Rule: quantifier_negation · Uses: S03, S02, G3

Leaf basis: quantifier_negation + numeric_evaluation

D3 terminates after finitely many steps, so (T) holds; but 9 mod 2=1 gives D3(9)=true while 9∉Y (S02.2), and also D3(2)=false while 2∈Y. A counterexample exists, so clause (C) fails and D3 is not a decider. Note that on the sample {3,4,5,6,7,8} D3 agrees with Y completely, so agreement on a sample does not prove agreement on the whole domain (MKO paragraph 2).







## Substeps and lemmas

S02.1 · impliesBefore

x\in\{0,1\}

After

0\notin Y,\ 1\notin Y

Conditions: x<2

Rule: prime_def · Uses: S01

Leaf basis: prime_def + order_basics

A prime must be at least 2; 0 and 1 are less than 2, so P(0) and P(1) are false and 0, 1 are not in Y.



S02.2 · impliesBefore

x\in\{4,6,8,9\}

After

4=2\cdot 2,\ 6=2\cdot 3,\ 8=2\cdot 4,\ 9=3\cdot 3\ \Rightarrow\ 4,6,8,9\notin Y

Conditions: 2\le d\le x-1

Rule: divides_def · Uses: S01

Leaf basis: divides_def + prime_def + numeric_evaluation

By the definition of divisibility, 2∣4, 2∣6, 2∣8 and 3∣9, and in each case 2≤d≤x−1. By the equivalent form in prime_def these four numbers are not prime and are not in Y.



S02.3 · impliesBefore

x\in\{2,3,5,7\}

After

2,3,5,7\in Y

Conditions: x\ge 2; x\bmod d\ne 0\ \text{for}\ 2\le d\le x-1

Rule: prime_def · Uses: S01

Leaf basis: prime_def + divides_def + numeric_evaluation

For x=2 the range 2≤d≤1 is empty; 3 mod 2=1; the remainders of 5 by 2, 3, 4 are 1, 2, 1; the remainders of 7 by 2, 3, 4, 5, 6 are 1, 1, 3, 2, 1. Each of these numbers is at least 2 and has no divisor between 2 and x−1, so by prime_def each is prime.



S05.1 · impliesBefore

d=2\ \text{at the first test}

After

\text{each pass either returns or replaces}\ d\ \text{by}\ d+1

Conditions: none

Rule: while_semantics · Uses: G3, while_semantics

Leaf basis: while_semantics

Line 2 sets d=2. The loop body has only two outcomes: if x mod d=0 it returns false and the run ends; otherwise it executes d:=d+1. No other statement in the body changes d.



S05.2 · induction_stepBefore

\text{after}\ k\ \text{completed passes without return:}\ d=2+k

After

\text{a pass starts only if}\ 2+k<x,\ \text{so at most}\ x-2\ \text{passes complete}

Conditions: x\ge 2

Rule: nat_induction · Uses: S05.1

Leaf basis: nat_induction + order_basics + while_semantics

Induct on k: for k=0, d=2; if d=2+k after k completed passes, one more completed pass gives d=2+(k+1) (S05.1). Pass number k can start only if the test d<x passes, that is 2+k<x, i.e. k≤x−3, so the possible passes are k=0 to x−3, which is x−2 passes. After the last one d=x, the test fails and line 4 returns. So the run ends after finitely many steps, proving Lemma L_loop_term.



S06.1 · induction_baseBefore

\text{first test},\ d=2

After

2\le 2\le x\ \wedge\ \{e:2\le e<2\}=\varnothing

Conditions: x\ge 2

Rule: nat_induction · Uses: G3, while_semantics

Leaf basis: nat_induction + order_basics

At the first test d=2. Since x≥2 we have 2≤d≤x; no integer e satisfies 2≤e<2, so 'no such e divides x' holds vacuously. The invariant holds initially.



S06.2 · induction_stepBefore

2\le d\le x,\ \neg\exists e\,(2\le e<d\wedge e\mid x),\ d<x,\ x\bmod d\ne 0

After

d'=d+1:\ 2\le d'\le x\ \wedge\ \neg\exists e\,(2\le e<d'\wedge e\mid x)

Conditions: d<x; x\bmod d\ne 0

Rule: nat_induction · Uses: S06.1, divides_def, while_semantics

Leaf basis: nat_induction + divides_def + order_basics + while_semantics

Suppose the invariant holds at a test, the test d<x is true, and the pass does not return, that is x mod d≠0, so d∤x. After the pass d′=d+1. From d<x we get d′≤x, and d′≥3≥2. Any e with 2≤e<d′ has either e<d (not a divisor by hypothesis) or e=d (just shown not to divide x). So the invariant holds at the next test. S06.1 and S06.2 together prove L_loop_inv.







## Reverse audits


- S13 · premise_audit · S02, quantifier_negation, numeric_evaluation — One counterexample refutes the universal clause (C) (recomputable as N8, N9). Conversely, agreement on a sample cannot prove (C), so only the counterexample direction is used.
- S12 · premise_audit · S03, quantifier_negation, G3 — One non-terminating input suffices to refute the universal clause (T). Nothing else about D2 is needed, although it also fails to terminate on 0, 1, 6, 8 and 9.
- S11 · premise_audit · S02, finite_exhaustion, numeric_evaluation — The table counts as a complete check only because it contains every element of X; a partial table would be a sample. It cannot be extrapolated to inputs outside X.
- S10 · sufficient_goal_reduction · S03, S05, S09, and_intro_elim — Goal G: D1 is a decider. Sufficient condition H: (T)∧(C), with H⇔G by S03. H is proved forwards in S04 to S09 from the program text and the definitions; G is never used as a premise.
- S09 · premise_audit · S05, S07, S08, iff_intro, contrapositive, forall_intro — The generic argument for D1 uses its proved termination: only when the result is known to be true or false does 'not false' imply true. D2 does return true on every yes-instance and does not violate that reverse implication; it diverges on no-instances and fails the separate total-termination clause (T) in S12.
- S08 · premise_audit · S04, S06, case_analysis, prime_def, divides_def — The case split must cover every 'return false' in the program, and the program text confirms there are only two. No converse is claimed here; it is handled in S09.
- S07 · premise_audit · S04, S06, prime_def, order_basics — It needs both parts of the invariant (d≤x and no small divisor) and that line 4 is reachable only through the loop exit. This step proves only 'output true ⇒ x∈Y'; the converse is handled separately in S09.
- S06.2 · premise_audit · S06.1, divides_def, while_semantics, order_basics — Preservation needs the condition that the pass did not return; if it did, the run has ended and there is no next test to preserve the invariant for. Passing from d<x to d+1≤x uses the order of the integers.
- S06.1 · premise_audit · G3, while_semantics, order_basics — It needs x≥2 and the assignment on line 2; this is the base of the induction.
- S06 · premise_audit · L_loop_inv, G3 — It needs x≥2 (otherwise line 1 has already returned and the loop never runs); the lemma is proved in S06.1 and S06.2 by establishment and preservation, not by checking a few sample states.
- S05.2 · premise_audit · S05.1, nat_induction, order_basics — It needs 'add 1 per pass' from S05.1 and natural induction. The bound x−2 is only an upper bound; it is not claimed that every input uses all passes; for example x=9 returns false at d=3.
- S05.1 · premise_audit · G3, while_semantics — Read directly from the program text and the semantics; it does not claim every pass returns, only that the sole change to d is adding 1.
- S05 · premise_audit · L_loop_term, G3 — It needs the lemma's hypothesis x≥2; the lemma is proved in S05.1 and S05.2. Termination comes from d increasing by 1 per pass with an upper bound, not from having tried a few inputs that happened to stop.
- S04 · premise_audit · G3, while_semantics, S02.1 — It needs the program text, the semantics of 'if', and the decision in S02.1. It handles only x<2; the case x≥2 is handled in S05 to S08.
- S03 · inverse_equivalence · mko_decision_problem_def, def_unfold — Unfolding and folding a definition are inverse moves, so the two sides are equivalent. Satisfying only one clause (for example halting only on yes-instances) does not make a decider.
- S02.3 · premise_audit · prime_def, numeric_evaluation — To show there is no divisor, every d from 2 to x−1 must be checked, not only d=2 (N3 and N4 are the complete finite checks over exactly these d).
- S02.2 · premise_audit · divides_def, prime_def — Each number needs only one divisor witness between 2 and x−1 (recomputable as N1, N2). The witness must lie in that range: d=1 and d=x always divide x and do not count.
- S02.1 · premise_audit · prime_def — Only the clause p≥2 of the definition is used. No converse is claimed: x≥2 alone does not make x prime.
- S02 · premise_audit · S01, prime_def, finite_exhaustion — It needs the definition of prime and the complete list of X. The conclusion is an equality of sets, and it rests on all ten elements having been checked; leaving out any element would not justify the equality.
- S01 · premise_audit · G1, set_builder, mko_decision_problem_def — This step only names and derives no new fact. Y⊆X holds because set-builder notation only collects elements of X; Y may not be defined backwards from the outputs of some program.





## Error controls and negative controls

A semidecision procedure need not be a deciderThe misconception identified in the MKO is treating a procedure that accepts only yes-instances as a total decider. D2 halts with true on every x∈Y and seems to 'get every yes right', but it never halts on x=4, violating clause (T). A decider must terminate with an answer on every input; the (⇐) direction of S09 holds only because of termination.

The limits of sampling and of finite tablesD3 agrees with Y on {3,4,5,6,7,8} but is wrong on 2 and 9: agreement on a sample does not prove the whole domain. On the other hand, the complete table in S11 counts as a proof only because X is finite and fully listed, and it covers X only; it does not establish primality testing on all natural numbers (MKO assumption a2 and paragraph 3).

The specification comes before the implementationY is defined by the specification P (S01, S02); it must not be defined as 'the inputs on which D1 outputs true', or every program would be 'correct' automatically. Correctness is always a comparison between a program and an independent specification.


- D2 outputs true on every x∈Y, so D2 decides (X,Y) → reject — D2 never terminates on x=4, violating the clause 'terminates on every x∈X'; it is only a semi-decision procedure.
- D3 agrees with Y on 3, 4, 5, 6, 7 and 8, so D3 is a decider on X → reject — D3(9)=true but 9=3·3∉Y; D3(2)=false but 2∈Y.
- D1's table agrees with Y on X={0,1,2,3,4,5,6,7,8,9}, so the table proves primality testing on all natural numbers → reject — A finite table establishes only that finite X (MKO assumption a2); a claim over all natural numbers is a new claim needing an argument for every input and a fixed representation.
- D1 is not a decider for (X,Y) because it does not handle the input −3 → reject — −3∉X; inputs outside the domain are not part of the problem (MKO paragraph 2), and a decider only has to terminate correctly on X.





## Result and limitations

In the model W, Y={2,3,5,7}, and the trial-division procedure D1 terminates on every x∈X with D1(x)=true ⇔ x∈Y, so D1 is a decider for (X,Y). D2 halts only on yes-instances and is a semi-decision procedure, not a decider; D3 always terminates but answers wrongly on 9 and 2, so it is not a decider either. The conclusion covers X={0,1,2,3,4,5,6,7,8,9} only.


- The argument in S05 to S09 uses x≤9 only for the pass bound; claiming that D1 decides primality on all natural numbers would require fixing the representation of every natural number in W and stating and reviewing that claim separately, which this guide does not do.
- The model W is described in prose; the semantic bridge to a formal model such as Turing machines (MKO formal next) is not built here.





## Verification and source binding

9 declared checks for this guide; only the listed expressions are covered.


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 8c1298a85a7e15de57c25d5f9f4225a8395a15a17de10382e9374e299407f3f6
- original source SHA-256: 50e70577152ab8bc0e89748c30ba626dddea3df36bb2c9b31d40e16c3abd912b
- 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-decision-problem-01.json)