YES
H-Termination proof of /tmp/aproveN7gh2V.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| ((mylength x) :: Main.Nat) |
module Main where
| import qualified Prelude
|
| data List a = Nil | Cons a (List a)
data Main.Nat = Z | S Main.Nat
|
|
mylength | Nil | = | Z |
mylength | (Cons x xs) | = | S (mylength xs) |
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((mylength x) :: Main.Nat) |
module Main where
| import qualified Prelude
|
| data List a = Nil | Cons a (List a)
data Main.Nat = Z | S Main.Nat
|
|
mylength | Nil | = | Z |
mylength | (Cons x xs) | = | S (mylength xs) |
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| ((mylength x) :: Main.Nat) |
module Main where
| import qualified Prelude
|
| data List a = Nil | Cons a (List a)
data Main.Nat = Z | S Main.Nat
|
|
mylength | Nil | = | Z |
mylength | (Cons x xs) | = | S (mylength xs) |
|
Haskell To QDPs
![](data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAYQAAAIpCAIAAAAttdgpAAA0nUlEQVR42u2dD0wU576wSaxRcjBq
QhpiCCF+Gm2kwRuNaQw52Xj5Io2eaD+9iTF+XHJCGg0Qay5Gc0LAKCl+IYaeUqWpRj3qRVtirJda
ajGggGLVSj0r5RBOy18BWQriiitdcb7fMu2cdXdZdmH/zO4+T00zzM7Ozrx/nvm977zzTpQCAKAD
okgCAEBGAADICACQEQAAMgIAZAQAgIwAABkBACAjAEBGAADICACQEQAAMgIAZAQAgIwAABkBACAj
AEBGAADICACQEQAAMgIAZAQAgIwAABkBACAjAEBGAADICACQEQAAMgIAZAQAgIwAABkBACAjAABk
BADICAAAGemDV+NWEgEAGQUTq+Wp6eHXP39TNGD86uWLZyQIADIKNONWy1DbjY7qI4+bLj3r/fHx
gy9lWda8HHtO4gAyggBp6En77c6aj/runn8x/EhbP/a0v//7ivZviwd//FYiJhIKkBH4i1evxp92
3e+s/bj3zn9bful0uY2sl08noqT68ZdjJBogI/CxhqQt1nXjWO93Zy1D3VNu/2KkT5pvXdc/Gem8
J98lAQEZgQ80ZO75e3fdp49unRodaPPKLNKIkyhJvjv6uBUlATKCmWrITaPME54PtovIpHEne0NJ
gIzAS4OYfpq5huyR4Eh22NNwQhZIXkBGMDVqD7RYw1cacgi13Pd/AyAj+E1DEr/4tT31atw60nmv
68ax/vsXPekLB0BGaMiPaB1StsFKI31kASAjNBRoDTkoaaTjTtf1TwaMX/06OkR2ADKKRLT77kG/
ySUNt6G2+s6aj1ASIKPIQiq8VHs9aMieiYfdbEoaaq2VZbIJkFH4a8hW4fX6rIZoyNT8zW9HiJIA
GYW5hnRfyUPraAGQUZhXbO3Ih39uZOg2ICM0FPyzePzgS731cAEgI48Iv56X4A5BAEBG09FQGN+T
0pT0rPdH8hqQkd41FPajdWxK+u4sD7gBMtIdE4MGb0TaoEGfTG8CgIx8pqEn7bcj9nEKX824BICM
ZlQPn3b/IPWw//uKMfNARAeGvyvp8YMveZoEkFGg617XjWN99z7neXf7ZBn+uZEH3AAZBYjRx609
N0/SKpmMyOnFB2QUVA01nOiu/+z5YDv57aGSTM3f8DQJICOfYZvQ/vbfJCB61t/CeD/vlNRaywNu
gIx8wIuRvt7vzqpj/NDQ9LB/wI2XSgIy8l5Dw4/67p7vunGMpx98riTSE5CRZ9Xm2WD/9xVd1z95
0n6bK7lvGTMPPG661F3/Ge+5BWQ0tYY6az9GQwFo/IruJeokNQAZvcbLF8+YSyzQUdLT/t+eueW2
ACAjwWp5anr4dce1ksGWazrRUFRUVNj/osboQFvPzZOPbp16bvqJWgQRKiPR0C//qLFp6MdvZVlH
SelnNTjvP4gyUnk+2G5T0u2/MZQUIktGL8eei4a6rn8ijTJZ1l1SRp6MFPuXSt77/MXwI2oUhLmM
fhsZXPuxyMjnjTKp0mazedeuXX+YYN++fbZmyOhoTk6Oumb37t3j47bOkZSUlOvXrzt8vaWlJT4+
3kENstmaNWvmzJkjH508edJBHwcPHly0aJF8unTp0qNHj9rv7cGDB+vWrZOP5HezsrLkwNSvRL2O
h3uzJz09PS8vz35Nfn7+tm3bfJWMtuf+rn/y+MGXEf74MYStjEQ9T9pvi4b81yiTKp2ZmXnp0iUx
zsDAwLvvvnv48GFtzeDg4Pr166XCy5ZffPGFLDt8XZQh29vLSIQidqiqqpKvt7W1vfXWW7Js/1tH
jhwZGRmRP5ubm99+++0TJ06on7a2toq8zp07Z52gvLx8x44dDupxPvLJ9ubA0NCQ7Fy2Uf+Uhbi4
ODk7X0ZJ49bhf97sunFswPiVrlrQgIxmWrJHOu8FYMohqdL2wYvU0tjYWPs1IpcVK1bYzDg+npCQ
IKHQv8IBs1lCGFGYvSy2b99uH6HU1NRoCpNtxB32v37r1q1Vq1apyxkZGQ6hjfzpXkZu9ubM1atX
tU9l4cKFC/7KuI47tgfcHn7NM7cQ2jJSL7BSmgMz5ZBU6bGxMfdrZs+erS4UFxdLg05bLy54//33
HWQxf/78/v7+fwV34+MiLG0bNYqx/zQ6Olr7osOnWjNtMhm52ZtL5OBLJti0aZNfU/Xl2HPtmVui
JAg9Gb16Na5GQ4+bLgXsoupJx7C2Rir/woULNQUsXry4qanJYZsoJ2bNmjXZnh2+6NWn7rd3ibTL
JCaS+K6rqyswrexf/lEjShpsuabDew6AjFxHQ+ZHD9WJUAM885lXMrLvJLpy5cratWudt5k3b57V
avXwtxxCKm8jI29ltHfvXmmsnT59es+ePQFLYevzJyKjztqPbW9eYYg86FZG2gSMtpnPhrqDkARe
yki9fSYNonXr1p07d855m/T09DNnzkxDRs59RqWlpdqnWng1bRnV1dVt2bJFXTYYDDU1NYFMZ1HS
4wdfMg0A6FRGowNt3fWf9TSckIWgJYGXMhLWr1+fn5+/aNEi9Za/wzatra3SfLt48eL4BA0NDe+9
954n+pAvyj5FcOoXHe6mLVu2TGwybRlJkCV76OnpsT9Ih0AsAIyZBwaMX0lL/GnXfQmHqYEQfBnZ
RsrVf6Y+TxDcR5ymIaPq6mpZo97vd7mN0WjcsGFDdHT0nDlzJICSlpGH+pAvauOMcnJyxCBa33ll
ZWVCQoLzOCMPZSTxWmFhof2aAwcOiOyCkuaiJAmEbTO9PHrIA24QNBmJfcRBoT7zmTjC/paZn7hz
505ycnK4Fr4XI3199z7n1dsQBBk9H2y3PfBd/9lIx53QDdGtVuvhw4ezsrL8sXNp0ImA1GaaxF/S
krIf8RSWWH7pVC9OKAkZBa7AddZ+bOspCOUCJw0oaXyJMqQB5Y/9X758OSUlJXoCWSgvL4+Qgjg6
0CYlpKfhBDOTICO/9Q487ZdQXH26lXso4B71mduemyeZmQQZ+TQaGuruv3+xs+YjJmAEz7G98rfr
vly9+r+v4F2byGjG0dDElMnqlEMvXzwjlcFrJU084CZFCCUho+lraMD4VUf1EX/M9QGRhjp1jCiJ
99wiIy+QsiLRUPu3xUwfAb5FnVQPJSEjD8rKi2fSHPv5myL+8S8A/2xtf565RUYwQ2w3sG//zUU2
REUZjUaXX3lu+qmz5iOmTwRkBL5kqO3GUGutSxm98cYbk33radf97vrPuBUAyAh8xqNbp1zOWq8+
cVZbWzvZF03N30hIxZOlgIzAB7wcey4NLpfDi1UZJSUlTTYRknyr//sK+cfoZEBGMFOe9bc8brrk
OhuiouLi4lJSUkpKSib7umio797ngy3XSElARjAjpKn1rPfHyWSUkZGxf//+xMTEvr5Jx/iNvxzr
uXlypOMOiQnICKZPT8MJ6/Mnk8no7NmzGzduLCsrcz/HkNXytOvGMQmySE9ARjAdxswD3fWfTZoN
UVESEC1YsMBisaxcudJNT7a6q45rJUGcGxMAGYUwI5333HT3qNMzrl69WjTU2NgoPpqsJ1vl+WC7
+IjhyICMwGv67n0uBnEvo9zc3P3798tCZmamm55sFfOjh9Jew0eAjMA7JJBx8xCDKqOqqioJjmTB
ZDJNKSNh+OfGnoYTPJAMyAg8xTLULZGRu2yYkJHFYin4939Xhoc937Pp4dd9d88zXRQgI/CIobYb
T7vuu9mgoKDgtyWDQams9Grn/fcvyj8GQwIygqmR4MXTGcJyc5W8PK92/mrc2vvd2YG//w8+AmQE
7ng59ry77lNPTVFdraxc6e1PqIOPRjrvkdqAjGBSnvX+aGr+xtOtzWZl7lzF4nWf9K+jQ501H40+
biXBARmBawZbrpl7/u7FFyQycjvocTIsQ90d10osv3SS5oCMwAXSRvNuHt5Dh5Sioun9ljoT26/P
Bkl2QEbweuvp2aDLqR3d2qtbaZn+o2cShUl8xMyQgIzgNZ603x7+580A/+hQ242u658wMyQgI/gX
XtzU9ymPmy4xMyQgI/gXEqFMxwinTillZTP5XfnRvnufi5IYfATICKZ+CmRSzp9X0tJm+Ouqj0zN
3+AjQEaRzlBrrfunQCZleFiJiVFMphkegDozJDPVAjKKdGxTO0775boGg3Lp0syP4eWLZ521HzM4
G5BR5CIaEhlN//v793v7kNpkvBjp66g+wmBIQEYRykjHHZfva/QUX3QbaTwfbJf4iMGQgIwikb57
n0/2LhCPMJuVuDgfHo8cTHfdpww+AmQUWbwat7Z/W+xmakePsPh4CsfhnxsZDAnIKLIYHWjr/e6s
Dg9ssOVaz82TzAwJyChSGGqrlzDEBztqb/f5sfXfvyhNSAZnAzKKCCQs8sGjqiaTEhvr88aaaKj/
+4rJXrQNgIzCh5cvnnXdOOabcc+rVyv19T4/QmmmPbp1KvBP8AIgo4DytPsH08OvfbOvzEyluNgf
B2m1PO2u+/RJ+23yC5BR2PL4wZfTfArEmfPnla1b/XSc4qPO2o+f9beQZYCMwhBpnXVcK5n+UyAO
mEy2h9Ss/upsHnvaLz6S/5NxgIzCjeeD7T03T/pyjytXKnfv+u+ARx+3dt04xuAjQEbhxmDLtaG2
G77cY1GRT56YdcNI573u+s/wESCjsOLRrVMvhh+F3GE/ab/NzJCAjMKH8ZdjPrupH3AGjF89fvAl
mQjIKBx41t/Sf/+i7/dbWzvzidamRBzae+e/fdzGBEBGQcHU/I1vngJxIDPTdo8/AJGd1dJd/9nT
7h/ISkBGoU3PzZO/jg75fr9lZcrOnYE5BevzJ911n+IjQEYhjNXytOvGMb/suq3Nt3MbTekjOZHR
x63kKSCjkORp130/Pn0aGzuT18x6y6/PBjtrPgrF24KAjMA2NYf50UN/7X3bNuX48UCezvPB9q7r
n/il1QmAjPxKZ+3HM53a0Q2lpbZu7MAibpX22rjVQuYCMgoZXoz0+avDSKW93faa2YAz1FZvm4mN
10ACMgoVhlprf/lHTbg2PweMX+EjQEa6pqioyDIxE2Pf3fPhevtJnYktXFULyChMSExMbG9vfz5q
/uA/016OPe/r6ysoKPDXjzU2BmboowsfWS09DSe08ZyHDh1qa2sj9wEZ6YjVq1ffvXvXaDQuWfK/
5M+8vLzU1FQ/yiglJVhnapuJreaj0QGbgzIyMnYGahAmICPwiLS0tKqqqrNnz27dutVsNsfHx1dX
V/vx9+Li/DfR2pS8GH6Un/V/mh/+0NTUFBMTY/L/43KAjMBTJEY4depUbm6utFxKS0slULL6VRYS
GVVVBfF8v/7q8sqVK0W7EgD6sUEKyAi8RTRUXFwsNbOioiIxMVFCJP/+ntT/oqLAn2ZJSYmc4O+H
ULBjxw6JB2NjY8VKlAFARrqgqKho//79cXFxoiT5v9Xfbaj6euWddwJ/mu3t7QaDQcLA4eFh+XPj
xo0SBkqIVFZWRhkAZKQLpI0mNXPBggXvvPOOhA9+/z2JRGJifP5aR8/Nu3z58traWlGSLGRnZy9Z
ssRqZXJIQEY6oLKy8o033oiKihIfqVGD37l7N1gyEpqamkRDEgw2NjZKs3Tu3Lla8w0AGQUTqZNR
E+Tm5kbIKVssFomJpI0mpywnnhK80QaAjOBftLe3qzLq6+uLqBOvrq6WNpp67vV+eAE3ICPwDrPZ
LLUxKSkpcD8p1tu2TSfnvnnzZtVHlARARjpIwQCHBmofdmD6pzxg586dkgISIVISABlFHitXKrSM
ABlB8MnOVhjgA8gIgk9JibJ/P8kAyAiCTWWl4r+5AQCQEXiKyRTINxcBICMAQEYAAMgIpsZiUbq7
SQZARhBsTp3SyThsAGQU2TQ2KqtXkwyAjGCS1Jx4SisQz2qZTEpsrMJcQoCMIpOffvopMTFR1c25
c+ccHDTZn/5iyRKlpSWQZy389a9/Xbp06Zw5cxYvXnzy5El//Fxvb+/atWtnz56dkpIiy1Panyd1
kVEkcubMmfT0dLUOrF+/vqenJ5gySkuzjX4M4FkXFxeLJpqbm1Vl5OTk+OPnMjIy8vLylIn3Psmy
5wEpIKOwJSsr69KlS7Jw+fJlWZaF7du3l5eXq6W/ra1tw4YNDpUhcM00ZeIJNT9MdOvmrCU+cvnu
xnv37iUnJ0ssI/+XZTUFDh8+PG/evNjYWDWE/PDDD+VP5yjG+edks5GREWViihJZdr8xMkJGEcH4
+LjoRhojEgSpaxISEjo6OrTSf/ToUWm2BE1G588rx48H/qydEQedPn1aFuRbsqxuKfGU7Or27dtv
vvmmrJGWnVhJ1kz5c/a/IoJzvzEyQkaRQkNDw6xZs9SrfVdXV3x8vEPpl7rR2toaHBkF/KwlMvrp
p5+ct7dXhrpsnwLqssRWf/zjH6Ojow8ePOjm59xHRs4bIyNkFBFYLBaDwVBXV5eamjo2NibVSRos
DqW/t7d33bp14SQjN2d95MgRl31GEg2pndkSH2mRkUtTiNocgh2Hn3PfZ+S8MTJCRhFBZmZmTU2N
LMj/ZTk9PV27f2Rf+qW6Bk1G3d0+f1OIm7NWJt7muHTpUolNFi9eLA0xdeWDBw+c+4wcTKH2Fs2f
P7+4uNjNzyl2d9Pk//39/e43jnodCi0yigiWLVsmLTJ9HVNqqr/fdq3HswZkBLpj504lAG+OBEBG
MAVioonWCgAygqBSX88TaoCMQAf09SkLFpAMgIxAB8TE2B6aBUBGEGQ++IBZ1gAZAQAgIwBARqAj
zGaltpZkAGQEwaatTfl95jMAZATBw2pV5s71+RNqAMhI17x88ayz9mPdHdby5YrRGB4pPDrQ1nPz
5PjLMQobMgJ3vBh+9Oj233R3WBs3KhPzH4YHv/yjxvTwawobMgJ3POtvedykv2r/wQdKUVHYJPKr
cWvvd2efdv9AeUNGMClP2m8PtlzT3WGVlYXZ47JWy9OuG8d+HR2iyCEjcI2YaKTjju4Oy2hUSkvD
LKlHB9q66z59+eIZpQ4ZgQukjSYtNdIhYOrvv3/x1atxkgIZgSOPbv/txfAj0iFg9N37fKjtBumA
jMCRrhvHrM+f6PHIKirC8tl9W+fR9U8sQzwJjIzgdTqqj4xbdTm8cOtW22vUwhHLL53iI7ESxQ8Z
wW+Mvxxr/7ZYpwd36JCSmxuuKT/UVi8N5FfjVgohMgIbvz4b7K77VKcHV1mppKWFa8q/ejXee+e/
RUkUQmQEv7UXer87q9ODu3tXSUoK48R/Ofa868YxOo+QEdgwP3o48Pf/0aspLWH/uOyL4Udd1z9h
5BEyAmX4nzeHWmv1e3yJibbpRMKawZZrEpzSeYSMIp3BH7/V4/BrjYICpb09vLPA1nn03dlf/lFD
aURGEU3//YsMvw460kyTxtroQBtJgYwil0e3/0YHqh6w/NLZca2EkUfIKHLR+3Pk0karrIyQvBj+
501b5xGPrSGjyKT96v/Tdemvr1feeSdysqPv7nlREsUSGUUctglnaz7S9SGaTEpsbETlSNf1T56b
fqJwIqPIYuxpf0/DCb0f5YIFEfWqa/WxNUYeIaPIQq7A0i7Q+1EmJSlNTRGVL0Nt9XQeIaPIwtzz
d/0Ov9bYvFk5ezai8kU01P99BZ1HyCiCGOm8FwKzfB06pOzfH2lZM261dN04RucRMoqc5sAN8ZHe
j7KxMXLu7tvzYqSPziNkFCmYHn7N8Gs9M/xzI51HyCgi6Lt7nuHXOqf/+wpdP8kMyMgn9DScCI3X
eBUUKGZzZOaRbc6j65886/2R4oqMwhm9D7/WWLJEaYnc5uTzwfaOayW8/REZhe8lV//DrzXCd2Z+
D5GWGhNmI6OwJTSGX6scOqTk5UVyZqkTZpuav6HcIqNwDP5NP/Xd+zw0jvX4cWXHDiJZiWRHH7dS
dJFRuPG0+4cB41ehcaxVVUpqKln2W+fRs0GSAhmFFb/8o2b458bQONa2NiU+nixTJuY86rl5ks4j
ZBRWPH7wpfnRw9A4VqtVKSoiy1RsnUcPvyYdkFFYlWkJ+0mHkEN925q0skkKZBQmdNd9ytCVEOXF
SB+dR8go5CkqKrJMsPv//u+hX0yHDh0KjeOurlZqa8k+jeGfG7vrPxu3WkgKZBSqJCYmtre3G43G
JUuWnD17Ni1UXmZfVhaBE4m45/GDL7X7oXJRaWvjTUfIKKRYvXr13bt3KyoqNm7cuHnz5uPHj4fG
cVdVKaHizUAx/nKs5+ZJ9W1rGRkZO3fuJE2QUSghoVBVVVVeXl5mZmZMTIwpVKaX7u62zT8Lr2N9
/qQge2vzwx+amppCKTeREaiX0FOnTm3dujVtglA69AULbPf44XW+/uryypUrzWZzampqQUEBCYKM
Qobc3Nzi4uKkpKT4+PiQaaOpJCYqdIv8TklJibS11WVx0I4dOyTgjY2NNUfqXCvIKPQoKir64IMP
oiYIsag+NdXWcwQTtLe3GwwGiXOHh4flz40bN5aWlkqIVFZWRuIgo9BA2mirV68WE6WFXH9wfb3t
bdfw+qVl+fLltbW1oiRZyM7OXrJkiZXGLDIKCSorK9WwKMTaaDAJTU1NoqH9+/c3NjYmJibOnTtX
a74BMtI1UmRDso0Gk2OxWCQmkjZabm6u5GxKSgppgoxCo69BlVHoHXp3t5KbSw5ORnV1tbTR1Myt
lyYtICOdYzabpbCG5AA5kRETiUyVuZs3bw7Viw0yisTUiYpqD8WeYKtViYmRNgk56B650oRqFiMj
n1d1mDZTJK73Q41IUvBxIQwtGXE18FfSrV5te9s12QGhU3+RUZiWg7Q0b8c9kh2AjMAPSZeRoZw6
RXYAMqL0BzvpTCZvO7DJDkBGoIukIzsAGQEyAgohMgrXclBZqWRnkx2AjCj9wU662lrFYCA7ABkF
v/QHvmp59YuycVxcnMuZ4bX9OC94JyMvnwKN5OwQurq65syZk5WVZb/y3r17//Ef/zFv3rzZs2fL
/7dt21ZXV6crI/T09GzZsiV6AlmQP6e9K6PRmJOTs3DhQuekk2SRxHHYOTLSS+mfjiBe3/jMmTMG
V8GLb2TU3m4bhE12eMz777+fnJxsP8PRyZMnly1bdvny5bGxMWViBpLt27frKn4cHR1NTEw8cuSI
dYLDhw8nJCTIyuntTU6/sLCwtbXV+RzHx8flU0kiZBSeMlJsMzKmnj59ehp7nvq3LBZl7lyyw0MG
BgYk9pE4SFvT3Ny8ePHioSHHl3dKzdePjEpKSjIzM+3X/PnPf575EbpMOnGxJJEkVATJSFaazeZd
u3b9YYJ9+/apVwAJINU1u3fvFk/LypSUlOvXrzt8vaWlJX7igXX7nctma9askThTPpLLncMBHDx4
cNGiRfLp0qVLjx49ar+3Bw8erFu3Tj6S35VIVX2OX3F6jMvDvTmfuzQN5FI2ODjo+8hoYiOyw8Ps
KCsrkwuDQ6B04sQJ9yl25cqVVatWqU0kWZAYysNzEcft2bNHTl+qt3x3/fr1lZWVLn8iPT09Ly/P
fk1+fr60FtXlDRs2XL161f5T+fPdd9+dxq48KV1ynPZz9UaEjET2ly5dkiIuGpaUleBTWyP1VlJE
8li2/OKLL2TZuXEr29vvXEqwFIiqqir5eltb21tvvVX1+3MS6m/JlWRkZES9GL799ttaEZR4VYrL
uXPn1Bi4vLx8x44d7gXhZm+Tnftf//pX2a1fZBQTo3gz53wkZ8eWLVtkz/ZrJCzq7e11k1wNDQ1v
vvmmeiKCLMTFxWk9Su5/XSQiXlDfCCBtQPmurHH5K6ItOWv5uhavya9oV6958+apTUgN+VNWTmNX
npQuSXNJqMiSkf3VUpIsNjbWfo2U5hUrVqjtWAkr5NqrfSS5K9dMNZLUdi7tfPuLUk1NjVZnZBuH
mPbWrVtyiVOXMzIyHK6l8qf70u9mb27Ofe3atXJUvpdRd7dXLyyK5OyQWipRqv0aiVncJ9emTZvO
nDljv0Za3H/60588+fUpd+4Q7GhflIULFy5oH82aNct5ezc7d7MrT0pXT0+PXEgiS0YOsndeoyV3
cXGxtCDs2/NaH5u28/nz5/f399t3xUkN0bZRL1z2n0rYrH3R4VOtXTBZ6XezNzfnLhVYAgTtHH0m
I7LD4+xwrsBT+kIO2/L6Azf2UYn7X/+3f/s3ad7a97+4R1K1ZAIxoP16b2XkZlceli5pckaWjDxf
I/m9cOFCLdcltG5qanKuyQ5oWej+ALz91MPTcbleWjpae15vMoqE7HCuwHLw7m+Tu9yVth/3v97R
0SEukI2Tk5OlsSltXvdZI40pCWQk8HQI37xqprnfFTKaaem375W4cuWKtHect5G8meyNNO4PYBqX
4mnLSL11qrbnfSaj3Fzl/Hmyw5N0k9aHQ+WcsgN7ysjIk0w3Go3nzp2ThEpPT3fzW3v37pUWljQD
9+zZY7/eqw5s97vysJkWFxeHjNy1caTBL/m6bt06+z5IbRvJZoe2vYcH4NxJUVpaqn3qHCHPREZq
54v6sgpfyqioiOzwJN2cO7DlwpCYmOjm1r6ENg7DMuS87PuMPP91sZibtlVdXZ3WbWwwGOy7F6W1
9ec//9l+Y/e39t3sig5sH5R+ZeKOY35+vlzc1HvMDtu0trZKyH3x4kX1rkdDQ8N7773nyQHIF2Wf
UkbVLzrcvlm2bJnDYNwZykjYt29fWVmZz2RUUKB480b5SM4O51v7yu+DHisrK9VQTq4W27Zt0/ag
3k2TAFA9HllwuJvm5tfF1BcuXFADvdHR0cLCwsnupkn0J8egNRjV1NMiRPmuNLgkFFXvMBYXF8un
kw16dL8rT1JJkijibu17u6a6ulrWqDeYXW4jwbBkdnR0tLR4pRxoke2UByBf1Aa25OTkSHZqVzAp
o1IOnAe2zERGcoVcs2aNz2QkYdH+/WSHJ+nmPOhR5c6dO+rjIPJFaSfKsv1YKhGQ5NfsCWRB/vQw
MW/durV9+3bZrQR0Ekj+13/9l0spqIGkqMp+zYEDB+zHgohcRJFzJpDDc9PPNeWu3M9yLYkTcYMe
p4ckk/09Gj8hRTM5OVnRAR4l3fnziqshbWSHS7KyshweBwGHPk0eB5kC9ZEch+cbfYW0IKTEq3G4
XPAlrLUfYqP3pPPywf0Izw6JKSRUkYAL9TizZ88eiUZ5UNYdEppKtC9l1OzNUGPPuXz5ckpKijre
XxbKy8t1Ujg8SjqjUUlKIjtA/y2bsGqmUQ5cRim2QdhkByAjSn9oJR3ZAcgIkBFQCJFReJeDQ4eU
qR41IDsAGVH6/Z90BQXK61PYkB2AjFyfDEwbj5K4okLZupXsgGAWwpCQUQT2ywQao1FZvpyspCSE
RjqTBOFcBC0W5Y03FP+M+qEkADKiCHrD6tVKdTW5SUlARhTBYFNQoNg9aQ3ICBlRBIGSAMiIIgiU
BGREEQw+bW1ePaQGyAgZUQT9Q26uV7OsATJCRhRB/1BZqbzzDhlKSUBGFMFgYzYrc+cqr7/KApAR
MqIIBoPVq5Xf3yINyAgZUQSDR16erecIKAnIiCIYZKqrlZUryVNKAjKiCAYbs9mrFzoCMkJGFEGg
JCAjoAgCJQEZUQT9jtVKHzYlARlRBPVBUpLS0kLOUhKQEUUw2GRm0o1NSUBGFEEdcOkSz4VQEpAR
RVAHmM1KTIxiMpG5yAgZUQSDjcGgnD1L5lISkBFFMNgUFysZGWQuJQEZUQSDzfAwzTRKAjKiCAIl
AZARRdAe3qRGSUBGFMHg09Rk68YGSgIyoggGn/h4eo4oCciIIqgDMjOVU6fIYkoCMqIIBpuqKmXz
ZrKYkoCMKILBxmpVYmOZop+SgIwogjrAYLA9qgaUBGREEQwyZWU8wU9JQEYUQaAkADKiCAIlARlR
BPVFX5/tzddASUBGFMEg09Zmu6dmtZLXyAgZ6ZGioiLTxOhktQhaLJaCgoKwPVuDQamvJ9MpCchI
j6SlpVVUVGhFsL6+PikpKWzPtqxM2b+fTKckICM9cujQoezsbK0IyuVR/TNsW2rLl5PplARkpEdq
a2vVC6BaBA0Gg3p5DFtSUuScyXdKAjLSHVarNSYmxmQySRG0WCwLFizo6+sL5xOWltrOneQ7JQEZ
6ZHU1FS5BkoRbGxsDP9uAqlg9GFTEpCRPikoKMjOzpYiqC6QIJQESgIyCg7qZVCKoHphJEEoCZQE
ZBQc1A4CKYJql0H4n7DVKg0SRj9SEpCRHjEYDFIEI6ibQGTEjCKUBGSkQ4qKiqQIRlA3wfnzyrZt
5DslARnpjvr6eimCEdRNIG2QuXNtr3iECC8JyEiHnQVSBCOrmyAtzRYfASUBGU33BKJC7p9Ok/LS
JVvPUWRnTXj/Q0Z+lxEH7KsYQFm50ocvm40i7qbgISMOmDMFZEQSU0WREdmBjDjgmVNVpbS0ICNk
hIyQUbApLfXVQ/zIiIKHjDjgGWAyKXFxPunGRkYUPGTEAc+MjAzbJEfICBkhI2QUZKqrbRP1IyNk
hIyCmMRRbokUGVmtypIlM+/GnuxMS0tLV6xYMXv27Hnz5m3ZsqWhocHNTrq6uubMmZOVleXjYhPw
tw/59heNRmNOTs7ChQuddytpJSnW09ODjMLT96dPn163bl0EhXIFBUpenj/O9MMPP5SUbJkwXUdH
R0ZGhvta+v777ycnJ1t9Pb2Jv2XkvH/f/qKkSWFhYWtrq/Nux8fH5VNJN2QUhjK6dOnSmjVrzD4a
mhwaMjKZbC8O8cOZxsXFDQwM2K85fPjwZHuQLSWAunfvns7jlMDLyP1um5qaJN0c0hkZhbyMqqur
3377bYd8pSdl2mc6a9YsuXR7uIeysrLU1x+Xk7onV4Vdu3b9YYJ9+/bJytHRUWmzqGt2796t7j8l
JeX69esOO5SILD4+3qEOy2ZysZGmjXx08uRJh3p+8ODBRYsWyadLly49evSo/d4ePHggUZ58JL8r
jSM5MPUrLlv3U+7NnvT09LzXI9P8/PxtruZ4mcxx69evL3v9LgQyCm0Z3bp1a9myZb29vSHXrvRZ
fOTrM5Vqb1/h3bNly5Zz58451L3MzEyJVcU4coV49913JbDS1gwODkollAovW37xxRey7NyfogZi
Wh0WoYgdqqqq5OttbW1vvfWWLNv/1pEjR0ZGRuTP5uZmuSydOHFC/VSaSCIvOTzrBOXl5Tt27HBQ
j/ORT7Y3B4aGhmTnso36pyxIRCln57mM5Hgk9ZBRmMjIaDSKidpm3FoJYRmtXDmTF4e4PFOpV4sX
L167dq1c6i9cuOA+eaVCdnV1OdQ9e5fJ3mJjY+3XiFxWrFihdp0kJCS02HXDS+QiIYwa5Gp1ePv2
7fYRSk1NjaYw2Ubc4XBxWrVqlbqckZHhENrIn+5l5GZvzly9elX7VBYkrbxqb/b09IhkkVE4yKij
o0NM5JfeihBK89JSJTPT52cqmpDo48CBAyICueBLS6e/v9/llrNnz3aue2NjY+7XaN8qLi6WBp22
XlygdetqdXj+/Pn2vy7HJsLStlGjGPtPo6OjtS86fKo10yaTkZu9uUQOvmSCTZs2TaPzSxqDyCjk
ZSTtMjFRXV1dKHZy+RKzWYITZbpvLvTkTKVC7t69W1pbnsvI8zVS+RcuXKgpQCKypqYmh22cB3DM
mjXLTT13oxv3n7rf3iXSLpOYSOI7h/AQGUWKjKQESGP+ypUrodjJ5Xvy8pTcXL+eqdVqdag2GtLQ
cG6meaUnrZNIMlTahs7bzJs3b7JxA+71MY3IyFsZ7d27Vxprp0+f3rNnj7cykmaaRJ3IKIRlJOVp
zZo1k7XPI1FGEhYtWDC9ubFdnulf/vIX52rz5ptvutyDyw5sr2Sk3j6T+Esag/a70rZJT08/c+bM
NGTk3GdUWlqqfaqFV9OWkQTmWg+0wWCoqanxSkZ0YIe8jCTXpUiFYieXH9mxQykp8dWZSuWRpodc
8McnuH379jvvvPPhhx+63IPLW/veNtzWr1+fn58vQZb9kAJtm9bWVmm+Xbx4UT2ehoaG9957zxN9
yBdlnyI49YsOd9Ocm/leyUguirIHbRS1epAOgZj7PUi6cWs/tGXE4yAuaGlRpvVuDJdnKvbJzMyU
aEVih+jo6D/+8Y9u7vQ7D3qchoyqq6tljXq/3+U2RqNxw4YNcjDSWpQASkTpoT7ki9o4o5ycHDGI
1slVWVmZkJDgPM7IQ5VIvFZYWGi/5sCBAyI79wVV+1RSjEGP4dBnxAHr6kyzsrJm/jiI1MzJbtj5
kDt37sihBj3ZeRyEuh3uMhIdeGkEn5ypNFXmzZsnccd0j9p6+PBhnz9nqyINOhGQ2kyT+EtaUp6P
5/Qfe/bskUiNB2Wp2+ErI2kjHD8eWmcqDShpfIkyzL575Yk9ly9fTklJiZ5AFsrLyyl4yIgD9j9N
TbYxR97UauYzouAhIw7YP2zdqhQXIyNqCjJCRvoIjjx+ehYZUfCQEQfsN3JzbTNkIyNqCjJCRkFm
eNj27hCjERlRU5CRiyQOuX+hneItLR7e4w/FrAnvf8gIgJgCkBH4ibNnld+n40BGgIwgeJSUKElJ
in8GEyIjZATgDTt3Kmlpiq9fIoSMkBGAl4iGUlKUDz5ARoCMINj09dmGQb4+bw4yAmQEwUAdlj3j
d2HrmVPyHyAjCAEioxsbkBGEDmEdHwEyghChu9vWXqusDL8zK5D/ABlBiEVGiYnh5yM6sJERhCDt
7cqSJcqpU8gIkBHooL0m8ZE307AhI0BG4B/6+mzjIWtrkREgIwg2YfSYCDJCRhAWSHwU4gORkBEy
grAgO9v2fH93d+ieAbf2kRGEC0VFtslq794lJQAZQbA5e1aJjQ3LIZGAjCDUMBptQ7RLS2mmATKC
YNPXF4rjj+jARkYAyAgZAfiV7m4lNdUWKCEjQEYQZIqKbF1IoTBKGxkhIwh3xETiI7ESMgJkBEFG
WmorVyoZGXp+fAQZISOIDMxmZfNmZf9+3R4gt/aREUQSw8OkATIC0A3d3WE2MRsgIwhNWlpsT9V+
8IGuHvSnmYaMICIRDW3dalNSe7tuKgnVBBlBxFJcbLvr39iIjJARQLCprrb56Px5ZISMAIKNtNR0
8MgIMkJGAL8jSjIakREyAtBHk62iAhkhI4Bgo971z8gI/PBIbu0jI4DXMZuVbdtsSmprC8CvFRUV
mUwmm4wKbDKyWCzqAiAjgAmOH7dN7+//6bTT0tIqJhqGUVG2alJfX58kHgRkBPAvGhsD8O6jQ4cO
ZWdnazKSQEn9E5ARgKuGm98GatfW1qqhkCojg8FQEaQedGQEoHvEDgsW2N6D5AesVmtMTIzJZBIZ
WSyWBQsW9IXIPLnICCAYNDXZ7vrn5vpjerbU1FSJhkRGjY2NdBghI4Cp6O5W0tKU1at93pFUUFCQ
nZ0tMlIXSGlkBOCROWwvra2v9+Eu1YBIZKSGSKQxMgLwDDGRT4cgqV1FIiO184gERkYAXuK7u2wG
g0FkRIcRMgKYbogUF+eTu2xFRUUiIzqMkBHAdJH22vLlM7/LVl9fLzKiwwgZAcwA0VBGxgzvslks
FpERHUbICCKmGPJv2v+QEQDFkKTjVIAaBcgIgGJI0nEqQI0CZARAMSTpOBWgRgEyAqAYknScClCj
ABkBhEUxVCeNDejZ+PQXjUZjTk7OwoULXe8WGQEgo8n279tfTE5OLiwsbG1tRUYAyCiYMppit8gI
wN/FUOqe2WzetWvXHybYt2+frBwdHZU2i7pm9+7d4+PjsjIlJeX69esOX29paYmPj3eow7LZmjVr
5syZIx+dPHnSoZ4fPHhw0aJF8unSpUuPHj1qv7cHDx6sW7dOPpLfzcrKkgNTvxL1Oh7uzZ709PS8
vDz7Nfn5+du2bUNGADqSUWZm5qVLl8Q4AwMD77777uHDh7U1g4OD69evlwovW37xxRey7PB1UYZs
b1+HRShih6qqKvl6W1vbW2+9Jcv2v3XkyJGRkRH5s7m5+e233z5x4oT6qTSRRF7nzp2zTlBeXr5j
xw4H9Tgf+WR7c2BoaEh2Ltuof8pCXFycnB0yAtCRjOyDF6mlsbGx9mtELitWrJAFkUtCQoKEQtpH
ErlICCMKs6/D27dvt49QampqNIXJNuIO+1+/devWqlWr1OWMjAyH0Eb+dC8jN3tz5urVq9qnsnDh
wgWaaQD6ktHY2Jj7NbNnz1YXiouLpUGnrRcXvP/++w51eP78+f39/do2ojARlraNGsXYfxodHa19
0eFTrZk2mYzc7M0lcvAlE2zatIk+IwDdycjzNVL5Fy5cqClg8eLFTU1NDttEOTFr1iw39dyNbtx/
6n57l0i7TGIiie+6urqQEUAIy8i+k+jKlStr16513mbevHnWSaagda+PaURG3spo79690lg7ffr0
nj17kBFAaMtIvX0mDaJ169adO3fOeZv09PQzZ85MQ0bOfUalpaXap1p4NW0Z1dXVbdmyRV02GAw1
NTXICCCEZSSsX78+Pz9/0aJF6i1/h21aW1ul+Xbx4sXxCRoaGt577z1P9CFflH2K4NQvOtxNW7Zs
mdhk2jKSIEv20NPTY3+QDoEYMgIIMRlVV1fLGvV+v8ttjEbjhg0boqOj58yZIwGUtIw81Id8URtn
lJOTIwbR+s4rKysTEhKcxxl5KCOJ1woLC+3XHDhwQGRn/0VnkBGA3ouhOML+lpmfuHPnTnJyMjWY
UwFk5AKr1Xr48OGsrCx/HKA06ERAajNN4i9pSdmPeKIGcypAMfwNaUBJ40uUIQ0ofxzg5cuXU1JS
oieQhfLycmowpwLICJARAMWQpONUgBoFyAiAYkjScSpAjQJkBBC4Ysi/af9DRgBEH0AyA1BLSGYA
agmQzADUEpIZgFoCJDMAtYRkBoh0TpEEyAgAkBEAADIC0BMFJAEyAqCWkMwAQC0hmQGoJSQzAFBL
SGYAagnJDADUEpIZQM8UkATICACQEQAAMgKgmYaMAIBaQjIDUEtIZgCglpDMANQSkpkkAKCWkMwA
1BIgmQE8pIAkQEYAgIwAAJARAM00ZAQA1BKSGYBaQjIDALWEZAaglpDMJAEAtYRkBqCWAMkM4CEF
JAEyAggeRUVFJpPJ5qICm40sFou6AMgIIKCkpaVVVFTYKkmUrZrU19cnJSWRLMgIINAcOnQoOztb
k5EESuqfgIwAAkptba0aCqkyMhgMaqAEyAggoFit1piYGJPJJDKyWCwLFizo6+sjWZARQBBITU2V
aEhk1NjYSIcRMgIIGgUFBdnZ2SIjdYEEQUYAwUENiERGaohEgiAjgOCgdhWJjNTOIxIEGQEEDYPB
IDKiwwgZAQSZoqIikREdRsgIIMjU19eLjOgwQkYAQcZisYiM6DBCRgCeF+WokPtHriEjCE8ZccDI
CIC6jYyQEQAyQkYA1G1khIwAkBEyAqBuIyNkBICMkBEAdRsZISOAYNdto9GYk5OzcOFCdSJaZISM
AIJTt5OTkwsLC1tbW5ERMgLQRd1GRsgIwI91Oz09PS8vz35Nfn7+tm3bkBEyAgho3R4aGoqPj29u
blb/lIW4uLjBwUFkhIwAAl23r169umrVKnVZFi5cuEAzDRkBBKdu79q1q2SCTZs2TfpbyAgZAfi7
bku7TGKihISErq4uZISMAIJWt/fu3SuNtdOnT+/ZswcZISOA4NTturq6LVu2qMsGg6GmpgYZISOA
QNdts9m8bNmynp4e9c/W1tbFixePjIwgI2QEENC6nZ6eXlhYaL/mwIEDO3bssHeQM8gIGQGEdt1G
RsgIkBEHjIwAqNvICBkBMuKAkREAdRsZISNARhwwMgKgbiMjZATIiANGRgDBqNsh949cQ0YAgIwA
AJARACAjAABkBADICAAAGQEAMgIAQEYAgIwAAJARACAjAABkBADICAAAGQEAMgIAQEYAgIwAAJAR
ACAjAABkBADICAAAGQEAMgIAQEYAgIwAAJARACAjAABkBADIiCQAAGQEAICMAAAZAQAgIwBARgAA
yAgAkBEAADICAGQEAICMAAAZAQAgIwBARgAAyAgAkBEAADICAGQEAICMAAAZAQAgIwAIR/4/2jbR
8BEhhOgAAAAASUVORK5CYII=)
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_mylength(Cons(x0, x1), h) → new_mylength(x1, h)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
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. From the DPs we obtained the following set of size-change graphs:
- new_mylength(Cons(x0, x1), h) → new_mylength(x1, h)
The graph contains the following edges 1 > 1, 2 >= 2