website v1.1+8.16

uds-psl · Oct 12, 2023 · 1138ff2 · 1138ff2
commit 1138ff2
Show file tree

Hide file tree

Showing 677 changed files with 314,758 additions and 0 deletions.
diff --git a/v1.1+8.16/Undecidability.CFG.CFG.html b/v1.1+8.16/Undecidability.CFG.CFG.html
diff --git a/v1.1+8.16/Undecidability.CFG.CFG_undec.html b/v1.1+8.16/Undecidability.CFG.CFG_undec.html
@@ -0,0 +1,70 @@
+<!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">
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Undecidability.CFG.CFG.html#"><span class="id" title="library">Undecidability.CFG.CFG</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Undecidability.CFG.Reductions</span> <span class="id" title="keyword">Require</span> <br/>
+&nbsp;&nbsp;<a class="idref" href="Undecidability.CFG.Reductions.CFPP_to_CFP.html#"><span class="id" title="library">CFPP_to_CFP</span></a> <a class="idref" href="Undecidability.CFG.Reductions.CFPI_to_CFI.html#"><span class="id" title="library">CFPI_to_CFI</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Undecidability.Synthetic.Undecidability.html#"><span class="id" title="library">Undecidability.Synthetic.Undecidability</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Require</span> <a class="idref" href="Undecidability.CFG.CFP_undec.html#"><span class="id" title="library">Undecidability.CFG.CFP_undec</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a id="CFP_undec" class="idref" href="#CFP_undec"><span class="id" title="lemma">CFP_undec</span></a> : <a class="idref" href="Undecidability.Synthetic.Undecidability.html#undecidable"><span class="id" title="definition">undecidable</span></a> <a class="idref" href="Undecidability.CFG.CFG.html#CFP"><span class="id" title="definition">CFP</span></a>.<br/>
+<span class="id" title="keyword">Proof</span>.<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.Synthetic.Undecidability.html#undecidability_from_reducibility"><span class="id" title="lemma">undecidability_from_reducibility</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">exact</span> <a class="idref" href="Undecidability.CFG.CFP_undec.html#CFPP_undec"><span class="id" title="lemma">CFP_undec.CFPP_undec</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">exact</span> <a class="idref" href="Undecidability.CFG.Reductions.CFPP_to_CFP.html#reduction"><span class="id" title="lemma">CFPP_to_CFP.reduction</span></a>.<br/>
+<span class="id" title="keyword">Qed</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Check</span> <a class="idref" href="Undecidability.CFG.CFG_undec.html#CFP_undec"><span class="id" title="lemma">CFP_undec</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a id="CFI_undec" class="idref" href="#CFI_undec"><span class="id" title="lemma">CFI_undec</span></a> : <a class="idref" href="Undecidability.Synthetic.Undecidability.html#undecidable"><span class="id" title="definition">undecidable</span></a> <a class="idref" href="Undecidability.CFG.CFG.html#CFI"><span class="id" title="definition">CFI</span></a>.<br/>
+<span class="id" title="keyword">Proof</span>.<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.Synthetic.Undecidability.html#undecidability_from_reducibility"><span class="id" title="lemma">undecidability_from_reducibility</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">exact</span> <a class="idref" href="Undecidability.CFG.CFP_undec.html#CFPI_undec"><span class="id" title="lemma">CFP_undec.CFPI_undec</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">exact</span> <a class="idref" href="Undecidability.CFG.Reductions.CFPI_to_CFI.html#reduction"><span class="id" title="lemma">CFPI_to_CFI.reduction</span></a>.<br/>
+<span class="id" title="keyword">Qed</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Check</span> <a class="idref" href="Undecidability.CFG.CFG_undec.html#CFI_undec"><span class="id" title="lemma">CFI_undec</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>
diff --git a/v1.1+8.16/Undecidability.CFG.CFP.html b/v1.1+8.16/Undecidability.CFG.CFP.html
diff --git a/v1.1+8.16/Undecidability.CFG.CFP_undec.html b/v1.1+8.16/Undecidability.CFG.CFP_undec.html
@@ -0,0 +1,64 @@
+<!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">
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Undecidability.CFG.CFP.html#"><span class="id" title="library">Undecidability.CFG.CFP</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Undecidability.CFG.Reductions</span> <span class="id" title="keyword">Require</span> <br/>
+&nbsp;&nbsp;<a class="idref" href="Undecidability.CFG.Reductions.PCP_to_CFPP.html#"><span class="id" title="library">PCP_to_CFPP</span></a> <a class="idref" href="Undecidability.CFG.Reductions.PCP_to_CFPI.html#"><span class="id" title="library">PCP_to_CFPI</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Undecidability.Synthetic.Undecidability.html#"><span class="id" title="library">Undecidability.Synthetic.Undecidability</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Require</span> <a class="idref" href="Undecidability.PCP.PCP_undec.html#"><span class="id" title="library">Undecidability.PCP.PCP_undec</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a id="CFPP_undec" class="idref" href="#CFPP_undec"><span class="id" title="lemma">CFPP_undec</span></a> : <a class="idref" href="Undecidability.Synthetic.Undecidability.html#undecidable"><span class="id" title="definition">undecidable</span></a> <a class="idref" href="Undecidability.CFG.CFP.html#CFPP"><span class="id" title="definition">CFPP</span></a>.<br/>
+<span class="id" title="keyword">Proof</span>.<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.Synthetic.Undecidability.html#undecidability_from_reducibility"><span class="id" title="lemma">undecidability_from_reducibility</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">exact</span> <a class="idref" href="Undecidability.PCP.PCP_undec.html#PCP_undec"><span class="id" title="lemma">PCP_undec.PCP_undec</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">exact</span> <a class="idref" href="Undecidability.CFG.Reductions.PCP_to_CFPP.html#reduction"><span class="id" title="lemma">PCP_to_CFPP.reduction</span></a>.<br/>
+<span class="id" title="keyword">Qed</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a id="CFPI_undec" class="idref" href="#CFPI_undec"><span class="id" title="lemma">CFPI_undec</span></a> : <a class="idref" href="Undecidability.Synthetic.Undecidability.html#undecidable"><span class="id" title="definition">undecidable</span></a> <a class="idref" href="Undecidability.CFG.CFP.html#CFPI"><span class="id" title="definition">CFPI</span></a>.<br/>
+<span class="id" title="keyword">Proof</span>.<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.Synthetic.Undecidability.html#undecidability_from_reducibility"><span class="id" title="lemma">undecidability_from_reducibility</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">exact</span> <a class="idref" href="Undecidability.PCP.PCP_undec.html#PCP_undec"><span class="id" title="lemma">PCP_undec.PCP_undec</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">exact</span> <a class="idref" href="Undecidability.CFG.Reductions.PCP_to_CFPI.html#reduction"><span class="id" title="lemma">PCP_to_CFPI.reduction</span></a>.<br/>
+<span class="id" title="keyword">Qed</span>.<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>
diff --git a/v1.1+8.16/Undecidability.CFG.Reductions.CFPI_to_CFI.html b/v1.1+8.16/Undecidability.CFG.Reductions.CFPI_to_CFI.html
@@ -0,0 +1,61 @@
+<!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">
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.16.0/stdlib//Coq.Lists.List.html#"><span class="id" title="library">List</span></a>.<br/>
+<span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.16.0/stdlib//Coq.Lists.List.html#ListNotations"><span class="id" title="module">ListNotations</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Undecidability.CFG.CFP.html#"><span class="id" title="library">Undecidability.CFG.CFP</span></a>.<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Undecidability.CFG.CFG.html#"><span class="id" title="library">Undecidability.CFG.CFG</span></a>.<br/>
+<span class="id" title="keyword">Require</span> <a class="idref" href="Undecidability.CFG.Reductions.CFPP_to_CFP.html#"><span class="id" title="library">Undecidability.CFG.Reductions.CFPP_to_CFP</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Undecidability.Synthetic.Definitions.html#"><span class="id" title="library">Undecidability.Synthetic.Definitions</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Theorem</span> <a id="reduction" class="idref" href="#reduction"><span class="id" title="lemma">reduction</span></a> :<br/>
+&nbsp;&nbsp;<a class="idref" href="Undecidability.CFG.CFP.html#CFPI"><span class="id" title="definition">CFPI</span></a> <a class="idref" href="Undecidability.Synthetic.Definitions.html#8d2edb2d53aefda0fb906bca2c603282"><span class="id" title="notation">⪯</span></a> <a class="idref" href="Undecidability.CFG.CFG.html#CFI"><span class="id" title="definition">CFI</span></a>.<br/>
+<span class="id" title="keyword">Proof</span>.<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">exists</span> (<span class="id" title="keyword">fun</span> '<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">R1</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">R2</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">a</span></a><a id="pat:8" class="idref" href="#pat:8"><span class="id" title="binder">)</span></a> =&gt; <a class="idref" href="http://coq.inria.fr/distrib/V8.16.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.CFG.Reductions.CFPP_to_CFP.html#G"><span class="id" title="definition">CFPP_to_CFP.G</span></a> <a class="idref" href="Undecidability.CFG.Reductions.CFPI_to_CFI.html#R1:3"><span class="id" title="variable">R1</span></a> <a class="idref" href="Undecidability.CFG.Reductions.CFPI_to_CFI.html#a:1"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.16.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="Undecidability.CFG.Reductions.CFPP_to_CFP.html#G"><span class="id" title="definition">CFPP_to_CFP.G</span></a> <a class="idref" href="Undecidability.CFG.Reductions.CFPI_to_CFI.html#R2:2"><span class="id" title="variable">R2</span></a> <a class="idref" href="Undecidability.CFG.Reductions.CFPI_to_CFI.html#a:1"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.16.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>). <span class="id" title="tactic">intros</span> [[<span class="id" title="var">R1</span> <span class="id" title="var">R2</span>] <span class="id" title="var">a</span>].<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">intuition</span>; <span class="id" title="var">cbn</span> <span class="id" title="tactic">in</span> *.<br/>
+&nbsp;&nbsp;- <span class="id" title="tactic">destruct</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> (<span class="id" title="var">A1</span> &amp; <span class="id" title="var">A2</span> &amp; <span class="id" title="var">HR1</span> &amp; <span class="id" title="var">HR2</span> &amp; <span class="id" title="var">HA1</span> &amp; <span class="id" title="var">HA2</span> &amp; <span class="id" title="var">H</span>).<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">exists</span> (<a class="idref" href="Undecidability.CFG.CFP.html#sigma"><span class="id" title="definition">sigma</span></a> <span class="id" title="var">a</span> <span class="id" title="var">A1</span>). <span class="id" title="tactic">split</span>; <span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.CFG.Reductions.CFPP_to_CFP.html#reduction_full"><span class="id" title="lemma">CFPP_to_CFP.reduction_full</span></a>; <span class="id" title="tactic">eauto</span>.<br/>
+&nbsp;&nbsp;- <span class="id" title="tactic">destruct</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> (<span class="id" title="var">x</span> &amp; <span class="id" title="var">HR1</span> &amp; <span class="id" title="var">HR2</span>).<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.CFG.Reductions.CFPP_to_CFP.html#reduction_full"><span class="id" title="lemma">CFPP_to_CFP.reduction_full</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">HR1</span> <span class="id" title="keyword">as</span> (<span class="id" title="var">A1</span> &amp; <span class="id" title="var">HR1</span> &amp; <span class="id" title="var">HA1</span> &amp; <span class="id" title="var">H1</span>).<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.CFG.Reductions.CFPP_to_CFP.html#reduction_full"><span class="id" title="lemma">CFPP_to_CFP.reduction_full</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">HR2</span> <span class="id" title="keyword">as</span> (<span class="id" title="var">A2</span> &amp; <span class="id" title="var">HR2</span> &amp; <span class="id" title="var">HA2</span> &amp; <span class="id" title="var">H2</span>).<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">exists</span> <span class="id" title="var">A1</span>, <span class="id" title="var">A2</span>. <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">eauto</span>.<br/>
+<span class="id" title="keyword">Qed</span>.<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>