Project Page Index Table of Contents
  • Preliminaries
    • Lists
    • Decisions
    • Discrete types
    • Tactics
    • Finite Types
  • Definitions
    • Reductions and Undecidability
    • String Rewriting
    • PCP and MPCP
    • Singletape Turing Machines
      • Definition of the tape
      • Definition of moves
      • Definition of a Sigletape Turing Machine
      • Configurations of TM
      • Machine execution
      • Definition of Reachability
  • Reducing MPCP to PCP
    • Definition of PCP Dominoes
    • Correctness Proof
      • MPCP Match to PCP Match
      • PCP Match to MPCP Match
  • Reducing String Rewriting to MPCP
    • Definition of MPCP Dominoes
    • Correctness Proof
      • String Rewriting to MPCP Match
      • MPCP Match to String Rewriting
  • Reducing the Reachability of Turing Configurations to String Rewriting
    • Encoding of Configurations
    • Definition of Rewrite Rules Simulating a Transition
    • Correctness Proof
  • Reducing the Halting Problem to String Rewriting
    • Definition of Rewrite Rules Deleting Symbols
    • Correctness Proof
  • Reducing the Halting Problem to MPCP
    • Definition of MPCP dominoes
    • Simulating one Machine Step with Dominoes
    • Correctness Proof
      • Halting Computations to MPCP Matches
      • MPCP Matches to Halting Computations
  • Reducing String Rewriting to Restricted String Rewriting
  • Reducing Restricted String Rewriting to PCP
    • Definition of PCP Dominoes
    • String Rewriting to PCP Match
    • PCP Match to String Rewriting
  • Undecidability of PCP
Generated by coqdoc and improved with CoqdocJS