H-Termination proof of ../tpdb/FP/full_haskell/Prelude_pred

YES H-Termination proof of ../tpdb/FP/full_haskell/Prelude_pred_1.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule Main

((pred :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

Lambda Reductions:
The following Lambda expression

\(m,_)→m

is transformed to

m0 (m,_) = m

The following Lambda expression

\(_,r)→r

is transformed to

r0 (_,r) = r

The following Lambda expression

\(q,_)→q

is transformed to

q1 (q,_) = q

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

mainModule Main

((pred :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

If Reductions:
The following If expression

if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to

primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))

primDivNatS0 x y False = Zero

The following If expression

if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to

primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)

primModNatS0 x y False = Succ x

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

mainModule Main

((pred :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern

frac@(Double vx vy)

is replaced by the following term

Double vx vy

The bind variable of the following binding Pattern

frac@(Float wv ww)

is replaced by the following term

Float wv ww

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

mainModule Main

((pred :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

The following Function with conditions

toEnum 0 = ()

is transformed to

toEnum xy = toEnum1 xy

toEnum0 True xy = ()

toEnum1 xy = toEnum0 (xy == 0) xy

The following Function with conditions

toEnum 0 = LT

toEnum 1 = EQ

toEnum 2 = GT

is transformed to

toEnum yy = toEnum7 yy

toEnum yu = toEnum5 yu

toEnum xz = toEnum3 xz

toEnum2 True xz = GT

toEnum3 xz = toEnum2 (xz == 2) xz

toEnum4 True yu = EQ

toEnum4 yv yw = toEnum3 yw

toEnum5 yu = toEnum4 (yu == 1) yu

toEnum5 yx = toEnum3 yx

toEnum6 True yy = LT

toEnum6 yz zu = toEnum5 zu

toEnum7 yy = toEnum6 (yy == 0) yy

toEnum7 zv = toEnum5 zv

The following Function with conditions

toEnum 0 = False

toEnum 1 = True

is transformed to

toEnum zx = toEnum11 zx

toEnum zw = toEnum9 zw

toEnum8 True zw = True

toEnum9 zw = toEnum8 (zw == 1) zw

toEnum10 True zx = False

toEnum10 zy zz = toEnum9 zz

toEnum11 zx = toEnum10 (zx == 0) zx

toEnum11 vuu = toEnum9 vuu

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

mainModule Main

((pred :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

m

where

m = m0 vu6

m0 (m,xu) = m

vu6 = properFraction x

are unpacked to the following functions on top level

truncateM vuv = truncateM0 vuv (truncateVu6 vuv)

truncateVu6 vuv = properFraction vuv

truncateM0 vuv (m,xu) = m

The bindings of the following Let/Where expression

(fromIntegral q,r :% y)

where

q = q1 vu30

q1 (q,xv) = q

r = r0 vu30

r0 (xw,r) = r

vu30 = quotRem x y

are unpacked to the following functions on top level

properFractionR0 vuw vux (xw,r) = r

properFractionR vuw vux = properFractionR0 vuw vux (properFractionVu30 vuw vux)

properFractionVu30 vuw vux = quotRem vuw vux

properFractionQ1 vuw vux (q,xv) = q

properFractionQ vuw vux = properFractionQ1 vuw vux (properFractionVu30 vuw vux)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

mainModule Main

((pred :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

Num Reduction:All numbers are transformed to thier corresponding representation with Succ, Pred and Zero.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

mainModule Main

(pred :: Enum a => a -> a)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="pred\n",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="pred vuy3\n",fontsize=16,color="blue",shape="triangle"];519[label="pred :: Float -> Float",fontsize=10,color="white",style="solid",shape="box"];3 -> 519[label="",style="solid", color="blue", weight=9];
519 -> 4[label="",style="solid", color="blue", weight=3];
520[label="pred :: (Ratio a) -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];3 -> 520[label="",style="solid", color="blue", weight=9];
520 -> 5[label="",style="solid", color="blue", weight=3];
521[label="pred :: Char -> Char",fontsize=10,color="white",style="solid",shape="box"];3 -> 521[label="",style="solid", color="blue", weight=9];
521 -> 6[label="",style="solid", color="blue", weight=3];
522[label="pred :: Double -> Double",fontsize=10,color="white",style="solid",shape="box"];3 -> 522[label="",style="solid", color="blue", weight=9];
522 -> 7[label="",style="solid", color="blue", weight=3];
523[label="pred :: () -> ()",fontsize=10,color="white",style="solid",shape="box"];3 -> 523[label="",style="solid", color="blue", weight=9];
523 -> 8[label="",style="solid", color="blue", weight=3];
524[label="pred :: Bool -> Bool",fontsize=10,color="white",style="solid",shape="box"];3 -> 524[label="",style="solid", color="blue", weight=9];
524 -> 9[label="",style="solid", color="blue", weight=3];
525[label="pred :: Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];3 -> 525[label="",style="solid", color="blue", weight=9];
525 -> 10[label="",style="solid", color="blue", weight=3];
526[label="pred :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];3 -> 526[label="",style="solid", color="blue", weight=9];
526 -> 11[label="",style="solid", color="blue", weight=3];
527[label="pred :: Ordering -> Ordering",fontsize=10,color="white",style="solid",shape="box"];3 -> 527[label="",style="solid", color="blue", weight=9];
527 -> 12[label="",style="solid", color="blue", weight=3];
4[label="pred vuy3\n",fontsize=16,color="black",shape="box"];4 -> 13[label="",style="solid", color="black", weight=3];
5[label="pred vuy3\n",fontsize=16,color="black",shape="box"];5 -> 14[label="",style="solid", color="black", weight=3];
6[label="pred vuy3\n",fontsize=16,color="black",shape="box"];6 -> 15[label="",style="solid", color="black", weight=3];
7[label="pred vuy3\n",fontsize=16,color="black",shape="box"];7 -> 16[label="",style="solid", color="black", weight=3];
8[label="pred vuy3\n",fontsize=16,color="black",shape="box"];8 -> 17[label="",style="solid", color="black", weight=3];
9[label="pred vuy3\n",fontsize=16,color="black",shape="box"];9 -> 18[label="",style="solid", color="black", weight=3];
10[label="pred vuy3\n",fontsize=16,color="burlywood",shape="box"];528[label="vuy3/Integer vuy30",fontsize=10,color="white",style="solid",shape="box"];10 -> 528[label="",style="solid", color="burlywood", weight=9];
528 -> 19[label="",style="solid", color="burlywood", weight=3];
11[label="pred vuy3\n",fontsize=16,color="burlywood",shape="triangle"];529[label="vuy3/Pos vuy30",fontsize=10,color="white",style="solid",shape="box"];11 -> 529[label="",style="solid", color="burlywood", weight=9];
529 -> 20[label="",style="solid", color="burlywood", weight=3];
530[label="vuy3/Neg vuy30",fontsize=10,color="white",style="solid",shape="box"];11 -> 530[label="",style="solid", color="burlywood", weight=9];
530 -> 21[label="",style="solid", color="burlywood", weight=3];
12[label="pred vuy3\n",fontsize=16,color="black",shape="box"];12 -> 22[label="",style="solid", color="black", weight=3];
13[label="toEnum . (subtract (Pos (Succ Zero))) . fromEnum\n",fontsize=16,color="black",shape="box"];13 -> 23[label="",style="solid", color="black", weight=3];
14[label="toEnum . (subtract (Pos (Succ Zero))) . fromEnum\n",fontsize=16,color="black",shape="box"];14 -> 24[label="",style="solid", color="black", weight=3];
15[label="toEnum . (subtract (Pos (Succ Zero))) . fromEnum\n",fontsize=16,color="black",shape="box"];15 -> 25[label="",style="solid", color="black", weight=3];
16[label="toEnum . (subtract (Pos (Succ Zero))) . fromEnum\n",fontsize=16,color="black",shape="box"];16 -> 26[label="",style="solid", color="black", weight=3];
17[label="toEnum . (subtract (Pos (Succ Zero))) . fromEnum\n",fontsize=16,color="black",shape="box"];17 -> 27[label="",style="solid", color="black", weight=3];
18[label="toEnum . (subtract (Pos (Succ Zero))) . fromEnum\n",fontsize=16,color="black",shape="box"];18 -> 28[label="",style="solid", color="black", weight=3];
19[label="pred (Integer vuy30)\n",fontsize=16,color="black",shape="box"];19 -> 29[label="",style="solid", color="black", weight=3];
20[label="pred (Pos vuy30)\n",fontsize=16,color="burlywood",shape="box"];531[label="vuy30/Succ vuy300",fontsize=10,color="white",style="solid",shape="box"];20 -> 531[label="",style="solid", color="burlywood", weight=9];
531 -> 30[label="",style="solid", color="burlywood", weight=3];
532[label="vuy30/Zero",fontsize=10,color="white",style="solid",shape="box"];20 -> 532[label="",style="solid", color="burlywood", weight=9];
532 -> 31[label="",style="solid", color="burlywood", weight=3];
21[label="pred (Neg vuy30)\n",fontsize=16,color="burlywood",shape="box"];533[label="vuy30/Succ vuy300",fontsize=10,color="white",style="solid",shape="box"];21 -> 533[label="",style="solid", color="burlywood", weight=9];
533 -> 32[label="",style="solid", color="burlywood", weight=3];
534[label="vuy30/Zero",fontsize=10,color="white",style="solid",shape="box"];21 -> 534[label="",style="solid", color="burlywood", weight=9];
534 -> 33[label="",style="solid", color="burlywood", weight=3];
22[label="toEnum . (subtract (Pos (Succ Zero))) . fromEnum\n",fontsize=16,color="black",shape="box"];22 -> 34[label="",style="solid", color="black", weight=3];
23[label="toEnum ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];23 -> 35[label="",style="solid", color="black", weight=3];
24[label="toEnum ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];24 -> 36[label="",style="solid", color="black", weight=3];
25[label="toEnum ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];25 -> 37[label="",style="solid", color="black", weight=3];
26[label="toEnum ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];26 -> 38[label="",style="solid", color="black", weight=3];
27[label="toEnum ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];27 -> 39[label="",style="solid", color="black", weight=3];
28[label="toEnum ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];28 -> 40[label="",style="solid", color="black", weight=3];
29[label="Integer (pred vuy30)\n",fontsize=16,color="green",shape="box"];29 -> 41[label="",style="dashed", color="green", weight=3];
30[label="pred (Pos (Succ vuy300))\n",fontsize=16,color="black",shape="box"];30 -> 42[label="",style="solid", color="black", weight=3];
31[label="pred (Pos Zero)\n",fontsize=16,color="black",shape="box"];31 -> 43[label="",style="solid", color="black", weight=3];
32[label="pred (Neg (Succ vuy300))\n",fontsize=16,color="black",shape="box"];32 -> 44[label="",style="solid", color="black", weight=3];
33[label="pred (Neg Zero)\n",fontsize=16,color="black",shape="box"];33 -> 45[label="",style="solid", color="black", weight=3];
34[label="toEnum ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];34 -> 46[label="",style="solid", color="black", weight=3];
35[label="primIntToFloat ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];35 -> 47[label="",style="solid", color="black", weight=3];
36[label="fromInt ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];36 -> 48[label="",style="solid", color="black", weight=3];
37[label="primIntToChar ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];37 -> 49[label="",style="solid", color="black", weight=3];
38[label="primIntToDouble ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];38 -> 50[label="",style="solid", color="black", weight=3];
39[label="toEnum1 ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];39 -> 51[label="",style="solid", color="black", weight=3];
40[label="toEnum11 ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];40 -> 52[label="",style="solid", color="black", weight=3];
41 -> 11[label="",style="dashed", color="red", weight=0];
41[label="pred vuy30\n",fontsize=16,color="magenta"];41 -> 53[label="",style="dashed", color="magenta", weight=3];
42[label="Pos vuy300\n",fontsize=16,color="green",shape="box"];43[label="Neg (Succ Zero)\n",fontsize=16,color="green",shape="box"];44[label="Neg (Succ (Succ vuy300))\n",fontsize=16,color="green",shape="box"];45[label="Neg (Succ Zero)\n",fontsize=16,color="green",shape="box"];46[label="toEnum7 ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];46 -> 54[label="",style="solid", color="black", weight=3];
47[label="Float ((subtract (Pos (Succ Zero))) . fromEnum) (Pos (Succ Zero))\n",fontsize=16,color="green",shape="box"];47 -> 55[label="",style="dashed", color="green", weight=3];
48[label="intToRatio ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];48 -> 56[label="",style="solid", color="black", weight=3];
49[label="Char ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="green",shape="box"];49 -> 57[label="",style="dashed", color="green", weight=3];
50[label="Double ((subtract (Pos (Succ Zero))) . fromEnum) (Pos (Succ Zero))\n",fontsize=16,color="green",shape="box"];50 -> 58[label="",style="dashed", color="green", weight=3];
51[label="toEnum0 ((subtract (Pos (Succ Zero))) . fromEnum == Pos Zero) ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];51 -> 59[label="",style="solid", color="black", weight=3];
52[label="toEnum10 ((subtract (Pos (Succ Zero))) . fromEnum == Pos Zero) ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];52 -> 60[label="",style="solid", color="black", weight=3];
53[label="vuy30\n",fontsize=16,color="green",shape="box"];54[label="toEnum6 ((subtract (Pos (Succ Zero))) . fromEnum == Pos Zero) ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];54 -> 61[label="",style="solid", color="black", weight=3];
55[label="(subtract (Pos (Succ Zero))) . fromEnum\n",fontsize=16,color="black",shape="box"];55 -> 62[label="",style="solid", color="black", weight=3];
56[label="fromInt ((subtract (Pos (Succ Zero))) . fromEnum) :% fromInt (Pos (Succ Zero))\n",fontsize=16,color="green",shape="box"];56 -> 63[label="",style="dashed", color="green", weight=3];
56 -> 64[label="",style="dashed", color="green", weight=3];
57[label="(subtract (Pos (Succ Zero))) . fromEnum\n",fontsize=16,color="black",shape="box"];57 -> 65[label="",style="solid", color="black", weight=3];
58[label="(subtract (Pos (Succ Zero))) . fromEnum\n",fontsize=16,color="black",shape="box"];58 -> 66[label="",style="solid", color="black", weight=3];
59[label="toEnum0 (primEqInt ((subtract (Pos (Succ Zero))) . fromEnum) (Pos Zero)) ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];59 -> 67[label="",style="solid", color="black", weight=3];
60[label="toEnum10 (primEqInt ((subtract (Pos (Succ Zero))) . fromEnum) (Pos Zero)) ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];60 -> 68[label="",style="solid", color="black", weight=3];
61[label="toEnum6 (primEqInt ((subtract (Pos (Succ Zero))) . fromEnum) (Pos Zero)) ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];61 -> 69[label="",style="solid", color="black", weight=3];
62[label="subtract (Pos (Succ Zero)) (fromEnum vuy3)\n",fontsize=16,color="black",shape="box"];62 -> 70[label="",style="solid", color="black", weight=3];
63[label="fromInt ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="blue",shape="box"];536[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];63 -> 536[label="",style="solid", color="blue", weight=9];
536 -> 71[label="",style="solid", color="blue", weight=3];
537[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];63 -> 537[label="",style="solid", color="blue", weight=9];
537 -> 72[label="",style="solid", color="blue", weight=3];
64[label="fromInt (Pos (Succ Zero))\n",fontsize=16,color="blue",shape="box"];538[label="fromInt :: -> Int Int",fontsize=10,color="white",style="solid",shape="box"];64 -> 538[label="",style="solid", color="blue", weight=9];
538 -> 73[label="",style="solid", color="blue", weight=3];
539[label="fromInt :: -> Int Integer",fontsize=10,color="white",style="solid",shape="box"];64 -> 539[label="",style="solid", color="blue", weight=9];
539 -> 74[label="",style="solid", color="blue", weight=3];
65[label="subtract (Pos (Succ Zero)) (fromEnum vuy3)\n",fontsize=16,color="black",shape="box"];65 -> 75[label="",style="solid", color="black", weight=3];
66[label="subtract (Pos (Succ Zero)) (fromEnum vuy3)\n",fontsize=16,color="black",shape="box"];66 -> 76[label="",style="solid", color="black", weight=3];
67[label="toEnum0 (primEqInt (subtract (Pos (Succ Zero)) (fromEnum vuy3)) (Pos Zero)) (subtract (Pos (Succ Zero)) (fromEnum vuy3))\n",fontsize=16,color="black",shape="box"];67 -> 77[label="",style="solid", color="black", weight=3];
68[label="toEnum10 (primEqInt (subtract (Pos (Succ Zero)) (fromEnum vuy3)) (Pos Zero)) (subtract (Pos (Succ Zero)) (fromEnum vuy3))\n",fontsize=16,color="black",shape="box"];68 -> 78[label="",style="solid", color="black", weight=3];
69[label="toEnum6 (primEqInt (subtract (Pos (Succ Zero)) (fromEnum vuy3)) (Pos Zero)) (subtract (Pos (Succ Zero)) (fromEnum vuy3))\n",fontsize=16,color="black",shape="box"];69 -> 79[label="",style="solid", color="black", weight=3];
70[label="flip (-) (Pos (Succ Zero)) (fromEnum vuy3)\n",fontsize=16,color="black",shape="box"];70 -> 80[label="",style="solid", color="black", weight=3];
71[label="fromInt ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];71 -> 81[label="",style="solid", color="black", weight=3];
72[label="fromInt ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="black",shape="box"];72 -> 82[label="",style="solid", color="black", weight=3];
73[label="fromInt (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];73 -> 83[label="",style="solid", color="black", weight=3];
74[label="fromInt (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];74 -> 84[label="",style="solid", color="black", weight=3];
75[label="flip (-) (Pos (Succ Zero)) (fromEnum vuy3)\n",fontsize=16,color="black",shape="box"];75 -> 85[label="",style="solid", color="black", weight=3];
76[label="flip (-) (Pos (Succ Zero)) (fromEnum vuy3)\n",fontsize=16,color="black",shape="box"];76 -> 86[label="",style="solid", color="black", weight=3];
77[label="toEnum0 (primEqInt (flip (-) (Pos (Succ Zero)) (fromEnum vuy3)) (Pos Zero)) (flip (-) (Pos (Succ Zero)) (fromEnum vuy3))\n",fontsize=16,color="black",shape="box"];77 -> 87[label="",style="solid", color="black", weight=3];
78[label="toEnum10 (primEqInt (flip (-) (Pos (Succ Zero)) (fromEnum vuy3)) (Pos Zero)) (flip (-) (Pos (Succ Zero)) (fromEnum vuy3))\n",fontsize=16,color="black",shape="box"];78 -> 88[label="",style="solid", color="black", weight=3];
79[label="toEnum6 (primEqInt (flip (-) (Pos (Succ Zero)) (fromEnum vuy3)) (Pos Zero)) (flip (-) (Pos (Succ Zero)) (fromEnum vuy3))\n",fontsize=16,color="black",shape="box"];79 -> 89[label="",style="solid", color="black", weight=3];
80[label="(-) fromEnum vuy3 Pos (Succ Zero)\n",fontsize=16,color="black",shape="box"];80 -> 90[label="",style="solid", color="black", weight=3];
81[label="(subtract (Pos (Succ Zero))) . fromEnum\n",fontsize=16,color="black",shape="box"];81 -> 91[label="",style="solid", color="black", weight=3];
82[label="Integer ((subtract (Pos (Succ Zero))) . fromEnum)\n",fontsize=16,color="green",shape="box"];82 -> 92[label="",style="dashed", color="green", weight=3];
83[label="Pos (Succ Zero)\n",fontsize=16,color="green",shape="box"];84[label="Integer (Pos (Succ Zero))\n",fontsize=16,color="green",shape="box"];85[label="(-) fromEnum vuy3 Pos (Succ Zero)\n",fontsize=16,color="black",shape="box"];85 -> 93[label="",style="solid", color="black", weight=3];
86[label="(-) fromEnum vuy3 Pos (Succ Zero)\n",fontsize=16,color="black",shape="box"];86 -> 94[label="",style="solid", color="black", weight=3];
87[label="toEnum0 (primEqInt ((-) fromEnum vuy3 Pos (Succ Zero)) (Pos Zero)) ((-) fromEnum vuy3 Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];87 -> 95[label="",style="solid", color="black", weight=3];
88[label="toEnum10 (primEqInt ((-) fromEnum vuy3 Pos (Succ Zero)) (Pos Zero)) ((-) fromEnum vuy3 Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];88 -> 96[label="",style="solid", color="black", weight=3];
89[label="toEnum6 (primEqInt ((-) fromEnum vuy3 Pos (Succ Zero)) (Pos Zero)) ((-) fromEnum vuy3 Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];89 -> 97[label="",style="solid", color="black", weight=3];
90[label="primMinusInt (fromEnum vuy3) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];90 -> 98[label="",style="solid", color="black", weight=3];
91[label="subtract (Pos (Succ Zero)) (fromEnum vuy3)\n",fontsize=16,color="black",shape="box"];91 -> 99[label="",style="solid", color="black", weight=3];
92[label="(subtract (Pos (Succ Zero))) . fromEnum\n",fontsize=16,color="black",shape="box"];92 -> 100[label="",style="solid", color="black", weight=3];
93[label="primMinusInt (fromEnum vuy3) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];93 -> 101[label="",style="solid", color="black", weight=3];
94[label="primMinusInt (fromEnum vuy3) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];94 -> 102[label="",style="solid", color="black", weight=3];
95[label="toEnum0 (primEqInt (primMinusInt (fromEnum vuy3) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum vuy3) (Pos (Succ Zero)))\n",fontsize=16,color="burlywood",shape="box"];540[label="vuy3/()",fontsize=10,color="white",style="solid",shape="box"];95 -> 540[label="",style="solid", color="burlywood", weight=9];
540 -> 103[label="",style="solid", color="burlywood", weight=3];
96[label="toEnum10 (primEqInt (primMinusInt (fromEnum vuy3) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum vuy3) (Pos (Succ Zero)))\n",fontsize=16,color="burlywood",shape="box"];541[label="vuy3/False",fontsize=10,color="white",style="solid",shape="box"];96 -> 541[label="",style="solid", color="burlywood", weight=9];
541 -> 104[label="",style="solid", color="burlywood", weight=3];
542[label="vuy3/True",fontsize=10,color="white",style="solid",shape="box"];96 -> 542[label="",style="solid", color="burlywood", weight=9];
542 -> 105[label="",style="solid", color="burlywood", weight=3];
97[label="toEnum6 (primEqInt (primMinusInt (fromEnum vuy3) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum vuy3) (Pos (Succ Zero)))\n",fontsize=16,color="burlywood",shape="box"];543[label="vuy3/LT",fontsize=10,color="white",style="solid",shape="box"];97 -> 543[label="",style="solid", color="burlywood", weight=9];
543 -> 106[label="",style="solid", color="burlywood", weight=3];
544[label="vuy3/EQ",fontsize=10,color="white",style="solid",shape="box"];97 -> 544[label="",style="solid", color="burlywood", weight=9];
544 -> 107[label="",style="solid", color="burlywood", weight=3];
545[label="vuy3/GT",fontsize=10,color="white",style="solid",shape="box"];97 -> 545[label="",style="solid", color="burlywood", weight=9];
545 -> 108[label="",style="solid", color="burlywood", weight=3];
98[label="primMinusInt (truncate vuy3) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];98 -> 109[label="",style="solid", color="black", weight=3];
99[label="flip (-) (Pos (Succ Zero)) (fromEnum vuy3)\n",fontsize=16,color="black",shape="box"];99 -> 110[label="",style="solid", color="black", weight=3];
100[label="subtract (Pos (Succ Zero)) (fromEnum vuy3)\n",fontsize=16,color="black",shape="box"];100 -> 111[label="",style="solid", color="black", weight=3];
101[label="primMinusInt (primCharToInt vuy3) (Pos (Succ Zero))\n",fontsize=16,color="burlywood",shape="box"];546[label="vuy3/Char vuy30",fontsize=10,color="white",style="solid",shape="box"];101 -> 546[label="",style="solid", color="burlywood", weight=9];
546 -> 112[label="",style="solid", color="burlywood", weight=3];
102[label="primMinusInt (truncate vuy3) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];102 -> 113[label="",style="solid", color="black", weight=3];
103[label="toEnum0 (primEqInt (primMinusInt (fromEnum ()) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum ()) (Pos (Succ Zero)))\n",fontsize=16,color="black",shape="box"];103 -> 114[label="",style="solid", color="black", weight=3];
104[label="toEnum10 (primEqInt (primMinusInt (fromEnum False) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum False) (Pos (Succ Zero)))\n",fontsize=16,color="black",shape="box"];104 -> 115[label="",style="solid", color="black", weight=3];
105[label="toEnum10 (primEqInt (primMinusInt (fromEnum True) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum True) (Pos (Succ Zero)))\n",fontsize=16,color="black",shape="box"];105 -> 116[label="",style="solid", color="black", weight=3];
106[label="toEnum6 (primEqInt (primMinusInt (fromEnum LT) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum LT) (Pos (Succ Zero)))\n",fontsize=16,color="black",shape="box"];106 -> 117[label="",style="solid", color="black", weight=3];
107[label="toEnum6 (primEqInt (primMinusInt (fromEnum EQ) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum EQ) (Pos (Succ Zero)))\n",fontsize=16,color="black",shape="box"];107 -> 118[label="",style="solid", color="black", weight=3];
108[label="toEnum6 (primEqInt (primMinusInt (fromEnum GT) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (fromEnum GT) (Pos (Succ Zero)))\n",fontsize=16,color="black",shape="box"];108 -> 119[label="",style="solid", color="black", weight=3];
109[label="primMinusInt (truncateM vuy3) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];109 -> 120[label="",style="solid", color="black", weight=3];
110[label="(-) fromEnum vuy3 Pos (Succ Zero)\n",fontsize=16,color="black",shape="box"];110 -> 121[label="",style="solid", color="black", weight=3];
111[label="flip (-) (Pos (Succ Zero)) (fromEnum vuy3)\n",fontsize=16,color="black",shape="box"];111 -> 122[label="",style="solid", color="black", weight=3];
112[label="primMinusInt (primCharToInt (Char vuy30)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];112 -> 123[label="",style="solid", color="black", weight=3];
113[label="primMinusInt (truncateM vuy3) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];113 -> 124[label="",style="solid", color="black", weight=3];
114[label="toEnum0 (primEqInt (primMinusInt (Pos Zero) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (Pos Zero) (Pos (Succ Zero)))\n",fontsize=16,color="black",shape="box"];114 -> 125[label="",style="solid", color="black", weight=3];
115[label="toEnum10 (primEqInt (primMinusInt (Pos Zero) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (Pos Zero) (Pos (Succ Zero)))\n",fontsize=16,color="black",shape="box"];115 -> 126[label="",style="solid", color="black", weight=3];
116[label="toEnum10 (primEqInt (primMinusInt (Pos (Succ Zero)) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (Pos (Succ Zero)) (Pos (Succ Zero)))\n",fontsize=16,color="black",shape="box"];116 -> 127[label="",style="solid", color="black", weight=3];
117[label="toEnum6 (primEqInt (primMinusInt (Pos Zero) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (Pos Zero) (Pos (Succ Zero)))\n",fontsize=16,color="black",shape="box"];117 -> 128[label="",style="solid", color="black", weight=3];
118[label="toEnum6 (primEqInt (primMinusInt (Pos (Succ Zero)) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (Pos (Succ Zero)) (Pos (Succ Zero)))\n",fontsize=16,color="black",shape="box"];118 -> 129[label="",style="solid", color="black", weight=3];
119[label="toEnum6 (primEqInt (primMinusInt (Pos (Succ (Succ Zero))) (Pos (Succ Zero))) (Pos Zero)) (primMinusInt (Pos (Succ (Succ Zero))) (Pos (Succ Zero)))\n",fontsize=16,color="black",shape="box"];119 -> 130[label="",style="solid", color="black", weight=3];
120[label="primMinusInt (truncateM0 vuy3 (truncateVu6 vuy3)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];120 -> 131[label="",style="solid", color="black", weight=3];
121[label="primMinusInt (fromEnum vuy3) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];121 -> 132[label="",style="solid", color="black", weight=3];
122[label="(-) fromEnum vuy3 Pos (Succ Zero)\n",fontsize=16,color="black",shape="box"];122 -> 133[label="",style="solid", color="black", weight=3];
123[label="primMinusInt vuy30 (Pos (Succ Zero))\n",fontsize=16,color="burlywood",shape="triangle"];547[label="vuy30/Pos vuy300",fontsize=10,color="white",style="solid",shape="box"];123 -> 547[label="",style="solid", color="burlywood", weight=9];
547 -> 134[label="",style="solid", color="burlywood", weight=3];
548[label="vuy30/Neg vuy300",fontsize=10,color="white",style="solid",shape="box"];123 -> 548[label="",style="solid", color="burlywood", weight=9];
548 -> 135[label="",style="solid", color="burlywood", weight=3];
124 -> 123[label="",style="dashed", color="red", weight=0];
124[label="primMinusInt (truncateM0 vuy3 (truncateVu6 vuy3)) (Pos (Succ Zero))\n",fontsize=16,color="magenta"];124 -> 136[label="",style="dashed", color="magenta", weight=3];
125[label="toEnum0 (primEqInt (primMinusNat Zero (Succ Zero)) (Pos Zero)) (primMinusNat Zero (Succ Zero))\n",fontsize=16,color="black",shape="box"];125 -> 137[label="",style="solid", color="black", weight=3];
126[label="toEnum10 (primEqInt (primMinusNat Zero (Succ Zero)) (Pos Zero)) (primMinusNat Zero (Succ Zero))\n",fontsize=16,color="black",shape="box"];126 -> 138[label="",style="solid", color="black", weight=3];
127[label="toEnum10 (primEqInt (primMinusNat (Succ Zero) (Succ Zero)) (Pos Zero)) (primMinusNat (Succ Zero) (Succ Zero))\n",fontsize=16,color="black",shape="box"];127 -> 139[label="",style="solid", color="black", weight=3];
128[label="toEnum6 (primEqInt (primMinusNat Zero (Succ Zero)) (Pos Zero)) (primMinusNat Zero (Succ Zero))\n",fontsize=16,color="black",shape="box"];128 -> 140[label="",style="solid", color="black", weight=3];
129[label="toEnum6 (primEqInt (primMinusNat (Succ Zero) (Succ Zero)) (Pos Zero)) (primMinusNat (Succ Zero) (Succ Zero))\n",fontsize=16,color="black",shape="box"];129 -> 141[label="",style="solid", color="black", weight=3];
130[label="toEnum6 (primEqInt (primMinusNat (Succ (Succ Zero)) (Succ Zero)) (Pos Zero)) (primMinusNat (Succ (Succ Zero)) (Succ Zero))\n",fontsize=16,color="black",shape="box"];130 -> 142[label="",style="solid", color="black", weight=3];
131 -> 123[label="",style="dashed", color="red", weight=0];
131[label="primMinusInt (truncateM0 vuy3 (properFraction vuy3)) (Pos (Succ Zero))\n",fontsize=16,color="magenta"];131 -> 143[label="",style="dashed", color="magenta", weight=3];
132 -> 123[label="",style="dashed", color="red", weight=0];
132[label="primMinusInt (truncate vuy3) (Pos (Succ Zero))\n",fontsize=16,color="magenta"];132 -> 144[label="",style="dashed", color="magenta", weight=3];
133 -> 123[label="",style="dashed", color="red", weight=0];
133[label="primMinusInt (fromEnum vuy3) (Pos (Succ Zero))\n",fontsize=16,color="magenta"];133 -> 145[label="",style="dashed", color="magenta", weight=3];
134[label="primMinusInt (Pos vuy300) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];134 -> 146[label="",style="solid", color="black", weight=3];
135[label="primMinusInt (Neg vuy300) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];135 -> 147[label="",style="solid", color="black", weight=3];
136[label="truncateM0 vuy3 (truncateVu6 vuy3)\n",fontsize=16,color="black",shape="box"];136 -> 148[label="",style="solid", color="black", weight=3];
137[label="toEnum0 (primEqInt (Neg (Succ Zero)) (Pos Zero)) (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];137 -> 149[label="",style="solid", color="black", weight=3];
138[label="toEnum10 (primEqInt (Neg (Succ Zero)) (Pos Zero)) (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];138 -> 150[label="",style="solid", color="black", weight=3];
139[label="toEnum10 (primEqInt (primMinusNat Zero Zero) (Pos Zero)) (primMinusNat Zero Zero)\n",fontsize=16,color="black",shape="box"];139 -> 151[label="",style="solid", color="black", weight=3];
140[label="toEnum6 (primEqInt (Neg (Succ Zero)) (Pos Zero)) (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];140 -> 152[label="",style="solid", color="black", weight=3];
141[label="toEnum6 (primEqInt (primMinusNat Zero Zero) (Pos Zero)) (primMinusNat Zero Zero)\n",fontsize=16,color="black",shape="box"];141 -> 153[label="",style="solid", color="black", weight=3];
142[label="toEnum6 (primEqInt (primMinusNat (Succ Zero) Zero) (Pos Zero)) (primMinusNat (Succ Zero) Zero)\n",fontsize=16,color="black",shape="box"];142 -> 154[label="",style="solid", color="black", weight=3];
143[label="truncateM0 vuy3 (properFraction vuy3)\n",fontsize=16,color="black",shape="box"];143 -> 155[label="",style="solid", color="black", weight=3];
144[label="truncate vuy3\n",fontsize=16,color="black",shape="box"];144 -> 156[label="",style="solid", color="black", weight=3];
145[label="fromEnum vuy3\n",fontsize=16,color="black",shape="box"];145 -> 157[label="",style="solid", color="black", weight=3];
146[label="primMinusNat vuy300 (Succ Zero)\n",fontsize=16,color="burlywood",shape="box"];553[label="vuy300/Succ vuy3000",fontsize=10,color="white",style="solid",shape="box"];146 -> 553[label="",style="solid", color="burlywood", weight=9];
553 -> 158[label="",style="solid", color="burlywood", weight=3];
554[label="vuy300/Zero",fontsize=10,color="white",style="solid",shape="box"];146 -> 554[label="",style="solid", color="burlywood", weight=9];
554 -> 159[label="",style="solid", color="burlywood", weight=3];
147[label="Neg (primPlusNat vuy300 (Succ Zero))\n",fontsize=16,color="green",shape="box"];147 -> 160[label="",style="dashed", color="green", weight=3];
148[label="truncateM0 vuy3 (properFraction vuy3)\n",fontsize=16,color="black",shape="box"];148 -> 161[label="",style="solid", color="black", weight=3];
149[label="toEnum0 False (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];149 -> 162[label="",style="solid", color="black", weight=3];
150[label="toEnum10 False (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];150 -> 163[label="",style="solid", color="black", weight=3];
151[label="toEnum10 (primEqInt (Pos Zero) (Pos Zero)) (Pos Zero)\n",fontsize=16,color="black",shape="box"];151 -> 164[label="",style="solid", color="black", weight=3];
152[label="toEnum6 False (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];152 -> 165[label="",style="solid", color="black", weight=3];
153[label="toEnum6 (primEqInt (Pos Zero) (Pos Zero)) (Pos Zero)\n",fontsize=16,color="black",shape="box"];153 -> 166[label="",style="solid", color="black", weight=3];
154[label="toEnum6 (primEqInt (Pos (Succ Zero)) (Pos Zero)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];154 -> 167[label="",style="solid", color="black", weight=3];
155[label="truncateM0 vuy3 (floatProperFractionFloat vuy3)\n",fontsize=16,color="burlywood",shape="box"];555[label="vuy3/Float vuy30 vuy31",fontsize=10,color="white",style="solid",shape="box"];155 -> 555[label="",style="solid", color="burlywood", weight=9];
555 -> 168[label="",style="solid", color="burlywood", weight=3];
156[label="truncateM vuy3\n",fontsize=16,color="black",shape="box"];156 -> 169[label="",style="solid", color="black", weight=3];
157[label="truncate vuy3\n",fontsize=16,color="black",shape="box"];157 -> 170[label="",style="solid", color="black", weight=3];
158[label="primMinusNat (Succ vuy3000) (Succ Zero)\n",fontsize=16,color="black",shape="box"];158 -> 171[label="",style="solid", color="black", weight=3];
159[label="primMinusNat Zero (Succ Zero)\n",fontsize=16,color="black",shape="box"];159 -> 172[label="",style="solid", color="black", weight=3];
160[label="primPlusNat vuy300 (Succ Zero)\n",fontsize=16,color="burlywood",shape="box"];556[label="vuy300/Succ vuy3000",fontsize=10,color="white",style="solid",shape="box"];160 -> 556[label="",style="solid", color="burlywood", weight=9];
556 -> 173[label="",style="solid", color="burlywood", weight=3];
557[label="vuy300/Zero",fontsize=10,color="white",style="solid",shape="box"];160 -> 557[label="",style="solid", color="burlywood", weight=9];
557 -> 174[label="",style="solid", color="burlywood", weight=3];
161[label="truncateM0 vuy3 (floatProperFractionDouble vuy3)\n",fontsize=16,color="burlywood",shape="box"];558[label="vuy3/Double vuy30 vuy31",fontsize=10,color="white",style="solid",shape="box"];161 -> 558[label="",style="solid", color="burlywood", weight=9];
558 -> 175[label="",style="solid", color="burlywood", weight=3];
162[label="error []\n",fontsize=16,color="red",shape="box"];163[label="toEnum9 (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];163 -> 176[label="",style="solid", color="black", weight=3];
164[label="toEnum10 True (Pos Zero)\n",fontsize=16,color="black",shape="box"];164 -> 177[label="",style="solid", color="black", weight=3];
165[label="toEnum5 (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];165 -> 178[label="",style="solid", color="black", weight=3];
166[label="toEnum6 True (Pos Zero)\n",fontsize=16,color="black",shape="box"];166 -> 179[label="",style="solid", color="black", weight=3];
167[label="toEnum6 False (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];167 -> 180[label="",style="solid", color="black", weight=3];
168[label="truncateM0 (Float vuy30 vuy31) (floatProperFractionFloat (Float vuy30 vuy31))\n",fontsize=16,color="black",shape="box"];168 -> 181[label="",style="solid", color="black", weight=3];
169[label="truncateM0 vuy3 (truncateVu6 vuy3)\n",fontsize=16,color="black",shape="box"];169 -> 182[label="",style="solid", color="black", weight=3];
170[label="truncateM vuy3\n",fontsize=16,color="black",shape="box"];170 -> 183[label="",style="solid", color="black", weight=3];
171[label="primMinusNat vuy3000 Zero\n",fontsize=16,color="burlywood",shape="box"];559[label="vuy3000/Succ vuy30000",fontsize=10,color="white",style="solid",shape="box"];171 -> 559[label="",style="solid", color="burlywood", weight=9];
559 -> 184[label="",style="solid", color="burlywood", weight=3];
560[label="vuy3000/Zero",fontsize=10,color="white",style="solid",shape="box"];171 -> 560[label="",style="solid", color="burlywood", weight=9];
560 -> 185[label="",style="solid", color="burlywood", weight=3];
172[label="Neg (Succ Zero)\n",fontsize=16,color="green",shape="box"];173[label="primPlusNat (Succ vuy3000) (Succ Zero)\n",fontsize=16,color="black",shape="box"];173 -> 186[label="",style="solid", color="black", weight=3];
174[label="primPlusNat Zero (Succ Zero)\n",fontsize=16,color="black",shape="box"];174 -> 187[label="",style="solid", color="black", weight=3];
175[label="truncateM0 (Double vuy30 vuy31) (floatProperFractionDouble (Double vuy30 vuy31))\n",fontsize=16,color="black",shape="box"];175 -> 188[label="",style="solid", color="black", weight=3];
176[label="toEnum8 (Neg (Succ Zero) == Pos (Succ Zero)) (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];176 -> 189[label="",style="solid", color="black", weight=3];
177[label="False\n",fontsize=16,color="green",shape="box"];178[label="toEnum4 (Neg (Succ Zero) == Pos (Succ Zero)) (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];178 -> 190[label="",style="solid", color="black", weight=3];
179[label="LT\n",fontsize=16,color="green",shape="box"];180[label="toEnum5 (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];180 -> 191[label="",style="solid", color="black", weight=3];
181[label="truncateM0 (Float vuy30 vuy31) (fromInt (vuy30 `quot` vuy31),Float vuy30 vuy31 - fromInt (vuy30 `quot` vuy31))\n",fontsize=16,color="black",shape="box"];181 -> 192[label="",style="solid", color="black", weight=3];
182[label="truncateM0 vuy3 (properFraction vuy3)\n",fontsize=16,color="burlywood",shape="box"];561[label="vuy3/vuy30 :% vuy31",fontsize=10,color="white",style="solid",shape="box"];182 -> 561[label="",style="solid", color="burlywood", weight=9];
561 -> 193[label="",style="solid", color="burlywood", weight=3];
183[label="truncateM0 vuy3 (truncateVu6 vuy3)\n",fontsize=16,color="black",shape="box"];183 -> 194[label="",style="solid", color="black", weight=3];
184[label="primMinusNat (Succ vuy30000) Zero\n",fontsize=16,color="black",shape="box"];184 -> 195[label="",style="solid", color="black", weight=3];
185[label="primMinusNat Zero Zero\n",fontsize=16,color="black",shape="box"];185 -> 196[label="",style="solid", color="black", weight=3];
186[label="Succ (Succ (primPlusNat vuy3000 Zero))\n",fontsize=16,color="green",shape="box"];186 -> 197[label="",style="dashed", color="green", weight=3];
187[label="Succ Zero\n",fontsize=16,color="green",shape="box"];188[label="truncateM0 (Double vuy30 vuy31) (fromInt (vuy30 `quot` vuy31),Double vuy30 vuy31 - fromInt (vuy30 `quot` vuy31))\n",fontsize=16,color="black",shape="box"];188 -> 198[label="",style="solid", color="black", weight=3];
189[label="toEnum8 (primEqInt (Neg (Succ Zero)) (Pos (Succ Zero))) (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];189 -> 199[label="",style="solid", color="black", weight=3];
190[label="toEnum4 (primEqInt (Neg (Succ Zero)) (Pos (Succ Zero))) (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];190 -> 200[label="",style="solid", color="black", weight=3];
191[label="toEnum4 (Pos (Succ Zero) == Pos (Succ Zero)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];191 -> 201[label="",style="solid", color="black", weight=3];
192[label="fromInt (vuy30 `quot` vuy31)\n",fontsize=16,color="black",shape="triangle"];192 -> 202[label="",style="solid", color="black", weight=3];
193[label="truncateM0 (vuy30 :% vuy31) (properFraction (vuy30 :% vuy31))\n",fontsize=16,color="black",shape="box"];193 -> 203[label="",style="solid", color="black", weight=3];
194[label="truncateM0 vuy3 (properFraction vuy3)\n",fontsize=16,color="burlywood",shape="box"];562[label="vuy3/vuy30 :% vuy31",fontsize=10,color="white",style="solid",shape="box"];194 -> 562[label="",style="solid", color="burlywood", weight=9];
562 -> 204[label="",style="solid", color="burlywood", weight=3];
195[label="Pos (Succ vuy30000)\n",fontsize=16,color="green",shape="box"];196[label="Pos Zero\n",fontsize=16,color="green",shape="box"];197[label="primPlusNat vuy3000 Zero\n",fontsize=16,color="burlywood",shape="box"];563[label="vuy3000/Succ vuy30000",fontsize=10,color="white",style="solid",shape="box"];197 -> 563[label="",style="solid", color="burlywood", weight=9];
563 -> 205[label="",style="solid", color="burlywood", weight=3];
564[label="vuy3000/Zero",fontsize=10,color="white",style="solid",shape="box"];197 -> 564[label="",style="solid", color="burlywood", weight=9];
564 -> 206[label="",style="solid", color="burlywood", weight=3];
198 -> 192[label="",style="dashed", color="red", weight=0];
198[label="fromInt (vuy30 `quot` vuy31)\n",fontsize=16,color="magenta"];198 -> 207[label="",style="dashed", color="magenta", weight=3];
198 -> 208[label="",style="dashed", color="magenta", weight=3];
199[label="toEnum8 False (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];199 -> 209[label="",style="solid", color="black", weight=3];
200[label="toEnum4 False (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];200 -> 210[label="",style="solid", color="black", weight=3];
201[label="toEnum4 (primEqInt (Pos (Succ Zero)) (Pos (Succ Zero))) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];201 -> 211[label="",style="solid", color="black", weight=3];
202[label="vuy30 `quot` vuy31\n",fontsize=16,color="black",shape="box"];202 -> 212[label="",style="solid", color="black", weight=3];
203[label="truncateM0 (vuy30 :% vuy31) (fromIntegral (properFractionQ vuy30 vuy31),properFractionR vuy30 vuy31 :% vuy31)\n",fontsize=16,color="black",shape="box"];203 -> 213[label="",style="solid", color="black", weight=3];
204[label="truncateM0 (vuy30 :% vuy31) (properFraction (vuy30 :% vuy31))\n",fontsize=16,color="black",shape="box"];204 -> 214[label="",style="solid", color="black", weight=3];
205[label="primPlusNat (Succ vuy30000) Zero\n",fontsize=16,color="black",shape="box"];205 -> 215[label="",style="solid", color="black", weight=3];
206[label="primPlusNat Zero Zero\n",fontsize=16,color="black",shape="box"];206 -> 216[label="",style="solid", color="black", weight=3];
207[label="vuy31\n",fontsize=16,color="green",shape="box"];208[label="vuy30\n",fontsize=16,color="green",shape="box"];209[label="error []\n",fontsize=16,color="red",shape="box"];210[label="toEnum3 (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];210 -> 217[label="",style="solid", color="black", weight=3];
211[label="toEnum4 (primEqNat Zero Zero) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];211 -> 218[label="",style="solid", color="black", weight=3];
212[label="primQuotInt vuy30 vuy31\n",fontsize=16,color="burlywood",shape="triangle"];566[label="vuy30/Pos vuy300",fontsize=10,color="white",style="solid",shape="box"];212 -> 566[label="",style="solid", color="burlywood", weight=9];
566 -> 219[label="",style="solid", color="burlywood", weight=3];
567[label="vuy30/Neg vuy300",fontsize=10,color="white",style="solid",shape="box"];212 -> 567[label="",style="solid", color="burlywood", weight=9];
567 -> 220[label="",style="solid", color="burlywood", weight=3];
213[label="fromIntegral (properFractionQ vuy30 vuy31)\n",fontsize=16,color="black",shape="box"];213 -> 221[label="",style="solid", color="black", weight=3];
214[label="truncateM0 (vuy30 :% vuy31) (fromIntegral (properFractionQ vuy30 vuy31),properFractionR vuy30 vuy31 :% vuy31)\n",fontsize=16,color="black",shape="box"];214 -> 222[label="",style="solid", color="black", weight=3];
215[label="Succ vuy30000\n",fontsize=16,color="green",shape="box"];216[label="Zero\n",fontsize=16,color="green",shape="box"];217[label="toEnum2 (Neg (Succ Zero) == Pos (Succ (Succ Zero))) (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];217 -> 223[label="",style="solid", color="black", weight=3];
218[label="toEnum4 True (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];218 -> 224[label="",style="solid", color="black", weight=3];
219[label="primQuotInt (Pos vuy300) vuy31\n",fontsize=16,color="burlywood",shape="box"];568[label="vuy31/Pos vuy310",fontsize=10,color="white",style="solid",shape="box"];219 -> 568[label="",style="solid", color="burlywood", weight=9];
568 -> 225[label="",style="solid", color="burlywood", weight=3];
569[label="vuy31/Neg vuy310",fontsize=10,color="white",style="solid",shape="box"];219 -> 569[label="",style="solid", color="burlywood", weight=9];
569 -> 226[label="",style="solid", color="burlywood", weight=3];
220[label="primQuotInt (Neg vuy300) vuy31\n",fontsize=16,color="burlywood",shape="box"];570[label="vuy31/Pos vuy310",fontsize=10,color="white",style="solid",shape="box"];220 -> 570[label="",style="solid", color="burlywood", weight=9];
570 -> 227[label="",style="solid", color="burlywood", weight=3];
571[label="vuy31/Neg vuy310",fontsize=10,color="white",style="solid",shape="box"];220 -> 571[label="",style="solid", color="burlywood", weight=9];
571 -> 228[label="",style="solid", color="burlywood", weight=3];
221[label="fromInteger . toInteger\n",fontsize=16,color="black",shape="box"];221 -> 229[label="",style="solid", color="black", weight=3];
222[label="fromIntegral (properFractionQ vuy30 vuy31)\n",fontsize=16,color="black",shape="box"];222 -> 230[label="",style="solid", color="black", weight=3];
223[label="toEnum2 (primEqInt (Neg (Succ Zero)) (Pos (Succ (Succ Zero)))) (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];223 -> 231[label="",style="solid", color="black", weight=3];
224[label="EQ\n",fontsize=16,color="green",shape="box"];225[label="primQuotInt (Pos vuy300) (Pos vuy310)\n",fontsize=16,color="burlywood",shape="box"];572[label="vuy310/Succ vuy3100",fontsize=10,color="white",style="solid",shape="box"];225 -> 572[label="",style="solid", color="burlywood", weight=9];
572 -> 232[label="",style="solid", color="burlywood", weight=3];
573[label="vuy310/Zero",fontsize=10,color="white",style="solid",shape="box"];225 -> 573[label="",style="solid", color="burlywood", weight=9];
573 -> 233[label="",style="solid", color="burlywood", weight=3];
226[label="primQuotInt (Pos vuy300) (Neg vuy310)\n",fontsize=16,color="burlywood",shape="box"];574[label="vuy310/Succ vuy3100",fontsize=10,color="white",style="solid",shape="box"];226 -> 574[label="",style="solid", color="burlywood", weight=9];
574 -> 234[label="",style="solid", color="burlywood", weight=3];
575[label="vuy310/Zero",fontsize=10,color="white",style="solid",shape="box"];226 -> 575[label="",style="solid", color="burlywood", weight=9];
575 -> 235[label="",style="solid", color="burlywood", weight=3];
227[label="primQuotInt (Neg vuy300) (Pos vuy310)\n",fontsize=16,color="burlywood",shape="box"];576[label="vuy310/Succ vuy3100",fontsize=10,color="white",style="solid",shape="box"];227 -> 576[label="",style="solid", color="burlywood", weight=9];
576 -> 236[label="",style="solid", color="burlywood", weight=3];
577[label="vuy310/Zero",fontsize=10,color="white",style="solid",shape="box"];227 -> 577[label="",style="solid", color="burlywood", weight=9];
577 -> 237[label="",style="solid", color="burlywood", weight=3];
228[label="primQuotInt (Neg vuy300) (Neg vuy310)\n",fontsize=16,color="burlywood",shape="box"];578[label="vuy310/Succ vuy3100",fontsize=10,color="white",style="solid",shape="box"];228 -> 578[label="",style="solid", color="burlywood", weight=9];
578 -> 238[label="",style="solid", color="burlywood", weight=3];
579[label="vuy310/Zero",fontsize=10,color="white",style="solid",shape="box"];228 -> 579[label="",style="solid", color="burlywood", weight=9];
579 -> 239[label="",style="solid", color="burlywood", weight=3];
229[label="fromInteger (toInteger (properFractionQ vuy30 vuy31))\n",fontsize=16,color="black",shape="box"];229 -> 240[label="",style="solid", color="black", weight=3];
230[label="fromInteger . toInteger\n",fontsize=16,color="black",shape="box"];230 -> 241[label="",style="solid", color="black", weight=3];
231[label="toEnum2 False (Neg (Succ Zero))\n",fontsize=16,color="black",shape="box"];231 -> 242[label="",style="solid", color="black", weight=3];
232[label="primQuotInt (Pos vuy300) (Pos (Succ vuy3100))\n",fontsize=16,color="black",shape="box"];232 -> 243[label="",style="solid", color="black", weight=3];
233[label="primQuotInt (Pos vuy300) (Pos Zero)\n",fontsize=16,color="black",shape="box"];233 -> 244[label="",style="solid", color="black", weight=3];
234[label="primQuotInt (Pos vuy300) (Neg (Succ vuy3100))\n",fontsize=16,color="black",shape="box"];234 -> 245[label="",style="solid", color="black", weight=3];
235[label="primQuotInt (Pos vuy300) (Neg Zero)\n",fontsize=16,color="black",shape="box"];235 -> 246[label="",style="solid", color="black", weight=3];
236[label="primQuotInt (Neg vuy300) (Pos (Succ vuy3100))\n",fontsize=16,color="black",shape="box"];236 -> 247[label="",style="solid", color="black", weight=3];
237[label="primQuotInt (Neg vuy300) (Pos Zero)\n",fontsize=16,color="black",shape="box"];237 -> 248[label="",style="solid", color="black", weight=3];
238[label="primQuotInt (Neg vuy300) (Neg (Succ vuy3100))\n",fontsize=16,color="black",shape="box"];238 -> 249[label="",style="solid", color="black", weight=3];
239[label="primQuotInt (Neg vuy300) (Neg Zero)\n",fontsize=16,color="black",shape="box"];239 -> 250[label="",style="solid", color="black", weight=3];
240[label="fromInteger (Integer (properFractionQ vuy30 vuy31))\n",fontsize=16,color="black",shape="box"];240 -> 251[label="",style="solid", color="black", weight=3];
241[label="fromInteger (toInteger (properFractionQ vuy30 vuy31))\n",fontsize=16,color="black",shape="box"];241 -> 252[label="",style="solid", color="black", weight=3];
242[label="error []\n",fontsize=16,color="red",shape="box"];243[label="Pos (primDivNatS vuy300 (Succ vuy3100))\n",fontsize=16,color="green",shape="box"];243 -> 253[label="",style="dashed", color="green", weight=3];
244[label="error []\n",fontsize=16,color="black",shape="triangle"];244 -> 254[label="",style="solid", color="black", weight=3];
245[label="Neg (primDivNatS vuy300 (Succ vuy3100))\n",fontsize=16,color="green",shape="box"];245 -> 255[label="",style="dashed", color="green", weight=3];
246 -> 244[label="",style="dashed", color="red", weight=0];
246[label="error []\n",fontsize=16,color="magenta"];247[label="Neg (primDivNatS vuy300 (Succ vuy3100))\n",fontsize=16,color="green",shape="box"];247 -> 256[label="",style="dashed", color="green", weight=3];
248 -> 244[label="",style="dashed", color="red", weight=0];
248[label="error []\n",fontsize=16,color="magenta"];249[label="Pos (primDivNatS vuy300 (Succ vuy3100))\n",fontsize=16,color="green",shape="box"];249 -> 257[label="",style="dashed", color="green", weight=3];
250 -> 244[label="",style="dashed", color="red", weight=0];
250[label="error []\n",fontsize=16,color="magenta"];251[label="properFractionQ vuy30 vuy31\n",fontsize=16,color="black",shape="box"];251 -> 258[label="",style="solid", color="black", weight=3];
252[label="fromInteger (properFractionQ vuy30 vuy31)\n",fontsize=16,color="black",shape="box"];252 -> 259[label="",style="solid", color="black", weight=3];
253[label="primDivNatS vuy300 (Succ vuy3100)\n",fontsize=16,color="burlywood",shape="triangle"];583[label="vuy300/Succ vuy3000",fontsize=10,color="white",style="solid",shape="box"];253 -> 583[label="",style="solid", color="burlywood", weight=9];
583 -> 260[label="",style="solid", color="burlywood", weight=3];
584[label="vuy300/Zero",fontsize=10,color="white",style="solid",shape="box"];253 -> 584[label="",style="solid", color="burlywood", weight=9];
584 -> 261[label="",style="solid", color="burlywood", weight=3];
254[label="error []\n",fontsize=16,color="red",shape="box"];255 -> 253[label="",style="dashed", color="red", weight=0];
255[label="primDivNatS vuy300 (Succ vuy3100)\n",fontsize=16,color="magenta"];255 -> 262[label="",style="dashed", color="magenta", weight=3];
256 -> 253[label="",style="dashed", color="red", weight=0];
256[label="primDivNatS vuy300 (Succ vuy3100)\n",fontsize=16,color="magenta"];256 -> 263[label="",style="dashed", color="magenta", weight=3];
257 -> 253[label="",style="dashed", color="red", weight=0];
257[label="primDivNatS vuy300 (Succ vuy3100)\n",fontsize=16,color="magenta"];257 -> 264[label="",style="dashed", color="magenta", weight=3];
257 -> 265[label="",style="dashed", color="magenta", weight=3];
258[label="properFractionQ1 vuy30 vuy31 (properFractionVu30 vuy30 vuy31)\n",fontsize=16,color="black",shape="box"];258 -> 266[label="",style="solid", color="black", weight=3];
259[label="fromInteger (properFractionQ1 vuy30 vuy31 (properFractionVu30 vuy30 vuy31))\n",fontsize=16,color="black",shape="box"];259 -> 267[label="",style="solid", color="black", weight=3];
260[label="primDivNatS (Succ vuy3000) (Succ vuy3100)\n",fontsize=16,color="black",shape="box"];260 -> 268[label="",style="solid", color="black", weight=3];
261[label="primDivNatS Zero (Succ vuy3100)\n",fontsize=16,color="black",shape="box"];261 -> 269[label="",style="solid", color="black", weight=3];
262[label="vuy3100\n",fontsize=16,color="green",shape="box"];263[label="vuy300\n",fontsize=16,color="green",shape="box"];264[label="vuy3100\n",fontsize=16,color="green",shape="box"];265[label="vuy300\n",fontsize=16,color="green",shape="box"];266[label="properFractionQ1 vuy30 vuy31 (quotRem vuy30 vuy31)\n",fontsize=16,color="black",shape="box"];266 -> 270[label="",style="solid", color="black", weight=3];
267[label="fromInteger (properFractionQ1 vuy30 vuy31 (quotRem vuy30 vuy31))\n",fontsize=16,color="burlywood",shape="box"];588[label="vuy30/Integer vuy300",fontsize=10,color="white",style="solid",shape="box"];267 -> 588[label="",style="solid", color="burlywood", weight=9];
588 -> 271[label="",style="solid", color="burlywood", weight=3];
268[label="primDivNatS0 vuy3000 vuy3100 (primGEqNatS vuy3000 vuy3100)\n",fontsize=16,color="burlywood",shape="box"];589[label="vuy3000/Succ vuy30000",fontsize=10,color="white",style="solid",shape="box"];268 -> 589[label="",style="solid", color="burlywood", weight=9];
589 -> 272[label="",style="solid", color="burlywood", weight=3];
590[label="vuy3000/Zero",fontsize=10,color="white",style="solid",shape="box"];268 -> 590[label="",style="solid", color="burlywood", weight=9];
590 -> 273[label="",style="solid", color="burlywood", weight=3];
269[label="Zero\n",fontsize=16,color="green",shape="box"];270[label="properFractionQ1 vuy30 vuy31 (primQrmInt vuy30 vuy31)\n",fontsize=16,color="black",shape="box"];270 -> 274[label="",style="solid", color="black", weight=3];
271[label="fromInteger (properFractionQ1 (Integer vuy300) vuy31 (quotRem (Integer vuy300) vuy31))\n",fontsize=16,color="burlywood",shape="box"];591[label="vuy31/Integer vuy310",fontsize=10,color="white",style="solid",shape="box"];271 -> 591[label="",style="solid", color="burlywood", weight=9];
591 -> 275[label="",style="solid", color="burlywood", weight=3];
272[label="primDivNatS0 (Succ vuy30000) vuy3100 (primGEqNatS (Succ vuy30000) vuy3100)\n",fontsize=16,color="burlywood",shape="box"];592[label="vuy3100/Succ vuy31000",fontsize=10,color="white",style="solid",shape="box"];272 -> 592[label="",style="solid", color="burlywood", weight=9];
592 -> 276[label="",style="solid", color="burlywood", weight=3];
593[label="vuy3100/Zero",fontsize=10,color="white",style="solid",shape="box"];272 -> 593[label="",style="solid", color="burlywood", weight=9];
593 -> 277[label="",style="solid", color="burlywood", weight=3];
273[label="primDivNatS0 Zero vuy3100 (primGEqNatS Zero vuy3100)\n",fontsize=16,color="burlywood",shape="box"];594[label="vuy3100/Succ vuy31000",fontsize=10,color="white",style="solid",shape="box"];273 -> 594[label="",style="solid", color="burlywood", weight=9];
594 -> 278[label="",style="solid", color="burlywood", weight=3];
595[label="vuy3100/Zero",fontsize=10,color="white",style="solid",shape="box"];273 -> 595[label="",style="solid", color="burlywood", weight=9];
595 -> 279[label="",style="solid", color="burlywood", weight=3];
274 -> 280[label="",style="dashed", color="red", weight=0];
274[label="properFractionQ1 vuy30 vuy31 (primQuotInt vuy30 vuy31,primRemInt vuy30 vuy31)\n",fontsize=16,color="magenta"];274 -> 281[label="",style="dashed", color="magenta", weight=3];
275[label="fromInteger (properFractionQ1 (Integer vuy300) (Integer vuy310) (quotRem (Integer vuy300) (Integer vuy310)))\n",fontsize=16,color="black",shape="box"];275 -> 282[label="",style="solid", color="black", weight=3];
276[label="primDivNatS0 (Succ vuy30000) (Succ vuy31000) (primGEqNatS (Succ vuy30000) (Succ vuy31000))\n",fontsize=16,color="black",shape="box"];276 -> 283[label="",style="solid", color="black", weight=3];
277[label="primDivNatS0 (Succ vuy30000) Zero (primGEqNatS (Succ vuy30000) Zero)\n",fontsize=16,color="black",shape="box"];277 -> 284[label="",style="solid", color="black", weight=3];
278[label="primDivNatS0 Zero (Succ vuy31000) (primGEqNatS Zero (Succ vuy31000))\n",fontsize=16,color="black",shape="box"];278 -> 285[label="",style="solid", color="black", weight=3];
279[label="primDivNatS0 Zero Zero (primGEqNatS Zero Zero)\n",fontsize=16,color="black",shape="box"];279 -> 286[label="",style="solid", color="black", weight=3];
281 -> 212[label="",style="dashed", color="red", weight=0];
281[label="primQuotInt vuy30 vuy31\n",fontsize=16,color="magenta"];281 -> 287[label="",style="dashed", color="magenta", weight=3];
281 -> 288[label="",style="dashed", color="magenta", weight=3];
280[label="properFractionQ1 vuy30 vuy31 (vuy4,primRemInt vuy30 vuy31)\n",fontsize=16,color="black",shape="triangle"];280 -> 289[label="",style="solid", color="black", weight=3];
282 -> 290[label="",style="dashed", color="red", weight=0];
282[label="fromInteger (properFractionQ1 (Integer vuy300) (Integer vuy310) (Integer (primQuotInt vuy300 vuy310),Integer (primRemInt vuy300 vuy310)))\n",fontsize=16,color="magenta"];282 -> 291[label="",style="dashed", color="magenta", weight=3];
283 -> 456[label="",style="dashed", color="red", weight=0];
283[label="primDivNatS0 (Succ vuy30000) (Succ vuy31000) (primGEqNatS vuy30000 vuy31000)\n",fontsize=16,color="magenta"];283 -> 457[label="",style="dashed", color="magenta", weight=3];
283 -> 458[label="",style="dashed", color="magenta", weight=3];
283 -> 459[label="",style="dashed", color="magenta", weight=3];
283 -> 460[label="",style="dashed", color="magenta", weight=3];
284[label="primDivNatS0 (Succ vuy30000) Zero True\n",fontsize=16,color="black",shape="box"];284 -> 294[label="",style="solid", color="black", weight=3];
285[label="primDivNatS0 Zero (Succ vuy31000) False\n",fontsize=16,color="black",shape="box"];285 -> 295[label="",style="solid", color="black", weight=3];
286[label="primDivNatS0 Zero Zero True\n",fontsize=16,color="black",shape="box"];286 -> 296[label="",style="solid", color="black", weight=3];
287[label="vuy31\n",fontsize=16,color="green",shape="box"];288[label="vuy30\n",fontsize=16,color="green",shape="box"];289[label="vuy4\n",fontsize=16,color="green",shape="box"];291 -> 212[label="",style="dashed", color="red", weight=0];
291[label="primQuotInt vuy300 vuy310\n",fontsize=16,color="magenta"];291 -> 297[label="",style="dashed", color="magenta", weight=3];
291 -> 298[label="",style="dashed", color="magenta", weight=3];
290[label="fromInteger (properFractionQ1 (Integer vuy300) (Integer vuy310) (Integer vuy5,Integer (primRemInt vuy300 vuy310)))\n",fontsize=16,color="black",shape="triangle"];290 -> 299[label="",style="solid", color="black", weight=3];
457[label="vuy30000\n",fontsize=16,color="green",shape="box"];458[label="vuy30000\n",fontsize=16,color="green",shape="box"];459[label="vuy31000\n",fontsize=16,color="green",shape="box"];460[label="vuy31000\n",fontsize=16,color="green",shape="box"];456[label="primDivNatS0 (Succ vuy22) (Succ vuy23) (primGEqNatS vuy24 vuy25)\n",fontsize=16,color="burlywood",shape="triangle"];601[label="vuy24/Succ vuy240",fontsize=10,color="white",style="solid",shape="box"];456 -> 601[label="",style="solid", color="burlywood", weight=9];
601 -> 489[label="",style="solid", color="burlywood", weight=3];
602[label="vuy24/Zero",fontsize=10,color="white",style="solid",shape="box"];456 -> 602[label="",style="solid", color="burlywood", weight=9];
602 -> 490[label="",style="solid", color="burlywood", weight=3];
294[label="Succ (primDivNatS (primMinusNatS (Succ vuy30000) Zero) (Succ Zero))\n",fontsize=16,color="green",shape="box"];294 -> 304[label="",style="dashed", color="green", weight=3];
295[label="Zero\n",fontsize=16,color="green",shape="box"];296[label="Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))\n",fontsize=16,color="green",shape="box"];296 -> 305[label="",style="dashed", color="green", weight=3];
297[label="vuy310\n",fontsize=16,color="green",shape="box"];298[label="vuy300\n",fontsize=16,color="green",shape="box"];299[label="fromInteger (Integer vuy5)\n",fontsize=16,color="black",shape="box"];299 -> 306[label="",style="solid", color="black", weight=3];
489[label="primDivNatS0 (Succ vuy22) (Succ vuy23) (primGEqNatS (Succ vuy240) vuy25)\n",fontsize=16,color="burlywood",shape="box"];603[label="vuy25/Succ vuy250",fontsize=10,color="white",style="solid",shape="box"];489 -> 603[label="",style="solid", color="burlywood", weight=9];
603 -> 491[label="",style="solid", color="burlywood", weight=3];
604[label="vuy25/Zero",fontsize=10,color="white",style="solid",shape="box"];489 -> 604[label="",style="solid", color="burlywood", weight=9];
604 -> 492[label="",style="solid", color="burlywood", weight=3];
490[label="primDivNatS0 (Succ vuy22) (Succ vuy23) (primGEqNatS Zero vuy25)\n",fontsize=16,color="burlywood",shape="box"];605[label="vuy25/Succ vuy250",fontsize=10,color="white",style="solid",shape="box"];490 -> 605[label="",style="solid", color="burlywood", weight=9];
605 -> 493[label="",style="solid", color="burlywood", weight=3];
606[label="vuy25/Zero",fontsize=10,color="white",style="solid",shape="box"];490 -> 606[label="",style="solid", color="burlywood", weight=9];
606 -> 494[label="",style="solid", color="burlywood", weight=3];
304 -> 253[label="",style="dashed", color="red", weight=0];
304[label="primDivNatS (primMinusNatS (Succ vuy30000) Zero) (Succ Zero)\n",fontsize=16,color="magenta"];304 -> 311[label="",style="dashed", color="magenta", weight=3];
304 -> 312[label="",style="dashed", color="magenta", weight=3];
305 -> 253[label="",style="dashed", color="red", weight=0];
305[label="primDivNatS (primMinusNatS Zero Zero) (Succ Zero)\n",fontsize=16,color="magenta"];305 -> 313[label="",style="dashed", color="magenta", weight=3];
305 -> 314[label="",style="dashed", color="magenta", weight=3];
306[label="vuy5\n",fontsize=16,color="green",shape="box"];491[label="primDivNatS0 (Succ vuy22) (Succ vuy23) (primGEqNatS (Succ vuy240) (Succ vuy250))\n",fontsize=16,color="black",shape="box"];491 -> 495[label="",style="solid", color="black", weight=3];
492[label="primDivNatS0 (Succ vuy22) (Succ vuy23) (primGEqNatS (Succ vuy240) Zero)\n",fontsize=16,color="black",shape="box"];492 -> 496[label="",style="solid", color="black", weight=3];
493[label="primDivNatS0 (Succ vuy22) (Succ vuy23) (primGEqNatS Zero (Succ vuy250))\n",fontsize=16,color="black",shape="box"];493 -> 497[label="",style="solid", color="black", weight=3];
494[label="primDivNatS0 (Succ vuy22) (Succ vuy23) (primGEqNatS Zero Zero)\n",fontsize=16,color="black",shape="box"];494 -> 498[label="",style="solid", color="black", weight=3];
311[label="Zero\n",fontsize=16,color="green",shape="box"];312[label="primMinusNatS (Succ vuy30000) Zero\n",fontsize=16,color="black",shape="triangle"];312 -> 320[label="",style="solid", color="black", weight=3];
313[label="Zero\n",fontsize=16,color="green",shape="box"];314[label="primMinusNatS Zero Zero\n",fontsize=16,color="black",shape="triangle"];314 -> 321[label="",style="solid", color="black", weight=3];
495 -> 456[label="",style="dashed", color="red", weight=0];
495[label="primDivNatS0 (Succ vuy22) (Succ vuy23) (primGEqNatS vuy240 vuy250)\n",fontsize=16,color="magenta"];495 -> 499[label="",style="dashed", color="magenta", weight=3];
495 -> 500[label="",style="dashed", color="magenta", weight=3];
496[label="primDivNatS0 (Succ vuy22) (Succ vuy23) True\n",fontsize=16,color="black",shape="triangle"];496 -> 501[label="",style="solid", color="black", weight=3];
497[label="primDivNatS0 (Succ vuy22) (Succ vuy23) False\n",fontsize=16,color="black",shape="box"];497 -> 502[label="",style="solid", color="black", weight=3];
498 -> 496[label="",style="dashed", color="red", weight=0];
498[label="primDivNatS0 (Succ vuy22) (Succ vuy23) True\n",fontsize=16,color="magenta"];320[label="Succ vuy30000\n",fontsize=16,color="green",shape="box"];321[label="Zero\n",fontsize=16,color="green",shape="box"];499[label="vuy240\n",fontsize=16,color="green",shape="box"];500[label="vuy250\n",fontsize=16,color="green",shape="box"];501[label="Succ (primDivNatS (primMinusNatS (Succ vuy22) (Succ vuy23)) (Succ (Succ vuy23)))\n",fontsize=16,color="green",shape="box"];501 -> 503[label="",style="dashed", color="green", weight=3];
502[label="Zero\n",fontsize=16,color="green",shape="box"];503 -> 253[label="",style="dashed", color="red", weight=0];
503[label="primDivNatS (primMinusNatS (Succ vuy22) (Succ vuy23)) (Succ (Succ vuy23))\n",fontsize=16,color="magenta"];503 -> 504[label="",style="dashed", color="magenta", weight=3];
503 -> 505[label="",style="dashed", color="magenta", weight=3];
504[label="Succ vuy23\n",fontsize=16,color="green",shape="box"];505[label="primMinusNatS (Succ vuy22) (Succ vuy23)\n",fontsize=16,color="black",shape="box"];505 -> 506[label="",style="solid", color="black", weight=3];
506[label="primMinusNatS vuy22 vuy23\n",fontsize=16,color="burlywood",shape="triangle"];612[label="vuy22/Succ vuy220",fontsize=10,color="white",style="solid",shape="box"];506 -> 612[label="",style="solid", color="burlywood", weight=9];
612 -> 507[label="",style="solid", color="burlywood", weight=3];
613[label="vuy22/Zero",fontsize=10,color="white",style="solid",shape="box"];506 -> 613[label="",style="solid", color="burlywood", weight=9];
613 -> 508[label="",style="solid", color="burlywood", weight=3];
507[label="primMinusNatS (Succ vuy220) vuy23\n",fontsize=16,color="burlywood",shape="box"];614[label="vuy23/Succ vuy230",fontsize=10,color="white",style="solid",shape="box"];507 -> 614[label="",style="solid", color="burlywood", weight=9];
614 -> 509[label="",style="solid", color="burlywood", weight=3];
615[label="vuy23/Zero",fontsize=10,color="white",style="solid",shape="box"];507 -> 615[label="",style="solid", color="burlywood", weight=9];
615 -> 510[label="",style="solid", color="burlywood", weight=3];
508[label="primMinusNatS Zero vuy23\n",fontsize=16,color="burlywood",shape="box"];616[label="vuy23/Succ vuy230",fontsize=10,color="white",style="solid",shape="box"];508 -> 616[label="",style="solid", color="burlywood", weight=9];
616 -> 511[label="",style="solid", color="burlywood", weight=3];
617[label="vuy23/Zero",fontsize=10,color="white",style="solid",shape="box"];508 -> 617[label="",style="solid", color="burlywood", weight=9];
617 -> 512[label="",style="solid", color="burlywood", weight=3];
509[label="primMinusNatS (Succ vuy220) (Succ vuy230)\n",fontsize=16,color="black",shape="box"];509 -> 513[label="",style="solid", color="black", weight=3];
510[label="primMinusNatS (Succ vuy220) Zero\n",fontsize=16,color="black",shape="box"];510 -> 514[label="",style="solid", color="black", weight=3];
511[label="primMinusNatS Zero (Succ vuy230)\n",fontsize=16,color="black",shape="box"];511 -> 515[label="",style="solid", color="black", weight=3];
512[label="primMinusNatS Zero Zero\n",fontsize=16,color="black",shape="box"];512 -> 516[label="",style="solid", color="black", weight=3];
513 -> 506[label="",style="dashed", color="red", weight=0];
513[label="primMinusNatS vuy220 vuy230\n",fontsize=16,color="magenta"];513 -> 517[label="",style="dashed", color="magenta", weight=3];
513 -> 518[label="",style="dashed", color="magenta", weight=3];
514[label="Succ vuy220\n",fontsize=16,color="green",shape="box"];515[label="Zero\n",fontsize=16,color="green",shape="box"];516[label="Zero\n",fontsize=16,color="green",shape="box"];517[label="vuy220\n",fontsize=16,color="green",shape="box"];518[label="vuy230\n",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNatS(Succ(vuy220), Succ(vuy230)) → new_primMinusNatS(vuy220, vuy230)

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_primMinusNatS(Succ(vuy220), Succ(vuy230)) → new_primMinusNatS(vuy220, vuy230)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy22, vuy23, Zero, Zero) → new_primDivNatS00(vuy22, vuy23)
new_primDivNatS0(vuy22, vuy23, Succ(vuy240), Succ(vuy250)) → new_primDivNatS0(vuy22, vuy23, vuy240, vuy250)
new_primDivNatS00(vuy22, vuy23) → new_primDivNatS(new_primMinusNatS0(vuy22, vuy23), Succ(vuy23))
new_primDivNatS(Succ(Succ(vuy30000)), Succ(vuy31000)) → new_primDivNatS0(vuy30000, vuy31000, vuy30000, vuy31000)
new_primDivNatS0(vuy22, vuy23, Succ(vuy240), Zero) → new_primDivNatS(new_primMinusNatS0(vuy22, vuy23), Succ(vuy23))
new_primDivNatS(Succ(Zero), Zero) → new_primDivNatS(new_primMinusNatS2, Zero)
new_primDivNatS(Succ(Succ(vuy30000)), Zero) → new_primDivNatS(new_primMinusNatS1(vuy30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(vuy230)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS1(vuy30000) → Succ(vuy30000)
new_primMinusNatS0(Succ(vuy220), Succ(vuy230)) → new_primMinusNatS0(vuy220, vuy230)
new_primMinusNatS0(Succ(vuy220), Zero) → Succ(vuy220)
new_primMinusNatS2 → Zero

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS2
new_primMinusNatS1(x0)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(vuy30000)), Zero) → new_primDivNatS(new_primMinusNatS1(vuy30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(vuy230)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS1(vuy30000) → Succ(vuy30000)
new_primMinusNatS0(Succ(vuy220), Succ(vuy230)) → new_primMinusNatS0(vuy220, vuy230)
new_primMinusNatS0(Succ(vuy220), Zero) → Succ(vuy220)
new_primMinusNatS2 → Zero

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS2
new_primMinusNatS1(x0)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(vuy30000)), Zero) → new_primDivNatS(new_primMinusNatS1(vuy30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS1(vuy30000) → Succ(vuy30000)

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS2
new_primMinusNatS1(x0)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS2
new_primMinusNatS0(Zero, Zero)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ RuleRemovalProof

                                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(vuy30000)), Zero) → new_primDivNatS(new_primMinusNatS1(vuy30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS1(vuy30000) → Succ(vuy30000)

The set Q consists of the following terms:

new_primMinusNatS1(x0)

We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

new_primDivNatS(Succ(Succ(vuy30000)), Zero) → new_primDivNatS(new_primMinusNatS1(vuy30000), Zero)

Strictly oriented rules of the TRS R:

new_primMinusNatS1(vuy30000) → Succ(vuy30000)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + 2·x₁
POL(Zero) = 0
POL(new_primDivNatS(x₁, x₂)) = x₁ + x₂
POL(new_primMinusNatS1(x₁)) = 2 + 2·x₁

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ RuleRemovalProof

                                                ↳ QDP

                                                  ↳ PisEmptyProof

                                    ↳ QDP

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

new_primMinusNatS1(x0)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy22, vuy23, Zero, Zero) → new_primDivNatS00(vuy22, vuy23)
new_primDivNatS0(vuy22, vuy23, Succ(vuy240), Succ(vuy250)) → new_primDivNatS0(vuy22, vuy23, vuy240, vuy250)
new_primDivNatS(Succ(Succ(vuy30000)), Succ(vuy31000)) → new_primDivNatS0(vuy30000, vuy31000, vuy30000, vuy31000)
new_primDivNatS00(vuy22, vuy23) → new_primDivNatS(new_primMinusNatS0(vuy22, vuy23), Succ(vuy23))
new_primDivNatS0(vuy22, vuy23, Succ(vuy240), Zero) → new_primDivNatS(new_primMinusNatS0(vuy22, vuy23), Succ(vuy23))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(vuy230)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS1(vuy30000) → Succ(vuy30000)
new_primMinusNatS0(Succ(vuy220), Succ(vuy230)) → new_primMinusNatS0(vuy220, vuy230)
new_primMinusNatS0(Succ(vuy220), Zero) → Succ(vuy220)
new_primMinusNatS2 → Zero

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS2
new_primMinusNatS1(x0)
new_primMinusNatS0(Zero, Zero)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy22, vuy23, Zero, Zero) → new_primDivNatS00(vuy22, vuy23)
new_primDivNatS0(vuy22, vuy23, Succ(vuy240), Succ(vuy250)) → new_primDivNatS0(vuy22, vuy23, vuy240, vuy250)
new_primDivNatS(Succ(Succ(vuy30000)), Succ(vuy31000)) → new_primDivNatS0(vuy30000, vuy31000, vuy30000, vuy31000)
new_primDivNatS00(vuy22, vuy23) → new_primDivNatS(new_primMinusNatS0(vuy22, vuy23), Succ(vuy23))
new_primDivNatS0(vuy22, vuy23, Succ(vuy240), Zero) → new_primDivNatS(new_primMinusNatS0(vuy22, vuy23), Succ(vuy23))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(vuy230)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(vuy220), Succ(vuy230)) → new_primMinusNatS0(vuy220, vuy230)
new_primMinusNatS0(Succ(vuy220), Zero) → Succ(vuy220)

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS2
new_primMinusNatS1(x0)
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS2
new_primMinusNatS1(x0)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy22, vuy23, Zero, Zero) → new_primDivNatS00(vuy22, vuy23)
new_primDivNatS00(vuy22, vuy23) → new_primDivNatS(new_primMinusNatS0(vuy22, vuy23), Succ(vuy23))
new_primDivNatS(Succ(Succ(vuy30000)), Succ(vuy31000)) → new_primDivNatS0(vuy30000, vuy31000, vuy30000, vuy31000)
new_primDivNatS0(vuy22, vuy23, Succ(vuy240), Succ(vuy250)) → new_primDivNatS0(vuy22, vuy23, vuy240, vuy250)
new_primDivNatS0(vuy22, vuy23, Succ(vuy240), Zero) → new_primDivNatS(new_primMinusNatS0(vuy22, vuy23), Succ(vuy23))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(vuy230)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(vuy220), Succ(vuy230)) → new_primMinusNatS0(vuy220, vuy230)
new_primMinusNatS0(Succ(vuy220), Zero) → Succ(vuy220)

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_primDivNatS0(vuy22, vuy23, Zero, Zero) → new_primDivNatS00(vuy22, vuy23)
new_primDivNatS(Succ(Succ(vuy30000)), Succ(vuy31000)) → new_primDivNatS0(vuy30000, vuy31000, vuy30000, vuy31000)
new_primDivNatS0(vuy22, vuy23, Succ(vuy240), Zero) → new_primDivNatS(new_primMinusNatS0(vuy22, vuy23), Succ(vuy23))

The remaining pairs can at least be oriented weakly.

new_primDivNatS00(vuy22, vuy23) → new_primDivNatS(new_primMinusNatS0(vuy22, vuy23), Succ(vuy23))
new_primDivNatS0(vuy22, vuy23, Succ(vuy240), Succ(vuy250)) → new_primDivNatS0(vuy22, vuy23, vuy240, vuy250)

Used ordering: Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 0
POL(new_primDivNatS(x₁, x₂)) = x₁
POL(new_primDivNatS0(x₁, x₂, x₃, x₄)) = 1 + x₁
POL(new_primDivNatS00(x₁, x₂)) = x₁
POL(new_primMinusNatS0(x₁, x₂)) = x₁

The following usable rules [17] were oriented:

new_primMinusNatS0(Zero, Succ(vuy230)) → Zero
new_primMinusNatS0(Succ(vuy220), Zero) → Succ(vuy220)
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(vuy220), Succ(vuy230)) → new_primMinusNatS0(vuy220, vuy230)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ QDPOrderProof

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy22, vuy23, Succ(vuy240), Succ(vuy250)) → new_primDivNatS0(vuy22, vuy23, vuy240, vuy250)
new_primDivNatS00(vuy22, vuy23) → new_primDivNatS(new_primMinusNatS0(vuy22, vuy23), Succ(vuy23))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(vuy230)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(vuy220), Succ(vuy230)) → new_primMinusNatS0(vuy220, vuy230)
new_primMinusNatS0(Succ(vuy220), Zero) → Succ(vuy220)

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ QDPOrderProof

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy22, vuy23, Succ(vuy240), Succ(vuy250)) → new_primDivNatS0(vuy22, vuy23, vuy240, vuy250)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(vuy230)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(vuy220), Succ(vuy230)) → new_primMinusNatS0(vuy220, vuy230)
new_primMinusNatS0(Succ(vuy220), Zero) → Succ(vuy220)

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Zero, Zero)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ QDPOrderProof

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy22, vuy23, Succ(vuy240), Succ(vuy250)) → new_primDivNatS0(vuy22, vuy23, vuy240, vuy250)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Zero, Zero)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ QDPOrderProof

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ QReductionProof

                                                            ↳ QDP

                                                              ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy22, vuy23, Succ(vuy240), Succ(vuy250)) → new_primDivNatS0(vuy22, vuy23, vuy240, vuy250)

From the DPs we obtained the following set of size-change graphs:

new_primDivNatS0(vuy22, vuy23, Succ(vuy240), Succ(vuy250)) → new_primDivNatS0(vuy22, vuy23, vuy240, vuy250)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

primDivNatS0	x y True	= Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0	x y False	= Zero

primModNatS0	x y True	= primModNatS (primMinusNatS x y) (Succ y)
primModNatS0	x y False	= Succ x

toEnum	yy	= toEnum7 yy
toEnum	yu	= toEnum5 yu
toEnum	xz	= toEnum3 xz