How a pencil, a word, and an ordered list of substitutions became a model of computation — and grew into a school of mathematics that refuses to say “exists” without showing you the thing.
Before the machines, before the philosophy, before the Russian school of constructive mathematics, take a pencil. Write a word. Cross out one piece. Write another piece in its place. That single gesture is the only physical act this whole book needs.
Andrey Andreyevich Markov Jr. (1903–1979) — son and full namesake of the great Petersburg mathematician, and a major mathematician in his own right — made a bold proposal: perhaps the vague human word algorithm could be pinned down with almost nothing more than a finite alphabet, a finite ordered list of substitutions, and a strict rule about which substitution fires first. He called the results normal algorithms, and in 1954 he devoted a monograph of nearly four hundred pages to their theory.
Most of what follows is Markov's mathematics: the machine itself, the theorems it made possible — including several notable impossibility results — and the school of constructive mathematics that grew around one stubborn question: what should “there exists” mean when a proof is required to compute? A short coda at the end follows the same rewriting instinct one generation forward, into Valentin Turchin's language Refal.
Five kinds of box recur. Learn them once:
The live panels are not animations pretending to be algorithms. They are small interpreters written for this page, and every program they contain was machine-tested before being printed here. Press the buttons. Change the words. Break them.
Suppose our alphabet contains three symbols: a, b, and c. A word is a finite row of them: abba, c, the empty word, whatever. Now write one instruction:
ab → c means: find ab inside the current word and replace it by c.On the word abab, the instruction could apparently act in two places. But an algorithm cannot shrug and say “whichever.” It must say exactly what happens next. Markov's mechanism decides for us: replace the leftmost occurrence.
The little machine below adds unary numbers. Three is 111; two is 11. The sum is written 111+11 — one plus sign between two blocks of strokes, and that shape is part of the specification. The first rule shuffles the plus rightward, one step at a time. The second rule erases it and halts immediately.
Input contract: words of the form 1…1+1…1 (exactly one plus). Edit it, then step through the ordered substitutions. ε means “write nothing.” The dot ● marks a terminal substitution that stops the machine.
111+11 — the first rule sees 1+ and swaps it to +1.11+111 — the plus has moved one place right.1+1111+1111111111 — the terminal rule + →● ε fires: erase the plus and stop. Four rewrite steps; five strokes remain, and 3 + 2 = 5.“Apply a rewrite rule” sounds simple until two rules match, or one rule matches twice, or a rule says we are done. A normal algorithm gets its exactness from four decisions. Forget any one of them and you have described a family of possible computations, not this single deterministic machine.
The list is not a bag: rule 1 is privileged over rule 2, rule 2 over rule 3, and so on, and this ordering is not an implementation detail but part of the program itself. The demo below proves it: same word, same two rules, and swapping the order changes the answer.
Input is always ab. Two rules: ab → x and a → y. Swap which one comes first and watch the result flip.
The machine scans from the top and stops searching the rule list as soon as it finds a left side that occurs in the word; a later rule may match more characters, look cleverer, or lead to a nicer answer, but none of that matters, because earlier means earlier.
Once the rule has been chosen, scan the word from the left and replace only the first occurrence you find: there is no parallel rewriting, so exactly one spot in the word changes per step.
An ordinary substitution says “rewrite, then begin another step.” A terminal substitution says “rewrite, and this result is the output.” Books use several notations for the terminal arrow or dot; the notation varies, the control idea does not.
We can now say the thing without metaphor: the definition itself is small, and its power comes not from a rich instruction set but from iteration — a tiny exact step, repeated without a promised bound.
u → v and terminal substitution formulas u →● v, where u and v are words over that alphabet. To run it on an input word: scan the formulas in order; choose the first formula whose left side u occurs in the word; replace the leftmost occurrence of u by v. If the formula was terminal, halt with the new word; otherwise repeat from the top. If no left side occurs at all, halt with the current word.One more possibility remains, and it matters: the rewrites may continue forever.
One rule: a → aa. There is always another a to rewrite, so this machine never halts. The “step budget” slider only limits how many steps this page will watch; it does not make the algorithm stop.
Two rules for addition may look like a lucky accident. It is not: there are reusable idioms. The most important is the marker — a fresh symbol, outside the input alphabet, that acts as a cursor. Rules move the marker through the word, transforming letters as it passes; a final rule deletes it and halts. A marker is, in effect, a machine “head” built out of nothing but substitutions. The gallery below contains nine small programs; each was run against an exhaustive machine test before being printed on this page.
ab — no rule mentioning m applies, so the last rule ε → m fires: the empty word occurs at the far left, and inserting m there gives mab.mab — rule ma → bm: the marker eats an a, writes a b, and moves right: bmb.bmb — rule mb → am: bam.bam — the marker has reached the end, so only m →● ε applies: erase it and halt with ba.ε → m anywhere but last and it fires on every step, flooding the word with markers. Put m →● ε before the two travel rules and the marker dies at birth. The ordered list is doing the work a Turing machine does with states — which is a first hint of the equivalence coming in Chapter 5.At the raw level: a partial function from words to words. But words can encode numbers, tuples, formulas, graphs, proofs, even other programs — anything with a finite symbolic description. Unary numerals are clumsy but honest; binary is efficient; delimiters pack several values into one word. Once the encoding is fixed, a string machine becomes a machine for mathematical objects.
The 1930s and 1940s had already produced several exact models of effective calculation: Gödel–Kleene recursive functions, Turing's machines, Church's λ-calculus. Markov did not arrive in an empty field. His normal algorithms belong to the same effort: replace the pre-mathematical phrase “there is a mechanical procedure” with a precise object that can itself be studied.
But first, a disambiguation this subject needs:
The son's path is worth a timeline, because the machine arrives in the middle of a long, wide-ranging career, and its arrival coincides with a philosophical turn.
A Turing machine asks you to imagine a head, a set of states, and a tape scrolling underneath. A normal algorithm asks you to look at the expression already written on the page and perform textual surgery on it. For problems that are themselves about words, group presentations, formulas, and symbol systems, that directness is a real advantage — as the impossibility results two chapters ahead will show.
The program is a list of local textual acts. The computation is the history of the text.
Can this little substitution machine do everything a computer can? In the formal sense of computability — yes. Normal algorithms compute the same partial functions as Turing machines, λ-calculus, and the recursive functions, once suitable encodings are fixed. The models look nothing alike, yet they carve out exactly the same class. Any one can be compiled into any other.
Markov's monograph builds the programming side of this equivalence: combination theorems showing how normal algorithms are composed, branched between, and iterated, which is the marker idiom of Chapter 3 raised to a system. The equivalence with the recursive functions was then established by his student V. K. Detlovs, who announced it in a short Doklady note in 1953 and worked it out in full in a sixty-five-page memoir in 1958. Markov himself credits the result to Detlovs in his introduction to the monograph, writing that it was natural to expect the theory of normal algorithms to coincide with the theory built on recursive functions, and that Detlovs was the one who showed this to actually be so.
On top of the theorem sits the school's own version of the Church–Turing thesis. The normalization principle, as the Encyclopedia of Mathematics states it, proposes that for every algorithm in an alphabet A one can construct an equivalent normal algorithm over A — and, the equivalence theorem in hand, this convention is equivalent to Church's thesis. The one small word is doing real work: over A, not in A. The constructed normal algorithm may use auxiliary letters beyond the input alphabet — and the sweeps of the markers m, R and C in the gallery show why that extra room matters.
Once a precise universal model exists, “method” itself becomes a mathematical noun. Does a method for this problem exist? Can one procedure interpret all programs? Can termination be decided? These stop being vibes and become theorem questions — and, crucially, some of them turn out to have the answer no. That negative power is the subject of the next chapter.
And for Markov's constructive programme, the word construct can now be tethered to a precise class of effective procedures. The machine is no longer merely a model of a calculating clerk. It becomes part of the ontology of the mathematics itself.
The reason mathematicians care about an exact model of computation is not mainly that it lets them compute things. It is that it lets them prove that certain things can never be computed at all — and Markov produced some notable examples, reaching far outside logic into algebra and topology.
Give yourself a finite alphabet and a finite list of two-way rewriting rules u ↔ v — a semigroup presentation, also called a Thue system. Two words count as “equal” if one can be turned into the other by applying rules in either direction, any number of times. A natural question: is there a single algorithm that, given any two words, decides whether they are equal?
P and Q, whether the rules make them equal. String rewriting is powerful enough to be its own undecidable oracle.This is a landmark: one of the earliest undecidability results about an everyday algebraic object rather than about self-referential logical sentences. And it lands in exactly the world of word rewriting that normal algorithms formalize — hardly a coincidence, since proving it means encoding machine histories as words.
The result set off a chain reaction across both cities. Markov himself widened it in 1951: not just equality — whole families of properties of associative calculi admit no recognition algorithm. In Moscow, P. S. Novikov then carried the hardness one algebraic floor up, proving in a memoir of some 140 pages that the word problem for groups is unsolvable (1955). Novikov's student S. I. Adian — with M. O. Rabin independently — took the recognition question to its conclusion: no algorithm decides, from a finite presentation, whether a group is trivial, finite, abelian, or has any other “Markov property.” The name is exact, not honorary: the notion generalizes precisely what Markov had proved for semigroups, and this Adian–Rabin theorem supplies the group-theoretic hardness that Markov's manifold construction, three years later, transports into topology. Leningrad added a miniature: G. S. Tseitin wrote down an explicit associative calculus with an unsolvable equivalence problem (1958) — published in the same Steklov volume as Detlovs' equivalence memoir.
A second theorem goes further. Two manifolds are homeomorphic if one can be continuously deformed into the other — the same shape, up to stretching. It is natural to expect that, for such a geometric question, a patient enough procedure could always decide.
d ≥ 4, the homeomorphy problem is algorithmically unsolvable: no algorithm decides whether two given d-dimensional manifolds are homeomorphic. Markov even exhibited specific manifolds that are, in this precise sense, unrecognizable.Classical mathematics is comfortable proving that an object must exist without handing you the object or any procedure for finding it. Constructive mathematics changes what the sentence is allowed to mean. “There exists an x” becomes a demand: produce x, and produce evidence that it works.
This is not merely a ban on proof by contradiction. Constructive mathematics happily proves negations by deriving contradictions. The delicate move is the step from ¬¬P back to P, and above all from ¬¬∃x P(x) — “it is impossible that no witness exists” — to an actual witness. Classically these are interchangeable. Constructively they are worlds apart, because only one of them hands you the thing.
Tap a connective. The panel says what a constructive proof of it must actually carry — the Brouwer–Heyting–Kolmogorov reading, where a proof is a construction you can run.
The logical instruments here have Moscow roots older than the school itself. A. N. Kolmogorov was studying intuitionistic logic as early as 1925, embedding classical reasoning into it by a double-negation translation; V. I. Glivenko proved, in 1928–29, the little theorems relating classical and intuitionistic provability that still carry his name; and it is Kolmogorov's 1932 reading of intuitionistic logic as a calculus of problems that put the K into the Brouwer–Heyting–Kolmogorov interpretation the demo above uses. When Markov's school later demanded an algorithm as the content of a proof, it was, in effect, filling Kolmogorov's “problems” with an exact notion of solution.
In the late 1940s Markov began developing a distinct variety of constructive mathematics, now commonly labelled recursive constructive mathematics, or RUSS. In the Stanford Encyclopedia's summary, RUSS is essentially recursive function theory with intuitionistic logic: mathematical objects are presented through Gödel numberings, and the procedures are all recursive. What separates RUSS from the classical “recursive analysis” developed in the West after Turing and Church is precisely the logic — RUSS reasons intuitionistically, so every theorem keeps its computational reading.
Now the two halves of this book connect. RUSS says a “construction” is a recursive procedure, and Chapter 5 showed normal algorithms compute exactly the recursive partial functions. So Markov's rewriting machine is a perfectly good official answer to “what counts as a construction?” The machine is not a warm-up act for the philosophy; it is the philosophy's model of what a proof may legitimately smuggle inside it.
“The Russian school” was never one seminar room. Markov's own circle formed in Moscow after his move there in the mid-1950s; a second, ultimately very influential centre grew in Leningrad around his student Nikolai Aleksandrovich Shanin (1919–2011). Mints and Nikolenko's history of the Leningrad school — written by a member of it and a successor at the same institute — is the dedicated account; the sketch below follows the record it belongs to.
Two Leningrad details deserve to be spelled out. First, Shanin insisted that constructive objects come packaged with their own effectivity: he defined a constructive real number as a “duplex” — a pair of algorithms, one producing rational approximations and one guaranteeing the rate at which they converge. That “object = data plus certified method” instinct is precisely the interface-flavoured thinking Chapter 9 develops. Second, the group Shanin founded at the Leningrad branch of the Steklov Institute in 1961 — its first three members were Gennady Davydov, Sergey Maslov, and Grigori Mints — was created not to contemplate algorithms but to build one: an automatic theorem prover. Out of that room came exports whose reach nobody predicted:
And the same rooms kept producing. Shanin turned his semantics itself into a procedure — an algorithm for the constructive decoding of mathematical judgments (1958). I. D. Zaslavsky worked with Tseitin on the singular constructions Chapter 9 will meet. A. O. Slisenko carried the seminar into computational complexity; his real-time recognition of palindromes became a landmark of the subject. And Grigori Mints spent a career threading Maslov's inverse method into Gentzen-style proof theory and resolution — the seminar's proof-search programme carried, personally, into modern automated deduction.
Here is the exact place where Markov's school parts company with many other constructivists — and it is named after him for good reason. Suppose a property of natural numbers is decidable: for each n, you can effectively check whether P(n) holds. Suppose further that assuming “no n satisfies P” leads to a contradiction. May you conclude that some n really does satisfy P?
(aₙ), if it is contradictory that all the terms aₙ equal 0, then there exists a term equal to 1.Equivalently, in the schematic form logic courses use: from ¬¬∃n P(n) conclude ∃n P(n), for decidable P. Markov's computational intuition is an unbounded search: test 0, test 1, test 2, and keep going. If it is impossible for the search to run forever without success, then — on this reading — the search must eventually strike the witness.
Choose where the hidden witness sits. The search knows only how to test one position at a time — and “no witness seen yet” is never the same statement as “no witness exists.”
¬¬∃n P(n) alone, you have not been handed any bound telling you where to stop looking. The search may run arbitrarily long before it succeeds. Markov's principle sanctions the leap anyway, for decidable predicates. Bishop-style and Brouwerian settings generally do not accept it wholesale; in the Stanford Encyclopedia's careful phrasing, its constructive status is less clear than that of the standard “omniscience” principles.MP is computational in one sense and non-trivial constructively in another. The proposed realizer is entirely concrete: enumerate and test. Yet the guarantee that this partial search must terminate is extracted from a double negation, not from a bound you can see. That tension is what makes the principle such a clean window into the school: it trusts effective search further than its neighbours do.
P(n) must itself be effective. MP concerns only the step from “the decidable search cannot fail forever” to the actual success of the unbounded search. It is a statement about search, not omniscience — and modern constructive reverse mathematics studies exactly which theorems need it.A classical real number is often treated as a completed point on an already-existing continuum. A constructive real must be something you can actually work with. Shanin's Leningrad formulation makes the demand explicit: a real is a duplex, a pair of algorithms — one producing rational approximations, one certifying how fast they converge. Ask for precision 1/2ⁿ; the number is obliged to hand you a rational within that error.
x = 0 is not freeConsider the innocent-looking claim “for every real number x, either x = 0 or x ≠ 0.” Classically it is a tautology. Computationally it demands a uniform decision procedure — and a real only ever arrives through finite approximations, so an extremely small nonzero value can keep masquerading as zero at every precision inspected so far. The sentence has quietly asked for an oracle, and the demo below shows why:
A hidden real is revealed only through rational approximations of shrinking error. You must decide “= 0” or “≠ 0” from finitely many of them. The catch: a small nonzero value hides inside the error band for a long time.
x = 0: staying inside the error band forever is consistent with a nonzero value smaller than every band inspected so far. So a single procedure deciding “= 0 versus ≠ 0” for arbitrary constructive reals cannot exist. The classical tautology was hiding a request for infinite information.Inside Markov's recursive world, where every real is named by a program, you can prove theorems that sound false to a classically trained ear. These are not paradoxes; they are honest facts about the recursively presented continuum, and they show that the constructive setting is a different mathematical universe, not classical mathematics with some moves forbidden.
[0,1] that is eventually bounded away from every real number: for each x, from some index on, the sequence keeps a fixed positive distance from x. It climbs forever inside a bounded interval, yet converges to nothing the constructive world can name — a recursive counterexample to the sequential compactness of [0,1].Two companions from the same world, both stated in the Stanford Encyclopedia's survey of RUSS: there is a pointwise continuous function on [0,1] that is not uniformly continuous, and a positive-valued uniformly continuous function on [0,1] whose infimum is 0 — so it never gets to claim the minimum the classical extreme-value theorem would promise. On the closed unit interval, several theorems every calculus student memorizes simply fail once “real number” means “program for a real number.”
Underneath examples of this kind sits one sharp construction from the Leningrad side: the singular coverings of I. D. Zaslavsky and G. S. Tseitin — sequences of intervals of arbitrarily small total length that nevertheless cover every constructive point of the unit interval. Classically, you cannot paint the whole of [0,1] with a tenth of a unit of paint; constructively, the points you can actually name are exactly that easy to paint over. Singular coverings are the raw material for several pathologies of this kind.
And the strangeness cuts in the opposite direction too, in a theorem from the Leningrad side of the school. Since a constructive function must act on programs for reals, it cannot secretly peek at an infinite decimal expansion — and Tseitin proved that, on constructive complete separable metric spaces, this forces continuity: every constructive function of a constructive real variable is continuous. You cannot program a genuine jump. Discontinuity, constructively, is not an available behaviour; what fails instead, as above, is uniform continuity.
Step back and the pattern is unmistakable. A constructive definition behaves like a data structure with methods — Shanin's duplex is the plainest example, an object that literally ships as two algorithms. A continuous function may need a modulus: an effective control saying how much input precision buys how much output precision. A Cauchy sequence carries a convergence rate. A proof of ∀x ∃y R(x,y) is expected to act like a program that receives x and returns y together with evidence of R.
Constructivizing did not merely delete theorems; it forced new statements, new hypotheses, and new proof techniques. Constructive analysis, algebra, and topology became deep subjects in their own right. Errett Bishop's 1967 book then showed that a great deal of analysis can be rebuilt constructively in recognizably ordinary mathematical prose — free of the recursion-theoretic notation that made RUSS a hard read even for sympathetic mathematicians.
The Russian school was one route among several, distinguished by its explicit allegiance to recursive procedures and its acceptance of Markov's principle. A fair map shows the neighbouring roads:
| Tradition | Characteristic emphasis | Markov's principle? |
|---|---|---|
| Markov / RUSS | Recursive presentations and procedures; intuitionistic logic; a strongly algorithmic reading of everything. | Yes — its signature. |
| Brouwerian intuitionism | Mental constructions, choice sequences, distinctive continuity principles. | Not in general. |
| Bishop-style (BISH) | Constructive mathematics in ordinary mathematical language, engineered to keep numerical meaning. | Usually not assumed. |
| Martin-Löf type theory | Judgements, dependent types, proofs as structured terms with computational meaning. | Not a default. |
A fair audit splits the record three ways — established, plausible, oversold — and this chapter cites its evidence for each verdict.
There is a genuine, non-hand-wavy bridge from constructive mathematics to computation, and it has a name: the Curry–Howard correspondence. Stated plainly: a constructive proof of an existential statement is an algorithm that produces a witness. Propositions correspond to types, proofs to programs of those types; running the proof computes the object it claims exists. This is not a metaphor and not a Markov-specific slogan — it is the organizing principle behind an entire family of proof assistants.
This is why systems in the Coq, Agda, Nuprl, Minlog, Isabelle, and Lean families can extract a program from a proof: prove ∀x ∃y R(x,y) constructively, and the assistant can emit executable code taking x to y, certified correct by the proof it came from. Markov's insistence that “exists” carry a construction is the ancestral form of the demand; the modern machinery is more powerful and vastly better engineered, but it is the same demand.
The constructive habit — treat a specification as a contract for evidence — reappears wherever a type system carries real guarantees. A well-typed program is, in a precise sense, a proof that its type is inhabited, and a type-checker is then a proof-checker. Dependent types (Coq, Agda, Idris, Lean) push this until software can be proven, not merely tested, to meet its specification. That lineage is real.
Does the specifically Markov flavour — strings, ordered rules — earn its keep? In narrow, specific ways. Term and string rewriting underlies real technology: semantics of rule-based systems, decision procedures built on confluent rewriting, completion methods in equational reasoning. Where the subject matter is itself symbolic — grammars, presentations, formula manipulation — the rewriting view is the natural one, exactly as the undecidability proofs of Chapter 6 suggested. And because one step of a normal algorithm is so simply defined, the model is a natural target for mechanized metatheory: formalizing “execute a normal algorithm” inside a proof assistant and proving exactly which class of functions the programs denote.
There is also the quieter channel from Chapter 7, worth restating because it is so easy to miss: the Leningrad seminar's automated-deduction ambitions produced Maslov's inverse method and Tseitin's clause translation, and SAT solving — where Tseitin's translation is standard equipment — now underpins a large share of modern automated verification. The constructive school did not conquer mathematics, but pieces of its toolbox quietly conquered the verifiers.
| Claim | Status | In plain terms |
|---|---|---|
| Constructive proofs yield algorithms for witnesses | Established | Curry–Howard; the backbone of program extraction in real proof assistants. |
| Constructive mathematics is a living field | Established | Active work in analysis, algebra, type theory, computable analysis, constructive reverse mathematics. |
| The school seeded automated deduction | Established | Maslov's inverse method; Tseitin's clause translation, still standard in SAT. |
| Rewriting / normal algorithms aid verification & metatheory | Real but narrow | Genuine in symbolic domains and mechanized metatheory; not a general-purpose engineering win. |
| Extracted programs are automatically fast | Oversold | Correct, yes; efficient only with deliberate effort. A documented limitation. |
| Markov's specific RUSS school won the field | False | It did not. Bishop-style and type-theoretic constructivism are far more prominent today. |
| “Everything modern descends from Markov” | False | These ideas have many independent lineages. Resemblance is not descent. |
A theorem can be true. A constructive mathematician also asks what it lets you compute.
Mathematics did not become Markov's constructive mathematics. Classical mathematics remains overwhelmingly standard, and even within constructivism, the recursive school is one historical variety among several — not the most widely taught. As a bid to replace classical practice, the programme failed.
That is the wrong scale for judging it. Ask instead where the demand for computational meaning is intellectually alive now, and the map fills up.
They remain a clean universal model and a natural formalism when the subject matter is symbolic transformation. They live in computability theory, in rewriting-oriented teaching, in historical and foundational work — and, as the previous chapter noted, their one-line operational semantics makes them attractive objects for mechanized metatheory.
RUSS is a historically specific school, but constructive mathematics is vigorously alive across several traditions. Current work spans constructive analysis and algebra, type theory, proof assistants, computable analysis, realizability, and constructive reverse mathematics — the last of which measures exactly which extra principles (Markov's principle among them) a given theorem really needs. The shared pressure is the one Markov named: make the information content of a theorem explicit.
Make the method explicit. Then make the method itself an object you can check.
The map could end the book. But the rewriting instinct did not stop with Markov, and one of its descendants — a Soviet one, fittingly — earns a coda. In 1968 the physicist and cybernetician Valentin Turchin proposed Refal, initially as a metaalgorithmic language: a notation for describing the semantics of other languages, which soon acquired efficient implementations and became a programming language in its own right. Its heart is pattern matching as the central act of computation — a program is a set of sentences, each pairing a pattern with a replacement.
Refal is not “Markov normal algorithms with nicer syntax” — its data model and semantics are its own, and claiming direct descent would be sloppy. But the family resemblance is immediate. Refal computes over object expressions: bidirectional sequences, with brackets, that can be split and concatenated anywhere — so the shape of the data drives the control flow, exactly the instinct behind Markov's substitutions. Patterns speak about that shape through three kinds of variables:
Here is the classic first program, a palindrome test, in genuine Refal-5 syntax — four sentences, tried top to bottom, the same priority discipline Markov's rule lists taught us to read:
Pal {
= True;
s.1 = True;
s.1 e.2 s.1 = <Pal e.2>;
e.1 = False;
}Line by line: the empty word is a palindrome; a single symbol is a palindrome; a word whose first and last symbols coincide (the repeated variable s.1) is a palindrome iff its interior e.2 is — recurse; anything else is not. The whole control flow lives in the patterns.
A didactic matcher, not a real Refal evaluator: it shows the intuition behind s- and e-variables on a flat token sequence.
First formalize the calculation. Then formalize the act of looking at the calculation.
This page is written as a narrative, not a literature review — but the history in it is not folklore. These are the works to open when a sentence makes you suspicious; every named theorem, date, and quotation above was checked against one of them.