YES
H-Termination proof of /tmp/aproveFFCgBE.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
module Main where
| import qualified Prelude
|
| data List a = Nil | Cons a (List a)
data Main.Nat = Z | S Main.Nat
|
|
mysum | Nil | = | Z |
mysum | (Cons x xs) | = | plus x (mysum xs) |
|
|
plus | Z y | = | y |
plus | (S x) y | = | S (plus x y) |
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
module Main where
| import qualified Prelude
|
| data List a = Nil | Cons a (List a)
data Main.Nat = Z | S Main.Nat
|
|
mysum | Nil | = | Z |
mysum | (Cons x xs) | = | plus x (mysum xs) |
|
|
plus | Z y | = | y |
plus | (S x) y | = | S (plus x y) |
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
module Main where
| import qualified Prelude
|
| data List a = Nil | Cons a (List a)
data Main.Nat = Z | S Main.Nat
|
|
mysum | Nil | = | Z |
mysum | (Cons x xs) | = | plus x (mysum xs) |
|
|
plus | Z y | = | y |
plus | (S x) y | = | S (plus x y) |
|
Haskell To QDPs
![](data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAcgAAAOBCAIAAAD6C6cwAABmFElEQVR42uy9D0xTZx+wbeIMM+o3
TchCDDHEaHRRo0azGEOWvr68UT9ddNElxBBeYngXfcVMMs3MEyJGzPALMWxzzmUuwKNOfUYWHscc
UwyodeIDbjyuU0aYAwEFAUGsWFll5/udHtfVAqWlp+Wc9rok5vS0Pb17/7n6u+9zn/uMUwAAQFfG
kQUAAIgVAACxAgAgVgAAQKwAAIgVAACxAgAAYgUAQKwAAIgVAAAQKwAAYgUAQKwAAIgVAAAQKwAA
YgUAQKwAAIBYAQAQKwAAYgUAAMQKAIBYAQAQKwAAIFYAAMQKAIBYAQAQKwAAIFYAAMQKAIBYAQAA
sQIAIFYAAMQKAACIFQAAsQIAIFYAg/HnnwNkAiBWAN3obar+/fvch43XBp71kxuAWAGC4mlv291r
/+z4+Zv+R+0dtm+bL336tOcu2QKIFWA0DDgdXbfO371a6Hhwx73zSeft1itfiGGdjkdkESBWgAB4
fO9Wi/Vz6fsPHlqVPb1N1U0X8nt+r2LgFRArwMhITHqv+kvp+z97+tjHy/7o675/498SvTq6W8g0
QKwAQyO9e9WVPxR49v1HtHDL5c86b34/4HSQgYBYAV7s3d+5fqfy40fNPwXau/9zwNldX3mn4sNR
vBcAsUJk8rTnrkSpEnX67vv75o++7rbr/7p77Z/99g6yFBArRC/P+p902L6Vvrz/fX/fPL53q/ni
J4wMAGKFKOVRy39FgtKL13fOvyhVjilHFsmSyYBYIVrof9QufXbpuYeu2y5Hvvef4/IRf/R1k+GA
WCGSkeC0q+6C9P3DE04+av7pTsWHugfFgFgBDMGffw48bLzWfOnTMGtuwOnovPm9qPxJ521KARAr
RA6OB3dar3wR0r6/b9SJB64EMDIAiBVMz7P+J52/fCcBY9/9+jEPmdWRgcqPuRAWECuYGBFZKM77
ByX6p4+fXwir0wQvQKwA4ep697YZ+aS8diGsGDaYSxIAsQKEr+/f8fM36nn/9jojp/PPPwd6fq+S
gJoLYQGxgqFVpc3577p13iwXPjmfPJSwmiWyALGCIfv+rtPu96q/7H/UbrrEs0QWIFYwFupE0V++
UxemavmvefvU2hJZEm7bW39mZAAQK4xp39913v/BrxWREeupF8JWf8kSWYBYYYwc9Ki99YeCu1cL
n/a2RdhX05bIUmeJMTIAiBXC1vfvbrhk9r7/iN+x8+b32nekxAGxQmix3/3lTsWHHbZvo2EGqDYb
9171l84nDyl6xAqgP47uFrHM3Wv/fNpzN6q+eG9TdfPFT3p+++HPASfVALEC6NQvftbfdev886vs
o1Iuz/qfSA6oS2R1NVIfECtAsDxur2u+9GnnL985HY+iPWZ/cKfF+nn7j8V/PO6iYiBWgNHwtLdN
Ov6iEtYrcaNOd22w3qn48GHjNXIDsQIE0vd3Oh78WtF0Ib/3znVmyw/G+eTh/Rv/jsLhZsQKMEoe
tfz3TuXH7T99Td/fN33369VBkpvfP+t/Qm4gVoBh+v49dyUKa/2hgLuYBDIyoE7p5UJYxAowqO//
rF+93t81dMikolGMDLRd/1eL9XNGBhArwHMkPtXuB8Wqz8Hw+N4tCV25IyxihWjnj8ddaqh1+bO+
jgZyQ5fAv6vuggT+9tafyQ3EClGH9Pe18/7dDZfo++uLukTWf4631ZxiiSzECtHVaW2++ImOd3wa
N26c3W7funXrJBfvv/++7Ozr69u+fbu259133x0YUM/tJCYmXrx40evtdXV18fHxstHd3Z2ZmSnb
EyZMmDhx4sqVK0tLS90fMeTnBpqAwaSmpmZlZXnu2bNnT3JycpB5oi6qUPmxuqAiIwOIFSK879/X
LZGU7jejFq+lp6eXlJSIvDo6OlavXn3gwAH3nq6uLlHkvn375JVfffWVbHu9fdu2bfJ62VizZo04
ThSpxn39/WVlZbLHT7H6mYDBiM1F5Tdv3tQeykZcXJy8Jfhscd/6WyRL3UOsELF9/zsVH3Y3WHWf
GCReKygocD8UN8XGxnruuXHjxrx582RDNDdjxgwJUf+O7Ox2iSjFhrItgaqPj/AtVj8TMCTnzp1b
smSJti0bp0+f1jFz1ElsVwvl94wlshArRBQSn0rc1GH7NkRz/sVrEmD63uOWZl5envTZ3fsPHjz4
zjvvaNuLFy+WPrsm2UDF6n8ChkSSlO9i3bp1ocgi7VYLPb9XMTKAWCES+v7tP30d6vP+g63nY09v
b++0adPkf+3hzJkza2trte2mpibxmhhw4cKFKSkp0pH3X6yjSJIn0veXWFWi6ebm5hDlkjYy0Hzp
U66/QKxg4r5/z28/uM77W0N9UVCgXnMPqp49e3b58uVerxwYGLDZbCdOnJCnUlNT3fGm19knu92u
o1h37dp17ty5oqKizMzMkOaVtkTW/doSRgYQK5iMJ12NEhndv/Hv8FzvH6jXtGkAIsoVK1aIQIc7
rPTl3f33xYsXX7161fNZ6bbrJdbLly9v2LBB27ZYLBUVFaH9zftzoOf3qjuVH6tr3DDXDbGC8RGT
tl3/V+uVL/Q976+vWIWVK1fu2bNn+vTpnnGoePb06dPaKEFfX9/+/fvdswIKCgrmzZunnbuXF+Tl
5W3evFkXsUrkO2fOnNbWVu1hfX39zJkz3SMVIS2p9h+L1QthI+5ujIgVIqjvr8VB2vX+4V0QZBRe
Ky8vlz1eU6AkJt20adOUKVPGjx8vIe17773nKbjDhw+LAeUp0bFIWdFpjDU1NVUM7rln7969KSkp
YepbdN6WvkXHz9+wRBZiBSP2/dXz/j9/Y6K1/qSb397eTtmpv4i//dB88ZNHzT+RG4gVDMGzp4/v
15bcvVpoonPNTqfzwIED27Zto/jcqNduXP/XveovGRlArDD2ff/nNxA1z2KgMTExEydOfOutt7Qr
rMAT+91fpEBZIguxwtjg6G65e+2f3OMv8hCldjdcar70KUuOIVYIa99ffGquvj8EPDLwuEt+OLkQ
FrFCOPr+vXeum67vD8GMDLRc/oylHRErhIqnvW2tV74I25x/MM7IQOfN76Xo6aAgVtC1aTkdHbZv
pWPoeHCH3IjSn9Weu60/FKjL6DAygFgh+L7/o5b//v59Ln/8uf+kSjAQhFgBAqDr1nnp+Qb2+l++
G/FlNTU141ycOnXK4XCQz4BYIVr4o6+7qfyg/B+Kt+Tk5Iz7i/T09MrKSjIcECtEPh0/fyMRaKDv
evBrxf3aEn9emZeXp4k1Li5u1qxZCQkJWVlZnrczAECsEFE8e/q48XxeQOGqhvPJQ3mjn5MlduzY
ER8fb3FRXFyckZERGxu7dOnSQ4cOdXZ2UgqAWCGikFhVItZRhrq2b/0ZadVITk5OSkoqLCyUiPXI
kSNOp7O0tFR25ubmUgqAWCFykEB1dOHqKN7ucDgkXE1JSWlpadm4caNItrGxkSIAxAqRhoSc8he2
I/T09CxatGj37t2yXVxcnL9+vXL8OKUAiBUIV4M6iISr2lCA+kAi1mXLlLQ0MS7FAYgVIoHOX74L
MlwdXdhrs9liY2Of3wvW6VR27lTi45WqKkoEECuYm2dPHwc6d9V30BrQWgqVlZUvnLMqL1fdmpOj
ehYAsYJJefBrhS7h6t/B72inFvx1iE4lOVlpYC1UQKxgTv543NV0IV/H9bq0+Lf/kU630iJuBcQK
piOg+ad+Esx8WG+ys5UtWxRuIYNYyQIwCxKoBj8ZYIgoWBtp1WV5PVFqWpoyf75SW0t5IVYAE6Dv
6KonEgWPYs2BYTl1SomLUwoLGRlArADGDlefPGwqPxiiZZt1nGnwnLo6ZelSZe1apY17UyNWAKOi
19zV8B1fwtWMDMYEECuAUcNVx6PQhat/f8SF/FB9BGMCiBXAgOGq7pMBhviUm9+HKijOzVXWr1dY
ZhCxAhgE/QdAhwsrQzeMKxHrjh3qGS2rlQJFrABjT6B3tQrqs+ouhDA0rqpSr3/Nz6dMESvAWIer
F/LDEK4+jyy1wVz9ruzyprNTnSqwbBmzBRArwNiFq3UX9Jxh6gcPfq0IeYCcm8tsAcQKMDZoZ+ol
aA1rjNz/5E7FhyGdgfA3djsTBhArQFjpbrgk8eMYfG59ZZg+9+hRZdEihRu9IFaAsEaOoRvu9PHR
Tx/fqfw4TB995Ih6Rqu0lBJHrADhCFe76i6M2aeHLWhVXNe/zpqluG6oBYgVIFQMOB3NFz8Zk3DV
M2gN3/BuT496BYHFwrAAYgUIXbhqDfNkgMFIvCxxa1g/UoLWsjJKH7EChCBaHLvRVe9khDNo9YLZ
AogVQM9u8e9VYbvUasSgdUymJagruiYlKS0tVAbECqBPnNh88ZOwXWrlT9A6NrGzNluAtQUQK0Dw
jO1kgCHSE87pAV7U1rK2AGIFCJYBp0ONEMNz1ZN/SLg6liOtLS1KYqK6vABLDiJWgNGGq1ZDhasa
ErGGe3qAJw6Hkp7O2gKIFWA0GGQywNBBa8WHYxa0eqeG2QKIFSCAcPWSQSYDDGbMpgd4UVjIsABi
BfAXbXTVKFHhUNG0us5W/5OxT8qOHer1r1VV1BnECjBSuFpfadhw9XnQeuu8IYJWxTXLNTZWjV4B
sQIMGw+G9zYBo+P5bVwNMgTc0qKuN5ierp7aAsQKMBiJVcNwE1ZdgtZQ3cZ1FIhS09K4ggCxAgwd
CTaez+u3dxg/qX887pKkGmqaLSBWgKHC1V++M1AY6EdwbcTU5uaqK2MxEwuxAija6Gr5QYOPrnrF
1+ptXI0WtNrt6jQsi4WbvyJWANfoqrEnAwymq+6CQUeEs7NZtwWxQrQjcV/j+TwThasmSHZJiToT
68gRahdihSil69Z504Wrf6fcsNMYbDZ1JlZdHRUMsULUIRGfEQcr/QxaXTMZjBtrcxYLsULUhqsd
P39j3vR32L41wdzb3Fz1Mi1ArBDBOByO7OxsxTUhVMJVU8xdHTbi9vgKubm5ncZcGKWyUomLU7Ky
iGERK0QsVqt1/vz5pgn3/A66V61aVVxcbNBUtrUpy5YpycnqlCxArBB5SGSXkZHRfKdxx/9eZbrJ
AEMErX3d7/+ftT/+WJ2TkyPfy7gJlXA1LU1dE6uxkUqIWCHSsFgsEtlt2bJl44YN8rCmpkZUa9Jf
iCrXwn0Z2/5vcnJyZWWlFokbmvx8dZYra7kiVogkHA7H1KlTRabyf21tbWNjY2xsbKE51747deqU
JL6urq6lpeXll1+WrzN58uRO4zsLqyJWiDAkxJOwTrrMGzduFAfNmjXLpOGqRl5eXnx8fFtb244d
O+QbJSUlGXeYdTCS1J4e6iRiBdOTnZ0tApL4Tgy7dOlSQw9K+ocoddGiRTab7aWXXpKvZqZvlJKi
zJ2rNDRQLRErmBuJ6eLi4ta6WL9+vTMiJgAlJyfL90pPT5evZoJhVk8KC9WZWGVl1EzECmZFNDrO
hcSqiYmJjkhZ916+iMViEbdq367NXItLlZerbj10iPqJWMGUVFZWauqZO3duZ2SdQunp6Vm0aJH2
7cw0zKrR2KgsXaqODABiBdOxZcsWTT0NkTiu19LS8tJLL8m3k+jVfKm329U1sQCxgvnqmYuamppI
/YI2m037jub+GpzOQqxgnpDIHgnSGYmjR4/Kd+wx7zQmCV3j4ljLFbECgK40NqrTsDIyuKs2YgUA
XePW5GQlKYnLtBArAOhKVpa6aAtDrogVAPTk+HHGWxErAABiBQBTUFWlpKdzOguxAoB+9PSo57IW
LVLMdcEuYgUAo7Nli5KQwOksxAoAupKTo0ydqpSWkhOIFQD0Q6wqbrVayQnECsaoaq5LWiP+wtbI
p6GBm2kjVggTt2/fTkhI0NR54sQJL58O99AU30j46KOPZs+eHRMTM3PmzIKCglB83L1795YvXz5h
woTExETZHvFXauyXX6itZaoAYoXQcuzYsdTUVK3Nr1y5srW11exidX+jvLw8Ud7Nmzc1/W3fvj0U
H5eWlpaVlaWoFz1lybb/nYAxY+dOdS1XbqmNWEEvtm3bVuJaxPPMmTOyLRubNm06efKk1tobGhrW
rFnj1fgNPhTg4xtJ3DrkMrLXr19fuHChxJjyv2xr3+7AgQNTpkyJjY3VwvYPPvhAHg6OLgd/nLys
t7dXcS0GJtu+X2yUX6kjR9SpAjYbLQKxgg4MDAyIOqVTLMGptmfGjBlNTU3u1n748GHpPptIrCN+
o8GIT4uKimRD3iXb2islzpVDXbt27dVXX5U9MTExYljZM+LHeX6KyNr3iw0U/h8/rsTGMlUAsYI+
XLlyZfz48Vqk1tzcHB8f79XaxQX19fVmEauPbyQR6+3btwe/3lN/2rbnt9O2JeZ94403Jk6cuG/f
Ph8f5ztiHfxiY42rWK3qQq55eTQKxApBod1E7/Lly0lJSf39/aIP6Th7tfZ79+6tWLHCLGL18Y0O
Hjw45BirRKnaiSyJW90R65DWE017BaFeH6f4HGMd/GJjiVVxLeTKZa+IFYIkPT29oqJCNuR/2U5N
TXWfK/ds7aIns4jVxzcS8vPzZ8+eLTHjzJkzpbOv7bxx48bgMVYv62mjq6+88kreiwGd18cpHrMC
5P/29nbfLx73IlRIxAoRyJw5c6TXzzcCpaVFsViYKoBYAUA/nE51VYH4+Ch3K2IFAL3Jz1fdGrk3
5UWsADAWlJWpUwXkf8QKAKAbVqu6YktxMWIFANCP2trovNsrYgWA0NPTE1VrYiFWAAg9aWlKcrJi
tyNWAACdEKWuXaveOys63IpYASBcpKcrc+dGw42zECsAhJHsbHWKa20tYgUA0I8jR9QxAcQKMCQ9
v1e1/1hMPgRK+09fdzdE9/34In2GAGKFUfLngLP54id991mpJGCedN6+U/nxwLP+aM8Iuz1S7z6A
WGGUPL53q/WHgj//HCArRsHdq4X2u79Eey5UVanjrfI/YgXQaKs51fN7FfkwOh42XrtX/SX5oC4m
MHVq5C0pgFhhNPTbO5rKDz7rf0JWjA7JOsnA/kftZIW6CNasWUphIWKFaKfz5vedv3xHPgSZhx22
b8kHlcZG1a1HjyJWiPZo64/HXWRFMEgGEvV7/M50qnOwenoQK0QpDxuvtV3/F/kQPO0/FjNOHZEg
VgiY5kuf9nU0kA/B86TzdvPFT5hZ4c2pU4gVoovH7XV3rxbiAr2495/jzLt6AbtdWbpUXQ3LzBcR
IFYIjBbr5+JW8kEv+u7Xt1z+jB+qF+jpUd26ezdihajA8eDOncqP/xxwkhV6IUptvvTpk87bZMUQ
bs3IQKwQ+dyvLen57QfyQV8eNl5r/+lr8mFot2ZlIVaIZJ49fdx88ROucNc/aB1wSj/A+eQhWTG0
W024ngBiBX/punW+q+4C+RAKHvxawQUXQ2POU1iIFfxCAtU7FR/+0ddNVoTEHo5H6npXTgdZMSyV
lYgVIo3epuqOn78hH0KHRKyMX/saE0hIUHJyECtEDuqZ64ufsGJISPnjcRczLnzR0qKuJ3D8OGKF
CKHvfj13CggD7T99/fjeLfJhWLS1WsywxiBihZG595/jXMMaBp72trVe+YKLBXxRV6eujW14tyJW
GKm199zlGtbw/YZVf+l4cId88EVtrRIbqxoWsYJ56bz5fW9TNfkQHh61/JeLBfwaEyBiBfPidDxq
vvgJa4aGDe0KV9a69buCGvRcH2IFX3Q3WLsbLpEP4aTntx8e/FpBPoxMQ4N6XVZnJ2IFMzHwrF+i
Jy61DDPSP7hT+TG9BL/YvVtZtkxxGO7CCsQKw/Ko+SeusxwTuuou9N65Tj74RXq6sn690cYEECsM
y92rhZyhHhOe9ra1WD9nJoZfiFJXrVJ27ECsYAKedDUyy2oMaf+xmAXF/UW76cChQ4gVjE7b9X/1
3a8nH8aKvo6Ge9Vfkg/+0tKiHDmCWMHQ/NHX3XzpU8LVsUWKoN/eQT6YEcQKQ9Bh+/ZR80/kwxh3
cFt/vn/j3+RDYNTUqCMDiBWMhjrdp+JD1gYdc7Q7CzDvKjB27FCSkxErGI7uhktMUKcszIrTqc5s
HesTWYgVBkVJFR8+e/qYrDBE7+Hp46YL+fQeAqOlRV0Bq6oKsYJRsN/9haVXDUX7T18/avkv+RAY
ZWXqHQfG7mpXxAov0PpDAbOsDEVfRwMXC4yG3bvVCwfG6IosxAovtOHmi5/Qho1G86VP+bULGFHq
0aOIFcaM7Oxsd6+TtawMSM9vP2jjMzk5OXYDzCUCxAojIA118uTJstH9oHPn5v+XtayMGHs5Hr2f
vvZ++9358+fX1NSQIYHR0BD+uBWxRjuNjY0JCQmyUVhYuHbNGtno7Ow8ZKTLrqOZ/Pz8Otc9SNav
W3fkyJGNGzceN8ltSg1ESkr475uNWKOdqqqqZcuWyYbFYjl16pRsrF279ujRo+SMESgtLZXScTqd
xcXFspGVlbVz506yJTA6O9XZVzYbYoWwNl0xqcStsbGxDodDwiJ5SLYYh/T09OzsbHGrFFBubi6l
MxoKC9WrBsI4PI1YqXKFaWlp0mLlf+l1JiQktLW1kS3GwW63z58/XzoWW7Zs2bhx46xZs8iT0SA/
SHl5iBXChCh19+7dc+fOLS8vl86mBLDkidEQq4pbpYDi4+PHjRvHxIDRYLMpcXFKuIIGxBrt7Ny5
MyUlRQLVrKwsiYnIEGOSnZ0tpSPhqoiViQGjZPdudUwAsUIYSEtLmzx5ssVikZiIUMiwOJ3OZS5E
rEwMMD6INdpJSkqStvrSSy9VjemiFTAidXV141xkZGSQG4gVjF0DXLgvvgIjc+TIEa28yIrRk5+v
1NYiVgiHWJ0Gu3sw+C4v8mH05OWpd8xGrEBDBTe1tbVMDAiKtjbl5ZdDPT2AFhU+eYEnZC+MWaVa
v14J8bWFiDVMYiUTQpchZC8EVg0KC5UQnwCkRiJWxApRVqmsViUpCbHiETKE7AX9qkFPj7J0KWLF
I2QI2QtmqgbUSMSKWIFKhVgpcjKE7IXgq4EjhDcVp0YiVsQK0VepkpOVUC65QI1ErIgVoq9S7dwZ
0uVZqZGIdZTfKC4urqGhwceXHbyBWP2nubk5JiZm27ZtnjuvX7/+9ttvT5kyZcKECfJ/cnLy5cuX
DZXs1tbWDRs2THQhG/Jw1Iey2Wzbt2+fNm3a4PKVbJHM8Tp4YNVArBrKm9wgVsQ6ym907Ngxi8WC
WEPEO++8s3DhQs81HAoKCubMmXPmzJn+/n7FdW3rpk2bDPXd+/r6EhISDh486HRx4MCBGTNmyM7R
HU2+/v79++vr6wd/x4GBAXlWsmj01eD4cfUmg4gVsRrwGyUlJRUVFY34ZRFroHR0dEhMKvGpe8/N
mzdnzpzZ3d3t9UqxmHGSnZ+fn/7i+iabN28OPoVDlq/8rkgWSUaNshpUVipDhQWI1fRi1ZbS2Lp1
6yQX77//vvabL90fbc+7774rv8yyMzEx8eLFi15vr6uri4+Plw1pbJmZmbIt9Uz6XytXrnTfXmW4
zw00AcMdRLqrEpJ0dXUZMGI1dfYeOXIk6cVLgyQ6++KLL3znw9mzZ5csWaJ1w2VDYluvVO3bt2/6
9OnSiZ49e/bhw4fdz/r4jl6kpqZmZWV57tmzZ09ycrK2vWbNmnPnznk+Kw9Xr149ikP5U1sknZJR
iBWxeu+Un/eSkhJpXfLDK/VPuk7uPWIrqTfSEuSVX331lWwPHmaS12u1WSqottyRdBLLyspkj58t
388E+DjIRx99lPJil8o4YjVv9m7YsOHEiROeeyRcvXfvno9MuHLlyquvvirJG3AhG3Fxce4RWC0x
Ejz29vZq8e+CBQvcpvbxHb0QBYt/5e3uOFo+xf3LOmXKFG2Ywo08lJ2jOJQ/teXkyZOSUaOsVDab
Esr73SLWsRRrQUGBZ18vNjbWc8+NGzfmzZunjShJYCgxlPspaQMS8mj9IIkyAv3cQBPg+8jLly+v
qKgwoFjNm71iHOkNeO7xkQyNdevWHTt2zHNPUVHRm2++6U6MV5f86tWrEtX6eXCvINT9Rtk4ffq0
+6nx48cPfr2Pg/s4lD+1pbW1VQJwY44IIdaxFKvXz/vgPe5KmZeXJ51Kz5E198j94sWLpVPpOdjk
f8v3PwE+jixKeu2119xvNI5YzZu9g/eP6D75JXC8OOPdM1qUj9ZiVTfycyK9/hG/45BIXuW7EJt7
7g9UrD4O5WdtiYmJQayIdYSdPvZIq5g2bZq7bUjHsPav20s0NTVJpZTqu3DhQumVS0/T/5Y/iiQN
uV+6tO7xMuOI1bzZO1hGkiTfU5eGPJT7OL6T6uM7Dol02CXAlDDfK6wOaCjA96HCIVaPPgpijVKx
eo76nT17VnrfXq+UAMRms504cUKeSk1Ndbcrr9Mj0skNhVi16S/aeJkZxWq07JUerpdoRjx5NWLE
6k8hDv6OQ7Jr1y7pxRcVFWVmZnruD+jkle9D+TkUEBcXN/pKFcoIF7GaRqzaeWqp/StWrPA6s+HV
nNxxinTxrl696vms9LlCIVZtxDAxMdG8YjVU9g4+eSU/WgkJCT6mW0nI6TX17dixY55jrP4Ly/M7
Duby5cvuU0YWi8VzeF2+/ubNmz1f7Hu6lY9D+ZPOoE5eIVbE6mblypV79uyRcMYzUBIRnD59WuvG
9vX17d+/331Kt6CgYN68eVogKS/Iy8uTih4isQrvv/++dhtRM4rVUNk7eLqV8tcFAqWlpdpVA/JL
lpyc7D6CNitAwm1tVoBseM0K8JFFPr6jFxKSSxrcgxL19fUzZ850D6HIe6VTL4G/doGAZIg8O9wF
Ar4P5U8uSRaNfrqV8NJLoVuHBbGaSazl5eWyx2uOjgRNmzZtkk7f+PHjJeZ67733PGvn4cOHpfrK
U+ILsUaIxljdkc7rr79uXrEaJ3sHXyCgUV1drV3SKm985ZVXZNtzBq7IVPJ/ggvZkId+ZpHv7+hJ
amqqaNdzz969ez3n24koRfcxLiR5PsaFRzyU77taSeYEdYGAkJCgNDYi1kgT6+iQytTe3k6GRHz2
btu2zeuSVnCjwyWtiBWxamgXX3utyoFYIzV7JdaTEHL79u00n8FkZmZOmjQpqEVYhFmzlKFWEUKs
UeQR6VhNnDjxrbfeiowbyhtNrBGWvbQyv0hOVqqqECseIUPIXjBHNaBGIlbEClQqxEqRkyFkL+hS
DUJ2bpAaiVgRK0RlpbJY1MUDESseIUPIXkCs8HeRw3AzvcleGJtKJWItL0esQHAHlKx+pKSE7g7Y
FAbNDyjZqCQtTSksRKxA8wNKFrECzQ8oWcOyc6dSXIxYgeYHlKxJioMsoPkBJQuIFWh+QMkGTWen
ErI1dygMmh9QslEJJ6+A5geULGIFmh9QsogVaH5AySJWxAo0P6BkESvQ/ICSNQxr1yqlpYgVaH5A
yeoH97wCmh9QsmYqDrKA5geULCBWoPkBJRs0bW2Kw4FYgeYHlKx+cGsWoPkBJYtYgeYHlCxiBZof
ULJRxdKlSk0NYgWaH1Cy+pGQoDQ2Ilag+QEli1iB5geUrGGZOxexAs0PKFnzFAdZQPMDShYQK9D8
gJINmpBddoVYaX5AyUZvliFWoPkBJYtYgeYHlCxiBZofULLRQk+PMnUqYgWaH1Cy+tHYqF4ggFiB
5geULGIFmh9QskaloUFZtAixAs0PKFnzFAdZQPMDShYQK9D8gJJFrDDW5ObmdnZ2upufw+HIzs4m
WyjZ6KWwUElLQ6wQFKtWrSouLnY3P6vVOn/+fLKFkkWsiBVGT05OTkZGhrv5SZijPQRKNkrJy1N2
7ECsEBSVlZVaIKM1P4vFooU5QMlGKdnZSijHTBBrVOB0OidPntzZ2SnNz+FwTJ06ta2tjWyhZKMX
CVfz8xErBEtSUpLEMtL8qqqqGIajZKOdtDR1mBWxQtBdn+yMjAxpftoGGULJRjVbtiBW0AEtnJHm
pwU4ZAglC4gVgkUbgJPmpw3JkSGULCBW0AGLxSLNj2E4ShYQK+hGbm6uND+G4ShZUOLilJYWxAo6
YLVapfkxDEfJgnpfFqcTsYIOOBwOaX4Mw1GyoIR4zRrEashCV4vdZH/GyTv+outvFPT0KJMnI9Zo
FCsJpkZDqIq7rk6ZNYtqiFhJMDUa9Ctuq1VJTKQaIlYSTI0G/Yq7rExZv55qiFhJMDUazFTcVEM8
hVgBsVINESsJpkZDMMXtcFANESsJpkaDrsW9dq1SUkI1RKwkmBoN+hW3xaJUVlINEWtwR/MJYg3/
jaNbW1s3bNgw0YVsyEMfL25ubo6Jidm2bVs01HybzbZ9+/Zp06YNLhTJAckH77waXdHNnatOZUWs
iDUUFBUVrVixArGGWax9fX0JCQkHDx50ujhw4MCMGTNk53Cvf+eddxYuXOgM5YXtxkG+6f79++vr
6wcXysDAgDwruaGDwCZPVi++QqyIVXdKSkpef/11u92OWMMs1vz8/PT0dM89mzdvFs8O+eKOjo4J
EyZcv3496prAUIVSW1sruSF5EpTAQn89K2KNUrGWl5cvWLDghQoa0WKVVio/IdKXnDRpknQnV69e
XefRE3S34SEbs3tnd3d3ZmZmfHy8tG3pwq9cubK0tHTIJKSmpmZlZXnu2bNnT3Jysra9Zs2ac+fO
eT4rDyVJQx7qyJEjSUlJg7/L1q1bJ7l4//33tShYetDannfffVeCO9mZmJh48eJFrwPKF5ev4Pvr
+M4H/xMQaM7482sn6ZQ8CUpgNps6FIBYEau+XL16dc6cOffu3TPd2EUwYk1LSysqKtJ637Ihve/b
t28HJFYRokhBi/H7+/vLyspkz5BJEGeJsG7evKk9lI24uLiuri7t4ZQpU+Ttnq+Xh7JzyENt2LDh
xIkTXumRgFc6HCIv+WkUIx84cMC9Rz5F1LNv3z555VdffSXbXgeUXxd5ve+vM6JY/UxAoDnjj1hP
njwpeRKUwMrL1VkBiBWx6ojNZhOrNjQ0mG7sIkixHjp0yHOPPBTVBiRWiez8T4UEoUuWLNG2ZeP0
6dPup8aPHz/49cMdXDTU3NzslZ6CggL3Q3FTbGys554bN27MmzdPcQ1Kyu+HZ2wuGpWIUuup+Pg6
I4rVzwQEmjP+iLW1tXX69OnGFxhijSKxNjU1iVVDMWBnfLH29vZ67hHFvPLKKwGJdfHixdLJ9X/8
RDrL+S7WrVvnuT8gsQ7eL+nxCngH73G/Ky8vT5Lh3n/w4EH3yR8fX2dEsfqfgIByxh+xCjExMYgV
jOIp6fuLVS9fvmy6sQtdxOrDWX6KVX6WRATyroULF6akpJSMNMNcergSkUnM6BVyBjQUMKRY/d8j
PyfTpk1z/6jMnDmztrZ2xK8zolhHkSR/ciZMYpXumk7nbBFrtItVqvKCBQvOnj1rurGLcEasYhmv
sy7yMq8WLi+w2WwnTpxYvnx5amqqj4Ts2rVLur1FRUWZmZme+wM6eSXd3sFDAQF5zT2oKqUvafZ6
5ZBfx3c+BC/W4XLGz6GAuLi4oAS2apVSU4NYEWuwSKt4/fXXhxvMihKxfvTRR557hhxjld7x1atX
PV8m3dXhWriEmT46vNIzcJ9jsVgsFRUVnsfcvHmz54t9TLca8uRVQF7TpgGIKFesWOF1qOG+ju98
CFKsPnLGnyPocPIqIYGIFbHqgFRfr1M3UShW0WhBQcGAC4mVxDXuM3juNiwvmDdvnnbOWiLcvLw8
UZ77WRGT/DhpkW9fX9/+/fuHmxUgv2Rz5sxxXyNUX18vfXB3yCzvlV6wRJHaFAX5FHl2uAsEhpxu
FajXVq5cuWfPHgl+PeNQH1/Hdz4EI1bfOePPESQ3gppuJUp1zTZDrIg16KNF/SWtXvNYRTTuGT9e
bfjw4cPS8sePHy8aEhl5PitB3KZNm6ZMmSLPipffe++9IY2guGZriqc89+zduzclJcWzP5ucnBzj
4u233/ZxSevgCwRG4bXy8nLZ4zUFyvfX8ZEPwYh1xJzxXUUlH4K9QKCmRlm0CLEiVhKsj1jNWxnk
9yD4S1rFR+3t7aZuFPpc0nr8uDLU9QiIFbGS4OgSq8SzEldu3759dG/XliOIgDVcMjMzpcMR7CIs
u3crOTmIFbGSYB1q9AsTdKIJ+eITJ05866237KE/XWOc4vZFerp65RViRawkmBoNpituqiGeQqyA
WKmGiJUEU6NhFMXd1qZ0dlINESsJpkaDfsW9ZYuSl0c1RKwkmBoN+hV3QkIYLmalGhraU6b7M1BL
4y+q/vyktlYVa7jucINYAUJJQ4OSlqbExio7dyp6L4NLUw5sHGD3bjpOACZHQiRNqdnZob51HU15
5J+3l19WWloQK4DJycpScnPDoVSa8ojIL9yL99qiNADMg9WqjLQANk15DJBYNbzXnlEaAHpgsylJ
ScrUqYrnonY05WiF0gAIjspKZf16ZdYs5ehRZQwvyacpD0lOTjiHVikNAD1ISVHmz1eVGq55PMP7
ncIYxKFD6rLW4braCrECBIe7rTY0jL1SYUiqqtQpGeG6IgCxAowWcejx48rSpcpf98sCg1JXp8aq
ZWVj9fmIFcAPHA71rNSsWYrFojZXA0apqN5NS4taUqdOjWESECvASEiUmpCgbNyo9i4NC03ZTXp6
eG4TQGkABEF2tqGVSlP2wgD9CUoDYBB2u3pCOVxLzNGUdfNpWxulAWA8enrU+DQ2Vj09FdI1U2jK
ultVimzLFkoDwEhIsCNKjYtTG6e5lEpTdjiUtWvVQXDDnFRErAAukpPVkx5jcZUOTVkHq0rxyQal
AWCIKNU9gdzs8/wLo7IEe3qUZcvUX0SDFR9ihWhV6s6d6hzysVozBXRh1Sp1+Wrj/SgiVogyGhuf
KzU8609DqCNWQ4JYIZrIyAjfkv5hJqquvKqqGsuFxBArgIr7tEZlZcRGqdHTlIuL1ckbY7S6CqUB
4FrSf+NGZceOyP+mUdKU8/PVdQBsNkoDYCyQtpecrF7jX1gYFSv7RUNTlh/IuXPVUXJKA2BsotT4
ePWaVGOPxNGU/cXhUG/TYLGMyarVlAaA6w7yR45EkVKjoSnX1qrFap4yRawQEZSWql3+aIamTGkA
6EZZmXo2Q/6Ki6M6H7Ij8UtJz2P3bsQKEN4oddky9V5+UXJ6KqqQApW+/9y56iAAYgUIE0lJqlUl
SkWpkYe2AsDateaddIxYwTw4HH8v6GeSs8MMBQSMhKjx8UpWlql/MhErmESp2j3io2GqfzQ35cZG
9aqq0lJKAyAsSrVYlPJy8iPym3JEXHOMWMHAiFK126Ma+8JwmnKw2GzqrXApDYBwII3NjHdJoSkH
REmJ2v2XH1FKAyBU3cDdu9X1UiFKmnJGhjoH2ZxzqhArGJ7OTiUnR41c0tOJUqOiKbe1qev/JyWZ
+D5jiBWMi7akf2ysGrxEYhsLE9mmSq3drv6IGvKuKogVIoK1a9UGhlKjjbo6+g8QWpyOR/dv/Pv3
73M7fv7G+eRh5H9h6ewzdyoKkZ9P889RRazmUGrnL981XcjvvPm948EdEWtT+UHZjli9ilLT0tR5
qUePUvp6Umj4FIpSpfsfHbfFRaxjp9QnD0WgotH7tSV/9HV7qrbD9q3s77p1PqL0Wlmp9vqjbf1p
mrLiWlFl5051RZWomY+MWMdGqQ9+rVCj1F++++Nx14iRbCToNQqX9Kcpa9hsyqJFagWIppuNI9Zw
K1Xt7F/IF7F6RqnDMeB0SNyqvd6UenXfHrWujmWoorEpa9f+R99SuYg1TEhkKhHonYoPVUU6HgX0
3mdPH3fVXbhT+fEo3jtmWK1qx581U2jK0RSoItYwKrWvW4s6pVPvT5TqQ68iVtFrd33ls/4nxv3C
paWqUqX3d+oUUWqUNuWSEvWP0oAQKbXD9q0WpYoW9RlMcDzqbrjUfPETI0av0uObO1dZuhSlRnVT
3r1bva1DdK+bg1hDq9TuBuuA06H78UXTcuTmS59K9BqK44+SQ4fUU/8wJqQZIA11derqjsnJnKJE
rCZTqidy/J7fq1oufxaGzxomfnaqC1BF1oJvMMqaUFiorvEY5bd0RKymVuoL0Wv/k+fRazg/V1t/
etYsdRENq5XSj3a0Gzs2NpITiNX0SvWKXnXXa1lZWW5urvde6eVpS/qvXcv602OOFFCn6/Zf2dnZ
rt87h7YxNkErINaIUWqI9Hr06NGpU6eWDr6y22JRr0llZT9jsGrVqmJX73vcOLUtW63W+fPnh+mz
RejJyfLzSykg1ohVqr56zcnJiY+Pr3EHpNKE3NsEJkZCSiojI8MtVglgtYfh6PvHxSlbtnCeCrHq
w9Oeu4ZVavB6dTqd6enpc+fOrXOt6ib/S0PN/V//S70aFYxHZWWlFqJqYrVYLMWhPn0kJhV3JyRE
yTpViDXkOB7cuVf9ZfPFTwyu1FHr1W63r1+/PjExsbOzUzqVsj158uS0tLTaiLtzRsQgP4RSRlJe
IlaHwzF16tS2trYQfp7UhLlzlawsAlXEqptSWy5/Zm/9+c8/B0yXfn/0Ko1z6dKlItNTp06JW6WJ
7ty5M7StFPQgKSlJolQRa1VVVcgHWI8fZyFdxIpS/dVrY2NjXFycNM6EhATZyM3NlYhVmmtWVtbG
jRuluebk5FAZjEl2dnZGRoaUnbYRks+I6NX+EStKDYletXjHzaxZs1566SX5f+3atRK0Hj9+vKam
xk7Xz6hogaoUnBa66t0MHOolqlOn4lbEilID0Kvt4un/Z/LL0ixffvnlHTt2oFHzVVfX0KqUoDbY
queha2rUq/4tFmbXIVaUqs/gAJgIi8UiYtVzgNXpfB6oHjrEBDvEilLRazSSm5srYtVzgFWiVAJV
xIpS0Ws0Y7VaRax6DrBWVhKoItZR8rTn7t1r/xSVRLlS0avpgwOHQ8Qa7ACrzaYw9wOxBsOTrkaJ
UluvfPGo+aeBZ/3UA/Q6+gbEn9cfRGE2SMf/7tXCFuvnRKnolQZEhpANwdLX0aCOpVo/f9xeh1ID
0mvP71Wi196mavSKR8gQsuFvpYpPJVB9fO8WSh21XtVbGVZ82HXrvGnuFEsDIkPIhhAp9e61f7b+
UECUqtvgQH2leqfYhktEr3iEDIm6bJDgVKJUUeqTrkaKWV+e9T95fiPuhkvOJw9pQECGRHg2SFgq
SpVe/73qLx0P7hClhlqvTeUHu+ouRO/gAB4hQyI7G8ShfffrJUptqzklSqVow6TXp49FrOqy3/WV
oloaEEaByMkGteN/+bO71/7JWOqY4JqYdelO5cdq9BpVgwN4hAyJvGwQhz5q/ik8Uap264tw0tra
umHDhokuZEMe6v4R1dXV6enpM2bMGD9+vHzKihUrTp48GWT02lR+8MGvFbJNA4pIbDbb9u3bp02b
NnSLQKymzgZ3x//u1ULZCEdOhVesfX19CQkJBw8edLo4cOCA6E926vspiYmJBQUFmrIHBgauXbv2
xhtv7Nu3L+jo1Xqn4kNVrxE/OBB9Hlm4cOH+/fvr6+sRa6TVC63jr52eCl9OhVes+fn5Ekt67tm8
ebN4NtSf29XVNWnSpOCPIxHr84lZ9ZWRHL1GsUcQa4TUC4lS7a0/t175Qp1E1Xk7FBXFbrdv27ZN
zBITE7N69eo6j1XT3dVoyPrk3tnd3Z2ZmRkfHz9hwgTpXK9cubJ0mJtZpqamZmVlee7Zs2dPcnKy
tr1mzZpz5855PisPJUleB2lqapIIYsjjz5s378qVK74/ZTC9vb1TpkzRK0vd0WvE6nXcsBVp69at
k1y8//77WhdEetDannfffVf6B1qP4eLFi15vl1on9cd3XfJdCf1PQKDVErFGlFg1pUrH/95/jj/p
agzR6SmpKGlpaUVFRVrvWzak93379u2AxCpClHqprcDf399fVlYme4b8OGk20mZu3rypPZSNuLg4
CRi1h2I3ebvn6+XhkMrbtGnT4IHRY8eOSaMd8VNekODAQHV1tbRer3alT/TqOrUVgYMDw4hVehsl
JSWSpR0dHfJzeODAAfceyXzJZG285auvvpJtr7fLT7u83nddGlGsfiYg0GqJWCNErNq8VOn4h2Gq
v1SUQ4cOee6Rh6LagMQqwYX/nyhB6JIlS7Rt2Th9+rT7qfHjxw9+/ZAHv3HjxsyZMz0DENmWPeV/
3U3Tx6e4E+8mKSkpRNn7fOZAxYc9v/0QOSuKDSPWgoIC90NxU2xsrOceKTLpT2glJT/enh0j0ahE
lGJD33VpRLH6mYBAqyViNb1YtTP+zRc/CWmU6lVRpCPsuUdq+SuvvBKQWBcvXiz9LK1h+IP01/Jd
rFu3znO//2IVJCT56KOP3A9l290wfH+KV8R69uxZMbLuEat39Fpfqa2YFQnR6zBi9eptDN7jLsq8
vDwpHff+gwcPvvPOOyPWpRHF6n8CAqqWiNXEYv1zwNl757ra8a/+0tHdErZ5qUNWFHf981OsTU1N
UhflXQsXLkxJSZHOl+8PlU6WSFDClubmZs/9/g8FCJcvX5b+msOhXrwv/0+fPv3MmTP+fMpgbDab
HCrUWe0ee+2qu2DusddxflUkH3vkt3zatGnuX3T5YautrR2xLo0o1lEkKdAKg1hNI1bpIWpRavuP
xaE4PaVLxCoV3WvgX17mVcnkBWKoEydOLF++PDU11ceH7tq1S3peRUVFmZmZnvv9PHnlZtmyZdqo
2f79+xcsWODnpwxJTExMeDJclKouSHjxExOv9xq0WBWPQVXpMUiFGdyTGFyXfFfC4MXqT4VBrCYQ
q4SlEqVKG2u7/q+xuiBVKopnh1oZZoxVOmhXr171fJn0mIarphJm+uhzSaS5YcMGbdtisVRUVHge
c/PmzZ4v9j3dqrS0VH4Dbt++Lf9LI/TzUwZz/fr14aYZhDR6Nety2nqIVZsGIKJcsWKFV9kNV5d8
V8IgxepnhUGshhardPx7fvtBeoVjfo2/NiugoKBgwIX8XEt1b/jrRpXuaiQvmDdvnnbaVCLcvLw8
UZ77WWkbp0+f1iLfvr4+iR+HmxUgIcacOXPc11PV19dLN9AdMst7pSMmgYw2RUE+RZ71fYHAa6+9
Jm+ZPXu2/5/y5ptvnjlzRhtzkP8l5dOnTy8rKxuDzorT0VV3wXzRqx5iFVauXLlnzx7JfM841Edd
8l0JgxGr7wqDWE0g1udL01/85F71l09728Y+L16cxyp13T3pxKsaHT58WCrf+PHjpSVIe/B8VuKI
TZs2TZkyRZ4VL7/33ntDVkrFNWFQmornnr1796akpLgfSuVOTk6OcfH222+PeEmr/BJIMuR//z/l
ypUr8hFaaqdNmyYpdw/wjQnPnj5+8GuFVAn53xwrZukk1vLyctnjNQXKd13yUQmDEeuI1XLcUCBW
Q4hVlNrbVN10IV86/k977holL8ZRKQyBe96rCe5WoF+VkW5+e3s7RkGso1Sq9PVEqe0/FhshSkWs
huX5zAGD61WPKqOtBSFdJYyCWEfTTrR1ke/f+LfRlKoRtrPhEFC10dZ7Nahex+lQ6yZOnPjWW29p
V1hhFMQaQM9OaxvtP31tnI4/mGtwwKC3MsQjZEj4s8H55OHzjv9PX/c/aie7Icjq1GH7Vr0ZjHH0
ikfIkHBmgxZiNJ7Pa/+xuN/eQUaDXvzR163ptfOX72QbjyDWqMgGCSWk3otS79eWjH29h8iNXtUh
+wv5UtnGsprhETIk1Nkg9bvz5vcSSkhdp+MPYUDrGI2lXvEIGRK6bFBPT906//v3ufzxN4Z/otdw
L+kyjr9Bf0A2GKRX23zxk8H7tWU1jh496rnzcXvdnYoPGbYGmjKlAb540tV47z/Hhy4eF14zHNU1
FS9/xvg10JQpDRgWe+vPHT9/M+RTiYmJItZFixY5nc4X3NpU3XzpU3NcTQ80ZUoDwk93w6UHvw69
MlteXp4WtHrdM0aQt7T+UBD595cGmjKlAaOg/cfix/duDflUWVlZQkKC5taqqiqvZyXObas5FTn3
jwKaMqUBetFy+bPhTka1tLRMnTp1y5YtotdZs2a1tb2wxsKfA06Rctv1f4Xt7jVAUwZKwxw0Xcj3
MUkoNja2pqbm5Zdf3rFjh8Vi8XpW3HrvP8e76yvJxmiHKoBYwc2z/iciVh8hZ1JSUmlpaUZGxsaN
G9PT03fv3u31ggGn4+61f3Y3XCIzARArqPiYa6Wxc+fOnJyclpaWyZMn19bWLl26dPCdX8WtLZc/
6/m9ivwEQKygTkrtvPm9jxccPXpUYlXZ2LJli2yIYfPz8we/zOl4JG591PwTWRqlpJEFiBX+orvB
Kn8+XlBTUzN37lzFdSIr+3/8D+WvmxsO4dYnD+9UfNh3v55cpSkDpRHVdPz8zaOW//p4gcPhyM7O
fv4gJUUZNMbqSb+9Q9zKauI0ZaA0opq7VwsD8GBlpRIXJ6718ZInXY13Kj9mMQGaMlAa0UtT+cHA
ZvgvXaoUFvp+yeP2OvWC1ycPyV6aMlAaUYc6Klr5cWDvyc9XVq0a8VW9TdUs1EJTBkojGnnSebut
5lRg7+npUaZOVVpa/HKr9XMWE6ApA6URXTxsvNZ163zAb9u9Wxm0JsuQdNVduPef47g1KigkCxAr
uBhxrtXQOBzKi6sI+qDz5vf3qr9kMQEAxBotjDjXKnhEqW3X/9X+09fkNgBijQruXvuno7tllG8u
LfXXrQNOcauErsStkQxXXiFW0GgqPzj6AdC5c5W6Oj9fqy7UcrWwq+4CeU5TBkojknn29PGdig9H
//7cXGXHDv9fri7UYv38YeM1cp6mDJRGxOJ4cMf3ulYj0NmpxMf7vgrLC/V2sJc+7b1zncynKQOl
EZk8avlvh+3boA6xceOIV2F58Udft4TJoT5jBjRlSgPGhge/VgS7gmplpZKYGOib+u0dTRfyh7vL
FtCUgdIwMe0/Fge7xJ/TqY4G+H0Ky83Tnrvi1tFPSACaMlAaxsTHPQQDoLZWHWwNnMftdeLW/kft
FESEkE0WINao588/BxrP5/054BzDNEi8fKfiwz8ed1EcAIg1EhCdScSq2+ECmRvgif3uL6pbWQQL
ALFGAMHOtfKkpMSfhQSH42HjtRbr5yzeylAAIFbT87i9Trfr97WFBG220R/gtx9afyhgESyaMlAa
5kZc9uDXCt0Ot2OHsnNnMAfobrCywCBNGSgNc9Nh+1bPWfq1tYFehTWYrroLbdf/xUItNGWgNMxK
UOtaDcmyZepga3Dcv/Hv9p++xq00ZaA0TEnThfxnTx/recTCQmXt2iCPIUq995/jEk3jVpoyUBom
41n/k6DWtRoShyPIYdbnbh1wSjTdefN7iommDJSGmXB0t4i8DJu8Aaej9YeC7oZLlJSZyCYLEGt0
o65r9fM3Rk6h0/Go5fJnvU3VFBYAYjUH3fWVPb/9EJJD5+aqMwT04I/HXSwwCIBYTUP7j8WP2+tC
cujdu5UtW/Q6WP+jdnHrk65GiswEFJIFiDW6abF+rsO6VkPS0KDExSl2u17H6+toELc6Htyh1GjK
QGkYmsZz/18I17VKSlKOHtXxeBJcswgWTRkoDUMz8Ky/8XxeCD/gyJFg1mQZEnvrz+JWFmqhKQOl
YVD6H7W3WD8P4Qf09CixsaNb/doHvXeuswgWTRkoDYMiPev7tSWh/YwdO5RTp/Q39m8/tF75goVa
aMpAaRgO0VN3fWVoPyO41Vh80FV34d5/jg84HZQjTRkoDQNx/8a/7a0/mzr9bTWnBp71U5TGIo0s
QKxRzL3qL8MxM9TpHMXdW/3hzwGnuPV+bcnY3rALALHC37Re+SIc90atqlJXaHWGxH3qIljVX3b8
/A2LYAEg1rEkNzfX4WLH/14dpn703LlKeXmIjj3gdNy9WqjnTRBgtPWq0zUDJDs7W1FH1x3aBiDW
qCAhIaGxsdFms82aNUsetrW1hbwB5OYqGRkhHGxgoRYDsGrVquLiYrUlj1PbstVqnT9/PtmCWKOF
pUuX1tTUSBtY61qOOisrKykpKbQf2dioTmh1hnAk9PlCLc0/uaOnWp2WgAE/ycnJyXD9fGpilSLI
COWvKSBWw0UWZWVl4tOdO3fa7fb4+PjykPXT/0aCF6s1pJ/wfKGWztuyLU06OTmZsg4nlZWVWoiq
idVisWgBLCDWqCAtLa2wsHDjxo3Hjx8/dOiQBLBOZ+jPqufmygeH+kOedDW+/3/e/O7bMy0tLS+/
/LItiBtxQ6BILZo8eXJnZ6eI1eFwTJ06ta2tjWxBrNGCBKp5eXkSXNTU1CQkJIhew/GpdXXKoUNh
+Jxv/v11bGxsbW3tjh075MeD4g4nSUlJEqWKWKuqqhhgRazRRW5urkjnpZdeEqXGxcWFI1wNPfku
tO9y5MiR+Ph4q9Uq35GgNZxkZ2dnZGSIWLUNMgSxRhGFhYXS/Z81a1ZiYqLIKDK+lPRA09PTJUqy
ukZyd+/evWjRopSUlPXr11PiYUMLVEWsWuhKhiDWKKK0tFSq/lQXPT094fvglhZFNBfKAFkatvxm
iE/b2tqSk5OlkRO0hhNtaFVqlzbYSoYg1ugKK8a52KnHTaoDQJQaH6/U1IT6c7ShgNzcXAnJ5Wsy
0hpOLBaL5DkDrIg16mhsbNTEOgYnbXfsUHJywjYyIHrVvilBa9iQ3zPJcAZYEWvUYbfbpeovWrRo
DD67vFxZujScsXlcXJzmVso9PFitVsltBlgRa1Tm9bhx1hBP1x9O6srkyTreYdAf1q5dK9+3oaGB
cg8DDodDcpsBVsQK4WXVKmVMnA7e7W2c6f4oNcQKw5CVFZ4rBWBEsZJgxAoAiBUQKwCeQqyIFcJE
W1vobjIIiBUQa1SybJkShoUKAbECYo0itmzh/BWeQqyIFXSlpERJTycb8BRiRaygHzabkphINuAp
xIpYQT+cTmXqVCUi1oFFrD5/QG3bt2+fNm2aLpcUI1bECiMRF6euIggRLdaFCxfu37+/vr4esSLW
yOTevXvLly+fMGFCYmKibMue27dvJyQkjHuRSZMmhSlBO3eGWazD5YBsnDt3bsGCBTExMbNnzz59
+vQoDjV4D2J94bMQK2KNSNLS0rKyshTXza7TXDf1O3bsWGpqqudr3nrrrbKysijMgdjY2NLS0oGB
gdbW1s2bN4/iUIP3RINYJfe0b+1mz549Q94cF7Ei1khg27ZtJSUlsnHmzBnZlo0pU6b09vYqrjUD
ZVs2Nm3adPLkSfdb0tPTRTTRmQMStx46dKiiomLI23/5c6jBe6JBrN3d3fHx8Tdv3tQeykZcXFxX
VxdiRayRiQRfa9asKSgoWLly5eCaLT1W+X/GjBlNTU3ann/84x/79+8PaxLt9pCucRVQDty+fXv7
9u0rVqwQJ544cWIUhxq8J0qGAs6dO7dkyRJtWzaGG0hBrIg1Qrhy5cr48eOvX7+uPfQKqZqbmyXW
0J7Kz89PD/+s0sZGxTW+aYQccCM7X3311UAPFbURq8bWrVu1W+SuW7du2M9CrIg1AnA4HBaL5fLl
y0lJSf39/cqgQUDpAktHWB7KxptvvjkGSezpCemMK/9zQNi8ebMoVTbOnj07WIsjHkqJ1jFWDen7
S6wq4b+Wh4gVsUYsEoFWVFTIhvyvRaPu09byf3t7e2pqqvRttRrvRfhSKQFjyFb19z8HhK+++mr2
7Nny1GuvvXbmzJlADzXknugR665du86dO1dUVJSZmYlYEWtUM2fOnPr6+jFORGLiGC7FYogcML9Y
JZDfsGGDti1xvfYLhFgRK4wdO3YoeXlkg3nFarfb5feptbVVeyg/VDNnztTGmhErYoUxQqwqbgXT
ijU1NdVrMsnevXtTUlI8farjWBNiRazgB1arcvw42WDqoQASjFgBALEiVgDAU4gVsUJgHD3Kza/w
FGJFrKArs2api14DnkKsiBV0w2LhroJ4CrEiVtCVjRuVU6fIBjyFWBEr6AfXCOApxIpYQWfy85WM
DLJhrDxluj9KDbEajmdPH9+p/NhYaTp1ShlqwXkD0mH7tvPm99QiQKzwAs4nD5svfWqsNNXVKbm5
psi9fntHU/lByUMqEiBW+JunvW13rxaSD6NGIlaJW8kHQKzwN44Hd+5Vf0k+jJo/+rolaH329DFZ
AYgVntN3v779p68Nl6xTp9T7X5klaP3lu65b56lLgFjhOfbWn43Yk120SKmpMVHQ2ng+71n/E6oT
IFYwsFjXrlVcN5c2TdB683umBwBihef0/F714NcKwyVryxblyBETZeMfj7vUoJWRVkCsIHQ3WOXP
cMnKyVFc9zc1U9D6y3dG/IkCQKyI9TmFhYpJ7hftRr3UouJDglZArKAODj5q/slwySotVVatMl1m
dt06b8RfKQDEGmY6bN/aW382XLJaWpTdu02XmU7Ho+aLnww4WaUbECtiNaBYzdwD6PntB/IBEGtU
01Zz6knnbfJBx6D1TuXHA8/6yQpArNHLveovHQ/uGDFlxcUmuvjKk65b53t+r6JqAWJFrMZj7lx1
mSvTBq1MDwDEGr20XP7sj8ddRkyZxaJUVpo0Vx/8WtHdcInaBYg1Smm+9KlBlxNNTjbvna+ej7Qy
PQAQa9SK1aCd1qws9for09JVd4GgFRBrlNJ43qi37cvLU3buNG/GSrh6p+JDglZArNFIU/lBg6bs
+HElJcXUeUvQCog1GvlzwGm4G165qatTb9dqZtSgtfJj1mkFxBpdGPFOgpGFa3oAqwcAYo0m+u0d
9/5znHwI6U8XQSsg1ujC6HcSLCuLgEzuunWedVoBsSJWwxAbq7S1EbQCIFYzYb/7y/0b/zZu+ubO
VWw2glYAxGoqsRrzToJukpIiYzRAvRCLOa2AWBGrIUhLU+/REhF0/vId67QCYo0KDHqLVjcZGWaf
yvp30PrkYdOFfAldqXWAWCMcg95J0E1Ojhlv0DJs0Hrz+65b56l1gFgjXaz1lYZektlqVS9sjRT+
6OsmaAXEGvlww6vwZ3jnL9+RD4BYI5n7tSWP2+vIh7Dx7OljCVq5uQAg1kjm7rV/OrpbjJs+h8O8
NxEYjq5b57vqLlD3ALFGLM2XPv2jr9u46WtrU+LiIizPnU8eNp7PM3S2A2KFYLhT8aHRL7UcF4EV
QIJWRloBsUYaOTk5dtedpd9N+Z8OhyM7O9u4aZ06VenpibSg1fFInR7gutVYbm5uZ2cndRIQq+mZ
P39+TU2NuHXy5MlWq1UeGjetpr0Jtm86b34vf7KxatWq4uJi6iQgVtOzcePG48ePNzY2JiQkSMSU
kZFh3LSa+SbYvoPW9//P2h9/rJbeg6HzHxAr+ElWVtbOnTurqqqWLVtmsVgMHTGtX6+UlERS5ssv
meS8bGRs+7/JycmVlZWG7jEAYgU/EZOuXbu2tLQ0KSlp6tSpbUZe81SsWlsbSZl/6tSp2NjYurq6
lpaWl19+uba2dvLkyQyzAmI1PTabbdasWYWFhXPnziVcCj95eXnx8fHye7Zjx46NGzfKzxvDrIBY
TY/D4XjppZeysrLGjRvHAN+YIEpdtGiR/MJJQYhbKQVArJGABKoWi0XEavRYqaFBKS+PyCJITk6W
WDU9PT0uLo5+AyDWSECipHEujD66J95fvz5S+w3y2yZu1Qqizfx39wLEGu1o4wDjjH9dU02NsmhR
pJZCT0/PokWLtIJgmBUQq+mRZiyNedmyZUZPaGOjkpAQwQXR0tLy0ksvSVlI9Eq1BMRqbmw2mzTm
vLw8oyc0EtdhGbIsxo2jqgNiNTkOh0NasoRLZqgCkV8Hjh49KsXRE3GrIgBiDY8iwJuRc00i1kBO
7JCl5i5uQKyjECslGnCGVFWpK16TydR/QKxUrLHKEDKZ+g+IlZZGJlPcgFipWGHOkOTkQMdYyVjq
PyBWWppPli5VLxMgk6n/gFipWLplSIBrXZPJ1H9ArLQ0xEpxA2KlYiFWoP4jVlNXLN3rYjjnb1dX
V6enp8+YMWP8+PETJ05csWLFyZMnDSjWUDT45ubmmJiYbdu2ufccOnRo3rx5EyZMmDJlyoYNG65c
uTLqg7e2tsoRJrqQDXno57OSHkmV1+vDU9aIFbFGsliHo6ioSBqDvsdMTEwsKCjQmvHAwMC1a9fe
eOONffv2RYNY33nnnYULFzqdTu3hBx98INlb57rjbFNTU1pa2qg/tK+vLyEh4eDBg04XBw4cEJ3J
Tn+elVKQVEnadP++I5Y1YkWsUSfWkpKS119/3W63h/qDurq6Jk2aFNi3KysL9XQr3TO5o6NDItPr
16+798TFxclOz9eI8kZ38Pz8fIkNPfds3rxZTOrPs0Jtba2kzSsxYShrxIpYwypW2SlGkz6a1ELp
pq1evVqLa7zeMtx7tY3u7u7MzMz4+HhpM9IRW7lyZWlpqZ+pKi8vX7BgwZAtTWIrCXCGfJf0aqUz
m5qampWV5bl/z549ycnJw31Wb2+vdIRD2tKMkMlHjhxJSkry3CMdZInj/PwKvnN1zZo1586d83xW
Hso38udZDUm5pDDMZY1YEWu4xSodQ+mJa3032ZC+2+3btwNq89KcpNJrIWd/f39ZWZns8SdJV69e
nTNnzr1794Z7waZNmwYPlh07dky6fpprRDQ3b97U9suGhGYSqgw+jmilurpamrRn4wynWMOZyRs2
bDhx4oTnHukQSE/Zz6/gO1fFVvLpnq+Xh26F+X5WQwpUUhjmskasiDXcYj106JDnHnkoFgiozUsM
NYr02Gw2sWpDQ4OP19y4cWPmzJme0ZZsy57yv25FJQHRkiVLtG3ZOH369OBEuvGK4/xqabm5ikd0
aYpMFgE1Nzd77hENSaYtX75cojzJIt957jtXJfgd/Hp32nw/q9Ha2jp9+vQwlzViRazhFqt0mjz3
SEz0yiuvBNTmFy9e/O677wY0cCZdP7Gq5zjgcEhH8qOPPnI/lG1369LYunVrvot169YNdxBpomfP
npVWGnDEqsfJqzBn8pAKlhyQIHfv3r0SGEqst2LFivb2dh8HGS5XgxerEBMTE+ayRqyINdxi9dES
/GzzYkmp6PKuhQsXpqSklJSU+E6J9P3FqpcvX/Yn2fIyEYHDtXaf/C/BzpkzZzxfIP1BaX7SufYK
04aMkeM87ggQTrGGM5NHjG1FPeJor6FPL4bL1eCHAnyINXRljVgRqxEjVmmrXmc/5GVeB5QXSG0+
ceKEdDlTU1N9tNgFCxZITOF/ypctW6ZNndm/f7+81+vZXbt2SSexqKgoMzNzxEN5NmmjRax6ZbL4
aETvOJ3O4ezmO1eDP3nV2toaN/wNb0JU1ogVsYZbrJ6dr+GG/6QfevXqVc+XSXdsuJoqQcpwQZOY
4vXXXx88Ouab0tJS0dDt27flf6/TMhLjuM+EWCyWiooKH8e5fv2656nncIo1nJk8+OTVP/7xD6/X
iN1effVVH72E4XJVkrR582bPF3tNt/LxrMZwJ69CWtaIFbGGW6zSwgsKCgZcSCwQHx/vPrnhfou8
YN68edo5WQm+8vLypMG4n12xYoW4UgvK+vr6JNYY7oS1tAev0zh+8tprr0kHcPbs2V6anjNnjvtK
nvr6+pkzZ7pjwzfffFM6klrPVP6XFEooV1ZWNiZiDWcmD55uJQeRHrTEeloCrl27JoHhBx98MNyP
n49clY+Wgjhw4IA2w0ESKc96XiDg41kNSdvg6VahLmvEiljDLVbPKZYrV650z2jxesvhw4elZo8f
P16q7J49ezyflThr06ZNU6ZMkWdFGe+9955Xz9fzgKO7pFVkJC+Q/z13Sl9Y/OK5Z+/evSkpKdr2
lStXkpOTtVRNmzZNUlhbWxtwS9NJrOHM5MEXCIhJ09PT5V3aFZ9vvPGGj9lXvnNVi3YlY2NcvP32
24MvafXxrKRqxAsEQlHWiBWxhlus0Vu6/nz3U6eUxkbTZbJI3POSVoMQuktadStuQKyI1YAtzSCZ
LHGihG/bt283VIZnZmZKzB6KRVgQK2I1lkd8nxpGrGQyxQ2IlYqld4boceUVUP8BsdLSPGCha+o/
IFYqls4ZkpioWK1kMvUfECsVS78MmTVLGWnJEjKZ+g+IFQLJkISE4KdbAfUfIlmsEPBdtgIXK5i4
uAGxEjuEgwDFSkkBIFaa60gUFyuhvxkXJQWIFWiulBQAYqW5AiUFiJXmahR27lQ6OykpAMRKc9UP
Tl4BIFaaK2JFrIBYaa6IlZICxAqIlZICQKw0V8SKWAGx0lwRKyUFiBUitbly5RUAYqW5AiUFiJXm
CpQUIFaIquaan6/09FBSAIiV5qofnLwCQKw0V8SKWAGx0lwRKyUFiBUQKyUFgFhprogVsQJipbki
VkoKECtEanNluhUAYqW5AiUFiJXmCpQUIFaIquZaWMgYKwBipbnqisWiVFZSUgCIleaKWBErIFaa
K2KlpACxAmKlpAAQK80VsSJWQKw0V8RKSQFihQhsrky3AkCsNFegpACx0lyBkgLECgwFUFIAiJXm
Ono4eQWAWGmuOrNxo1JcTEkBIFaDkpub29nZ6W6uDocjOzvb6IlOS1NHAygp45cUINboZNWqVcWu
6E9rrlardf78+YiVkgLECqMnJycnIyPD3VwlLNIeIlZKChArjJLKykot8NGaq8ViKTb+8GVUitWU
JQWINTpxOp2TJ0/u7OyU5upwOKZOndrW1mb0RJeUKLW1lJQJSgoQa9SSlJQksY8016qqKobtKClA
rKAD2dnZGRkZ0ly1DTKEkgLECsGihT/SXLWAyAQprqyMzgsEzFdSgFijFm3ATpqrNoRnishNicop
nOYrKUCs0YzFYpHmapphu2gVq/lKChBrNJObmyvN1TTDdrm5yu7dlBQAYjU0VqtVmqtphu0KC9Wp
rJQUAGI1Mg6HQ5qraYbtolisJispQKwm+fLjTPc35mI1Y6ZFzx9GQ6yGECsJVi+7KimJ4EyjPgNi
pSIaPcG0XqoHIFbESuulPgNipSKGOcGNjQGtbkXrpT4DYkWsI1FToyxdSuulPgNiRay6RqwJCbRe
6jMgVsSqH3a7MnkyrZf6DIgVsep73HG0XuozIFbzVcTq6ur09PQZM2aMHz9+4sSJK1asOHnypFES
/PLLisMRZBoOHTo0b968CRMmTJkyZcOGDVeuXPFxkObm5piYmG3btvmn/XDX0tbWVvkKE13Ihjz0
/9kw1BbJN8m9wZ+LWBFr1Ik1MTGxoKBAawwDAwPXrl1744039u3bZ4gEJySoI61BpOGDDz6Qxl9X
VyfbTU1NaWlpvm34zjvvLFy40Ol0GlCsfX19CQkJBw8edLo4cOCACE52+vNseGqL7JHckzxErIiV
rpM3XV1dkyZNMkSC8/OVnp5g0hAXF9fR0eG5R4wz3BHklRLYXr9+3e+BirAWU35+vkSLnns2b94s
JvXn2bDVltraWslDrzxHrIjVfGKVQEzChCGfki6w9HxTU1OzsrI89+/Zsyc5OXm4A/b29kqv2US/
BD7SID1WCaP8PMKRI0eSkpK81Gm326WHK+6QTu7q1au14NdLrEMa1r2zu7s7MzMzPj5ejCPd55Ur
V5aWlg6ZAN8ltWbNmnPnznk+Kw8lSf48G87aIl9QchKxIlbTR6ybNm0aPDB67Ngx6bhpDVta9c2b
N7X9siFxnAQag48jDqqurpaG4dW0zCvW119/Xbqufh5hw4YNJ06c8JJjWlpaUVGR1r+WDelf3759
OyCxivIkP0XQst3f319WViZ7hkyA75ISf8nbPV8vD91S8/1sOGuLHFxyErEiVtOL9caNGzNnzvQM
zWRb9pSXl7uDlyVLlmjbsnH69OnBFnDjFbWNpVitVsUjQhxFGsQLkg/Lly+XsEu+dUNDg48jiFCa
m5u9suXQoUOee+Rh2l9rbvkpVglU/f/GPkpKou/Br3cf3Pez4awtra2t06dPR6yI1fRiFaTT99FH
H7kfyra7bWhs3bo138W6deuGO4g0sLNnz0obM0rEKgo7ejTINMiXkiBx7969EqlJ8LVixYr29vYh
XzlYQyIO6ep67pHA85VXXglIrIsXL3733Xe9hh19MFxJ6SXWMNSWmJgYxIpYI0Gsly9fFms4XJOT
5H8JGc6cOeP5AunNSeORnqxXUDYYm80mhzKEWKXF+n3bK3/SIC4Qxw0eefQhVh8v81OsTU1Noid5
18KFC1NSUkpGWgtxuJLSayggDLUFsSLWCBGrsGzZMm3iy/79+xcsWOD17K5du6SLV1RUlJmZOeKh
vBrGmIk1P1/x+75PfqbB6XQO9+3EL4OHAvyJWEWaXqfI5GVetpUXiINOnDixfPny1NRUHykcrqR0
OXkVhtrS2trqpVrEilhNLNbS0lJp87dv35b/vU7CSITiPp9gsVgqKip8HOf69evDnTgOt1hPnVI2
bgwmDf/4xz+89kizf/XVV4c8wpAnrzy7zMowY6zS2b969eqLvwj5w03GkkDSx6irj5KSY27evNnz
xV7TrXw8G87awskrxBpRYhVee+016b7Nnj3bK3qaM2eO+3qY+vr6mTNnugOxN998U7qBWi9S/j99
+rQEbmVlZYYQq9UqLTuYNIjdpEsrwdeAi2vXrkmk9sEHHwx5hCGnW4lGCwoKtLdLBBcfH+8+A+ZW
p7xg3rx52pl0ydi8vDyRmvvZFStWSK5qGd7X1ycR4nCzAnyXlLxXCvfAgQPaFAX5FHnW8wIBH8+G
s7ZIHjLdCrFGlFil5Ut7lv89d0rHUxqz5569e/empKRo21euXElOTp4yZcr48eOnTZu2adOm2tra
sCV4BERhy5YFkwYxaXp6uthQuwTzjTfe8DH7avAFAl7zWFeuXOmeh6S8OLR6+PBh8ZF8iohmz549
ns9KMCu5quWwpOS9997zGl7ws6S0cFsKK8bF22+/PfiSVh/Phqe2SO5xgQBijTSxRlqCOzsVv+cn
6JIGcajnJa3hXw3A1HBJK2JFrJGWYF3SIFGehGPbt29HrKMgMzNTQnsWYUGseAqx+iLQ2REQGfUZ
sVIRIz3Bp06p92ih9VKfAbEiVt3YuVPJyaH1Up8BsSJW/Th0SPlr3iitl/oMiBWx6kFtrTJ3Lq2X
+gyIFbHqh3ZLwc5OWi/1GRBrsBXRdH8hzI5Vq5Ti4ojMtOj5w2iIFQxGXp7icfURUR4AYoWgaWlR
Aly7ALECIFYAxAqIFcKP1ernlQKIFQCxgt9inTtXcd2SD7ECIFbQiYwMZfj7MCNWAMQKgeN0KomJ
Sm5uNHzXQvkHgFghHLS1KfHx6rAAACBW0A2xalyc8tf9UQAAsYJObnXdujmCyZZ/AIgVQNcGQBMA
xArhx25XJwn4sT4LYgVArOA3ubnK/PkROd6KWAGxwtiRk6POE2hsRKwAiBX0IztbSUiIMLciVkCs
YIy4tbYWsQIgVtCPkpJIOpHFdCtArAAAiBUimIwM9d6uAIBYQTfq6tTx1t27GQoAQKygHy0tytKl
6p2ynE7TNgCaACBWMBoOh7J2rZKUpPT0IFYAxAr6sXOnYrEgVgDECrpCxAqAWCFUFBebaMgVsQJi
BcNjt6tjAuvXm2UhV8QKiBVMwpYt6q1ebTbjp5TpVoBYwTyUlKh3dqmsJCcAsQLoh9WqroaVTUgI
iBVAR+x2paqKoQBArAChwZBDrpy8AsQKpqWxUR1yzckx2kwsxAqIFcxMW5s6EyspSV1hALECYgXQ
B4dDvfg1IcE4swUQKyBWiAjKy9X1Bo0xWwCxAmKFSKGlRdUrYgXEChASxnQ+FtOtALFCxNHTo178
unNnmNcWyM3N7XTdEjHbNSLhcDiyuZABECtEDna7umjL/PnhnOi6atWq4uJitQGMU5uA1WqdLwkA
QKwQURQWqme08vPD82k5OTkZGRlusUoAqz0EQKwQWbS0PF9yMPRUVlZqIaomVovFogWwAIgVIhGr
NQwf4nQ6J0+e3NnZKWJ1OBxTp05ta2sj7wGxQqRz6pQ6/BoykpKSJEoVsVZVVTHACogVooPkZGXW
rNBNxsrOzs7IyBCxahvkNyBWiA5KS0M3GUsLVEWsWuhKZgNihajBbldSUtTQVe/JWNrQqohVG2wl
pwGxQpRx5IgSG6vorT+LxSJiZYAVECtEKyEIKnNzc0WsDLACYoWoJztbXTBbD6xWq4iVAVZArBD1
tLUpa9cqq1YFv2C2w+EQsTLACogVTFW5+NPlDxArAJWLbKTQAKhcZCNQaEDlIhuBQgMqF5CNFBoA
lYtsBAoNqFxkI1BoQOUCspFCA6BykY1AoYGpKpd2o5Rw0traumHDhokuZEMe+v+sLlRXV6enp8+Y
MWP8+PHyKStWrDh58iRtFLECmFWsfX19CQkJBw8edLo4cOCACE52+vOsXiQmJhYUFGjKHhgYuHbt
2htvvLFv3z7aKGIFMKVY8/PzJVr03LN582YxqT/Pho6urq5JkybRRhErgL+VS9Rpt9u3bdsm7oiJ
iVm9enVdXd1gsQ5pWPfO7u7uzMzM+Pj4CRMmSPd55cqVpaWlQyYhNTU1KyvLc8+ePXuSk5O17TVr
1pw7d87zWXkoSfLnWTdNTU0LFy4c8tPnzZt35coV32kYTG9v75QpU2ijiBUgALGmpaUVFRVp/WvZ
kP717du3AxKrKE9UZXfdarC/v7+srEz2DJkEUbD49+bNm9pD2YiLi5OQUHso/pK3e75eHrql5vtZ
TzZt2uQ9MKoox44dk27+iGnwZGBgoLq6Wn4nXhAxbRSxAowo1kOHDnnukYei2oDEKoGq/6mQMHPJ
kiXatmycPn3a/dT48eMHv959cN/PenLjxo2ZM2eKFj0VKXvKy8tHTIP7q7lJSkqijSJWgMDEKl1d
zz0SeL7yyisBiXXx4sXvvvtuR0eHnwnZunVrvot169Z57tdLrMLq1as/+ugj90PZdpvUdxq8Itaz
Z8+KkYlYEStAYGL1YSs/xdrU1CR6knctXLgwJSWlpKTEd0Kk3y2amzFjRnNzs+d+vYYChMuXL0sH
3+G6m6z8P3369DNnzviThsHYbDY5FG0UsQLoHLGKND171trLvGwrLxAHnThxYvny5ampqT4SsmvX
LumMFxUVZWZmeu7X5eSVm2XLlmnTpPbv379gwQI/0zAkMTExtFHEChCAWD27zMowY6zS2b969arn
y6QT/f+3b8cuba1hAIcLUsqFCnYrRYIIItJu/QdCKbRFSocgBJEMoYvgUsStGMGCASmZuvZ2FDqV
DsVFQQUXwclBpEspOCiFIiGIXO599UA4xjY3jYFbb54HkSRfbI/nfN/P4zH52Yux4kSyyVXXOJfM
5XLJ7Ww2u7Kykv43i8Vi+skNL7dqMnrRx48f4yfE58+f43PkvsVtuGhra+vcywysUWGFfw1rZPTt
27d/nYkzuP7+/r29vYawxhPu3r2b/CU9znAXFxcjavXRBw8eLC0tJWe+1Wo1zhB/9qqAOM8dHh6u
v2Nqd3d3cHCwfsocXxu/m5fL5eQlCvG/xGj6DQJNRn9oZGQkvmRoaKj1bXj69OmHDx+Saw7xOb6v
O3fufPr0yRoVVviFsKZfx/ro0aP665D+Pn9p9c2bN9Gjnp6eCM3s7Gx6NE5mx8fHe3t7YzS6PD09
3XB5oa5QKER204/Mzc1NTEzU70bv8vn8jTNjY2MX39LaZPSi+DkRGxmfW9+GjY2N+C+S7+XWrVvx
fW1vb1ujwgq/FlY7xhp10EBYrVEcNH7jyXXu791Yow4amFx2Iw4aJpfdiIOGyYXd6KCByWU34qBh
ctmNOGhc3cnloyMfCCtYAZhWYAWAaQVWAKYVWAGYVmAFgGkFVgCmFfz3/rQLEFYAYQUQVugmJbsA
YQUrANMKrABMK7ACwLQCKwDTCqwATCuwAsC0glaU7AKEFUBYAYQVXAoAYQUrANMKrABMK7ACwLQC
KwDTCqwATCuwAsC0ggYluwBhBRBWAGEFlwJAWMEKwLQCKwDTCqwAMK3ACsC0AisA0wqsADCtoEHJ
LkBYoRMWFhYODg5Ou1o6LWutVktugLBCmx4/fvz+/fvTBXDtdAmsr6/fu3fPbkFYoX3z8/NTU1P1
sMYJbHIXhBXatLq6mpyiJmHNZrPJCSwIK7Tp5OTk5s2bBwcHEdZardbX17e/v2+3IKxwKQ8fPoyz
1Ajr5uamC6wIK3RAqVSampqKsCY37BCEFS4rOVGNsCanrnYIwgqXlVxajbAmF1vtEIQVOiCbzUZY
XWBFWKFjFhYWIqwusCKs0DHr6+sRVhdYEVbomFqtFmF1gRVhpTun6bUr9+GoCSv87mG1wQgrCCvC
CjolrAgrwmqDEVYQVoQVdEpYEVaE1QYjrCCsCCv8Lzr19evXXC73x5m4EXdbHxVWhBVhbVStVgcG
Bl6/fn1yplwuZzKZeLCVUWFFWBHWH6hUKs+fP08/UiwWo6StjAorwkqXhrVQKLx8+TL9yOzsbD6f
T26Pjo4uLy+nR+PukydPWhkVVoSVLg3rt2/f+vv7d3Z2krtx4/bt24eHh8nd3t7e4+Pj9PPjbjzY
yqiwIqx076WAOM28f/9+cjtuLC0t1Yd6enouPv/69eutjAorwkr3hjVMTk5Wzjx79iz9uLAirJim
bU7U+N0/zlUzmcyXL1/Sj7sUgLBimrY5UWdmZpaXl9+9e/fixYv04/54hbBimrYzUdfW1nK5XHI7
m82urKzUhyqVSrFYTD+54eVWTUaFFWGlS8N6dHQ0PDxcf8fU7u7u4ODg9+/fk7vVajWTyZTL5eQt
AIuLizGafoNAk1FhRVjp0rAWCoVXr16lH5mbm5uYmKjfjebm8/kbZ8bGxi6+pbXJqLAirHTppQAb
jLCCsCKsoFPCirAirDYYYQVhRVhBp4TVjLUL0CkbjLAirDYYYYVLd+rKfThqwgqAsAIIK4CwAiCs
AMIKIKwACCuAsAIIKwDCCiCsAMIKIKwACCuAsAIIKwDCCiCsAMIKgLACCCuAsAIgrADCCiCsAMIK
gLACCCuAsAIgrADCCiCsAAgrgLACCCsAwgogrADCCiCsAAgrgLACCCsAwgogrADCCoCwAggrgLAC
CCsAnfMPP0DhyditwyQAAAAASUVORK5CYII=)
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_plus(S(x00), vx3) → new_plus(x00, vx3)
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_plus(S(x00), vx3) → new_plus(x00, vx3)
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_mysum(Cons(x0, x1)) → new_mysum(x1)
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_mysum(Cons(x0, x1)) → new_mysum(x1)
The graph contains the following edges 1 > 1