A mechanical proof of the termination of Takeuchi's function

DOI10.1016/0020-0190(79)90063-2zbMath0411.68079OpenAlexW2099878868MaRDI QIDQ1259437

J. Strother Moore

Publication date: 1979

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0020-0190(79)90063-2

zbMATH Keywords

automatic theorem-provinglexicographic relationtermination of Takeuchi's function

Mathematics Subject Classification ID

Related Items (6)

On proving the termination of algorithms by machine ⋮ Mechanizing structural induction. I: Formal system ⋮ Mechanizing structural induction. II: Strategies ⋮ Relativistic Feynman-type integrals ⋮ The termination of the higher-dimensional tarai functions ⋮ Computer theorem proving in mathematics

Cites Work

• Inductive methods for proving properties of programs
• Unnamed Item
• Unnamed Item

This page was built for publication: A mechanical proof of the termination of Takeuchi's function