YES
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Frameset//EN"
"http:/www.w3.org/TR/html4/frameset.dtd">
<html>
<head>
<title>H-Termination proof of ../tpdb/FP/full_haskell/Prelude_atanh_1.hs</title>
</head>
<body>
<BR><B>H-Termination</B> of the given <I>Haskell-Program with start terms</I> could successfully be <font color=#00ff00>proven</font>:<BR><BR><BR><BR><pre>&#8627 <B>HASKELL</B></pre><pre>  &#8627 BR</pre><BR><html>
<body>mainModule Main<table cellspacing="0" cellpadding="0" border="0" frame="void">
<tr>
<td>
                   &nbsp;
                </td><td>((<FONT COLOR="#000088">atanh</FONT> :: <FONT COLOR="#666600">Float</FONT>&nbsp;<FONT COLOR="#666600">&nbsp;-&gt;&nbsp;</FONT>&nbsp;<FONT COLOR="#666600">Float</FONT>) :: <FONT COLOR="#666600">Float</FONT>&nbsp;<FONT COLOR="#666600">&nbsp;-&gt;&nbsp;</FONT>&nbsp;<FONT COLOR="#666600">Float</FONT>)</td>
</tr>
</table>
<br>module Main where<br>
<table cellspacing="0" cellpadding="0" border="0" frame="void">
<tr>
<td>&nbsp;&nbsp;</td><td valign="top">import qualified Prelude<br>
<br>
</td>
</tr>
</table>
<br>
</body>
</html>
<BR>Replaced joker patterns by fresh variables and removed binding patterns.<BR><BR><pre>&#8627 HASKELL</pre><pre>  &#8627 BR</pre><pre>    &#8627 <B>HASKELL</B></pre><pre>      &#8627 NumRed</pre><BR><html>
<body>mainModule Main<table cellspacing="0" cellpadding="0" border="0" frame="void">
<tr>
<td>
                   &nbsp;
                </td><td>((<FONT COLOR="#000088">atanh</FONT> :: <FONT COLOR="#666600">Float</FONT>&nbsp;<FONT COLOR="#666600">&nbsp;-&gt;&nbsp;</FONT>&nbsp;<FONT COLOR="#666600">Float</FONT>) :: <FONT COLOR="#666600">Float</FONT>&nbsp;<FONT COLOR="#666600">&nbsp;-&gt;&nbsp;</FONT>&nbsp;<FONT COLOR="#666600">Float</FONT>)</td>
</tr>
</table>
<br>module Main where<br>
<table cellspacing="0" cellpadding="0" border="0" frame="void">
<tr>
<td>&nbsp;&nbsp;</td><td valign="top">import qualified Prelude<br>
<br>
</td>
</tr>
</table>
<br>
</body>
</html>
<BR>Num Reduction:All numbers are transformed to thier corresponding representation with Succ, Pred and Zero.<BR><BR><pre>&#8627 HASKELL</pre><pre>  &#8627 BR</pre><pre>    &#8627 HASKELL</pre><pre>      &#8627 NumRed</pre><pre>        &#8627 <B>HASKELL</B></pre><pre>          &#8627 Narrow</pre><BR><html>
<body>mainModule Main<table cellspacing="0" cellpadding="0" border="0" frame="void">
<tr>
<td>
                   &nbsp;
                </td><td>(<FONT COLOR="#000088">atanh</FONT> :: <FONT COLOR="#666600">Float</FONT>&nbsp;<FONT COLOR="#666600">&nbsp;-&gt;&nbsp;</FONT>&nbsp;<FONT COLOR="#666600">Float</FONT>)</td>
