Project Page Index Table of Contents
  • Shared libraries
    • Finitary sums and products over monoids
    • Binomial theorem
    • Bitwise operations on nat as list bool
    • Bitwise operations on nat
    • Euclidian division and Bezout's identity
    • Prime numbers
    • Base p representation
    • Reification for bounded quantification
    • Pidgeon hole principle
    • Iteration of binary relations
  • Minsky machines to FRACTRAN programs
    • Removal of self-loops in MMs
    • Two infinite sequences of primes
    • Definition of FRACTRAN
    • Compiler from MM to FRACTRAN
  • Arithmetic libraries for Matiyasevich's theorems
    • Modular arithmetic
    • Matric computation
    • Luca's theorem
    • Solutions of Pell's equation
    • Exponentiation is Diophantine
    • Sparse ciphers
  • Object-level representation of Diophantine equations
    • Diophantine logic
    • Elementary diophantine constraints
    • Single Diophantine equations
    • Object-level encoding of exponential
    • Object-level encoding of bounded universal quantification I
    • Object-level encoding of bounded universal quantification II
    • Object-level encoding of bounded universal quantification III
    • Reflexive transitive closure is Diophantine
    • FRACTRAN termination is Diophantine
  • Main undecidability results and DPRM theorem
    • HALT reduces to MM
    • MM reduces to FRACTRAN
    • FRACTRAN reduces to Diophantine logic
    • Hilbert's tenth problem is undecidable
    • The DPRM theorem
    • Generated by coqdoc and improved with CoqdocJS