https://github.com/uds-psl/cook-levin
Tip revision: e24a92af25746f6758a09ea1dc51e57491508e60 authored by Fabian Kunze on 03 February 2021, 23:29:51 UTC
added missing html doc
added missing html doc
Tip revision: e24a92a
Undecidability.TM.SBTM.html
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="config.js"></script>
<script type="text/javascript" src="coqdocjs.js"></script>
</head>
<body onload="document.getElementById('content').focus()">
<div id="header">
<span class="left">
<span class="modulename"> <script> document.write(document.title) </script> </span>
</span>
<span class="button" id="toggle-proofs"></span>
<span class="right">
<a href="../">Project Page</a>
<a href="./indexpage.html"> Index </a>
<a href="./toc.html"> Table of Contents </a>
</span>
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
<div id="main">
<div class="code">
</div>
<div class="doc">
<a id="lab3"></a><h1 class="section">Halting problem for simple binary single-tape Turing machines HaltSBTM</h1>
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#"><span class="id" title="library">List</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Bool.Bool.html#"><span class="id" title="library">Bool</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Nat.html#"><span class="id" title="library">Nat</span></a>.<br/>
<span class="id" title="keyword">Require</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Vectors.Fin.html#"><span class="id" title="library">Coq.Vectors.Fin</span></a>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">ListNotations</span>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="tape" class="idref" href="#tape"><span class="id" title="definition">tape</span></a> : <span class="id" title="keyword">Type</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="left" class="idref" href="#left"><span class="id" title="definition">left</span></a> <a id="pat:4" class="idref" href="#pat:4"><span class="id" title="binder">'(</span></a> <a id="pat:4" class="idref" href="#pat:4"><span class="id" title="binder">(</span></a><a id="pat:4" class="idref" href="#pat:4"><span class="id" title="binder">ls</span></a><a id="pat:4" class="idref" href="#pat:4"><span class="id" title="binder">,</span></a> <a id="pat:4" class="idref" href="#pat:4"><span class="id" title="binder">m</span></a><a id="pat:4" class="idref" href="#pat:4"><span class="id" title="binder">,</span></a> <a id="pat:4" class="idref" href="#pat:4"><span class="id" title="binder">rs</span></a><a id="pat:4" class="idref" href="#pat:4"><span class="id" title="binder">)</span></a> <a id="pat:4" class="idref" href="#pat:4"><span class="id" title="binder">:</span></a> <a id="pat:4" class="idref" href="#pat:4"><span class="id" title="binder">tape</span></a><a id="pat:4" class="idref" href="#pat:4"><span class="id" title="binder">)</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> := <a class="idref" href="Undecidability.TM.SBTM.html#ls:3"><span class="id" title="variable">ls</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="right" class="idref" href="#right"><span class="id" title="definition">right</span></a> <a id="pat:8" class="idref" href="#pat:8"><span class="id" title="binder">'((</span></a><a id="pat:8" class="idref" href="#pat:8"><span class="id" title="binder">ls</span></a><a id="pat:8" class="idref" href="#pat:8"><span class="id" title="binder">,</span></a> <a id="pat:8" class="idref" href="#pat:8"><span class="id" title="binder">m</span></a><a id="pat:8" class="idref" href="#pat:8"><span class="id" title="binder">,</span></a> <a id="pat:8" class="idref" href="#pat:8"><span class="id" title="binder">rs</span></a><a id="pat:8" class="idref" href="#pat:8"><span class="id" title="binder">)</span></a> <a id="pat:8" class="idref" href="#pat:8"><span class="id" title="binder">:</span></a> <a id="pat:8" class="idref" href="#pat:8"><span class="id" title="binder">tape</span></a><a id="pat:8" class="idref" href="#pat:8"><span class="id" title="binder">)</span></a> := <a class="idref" href="Undecidability.TM.SBTM.html#rs:5"><span class="id" title="variable">rs</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="curr" class="idref" href="#curr"><span class="id" title="definition">curr</span></a> <a id="pat:12" class="idref" href="#pat:12"><span class="id" title="binder">'((</span></a><a id="pat:12" class="idref" href="#pat:12"><span class="id" title="binder">ls</span></a><a id="pat:12" class="idref" href="#pat:12"><span class="id" title="binder">,</span></a> <a id="pat:12" class="idref" href="#pat:12"><span class="id" title="binder">m</span></a><a id="pat:12" class="idref" href="#pat:12"><span class="id" title="binder">,</span></a> <a id="pat:12" class="idref" href="#pat:12"><span class="id" title="binder">rs</span></a><a id="pat:12" class="idref" href="#pat:12"><span class="id" title="binder">)</span></a> <a id="pat:12" class="idref" href="#pat:12"><span class="id" title="binder">:</span></a> <a id="pat:12" class="idref" href="#pat:12"><span class="id" title="binder">tape</span></a><a id="pat:12" class="idref" href="#pat:12"><span class="id" title="binder">)</span></a> := <a class="idref" href="Undecidability.TM.SBTM.html#m:10"><span class="id" title="variable">m</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="wr" class="idref" href="#wr"><span class="id" title="definition">wr</span></a> (<a id="o:13" class="idref" href="#o:13"><span class="id" title="binder">o</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>) (<a id="t:14" class="idref" href="#t:14"><span class="id" title="binder">t</span></a> : <a class="idref" href="Undecidability.TM.SBTM.html#tape"><span class="id" title="definition">tape</span></a>) := <br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Undecidability.TM.SBTM.html#o:13"><span class="id" title="variable">o</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">c</span> => <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.TM.SBTM.html#left"><span class="id" title="definition">left</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:14"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">c</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#right"><span class="id" title="definition">right</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:14"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> => <a class="idref" href="Undecidability.TM.SBTM.html#t:14"><span class="id" title="variable">t</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Inductive</span> <a id="move" class="idref" href="#move"><span class="id" title="inductive">move</span></a> : <span class="id" title="keyword">Type</span> := <br/>
| <a id="Lmove" class="idref" href="#Lmove"><span class="id" title="constructor">Lmove</span></a> : <a class="idref" href="Undecidability.TM.SBTM.html#move:16"><span class="id" title="inductive">move</span></a> <br/>
| <a id="Rmove" class="idref" href="#Rmove"><span class="id" title="constructor">Rmove</span></a> : <a class="idref" href="Undecidability.TM.SBTM.html#move:16"><span class="id" title="inductive">move</span></a> <br/>
| <a id="Nmove" class="idref" href="#Nmove"><span class="id" title="constructor">Nmove</span></a> : <a class="idref" href="Undecidability.TM.SBTM.html#move:16"><span class="id" title="inductive">move</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="mv" class="idref" href="#mv"><span class="id" title="definition">mv</span></a> (<a id="m:18" class="idref" href="#m:18"><span class="id" title="binder">m</span></a> : <a class="idref" href="Undecidability.TM.SBTM.html#move"><span class="id" title="inductive">move</span></a>) (<a id="t:19" class="idref" href="#t:19"><span class="id" title="binder">t</span></a> : <a class="idref" href="Undecidability.TM.SBTM.html#tape"><span class="id" title="definition">tape</span></a>) :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Undecidability.TM.SBTM.html#m:18"><span class="id" title="variable">m</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="Undecidability.TM.SBTM.html#Lmove"><span class="id" title="constructor">Lmove</span></a> => <span class="id" title="keyword">match</span> <a class="idref" href="Undecidability.TM.SBTM.html#left"><span class="id" title="definition">left</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:19"><span class="id" title="variable">t</span></a>, <a class="idref" href="Undecidability.TM.SBTM.html#curr"><span class="id" title="definition">curr</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:19"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/>
| <span class="id" title="var">l</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">ls</span>, <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">ls</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">l</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#right"><span class="id" title="definition">right</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:19"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
| <span class="id" title="var">l</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">ls</span>, <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">c</span> => <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">ls</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">l</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">c</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#right"><span class="id" title="definition">right</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:19"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a>, <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">c</span> => <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">c</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#right"><span class="id" title="definition">right</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:19"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
| <span class="id" title="var">_</span>, <span class="id" title="var">_</span> => <a class="idref" href="Undecidability.TM.SBTM.html#t:19"><span class="id" title="variable">t</span></a><br/>
<span class="id" title="keyword">end</span><br/>
| <a class="idref" href="Undecidability.TM.SBTM.html#Rmove"><span class="id" title="constructor">Rmove</span></a> => <span class="id" title="keyword">match</span> <a class="idref" href="Undecidability.TM.SBTM.html#curr"><span class="id" title="definition">curr</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:19"><span class="id" title="variable">t</span></a>, <a class="idref" href="Undecidability.TM.SBTM.html#right"><span class="id" title="definition">right</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:19"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>, <span class="id" title="var">r</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">rs</span> => <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.TM.SBTM.html#left"><span class="id" title="definition">left</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:19"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">r</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">rs</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">c</span>, <span class="id" title="var">r</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">rs</span> => <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">c</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#left"><span class="id" title="definition">left</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:19"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">r</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">rs</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">c</span>, <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">c</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#left"><span class="id" title="definition">left</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:19"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
| <span class="id" title="var">_</span> , <span class="id" title="var">_</span> => <a class="idref" href="Undecidability.TM.SBTM.html#t:19"><span class="id" title="variable">t</span></a><br/>
<span class="id" title="keyword">end</span><br/>
| <a class="idref" href="Undecidability.TM.SBTM.html#Nmove"><span class="id" title="constructor">Nmove</span></a> => <a class="idref" href="Undecidability.TM.SBTM.html#t:19"><span class="id" title="variable">t</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Record</span> <a id="SBTM" class="idref" href="#SBTM"><span class="id" title="record">SBTM</span></a> := { <a id="num_states" class="idref" href="#num_states"><span class="id" title="projection">num_states</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> ; <a id="trans" class="idref" href="#trans"><span class="id" title="projection">trans</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Vectors.Fin.html#t"><span class="id" title="inductive">Fin.t</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#num_states:22"><span class="id" title="method">num_states</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Vectors.Fin.html#t"><span class="id" title="inductive">Fin.t</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#num_states:22"><span class="id" title="method">num_states</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#move"><span class="id" title="inductive">move</span></a>)}.<br/>
<br/>
<span class="id" title="keyword">Notation</span> <a id="state" class="idref" href="#state"><span class="id" title="abbreviation">state</span></a> <span class="id" title="var">M</span> := (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Vectors.Fin.html#t"><span class="id" title="inductive">Fin.t</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> (<a class="idref" href="Undecidability.TM.SBTM.html#num_states"><span class="id" title="projection">num_states</span></a> <span class="id" title="var">M</span>))).<br/>
<br/>
<span class="id" title="keyword">Inductive</span> <a id="eval" class="idref" href="#eval"><span class="id" title="inductive">eval</span></a> (<a id="M:24" class="idref" href="#M:24"><span class="id" title="binder">M</span></a> : <a class="idref" href="Undecidability.TM.SBTM.html#SBTM"><span class="id" title="record">SBTM</span></a>) : <a class="idref" href="Undecidability.TM.SBTM.html#state"><span class="id" title="abbreviation">state</span></a> <span class="id" title="var">M</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Undecidability.TM.SBTM.html#tape"><span class="id" title="definition">tape</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Undecidability.TM.SBTM.html#state"><span class="id" title="abbreviation">state</span></a> <span class="id" title="var">M</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Undecidability.TM.SBTM.html#tape"><span class="id" title="definition">tape</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <span class="id" title="keyword">Prop</span> :=<br/>
| <a id="eval_halt" class="idref" href="#eval_halt"><span class="id" title="constructor">eval_halt</span></a> <a id="q:27" class="idref" href="#q:27"><span class="id" title="binder">q</span></a> <a id="t:28" class="idref" href="#t:28"><span class="id" title="binder">t</span></a> :<br/>
<a class="idref" href="Undecidability.TM.SBTM.html#trans"><span class="id" title="projection">trans</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#M:24"><span class="id" title="variable">M</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.TM.SBTM.html#q:27"><span class="id" title="variable">q</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.TM.SBTM.html#curr"><span class="id" title="definition">curr</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:28"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">))</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a><br/>
<a class="idref" href="Undecidability.TM.SBTM.html#eval:25"><span class="id" title="inductive">eval</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#M:24"><span class="id" title="variable">M</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#q:27"><span class="id" title="variable">q</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:28"><span class="id" title="variable">t</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#q:27"><span class="id" title="variable">q</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:28"><span class="id" title="variable">t</span></a><br/>
| <a id="eval_step" class="idref" href="#eval_step"><span class="id" title="constructor">eval_step</span></a> <a id="q:29" class="idref" href="#q:29"><span class="id" title="binder">q</span></a> <a id="t:30" class="idref" href="#t:30"><span class="id" title="binder">t</span></a> <a id="q':31" class="idref" href="#q':31"><span class="id" title="binder">q'</span></a> <a id="w:32" class="idref" href="#w:32"><span class="id" title="binder">w</span></a> <a id="m:33" class="idref" href="#m:33"><span class="id" title="binder">m</span></a> <a id="q'':34" class="idref" href="#q'':34"><span class="id" title="binder">q''</span></a> <a id="t':35" class="idref" href="#t':35"><span class="id" title="binder">t'</span></a> :<br/>
<a class="idref" href="Undecidability.TM.SBTM.html#trans"><span class="id" title="projection">trans</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#M:24"><span class="id" title="variable">M</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.TM.SBTM.html#q:29"><span class="id" title="variable">q</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#curr"><span class="id" title="definition">curr</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:30"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.TM.SBTM.html#q':31"><span class="id" title="variable">q'</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#w:32"><span class="id" title="variable">w</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#m:33"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a><br/>
<a class="idref" href="Undecidability.TM.SBTM.html#eval:25"><span class="id" title="inductive">eval</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#M:24"><span class="id" title="variable">M</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#q':31"><span class="id" title="variable">q'</span></a> (<a class="idref" href="Undecidability.TM.SBTM.html#mv"><span class="id" title="definition">mv</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#m:33"><span class="id" title="variable">m</span></a> (<a class="idref" href="Undecidability.TM.SBTM.html#wr"><span class="id" title="definition">wr</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#w:32"><span class="id" title="variable">w</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:30"><span class="id" title="variable">t</span></a>)) <a class="idref" href="Undecidability.TM.SBTM.html#q'':34"><span class="id" title="variable">q''</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t':35"><span class="id" title="variable">t'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a><br/>
<a class="idref" href="Undecidability.TM.SBTM.html#eval:25"><span class="id" title="inductive">eval</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#M:24"><span class="id" title="variable">M</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#q:29"><span class="id" title="variable">q</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:30"><span class="id" title="variable">t</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#q'':34"><span class="id" title="variable">q''</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t':35"><span class="id" title="variable">t'</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="HaltSBTM" class="idref" href="#HaltSBTM"><span class="id" title="definition">HaltSBTM</span></a> <a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">'(</span></a> <a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">(</span></a><a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">M</span></a><a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">,</span></a> <a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">t</span></a><a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">)</span></a> <a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">:</span></a> <a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">SBTM</span></a> <a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">*</span></a> <a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">tape</span></a><a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">)</span></a> :=<br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">exists</span></a> <a id="q':39" class="idref" href="#q':39"><span class="id" title="binder">q'</span></a> <a id="t':40" class="idref" href="#t':40"><span class="id" title="binder">t'</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#eval"><span class="id" title="inductive">eval</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#M:37"><span class="id" title="variable">M</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Vectors.Fin.html#F1"><span class="id" title="constructor">Fin.F1</span></a>) <a class="idref" href="Undecidability.TM.SBTM.html#t:36"><span class="id" title="variable">t</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#q':39"><span class="id" title="variable">q'</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t':40"><span class="id" title="variable">t'</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="HaltSBTMu" class="idref" href="#HaltSBTMu"><span class="id" title="definition">HaltSBTMu</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">{</span></a> <a id="M:41" class="idref" href="#M:41"><span class="id" title="binder">M</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">:</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#SBTM"><span class="id" title="record">SBTM</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">{</span></a><a id="q:42" class="idref" href="#q:42"><span class="id" title="binder">q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">:</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#state"><span class="id" title="abbreviation">state</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#M:41"><span class="id" title="variable">M</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">|</span></a> <span class="id" title="keyword">forall</span> <a id="c:43" class="idref" href="#c:43"><span class="id" title="binder">c</span></a>, <a class="idref" href="Undecidability.TM.SBTM.html#trans"><span class="id" title="projection">trans</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#M:41"><span class="id" title="variable">M</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.TM.SBTM.html#q:42"><span class="id" title="variable">q</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><a class="idref" href="Undecidability.TM.SBTM.html#c:43"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">/\</span></a> <span class="id" title="keyword">forall</span> <a id="q':44" class="idref" href="#q':44"><span class="id" title="binder">q'</span></a>, <a class="idref" href="Undecidability.TM.SBTM.html#trans"><span class="id" title="projection">trans</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#M:41"><span class="id" title="variable">M</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.TM.SBTM.html#q':44"><span class="id" title="variable">q'</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><a class="idref" href="Undecidability.TM.SBTM.html#c:43"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Undecidability.TM.SBTM.html#q':44"><span class="id" title="variable">q'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#q:42"><span class="id" title="variable">q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Specif.html#cc5e56ba3765e2d6b17e66d19b966f1d"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#tape"><span class="id" title="definition">tape</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <span class="id" title="keyword">Prop</span> := <span class="id" title="keyword">fun</span> <a id="pat:49" class="idref" href="#pat:49"><span class="id" title="binder">'((</span></a><a id="pat:49" class="idref" href="#pat:49"><span class="id" title="binder">existT</span></a> <a id="pat:49" class="idref" href="#pat:49"><span class="id" title="binder">_</span></a> <a id="pat:49" class="idref" href="#pat:49"><span class="id" title="binder">M</span></a> <a id="pat:49" class="idref" href="#pat:49"><span class="id" title="binder">(</span></a><a id="pat:49" class="idref" href="#pat:49"><span class="id" title="binder">exist</span></a> <a id="pat:49" class="idref" href="#pat:49"><span class="id" title="binder">_</span></a> <a id="pat:49" class="idref" href="#pat:49"><span class="id" title="binder">q</span></a> <a id="pat:49" class="idref" href="#pat:49"><span class="id" title="binder">H</span></a><a id="pat:49" class="idref" href="#pat:49"><span class="id" title="binder">)),</span></a> <a id="pat:49" class="idref" href="#pat:49"><span class="id" title="binder">t</span></a><a id="pat:49" class="idref" href="#pat:49"><span class="id" title="binder">)</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">exists</span></a> <a id="t':50" class="idref" href="#t':50"><span class="id" title="binder">t'</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#eval"><span class="id" title="inductive">eval</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#M:48"><span class="id" title="variable">M</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Vectors.Fin.html#F1"><span class="id" title="constructor">Fin.F1</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t:45"><span class="id" title="variable">t</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#q:47"><span class="id" title="variable">q</span></a> <a class="idref" href="Undecidability.TM.SBTM.html#t':50"><span class="id" title="variable">t'</span></a>.<br/>
</div>
</div>
<div id="footer">
Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
</div>
</div>
</body>
</html>