</tr>
</table>
<br>module Main where<br>
<table cellspacing="0" cellpadding="0" border="0" frame="void">
<tr>
<td>&nbsp;&nbsp;</td><td valign="top">import qualified Prelude<br>
<br>
</td>
</tr>
</table>
<br>
</body>
</html>
<BR>Haskell To QDPs<BR><textarea cols="80" rows="25">digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="atanh\n",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="atanh vx3\n",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="(log (fromInt (Pos (Succ Zero)) + vx3) - log (fromInt (Pos (Succ Zero)) - vx3)) / fromInt (Pos (Succ (Succ Zero)))\n",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="primDivFloat (log (fromInt (Pos (Succ Zero)) + vx3) - log (fromInt (Pos (Succ Zero)) - vx3)) (fromInt (Pos (Succ (Succ Zero))))\n",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6 -> 10[label="",style="dashed", color="red", weight=0];
6[label="primDivFloat (primMinusFloat (log (fromInt (Pos (Succ Zero)) + vx3)) (log (fromInt (Pos (Succ Zero)) - vx3))) (fromInt (Pos (Succ (Succ Zero))))\n",fontsize=16,color="magenta"];6 -> 11[label="",style="dashed", color="magenta", weight=3];
11[label="log (fromInt (Pos (Succ Zero)) + vx3)\n",fontsize=16,color="black",shape="box"];11 -> 15[label="",style="solid", color="black", weight=3];
10[label="primDivFloat (primMinusFloat vx4 (log (fromInt (Pos (Succ Zero)) - vx3))) (fromInt (Pos (Succ (Succ Zero))))\n",fontsize=16,color="burlywood",shape="triangle"];239[label="vx4/Float vx40 vx41",fontsize=10,color="white",style="solid",shape="box"];10 -> 239[label="",style="solid", color="burlywood", weight=9];
239 -> 16[label="",style="solid", color="burlywood", weight=3];
15[label="primLogFloat (fromInt (Pos (Succ Zero)) + vx3)\n",fontsize=16,color="black",shape="box"];15 -> 18[label="",style="solid", color="black", weight=3];
16[label="primDivFloat (primMinusFloat (Float vx40 vx41) (log (fromInt (Pos (Succ Zero)) - vx3))) (fromInt (Pos (Succ (Succ Zero))))\n",fontsize=16,color="black",shape="box"];16 -> 19[label="",style="solid", color="black", weight=3];
18 -> 21[label="",style="dashed", color="red", weight=0];
18[label="terminator (fromInt (Pos (Succ Zero)) + vx3)\n",fontsize=16,color="magenta"];18 -> 22[label="",style="dashed", color="magenta", weight=3];
19 -> 26[label="",style="dashed", color="red", weight=0];
19[label="primDivFloat (primMinusFloat (Float vx40 vx41) (primLogFloat (fromInt (Pos (Succ Zero)) - vx3))) (fromInt (Pos (Succ (Succ Zero))))\n",fontsize=16,color="magenta"];19 -> 27[label="",style="dashed", color="magenta", weight=3];
22[label="fromInt (Pos (Succ Zero)) + vx3\n",fontsize=16,color="black",shape="box"];22 -> 24[label="",style="solid", color="black", weight=3];
21[label="terminator vx5\n",fontsize=16,color="black",shape="triangle"];21 -> 25[label="",style="solid", color="black", weight=3];
27[label="primLogFloat (fromInt (Pos (Succ Zero)) - vx3)\n",fontsize=16,color="black",shape="box"];27 -> 29[label="",style="solid", color="black", weight=3];
26[label="primDivFloat (primMinusFloat (Float vx40 vx41) vx6) (fromInt (Pos (Succ (Succ Zero))))\n",fontsize=16,color="burlywood",shape="triangle"];242[label="vx6/Float vx60 vx61",fontsize=10,color="white",style="solid",shape="box"];26 -> 242[label="",style="solid", color="burlywood", weight=9];
242 -> 30[label="",style="solid", color="burlywood", weight=3];
24[label="primPlusFloat (fromInt (Pos (Succ Zero))) vx3\n",fontsize=16,color="black",shape="box"];24 -> 31[label="",style="solid", color="black", weight=3];
25[label="ter1m vx5\n",fontsize=16,color="green",shape="box"];25 -> 32[label="",style="dashed", color="green", weight=3];
29 -> 21[label="",style="dashed", color="red", weight=0];
29[label="terminator (fromInt (Pos (Succ Zero)) - vx3)\n",fontsize=16,color="magenta"];29 -> 33[label="",style="dashed", color="magenta", weight=3];
30[label="primDivFloat (primMinusFloat (Float vx40 vx41) (Float vx60 vx61)) (fromInt (Pos (Succ (Succ Zero))))\n",fontsize=16,color="black",shape="box"];30 -> 34[label="",style="solid", color="black", weight=3];
31[label="primPlusFloat (primIntToFloat (Pos (Succ Zero))) vx3\n",fontsize=16,color="black",shape="box"];31 -> 35[label="",style="solid", color="black", weight=3];
32[label="vx5\n",fontsize=16,color="green",shape="box"];33[label="fromInt (Pos (Succ Zero)) - vx3\n",fontsize=16,color="black",shape="box"];33 -> 36[label="",style="solid", color="black", weight=3];
34[label="primDivFloat (Float (vx40 - vx60) (vx41 * vx61)) (fromInt (Pos (Succ (Succ Zero))))\n",fontsize=16,color="black",shape="box"];34 -> 37[label="",style="solid", color="black", weight=3];
35[label="primPlusFloat (Float (Pos (Succ Zero)) (Pos (Succ Zero))) vx3\n",fontsize=16,color="burlywood",shape="box"];244[label="vx3/Float vx30 vx31",fontsize=10,color="white",style="solid",shape="box"];35 -> 244[label="",style="solid", color="burlywood", weight=9];
244 -> 38[label="",style="solid", color="burlywood", weight=3];
36[label="primMinusFloat (fromInt (Pos (Succ Zero))) vx3\n",fontsize=16,color="black",shape="box"];36 -> 39[label="",style="solid", color="black", weight=3];
37[label="primDivFloat (Float (vx40 - vx60) (vx41 * vx61)) (primIntToFloat (Pos (Succ (Succ Zero))))\n",fontsize=16,color="black",shape="box"];37 -> 40[label="",style="solid", color="black", weight=3];
38[label="primPlusFloat (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (Float vx30 vx31)\n",fontsize=16,color="black",shape="box"];38 -> 41[label="",style="solid", color="black", weight=3];
39[label="primMinusFloat (primIntToFloat (Pos (Succ Zero))) vx3\n",fontsize=16,color="black",shape="box"];39 -> 42[label="",style="solid", color="black", weight=3];
40[label="primDivFloat (Float (vx40 - vx60) (vx41 * vx61)) (Float (Pos (Succ (Succ Zero))) (Pos (Succ Zero)))\n",fontsize=16,color="black",shape="box"];40 -> 43[label="",style="solid", color="black", weight=3];
41[label="Float (Pos (Succ Zero) + vx30) (Pos (Succ Zero) * vx31)\n",fontsize=16,color="green",shape="box"];41 -> 44[label="",style="dashed", color="green", weight=3];
41 -> 45[label="",style="dashed", color="green", weight=3];
42[label="primMinusFloat (Float (Pos (Succ Zero)) (Pos (Succ Zero))) vx3\n",fontsize=16,color="burlywood",shape="box"];245[label="vx3/Float vx30 vx31",fontsize=10,color="white",style="solid",shape="box"];42 -> 245[label="",style="solid", color="burlywood", weight=9];
245 -> 46[label="",style="solid", color="burlywood", weight=3];
43[label="Float ((vx40 - vx60) * Pos (Succ Zero)) (vx41 * vx61 * Pos (Succ (Succ Zero)))\n",fontsize=16,color="green",shape="box"];43 -> 47[label="",style="dashed", color="green", weight=3];
43 -> 48[label="",style="dashed", color="green", weight=3];
44[label="Pos (Succ Zero) + vx30\n",fontsize=16,color="black",shape="box"];44 -> 49[label="",style="solid", color="black", weight=3];
45[label="Pos (Succ Zero) * vx31\n",fontsize=16,color="black",shape="triangle"];45 -> 50[label="",style="solid", color="black", weight=3];
46[label="primMinusFloat (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (Float vx30 vx31)\n",fontsize=16,color="black",shape="box"];46 -> 51[label="",style="solid", color="black", weight=3];
47[label="(vx40 - vx60) * Pos (Succ Zero)\n",fontsize=16,color="black",shape="box"];47 -> 52[label="",style="solid", color="black", weight=3];
48[label="vx41 * vx61 * Pos (Succ (Succ Zero))\n",fontsize=16,color="black",shape="box"];48 -> 53[label="",style="solid", color="black", weight=3];
49[label="primPlusInt (Pos (Succ Zero)) vx30\n",fontsize=16,color="burlywood",shape="box"];246[label="vx30/Pos vx300",fontsize=10,color="white",style="solid",shape="box"];49 -> 246[label="",style="solid", color="burlywood", weight=9];
246 -> 54[label="",style="solid", color="burlywood", weight=3];
247[label="vx30/Neg vx300",fontsize=10,color="white",style="solid",shape="box"];49 -> 247[label="",style="solid", color="burlywood", weight=9];
247 -> 55[label="",style="solid", color="burlywood", weight=3];
50[label="primMulInt (Pos (Succ Zero)) vx31\n",fontsize=16,color="burlywood",shape="box"];248[label="vx31/Pos vx310",fontsize=10,color="white",style="solid",shape="box"];50 -> 248[label="",style="solid", color="burlywood", weight=9];
248 -> 56[label="",style="solid", color="burlywood", weight=3];
249[label="vx31/Neg vx310",fontsize=10,color="white",style="solid",shape="box"];50 -> 249[label="",style="solid", color="burlywood", weight=9];
249 -> 57[label="",style="solid", color="burlywood", weight=3];
51[label="Float (Pos (Succ Zero) - vx30) (Pos (Succ Zero) * vx31)\n",fontsize=16,color="green",shape="box"];51 -> 58[label="",style="dashed", color="green", weight=3];
51 -> 59[label="",style="dashed", color="green", weight=3];
52[label="primMulInt (vx40 - vx60) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];52 -> 60[label="",style="solid", color="black", weight=3];
53[label="primMulInt (vx41 * vx61) (Pos (Succ (Succ Zero)))\n",fontsize=16,color="black",shape="box"];53 -> 61[label="",style="solid", color="black", weight=3];
54[label="primPlusInt (Pos (Succ Zero)) (Pos vx300)\n",fontsize=16,color="black",shape="box"];54 -> 62[label="",style="solid", color="black", weight=3];
55[label="primPlusInt (Pos (Succ Zero)) (Neg vx300)\n",fontsize=16,color="black",shape="box"];55 -> 63[label="",style="solid", color="black", weight=3];
56[label="primMulInt (Pos (Succ Zero)) (Pos vx310)\n",fontsize=16,color="black",shape="box"];56 -> 64[label="",style="solid", color="black", weight=3];
57[label="primMulInt (Pos (Succ Zero)) (Neg vx310)\n",fontsize=16,color="black",shape="box"];57 -> 65[label="",style="solid", color="black", weight=3];
58[label="Pos (Succ Zero) - vx30\n",fontsize=16,color="black",shape="box"];58 -> 66[label="",style="solid", color="black", weight=3];
59 -> 45[label="",style="dashed", color="red", weight=0];
59[label="Pos (Succ Zero) * vx31\n",fontsize=16,color="magenta"];60[label="primMulInt (primMinusInt vx40 vx60) (Pos (Succ Zero))\n",fontsize=16,color="burlywood",shape="box"];251[label="vx40/Pos vx400",fontsize=10,color="white",style="solid",shape="box"];60 -> 251[label="",style="solid", color="burlywood", weight=9];
251 -> 67[label="",style="solid", color="burlywood", weight=3];
252[label="vx40/Neg vx400",fontsize=10,color="white",style="solid",shape="box"];60 -> 252[label="",style="solid", color="burlywood", weight=9];
252 -> 68[label="",style="solid", color="burlywood", weight=3];
61[label="primMulInt (primMulInt vx41 vx61) (Pos (Succ (Succ Zero)))\n",fontsize=16,color="burlywood",shape="box"];253[label="vx41/Pos vx410",fontsize=10,color="white",style="solid",shape="box"];61 -> 253[label="",style="solid", color="burlywood", weight=9];
253 -> 69[label="",style="solid", color="burlywood", weight=3];
254[label="vx41/Neg vx410",fontsize=10,color="white",style="solid",shape="box"];61 -> 254[label="",style="solid", color="burlywood", weight=9];
254 -> 70[label="",style="solid", color="burlywood", weight=3];
62[label="Pos (primPlusNat (Succ Zero) vx300)\n",fontsize=16,color="green",shape="box"];62 -> 71[label="",style="dashed", color="green", weight=3];
63[label="primMinusNat (Succ Zero) vx300\n",fontsize=16,color="burlywood",shape="triangle"];255[label="vx300/Succ vx3000",fontsize=10,color="white",style="solid",shape="box"];63 -> 255[label="",style="solid", color="burlywood", weight=9];
255 -> 72[label="",style="solid", color="burlywood", weight=3];
256[label="vx300/Zero",fontsize=10,color="white",style="solid",shape="box"];63 -> 256[label="",style="solid", color="burlywood", weight=9];
256 -> 73[label="",style="solid", color="burlywood", weight=3];
64[label="Pos (primMulNat (Succ Zero) vx310)\n",fontsize=16,color="green",shape="box"];64 -> 74[label="",style="dashed", color="green", weight=3];
65[label="Neg (primMulNat (Succ Zero) vx310)\n",fontsize=16,color="green",shape="box"];65 -> 75[label="",style="dashed", color="green", weight=3];
66[label="primMinusInt (Pos (Succ Zero)) vx30\n",fontsize=16,color="burlywood",shape="box"];257[label="vx30/Pos vx300",fontsize=10,color="white",style="solid",shape="box"];66 -> 257[label="",style="solid", color="burlywood", weight=9];
257 -> 76[label="",style="solid", color="burlywood", weight=3];
258[label="vx30/Neg vx300",fontsize=10,color="white",style="solid",shape="box"];66 -> 258[label="",style="solid", color="burlywood", weight=9];
258 -> 77[label="",style="solid", color="burlywood", weight=3];
67[label="primMulInt (primMinusInt (Pos vx400) vx60) (Pos (Succ Zero))\n",fontsize=16,color="burlywood",shape="box"];259[label="vx60/Pos vx600",fontsize=10,color="white",style="solid",shape="box"];67 -> 259[label="",style="solid", color="burlywood", weight=9];
259 -> 78[label="",style="solid", color="burlywood", weight=3];
260[label="vx60/Neg vx600",fontsize=10,color="white",style="solid",shape="box"];67 -> 260[label="",style="solid", color="burlywood", weight=9];
260 -> 79[label="",style="solid", color="burlywood", weight=3];
68[label="primMulInt (primMinusInt (Neg vx400) vx60) (Pos (Succ Zero))\n",fontsize=16,color="burlywood",shape="box"];261[label="vx60/Pos vx600",fontsize=10,color="white",style="solid",shape="box"];68 -> 261[label="",style="solid", color="burlywood", weight=9];
261 -> 80[label="",style="solid", color="burlywood", weight=3];
262[label="vx60/Neg vx600",fontsize=10,color="white",style="solid",shape="box"];68 -> 262[label="",style="solid", color="burlywood", weight=9];
262 -> 81[label="",style="solid", color="burlywood", weight=3];
69[label="primMulInt (primMulInt (Pos vx410) vx61) (Pos (Succ (Succ Zero)))\n",fontsize=16,color="burlywood",shape="box"];263[label="vx61/Pos vx610",fontsize=10,color="white",style="solid",shape="box"];69 -> 263[label="",style="solid", color="burlywood", weight=9];
263 -> 82[label="",style="solid", color="burlywood", weight=3];
264[label="vx61/Neg vx610",fontsize=10,color="white",style="solid",shape="box"];69 -> 264[label="",style="solid", color="burlywood", weight=9];
264 -> 83[label="",style="solid", color="burlywood", weight=3];
70[label="primMulInt (primMulInt (Neg vx410) vx61) (Pos (Succ (Succ Zero)))\n",fontsize=16,color="burlywood",shape="box"];265[label="vx61/Pos vx610",fontsize=10,color="white",style="solid",shape="box"];70 -> 265[label="",style="solid", color="burlywood", weight=9];
265 -> 84[label="",style="solid", color="burlywood", weight=3];
266[label="vx61/Neg vx610",fontsize=10,color="white",style="solid",shape="box"];70 -> 266[label="",style="solid", color="burlywood", weight=9];
266 -> 85[label="",style="solid", color="burlywood", weight=3];
71[label="primPlusNat (Succ Zero) vx300\n",fontsize=16,color="burlywood",shape="triangle"];267[label="vx300/Succ vx3000",fontsize=10,color="white",style="solid",shape="box"];71 -> 267[label="",style="solid", color="burlywood", weight=9];
267 -> 86[label="",style="solid", color="burlywood", weight=3];
268[label="vx300/Zero",fontsize=10,color="white",style="solid",shape="box"];71 -> 268[label="",style="solid", color="burlywood", weight=9];
268 -> 87[label="",style="solid", color="burlywood", weight=3];
72[label="primMinusNat (Succ Zero) (Succ vx3000)\n",fontsize=16,color="black",shape="box"];72 -> 88[label="",style="solid", color="black", weight=3];
73[label="primMinusNat (Succ Zero) Zero\n",fontsize=16,color="black",shape="box"];73 -> 89[label="",style="solid", color="black", weight=3];
74[label="primMulNat (Succ Zero) vx310\n",fontsize=16,color="burlywood",shape="triangle"];269[label="vx310/Succ vx3100",fontsize=10,color="white",style="solid",shape="box"];74 -> 269[label="",style="solid", color="burlywood", weight=9];
269 -> 90[label="",style="solid", color="burlywood", weight=3];
270[label="vx310/Zero",fontsize=10,color="white",style="solid",shape="box"];74 -> 270[label="",style="solid", color="burlywood", weight=9];
270 -> 91[label="",style="solid", color="burlywood", weight=3];
75 -> 74[label="",style="dashed", color="red", weight=0];
75[label="primMulNat (Succ Zero) vx310\n",fontsize=16,color="magenta"];75 -> 92[label="",style="dashed", color="magenta", weight=3];
76[label="primMinusInt (Pos (Succ Zero)) (Pos vx300)\n",fontsize=16,color="black",shape="box"];76 -> 93[label="",style="solid", color="black", weight=3];
77[label="primMinusInt (Pos (Succ Zero)) (Neg vx300)\n",fontsize=16,color="black",shape="box"];77 -> 94[label="",style="solid", color="black", weight=3];
78[label="primMulInt (primMinusInt (Pos vx400) (Pos vx600)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];78 -> 95[label="",style="solid", color="black", weight=3];
79[label="primMulInt (primMinusInt (Pos vx400) (Neg vx600)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];79 -> 96[label="",style="solid", color="black", weight=3];
80[label="primMulInt (primMinusInt (Neg vx400) (Pos vx600)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];80 -> 97[label="",style="solid", color="black", weight=3];
81[label="primMulInt (primMinusInt (Neg vx400) (Neg vx600)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];81 -> 98[label="",style="solid", color="black", weight=3];
82[label="primMulInt (primMulInt (Pos vx410) (Pos vx610)) (Pos (Succ (Succ Zero)))\n",fontsize=16,color="black",shape="box"];82 -> 99[label="",style="solid", color="black", weight=3];
83[label="primMulInt (primMulInt (Pos vx410) (Neg vx610)) (Pos (Succ (Succ Zero)))\n",fontsize=16,color="black",shape="box"];83 -> 100[label="",style="solid", color="black", weight=3];
84[label="primMulInt (primMulInt (Neg vx410) (Pos vx610)) (Pos (Succ (Succ Zero)))\n",fontsize=16,color="black",shape="box"];84 -> 101[label="",style="solid", color="black", weight=3];
85[label="primMulInt (primMulInt (Neg vx410) (Neg vx610)) (Pos (Succ (Succ Zero)))\n",fontsize=16,color="black",shape="box"];85 -> 102[label="",style="solid", color="black", weight=3];
86[label="primPlusNat (Succ Zero) (Succ vx3000)\n",fontsize=16,color="black",shape="box"];86 -> 103[label="",style="solid", color="black", weight=3];
87[label="primPlusNat (Succ Zero) Zero\n",fontsize=16,color="black",shape="box"];87 -> 104[label="",style="solid", color="black", weight=3];
88[label="primMinusNat Zero vx3000\n",fontsize=16,color="burlywood",shape="box"];272[label="vx3000/Succ vx30000",fontsize=10,color="white",style="solid",shape="box"];88 -> 272[label="",style="solid", color="burlywood", weight=9];
272 -> 105[label="",style="solid", color="burlywood", weight=3];
273[label="vx3000/Zero",fontsize=10,color="white",style="solid",shape="box"];88 -> 273[label="",style="solid", color="burlywood", weight=9];
273 -> 106[label="",style="solid", color="burlywood", weight=3];
89[label="Pos (Succ Zero)\n",fontsize=16,color="green",shape="box"];90[label="primMulNat (Succ Zero) (Succ vx3100)\n",fontsize=16,color="black",shape="box"];90 -> 107[label="",style="solid", color="black", weight=3];
91[label="primMulNat (Succ Zero) Zero\n",fontsize=16,color="black",shape="box"];91 -> 108[label="",style="solid", color="black", weight=3];
92[label="vx310\n",fontsize=16,color="green",shape="box"];93 -> 63[label="",style="dashed", color="red", weight=0];
93[label="primMinusNat (Succ Zero) vx300\n",fontsize=16,color="magenta"];93 -> 109[label="",style="dashed", color="magenta", weight=3];
94[label="Pos (primPlusNat (Succ Zero) vx300)\n",fontsize=16,color="green",shape="box"];94 -> 110[label="",style="dashed", color="green", weight=3];
95[label="primMulInt (primMinusNat vx400 vx600) (Pos (Succ Zero))\n",fontsize=16,color="burlywood",shape="triangle"];275[label="vx400/Succ vx4000",fontsize=10,color="white",style="solid",shape="box"];95 -> 275[label="",style="solid", color="burlywood", weight=9];
275 -> 111[label="",style="solid", color="burlywood", weight=3];
276[label="vx400/Zero",fontsize=10,color="white",style="solid",shape="box"];95 -> 276[label="",style="solid", color="burlywood", weight=9];
276 -> 112[label="",style="solid", color="burlywood", weight=3];
96[label="primMulInt (Pos (primPlusNat vx400 vx600)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];96 -> 113[label="",style="solid", color="black", weight=3];
97[label="primMulInt (Neg (primPlusNat vx400 vx600)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];97 -> 114[label="",style="solid", color="black", weight=3];
98 -> 95[label="",style="dashed", color="red", weight=0];
98[label="primMulInt (primMinusNat vx600 vx400) (Pos (Succ Zero))\n",fontsize=16,color="magenta"];98 -> 115[label="",style="dashed", color="magenta", weight=3];
98 -> 116[label="",style="dashed", color="magenta", weight=3];
99[label="primMulInt (Pos (primMulNat vx410 vx610)) (Pos (Succ (Succ Zero)))\n",fontsize=16,color="black",shape="triangle"];99 -> 117[label="",style="solid", color="black", weight=3];
100[label="primMulInt (Neg (primMulNat vx410 vx610)) (Pos (Succ (Succ Zero)))\n",fontsize=16,color="black",shape="triangle"];100 -> 118[label="",style="solid", color="black", weight=3];
101 -> 100[label="",style="dashed", color="red", weight=0];
101[label="primMulInt (Neg (primMulNat vx410 vx610)) (Pos (Succ (Succ Zero)))\n",fontsize=16,color="magenta"];101 -> 119[label="",style="dashed", color="magenta", weight=3];
101 -> 120[label="",style="dashed", color="magenta", weight=3];
102 -> 99[label="",style="dashed", color="red", weight=0];
102[label="primMulInt (Pos (primMulNat vx410 vx610)) (Pos (Succ (Succ Zero)))\n",fontsize=16,color="magenta"];102 -> 121[label="",style="dashed", color="magenta", weight=3];
102 -> 122[label="",style="dashed", color="magenta", weight=3];
103[label="Succ (Succ (primPlusNat Zero vx3000))\n",fontsize=16,color="green",shape="box"];103 -> 123[label="",style="dashed", color="green", weight=3];
104[label="Succ Zero\n",fontsize=16,color="green",shape="box"];105[label="primMinusNat Zero (Succ vx30000)\n",fontsize=16,color="black",shape="box"];105 -> 124[label="",style="solid", color="black", weight=3];
106[label="primMinusNat Zero Zero\n",fontsize=16,color="black",shape="box"];106 -> 125[label="",style="solid", color="black", weight=3];
107[label="primPlusNat (primMulNat Zero (Succ vx3100)) (Succ vx3100)\n",fontsize=16,color="black",shape="box"];107 -> 126[label="",style="solid", color="black", weight=3];
108[label="Zero\n",fontsize=16,color="green",shape="box"];109[label="vx300\n",fontsize=16,color="green",shape="box"];110 -> 71[label="",style="dashed", color="red", weight=0];
110[label="primPlusNat (Succ Zero) vx300\n",fontsize=16,color="magenta"];110 -> 127[label="",style="dashed", color="magenta", weight=3];
111[label="primMulInt (primMinusNat (Succ vx4000) vx600) (Pos (Succ Zero))\n",fontsize=16,color="burlywood",shape="box"];281[label="vx600/Succ vx6000",fontsize=10,color="white",style="solid",shape="box"];111 -> 281[label="",style="solid", color="burlywood", weight=9];
281 -> 128[label="",style="solid", color="burlywood", weight=3];
282[label="vx600/Zero",fontsize=10,color="white",style="solid",shape="box"];111 -> 282[label="",style="solid", color="burlywood", weight=9];
282 -> 129[label="",style="solid", color="burlywood", weight=3];
112[label="primMulInt (primMinusNat Zero vx600) (Pos (Succ Zero))\n",fontsize=16,color="burlywood",shape="box"];283[label="vx600/Succ vx6000",fontsize=10,color="white",style="solid",shape="box"];112 -> 283[label="",style="solid", color="burlywood", weight=9];
283 -> 130[label="",style="solid", color="burlywood", weight=3];
284[label="vx600/Zero",fontsize=10,color="white",style="solid",shape="box"];112 -> 284[label="",style="solid", color="burlywood", weight=9];
284 -> 131[label="",style="solid", color="burlywood", weight=3];
113[label="Pos (primMulNat (primPlusNat vx400 vx600) (Succ Zero))\n",fontsize=16,color="green",shape="box"];113 -> 132[label="",style="dashed", color="green", weight=3];
114[label="Neg (primMulNat (primPlusNat vx400 vx600) (Succ Zero))\n",fontsize=16,color="green",shape="box"];114 -> 133[label="",style="dashed", color="green", weight=3];
115[label="vx400\n",fontsize=16,color="green",shape="box"];116[label="vx600\n",fontsize=16,color="green",shape="box"];117[label="Pos (primMulNat (primMulNat vx410 vx610) (Succ (Succ Zero)))\n",fontsize=16,color="green",shape="box"];117 -> 134[label="",style="dashed", color="green", weight=3];
118[label="Neg (primMulNat (primMulNat vx410 vx610) (Succ (Succ Zero)))\n",fontsize=16,color="green",shape="box"];118 -> 135[label="",style="dashed", color="green", weight=3];
119[label="vx410\n",fontsize=16,color="green",shape="box"];120[label="vx610\n",fontsize=16,color="green",shape="box"];121[label="vx410\n",fontsize=16,color="green",shape="box"];122[label="vx610\n",fontsize=16,color="green",shape="box"];123[label="primPlusNat Zero vx3000\n",fontsize=16,color="burlywood",shape="triangle"];285[label="vx3000/Succ vx30000",fontsize=10,color="white",style="solid",shape="box"];123 -> 285[label="",style="solid", color="burlywood", weight=9];
285 -> 136[label="",style="solid", color="burlywood", weight=3];
286[label="vx3000/Zero",fontsize=10,color="white",style="solid",shape="box"];123 -> 286[label="",style="solid", color="burlywood", weight=9];
286 -> 137[label="",style="solid", color="burlywood", weight=3];
124[label="Neg (Succ vx30000)\n",fontsize=16,color="green",shape="box"];125[label="Pos Zero\n",fontsize=16,color="green",shape="box"];126 -> 123[label="",style="dashed", color="red", weight=0];
126[label="primPlusNat Zero (Succ vx3100)\n",fontsize=16,color="magenta"];126 -> 138[label="",style="dashed", color="magenta", weight=3];
127[label="vx300\n",fontsize=16,color="green",shape="box"];128[label="primMulInt (primMinusNat (Succ vx4000) (Succ vx6000)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];128 -> 139[label="",style="solid", color="black", weight=3];
129[label="primMulInt (primMinusNat (Succ vx4000) Zero) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];129 -> 140[label="",style="solid", color="black", weight=3];
130[label="primMulInt (primMinusNat Zero (Succ vx6000)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];130 -> 141[label="",style="solid", color="black", weight=3];
131[label="primMulInt (primMinusNat Zero Zero) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];131 -> 142[label="",style="solid", color="black", weight=3];
132[label="primMulNat (primPlusNat vx400 vx600) (Succ Zero)\n",fontsize=16,color="burlywood",shape="triangle"];288[label="vx400/Succ vx4000",fontsize=10,color="white",style="solid",shape="box"];132 -> 288[label="",style="solid", color="burlywood", weight=9];
288 -> 143[label="",style="solid", color="burlywood", weight=3];
289[label="vx400/Zero",fontsize=10,color="white",style="solid",shape="box"];132 -> 289[label="",style="solid", color="burlywood", weight=9];
289 -> 144[label="",style="solid", color="burlywood", weight=3];
133 -> 132[label="",style="dashed", color="red", weight=0];
133[label="primMulNat (primPlusNat vx400 vx600) (Succ Zero)\n",fontsize=16,color="magenta"];133 -> 145[label="",style="dashed", color="magenta", weight=3];
133 -> 146[label="",style="dashed", color="magenta", weight=3];
134 -> 193[label="",style="dashed", color="red", weight=0];
134[label="primMulNat (primMulNat vx410 vx610) (Succ (Succ Zero))\n",fontsize=16,color="magenta"];134 -> 194[label="",style="dashed", color="magenta", weight=3];
135 -> 193[label="",style="dashed", color="red", weight=0];
135[label="primMulNat (primMulNat vx410 vx610) (Succ (Succ Zero))\n",fontsize=16,color="magenta"];135 -> 195[label="",style="dashed", color="magenta", weight=3];
136[label="primPlusNat Zero (Succ vx30000)\n",fontsize=16,color="black",shape="box"];136 -> 150[label="",style="solid", color="black", weight=3];
137[label="primPlusNat Zero Zero\n",fontsize=16,color="black",shape="box"];137 -> 151[label="",style="solid", color="black", weight=3];
138[label="Succ vx3100\n",fontsize=16,color="green",shape="box"];139 -> 95[label="",style="dashed", color="red", weight=0];
139[label="primMulInt (primMinusNat vx4000 vx6000) (Pos (Succ Zero))\n",fontsize=16,color="magenta"];139 -> 152[label="",style="dashed", color="magenta", weight=3];
139 -> 153[label="",style="dashed", color="magenta", weight=3];
140[label="primMulInt (Pos (Succ vx4000)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];140 -> 154[label="",style="solid", color="black", weight=3];
141[label="primMulInt (Neg (Succ vx6000)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];141 -> 155[label="",style="solid", color="black", weight=3];
142[label="primMulInt (Pos Zero) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];142 -> 156[label="",style="solid", color="black", weight=3];
143[label="primMulNat (primPlusNat (Succ vx4000) vx600) (Succ Zero)\n",fontsize=16,color="burlywood",shape="box"];294[label="vx600/Succ vx6000",fontsize=10,color="white",style="solid",shape="box"];143 -> 294[label="",style="solid", color="burlywood", weight=9];
294 -> 157[label="",style="solid", color="burlywood", weight=3];
295[label="vx600/Zero",fontsize=10,color="white",style="solid",shape="box"];143 -> 295[label="",style="solid", color="burlywood", weight=9];
295 -> 158[label="",style="solid", color="burlywood", weight=3];
144[label="primMulNat (primPlusNat Zero vx600) (Succ Zero)\n",fontsize=16,color="burlywood",shape="box"];296[label="vx600/Succ vx6000",fontsize=10,color="white",style="solid",shape="box"];144 -> 296[label="",style="solid", color="burlywood", weight=9];
296 -> 159[label="",style="solid", color="burlywood", weight=3];
297[label="vx600/Zero",fontsize=10,color="white",style="solid",shape="box"];144 -> 297[label="",style="solid", color="burlywood", weight=9];
297 -> 160[label="",style="solid", color="burlywood", weight=3];
145[label="vx600\n",fontsize=16,color="green",shape="box"];146[label="vx400\n",fontsize=16,color="green",shape="box"];194[label="primMulNat vx410 vx610\n",fontsize=16,color="burlywood",shape="triangle"];298[label="vx410/Succ vx4100",fontsize=10,color="white",style="solid",shape="box"];194 -> 298[label="",style="solid", color="burlywood", weight=9];
298 -> 202[label="",style="solid", color="burlywood", weight=3];
299[label="vx410/Zero",fontsize=10,color="white",style="solid",shape="box"];194 -> 299[label="",style="solid", color="burlywood", weight=9];
299 -> 203[label="",style="solid", color="burlywood", weight=3];
193 -> 194[label="",style="dashed", color="red", weight=0];
193[label="primMulNat vx7 (Succ (Succ Zero))\n",fontsize=16,color="magenta"];193 -> 204[label="",style="dashed", color="magenta", weight=3];
193 -> 205[label="",style="dashed", color="magenta", weight=3];
195 -> 194[label="",style="dashed", color="red", weight=0];
195[label="primMulNat vx410 vx610\n",fontsize=16,color="magenta"];195 -> 206[label="",style="dashed", color="magenta", weight=3];
150[label="Succ vx30000\n",fontsize=16,color="green",shape="box"];151[label="Zero\n",fontsize=16,color="green",shape="box"];152[label="vx6000\n",fontsize=16,color="green",shape="box"];153[label="vx4000\n",fontsize=16,color="green",shape="box"];154[label="Pos (primMulNat (Succ vx4000) (Succ Zero))\n",fontsize=16,color="green",shape="box"];154 -> 165[label="",style="dashed", color="green", weight=3];
155[label="Neg (primMulNat (Succ vx6000) (Succ Zero))\n",fontsize=16,color="green",shape="box"];155 -> 166[label="",style="dashed", color="green", weight=3];
156[label="Pos (primMulNat Zero (Succ Zero))\n",fontsize=16,color="green",shape="box"];156 -> 167[label="",style="dashed", color="green", weight=3];
157[label="primMulNat (primPlusNat (Succ vx4000) (Succ vx6000)) (Succ Zero)\n",fontsize=16,color="black",shape="box"];157 -> 168[label="",style="solid", color="black", weight=3];
158[label="primMulNat (primPlusNat (Succ vx4000) Zero) (Succ Zero)\n",fontsize=16,color="black",shape="box"];158 -> 169[label="",style="solid", color="black", weight=3];
159[label="primMulNat (primPlusNat Zero (Succ vx6000)) (Succ Zero)\n",fontsize=16,color="black",shape="box"];159 -> 170[label="",style="solid", color="black", weight=3];
160[label="primMulNat (primPlusNat Zero Zero) (Succ Zero)\n",fontsize=16,color="black",shape="box"];160 -> 171[label="",style="solid", color="black", weight=3];
202[label="primMulNat (Succ vx4100) vx610\n",fontsize=16,color="burlywood",shape="box"];302[label="vx610/Succ vx6100",fontsize=10,color="white",style="solid",shape="box"];202 -> 302[label="",style="solid", color="burlywood", weight=9];
302 -> 215[label="",style="solid", color="burlywood", weight=3];
303[label="vx610/Zero",fontsize=10,color="white",style="solid",shape="box"];202 -> 303[label="",style="solid", color="burlywood", weight=9];
303 -> 216[label="",style="solid", color="burlywood", weight=3];
203[label="primMulNat Zero vx610\n",fontsize=16,color="burlywood",shape="box"];304[label="vx610/Succ vx6100",fontsize=10,color="white",style="solid",shape="box"];203 -> 304[label="",style="solid", color="burlywood", weight=9];
304 -> 217[label="",style="solid", color="burlywood", weight=3];
305[label="vx610/Zero",fontsize=10,color="white",style="solid",shape="box"];203 -> 305[label="",style="solid", color="burlywood", weight=9];
305 -> 218[label="",style="solid", color="burlywood", weight=3];
204[label="vx7\n",fontsize=16,color="green",shape="box"];205[label="Succ (Succ Zero)\n",fontsize=16,color="green",shape="box"];206[label="vx610\n",fontsize=16,color="green",shape="box"];165[label="primMulNat (Succ vx4000) (Succ Zero)\n",fontsize=16,color="black",shape="triangle"];165 -> 176[label="",style="solid", color="black", weight=3];
166 -> 165[label="",style="dashed", color="red", weight=0];
166[label="primMulNat (Succ vx6000) (Succ Zero)\n",fontsize=16,color="magenta"];166 -> 177[label="",style="dashed", color="magenta", weight=3];
167[label="primMulNat Zero (Succ Zero)\n",fontsize=16,color="black",shape="triangle"];167 -> 178[label="",style="solid", color="black", weight=3];
168 -> 165[label="",style="dashed", color="red", weight=0];
168[label="primMulNat (Succ (Succ (primPlusNat vx4000 vx6000))) (Succ Zero)\n",fontsize=16,color="magenta"];168 -> 179[label="",style="dashed", color="magenta", weight=3];
169 -> 165[label="",style="dashed", color="red", weight=0];
169[label="primMulNat (Succ vx4000) (Succ Zero)\n",fontsize=16,color="magenta"];170 -> 165[label="",style="dashed", color="red", weight=0];
170[label="primMulNat (Succ vx6000) (Succ Zero)\n",fontsize=16,color="magenta"];170 -> 180[label="",style="dashed", color="magenta", weight=3];
171 -> 167[label="",style="dashed", color="red", weight=0];
171[label="primMulNat Zero (Succ Zero)\n",fontsize=16,color="magenta"];215[label="primMulNat (Succ vx4100) (Succ vx6100)\n",fontsize=16,color="black",shape="box"];215 -> 225[label="",style="solid", color="black", weight=3];
216[label="primMulNat (Succ vx4100) Zero\n",fontsize=16,color="black",shape="box"];216 -> 226[label="",style="solid", color="black", weight=3];
217[label="primMulNat Zero (Succ vx6100)\n",fontsize=16,color="black",shape="box"];217 -> 227[label="",style="solid", color="black", weight=3];
218[label="primMulNat Zero Zero\n",fontsize=16,color="black",shape="box"];218 -> 228[label="",style="solid", color="black", weight=3];
176[label="primPlusNat (primMulNat vx4000 (Succ Zero)) (Succ Zero)\n",fontsize=16,color="burlywood",shape="box"];311[label="vx4000/Succ vx40000",fontsize=10,color="white",style="solid",shape="box"];176 -> 311[label="",style="solid", color="burlywood", weight=9];
311 -> 184[label="",style="solid", color="burlywood", weight=3];
312[label="vx4000/Zero",fontsize=10,color="white",style="solid",shape="box"];176 -> 312[label="",style="solid", color="burlywood", weight=9];
312 -> 185[label="",style="solid", color="burlywood", weight=3];
177[label="vx6000\n",fontsize=16,color="green",shape="box"];178[label="Zero\n",fontsize=16,color="green",shape="box"];179[label="Succ (primPlusNat vx4000 vx6000)\n",fontsize=16,color="green",shape="box"];179 -> 186[label="",style="dashed", color="green", weight=3];
180[label="vx6000\n",fontsize=16,color="green",shape="box"];225 -> 186[label="",style="dashed", color="red", weight=0];
225[label="primPlusNat (primMulNat vx4100 (Succ vx6100)) (Succ vx6100)\n",fontsize=16,color="magenta"];225 -> 232[label="",style="dashed", color="magenta", weight=3];
225 -> 233[label="",style="dashed", color="magenta", weight=3];
226[label="Zero\n",fontsize=16,color="green",shape="box"];227[label="Zero\n",fontsize=16,color="green",shape="box"];228[label="Zero\n",fontsize=16,color="green",shape="box"];184[label="primPlusNat (primMulNat (Succ vx40000) (Succ Zero)) (Succ Zero)\n",fontsize=16,color="black",shape="box"];184 -> 189[label="",style="solid", color="black", weight=3];
185[label="primPlusNat (primMulNat Zero (Succ Zero)) (Succ Zero)\n",fontsize=16,color="black",shape="box"];185 -> 190[label="",style="solid", color="black", weight=3];
186[label="primPlusNat vx4000 vx6000\n",fontsize=16,color="burlywood",shape="triangle"];314[label="vx4000/Succ vx40000",fontsize=10,color="white",style="solid",shape="box"];186 -> 314[label="",style="solid", color="burlywood", weight=9];
314 -> 191[label="",style="solid", color="burlywood", weight=3];
315[label="vx4000/Zero",fontsize=10,color="white",style="solid",shape="box"];186 -> 315[label="",style="solid", color="burlywood", weight=9];
315 -> 192[label="",style="solid", color="burlywood", weight=3];
232[label="Succ vx6100\n",fontsize=16,color="green",shape="box"];233 -> 194[label="",style="dashed", color="red", weight=0];
233[label="primMulNat vx4100 (Succ vx6100)\n",fontsize=16,color="magenta"];233 -> 236[label="",style="dashed", color="magenta", weight=3];
233 -> 237[label="",style="dashed", color="magenta", weight=3];
189 -> 186[label="",style="dashed", color="red", weight=0];
189[label="primPlusNat (primPlusNat (primMulNat vx40000 (Succ Zero)) (Succ Zero)) (Succ Zero)\n",fontsize=16,color="magenta"];189 -> 207[label="",style="dashed", color="magenta", weight=3];
189 -> 208[label="",style="dashed", color="magenta", weight=3];
190 -> 186[label="",style="dashed", color="red", weight=0];
190[label="primPlusNat Zero (Succ Zero)\n",fontsize=16,color="magenta"];190 -> 209[label="",style="dashed", color="magenta", weight=3];
190 -> 210[label="",style="dashed", color="magenta", weight=3];
191[label="primPlusNat (Succ vx40000) vx6000\n",fontsize=16,color="burlywood",shape="box"];319[label="vx6000/Succ vx60000",fontsize=10,color="white",style="solid",shape="box"];191 -> 319[label="",style="solid", color="burlywood", weight=9];
319 -> 211[label="",style="solid", color="burlywood", weight=3];
320[label="vx6000/Zero",fontsize=10,color="white",style="solid",shape="box"];191 -> 320[label="",style="solid", color="burlywood", weight=9];
320 -> 212[label="",style="solid", color="burlywood", weight=3];
192[label="primPlusNat Zero vx6000\n",fontsize=16,color="burlywood",shape="box"];321[label="vx6000/Succ vx60000",fontsize=10,color="white",style="solid",shape="box"];192 -> 321[label="",style="solid", color="burlywood", weight=9];
321 -> 213[label="",style="solid", color="burlywood", weight=3];
322[label="vx6000/Zero",fontsize=10,color="white",style="solid",shape="box"];192 -> 322[label="",style="solid", color="burlywood", weight=9];
322 -> 214[label="",style="solid", color="burlywood", weight=3];
236[label="vx4100\n",fontsize=16,color="green",shape="box"];237[label="Succ vx6100\n",fontsize=16,color="green",shape="box"];207[label="Succ Zero\n",fontsize=16,color="green",shape="box"];208 -> 186[label="",style="dashed", color="red", weight=0];
208[label="primPlusNat (primMulNat vx40000 (Succ Zero)) (Succ Zero)\n",fontsize=16,color="magenta"];208 -> 219[label="",style="dashed", color="magenta", weight=3];
208 -> 220[label="",style="dashed", color="magenta", weight=3];
209[label="Succ Zero\n",fontsize=16,color="green",shape="box"];210[label="Zero\n",fontsize=16,color="green",shape="box"];211[label="primPlusNat (Succ vx40000) (Succ vx60000)\n",fontsize=16,color="black",shape="box"];211 -> 221[label="",style="solid", color="black", weight=3];
212[label="primPlusNat (Succ vx40000) Zero\n",fontsize=16,color="black",shape="box"];212 -> 222[label="",style="solid", color="black", weight=3];
213[label="primPlusNat Zero (Succ vx60000)\n",fontsize=16,color="black",shape="box"];213 -> 223[label="",style="solid", color="black", weight=3];
214[label="primPlusNat Zero Zero\n",fontsize=16,color="black",shape="box"];214 -> 224[label="",style="solid", color="black", weight=3];
219[label="Succ Zero\n",fontsize=16,color="green",shape="box"];220 -> 194[label="",style="dashed", color="red", weight=0];
220[label="primMulNat vx40000 (Succ Zero)\n",fontsize=16,color="magenta"];220 -> 229[label="",style="dashed", color="magenta", weight=3];
220 -> 230[label="",style="dashed", color="magenta", weight=3];
221[label="Succ (Succ (primPlusNat vx40000 vx60000))\n",fontsize=16,color="green",shape="box"];221 -> 231[label="",style="dashed", color="green", weight=3];
222[label="Succ vx40000\n",fontsize=16,color="green",shape="box"];223[label="Succ vx60000\n",fontsize=16,color="green",shape="box"];224[label="Zero\n",fontsize=16,color="green",shape="box"];229[label="vx40000\n",fontsize=16,color="green",shape="box"];230[label="Succ Zero\n",fontsize=16,color="green",shape="box"];231 -> 186[label="",style="dashed", color="red", weight=0];
231[label="primPlusNat vx40000 vx60000\n",fontsize=16,color="magenta"];231 -> 234[label="",style="dashed", color="magenta", weight=3];
231 -> 235[label="",style="dashed", color="magenta", weight=3];
234[label="vx60000\n",fontsize=16,color="green",shape="box"];235[label="vx40000\n",fontsize=16,color="green",shape="box"];}
</textarea><BR><BR><pre>&#8627 HASKELL</pre><pre>  &#8627 BR</pre><pre>    &#8627 HASKELL</pre><pre>      &#8627 NumRed</pre><pre>        &#8627 HASKELL</pre><pre>          &#8627 Narrow</pre><pre>            &#8627 AND</pre><pre>              &#8627 <B>QDP</B></pre><pre>                &#8627 QDPSizeChangeProof</pre><pre>              &#8627 QDP</pre><pre>              &#8627 QDP</pre><BR>Q DP problem:<BR>The TRS P consists of the following rules:<BR><BLOCKQUOTE><BR><FONT COLOR=#0000cc>new_primMulNat</font>(<FONT COLOR=#0000cc>Succ</font>(<FONT COLOR=#cc0000>vx4100</font>), <FONT COLOR=#0000cc>Succ</font>(<FONT COLOR=#cc0000>vx6100</font>)) &#8594; <FONT COLOR=#0000cc>new_primMulNat</font>(<FONT COLOR=#cc0000>vx4100</font>, <FONT COLOR=#0000cc>Succ</font>(<FONT COLOR=#cc0000>vx6100</font>))</BLOCKQUOTE><BR>R is empty.<BR>Q is empty.<BR>We have to consider all minimal (P,Q,R)-chains.<BR>By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. <P>From the DPs we obtained the following set of size-change graphs:
<UL><LI><FONT COLOR=#0000cc>new_primMulNat</font>(<FONT COLOR=#0000cc>Succ</font>(<FONT COLOR=#cc0000>vx4100</font>), <FONT COLOR=#0000cc>Succ</font>(<FONT COLOR=#cc0000>vx6100</font>)) &#8594; <FONT COLOR=#0000cc>new_primMulNat</font>(<FONT COLOR=#cc0000>vx4100</font>, <FONT COLOR=#0000cc>Succ</font>(<FONT COLOR=#cc0000>vx6100</font>))<BR>The graph contains the following edges 1 > 1, 2 >= 2<P></LI></UL><BR><BR><pre>&#8627 HASKELL</pre><pre>  &#8627 BR</pre><pre>    &#8627 HASKELL</pre><pre>      &#8627 NumRed</pre><pre>        &#8627 HASKELL</pre><pre>          &#8627 Narrow</pre><pre>            &#8627 AND</pre><pre>              &#8627 QDP</pre><pre>              &#8627 <B>QDP</B></pre><pre>                &#8627 QDPSizeChangeProof</pre><pre>              &#8627 QDP</pre><BR>Q DP problem:<BR>The TRS P consists of the following rules:<BR><BLOCKQUOTE><BR><FONT COLOR=#0000cc>new_primPlusNat</font>(<FONT COLOR=#0000cc>Succ</font>(<FONT COLOR=#cc0000>vx40000</font>), <FONT COLOR=#0000cc>Succ</font>(<FONT COLOR=#cc0000>vx60000</font>)) &#8594; <FONT COLOR=#0000cc>new_primPlusNat</font>(<FONT COLOR=#cc0000>vx40000</font>, <FONT COLOR=#cc0000>vx60000</font>)</BLOCKQUOTE><BR>R is empty.<BR>Q is empty.<BR>We have to consider all minimal (P,Q,R)-chains.<BR>By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. <P>From the DPs we obtained the following set of size-change graphs:
<UL><LI><FONT COLOR=#0000cc>new_primPlusNat</font>(<FONT COLOR=#0000cc>Succ</font>(<FONT COLOR=#cc0000>vx40000</font>), <FONT COLOR=#0000cc>Succ</font>(<FONT COLOR=#cc0000>vx60000</font>)) &#8594; <FONT COLOR=#0000cc>new_primPlusNat</font>(<FONT COLOR=#cc0000>vx40000</font>, <FONT COLOR=#cc0000>vx60000</font>)<BR>The graph contains the following edges 1 > 1, 2 > 2<P></LI></UL><BR><BR><pre>&#8627 HASKELL</pre><pre>  &#8627 BR</pre><pre>    &#8627 HASKELL</pre><pre>      &#8627 NumRed</pre><pre>        &#8627 HASKELL</pre><pre>          &#8627 Narrow</pre><pre>            &#8627 AND</pre><pre>              &#8627 QDP</pre><pre>              &#8627 QDP</pre><pre>              &#8627 <B>QDP</B></pre><pre>                &#8627 QDPSizeChangeProof</pre><BR>Q DP problem:<BR>The TRS P consists of the following rules:<BR><BLOCKQUOTE><BR><FONT COLOR=#0000cc>new_primMulInt</font>(<FONT COLOR=#0000cc>Succ</font>(<FONT COLOR=#cc0000>vx4000</font>), <FONT COLOR=#0000cc>Succ</font>(<FONT COLOR=#cc0000>vx6000</font>)) &#8594; <FONT COLOR=#0000cc>new_primMulInt</font>(<FONT COLOR=#cc0000>vx4000</font>, <FONT COLOR=#cc0000>vx6000</font>)</BLOCKQUOTE><BR>R is empty.<BR>Q is empty.<BR>We have to consider all minimal (P,Q,R)-chains.<BR>By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. <P>From the DPs we obtained the following set of size-change graphs:
<UL><LI><FONT COLOR=#0000cc>new_primMulInt</font>(<FONT COLOR=#0000cc>Succ</font>(<FONT COLOR=#cc0000>vx4000</font>), <FONT COLOR=#0000cc>Succ</font>(<FONT COLOR=#cc0000>vx6000</font>)) &#8594; <FONT COLOR=#0000cc>new_primMulInt</font>(<FONT COLOR=#cc0000>vx4000</font>, <FONT COLOR=#cc0000>vx6000</font>)<BR>The graph contains the following edges 1 > 1, 2 > 2<P></LI></UL><BR><BR></body>


