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

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

↳ HASKELL

  ↳ LR

mainModule Main

((lexDigits :: [Char] -> [([Char],[Char])]) :: [Char] -> [([Char],[Char])])

module Main where

import qualified Prelude

Lambda Reductions:
The following Lambda expression

\vu68→

case vu68 of
(cs@(_ : _),t) → (cs,t) : []

_ → []

is transformed to

nonnull0 vu68 =

case vu68 of
(cs@(_ : _),t) → (cs,t) : []

_ → []

The following Lambda expression

\(_,zs)→zs

is transformed to

zs0 (_,zs) = zs

The following Lambda expression

\(ys,_)→ys

is transformed to

ys0 (ys,_) = ys

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

mainModule Main

((lexDigits :: [Char] -> [([Char],[Char])]) :: [Char] -> [([Char],[Char])])

module Main where

import qualified Prelude

Case Reductions:
The following Case expression

case vu68 of
(cs@(_ : _),t) → (cs,t) : []

_ → []

is transformed to

nonnull00 (cs@(_ : _),t) = (cs,t) : []

nonnull00 _ = []

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

mainModule Main

((lexDigits :: [Char] -> [([Char],[Char])]) :: [Char] -> [([Char],[Char])])

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

cs@(vy : vz)

is replaced by the following term

vy : vz

The bind variable of the following binding Pattern

xs@(wv : ww)

is replaced by the following term

wv : ww

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

mainModule Main

((lexDigits :: [Char] -> [([Char],[Char])]) :: [Char] -> [([Char],[Char])])

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

span p [] = ([],[])

span p (wv : ww)

| p wv

= (wv : ys,zs)

| otherwise

= ([],wv : ww)

where

vu43 = span p ww

ys = ys0 vu43

ys0 (ys,wx) = ys

zs = zs0 vu43

zs0 (wy,zs) = zs

is transformed to

span p [] = span3 p []

span p (wv : ww) = span2 p (wv : ww)

span2 p (wv : ww) =

span1 p wv ww (p wv)

where

span0 p wv ww True = ([],wv : ww)

span1 p wv ww True = (wv : ys,zs)

span1 p wv ww False = span0 p wv ww otherwise

vu43 = span p ww

ys = ys0 vu43

ys0 (ys,wx) = ys

zs = zs0 vu43

zs0 (wy,zs) = zs

span3 p [] = ([],[])

span3 xw xx = span2 xw xx

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

mainModule Main

((lexDigits :: [Char] -> [([Char],[Char])]) :: [Char] -> [([Char],[Char])])

module Main where

import qualified Prelude

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

span1 p wv ww (p wv)

where

span0 p wv ww True = ([],wv : ww)

span1 p wv ww True = (wv : ys,zs)

span1 p wv ww False = span0 p wv ww otherwise

vu43 = span p ww

ys = ys0 vu43

ys0 (ys,wx) = ys

zs = zs0 vu43

zs0 (wy,zs) = zs

are unpacked to the following functions on top level

span2Span0 xy xz p wv ww True = ([],wv : ww)

span2Span1 xy xz p wv ww True = (wv : span2Ys xy xz,span2Zs xy xz)

span2Span1 xy xz p wv ww False = span2Span0 xy xz p wv ww otherwise

span2Vu43 xy xz = span xy xz

span2Ys0 xy xz (ys,wx) = ys

span2Ys xy xz = span2Ys0 xy xz (span2Vu43 xy xz)

span2Zs0 xy xz (wy,zs) = zs

span2Zs xy xz = span2Zs0 xy xz (span2Vu43 xy xz)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

mainModule Main

((lexDigits :: [Char] -> [([Char],[Char])]) :: [Char] -> [([Char],[Char])])

module Main where

import qualified Prelude

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

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

mainModule Main

(lexDigits :: [Char] -> [([Char],[Char])])

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="lexDigits\n",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="lexDigits yu3\n",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="nonnull isDigit yu3\n",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="concatMap nonnull0 (span isDigit yu3 : [])\n",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="concat . map nonnull0\n",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="concat (map nonnull0 (span isDigit yu3 : []))\n",fontsize=16,color="black",shape="box"];7 -> 8[label="",style="solid", color="black", weight=3];
8[label="foldr (++) [] (map nonnull0 (span isDigit yu3 : []))\n",fontsize=16,color="black",shape="box"];8 -> 9[label="",style="solid", color="black", weight=3];
9[label="foldr (++) [] (nonnull0 (span isDigit yu3) : map nonnull0 [])\n",fontsize=16,color="black",shape="box"];9 -> 10[label="",style="solid", color="black", weight=3];
10[label="(++) nonnull0 (span isDigit yu3) foldr (++) [] (map nonnull0 [])\n",fontsize=16,color="black",shape="box"];10 -> 11[label="",style="solid", color="black", weight=3];
11[label="(++) nonnull00 (span isDigit yu3) foldr (++) [] (map nonnull0 [])\n",fontsize=16,color="burlywood",shape="box"];1787[label="yu3/yu30 : yu31",fontsize=10,color="white",style="solid",shape="box"];11 -> 1787[label="",style="solid", color="burlywood", weight=9];
1787 -> 12[label="",style="solid", color="burlywood", weight=3];
1788[label="yu3/[]",fontsize=10,color="white",style="solid",shape="box"];11 -> 1788[label="",style="solid", color="burlywood", weight=9];
1788 -> 13[label="",style="solid", color="burlywood", weight=3];
12[label="(++) nonnull00 (span isDigit (yu30 : yu31)) foldr (++) [] (map nonnull0 [])\n",fontsize=16,color="black",shape="box"];12 -> 14[label="",style="solid", color="black", weight=3];
13[label="(++) nonnull00 (span isDigit []) foldr (++) [] (map nonnull0 [])\n",fontsize=16,color="black",shape="box"];13 -> 15[label="",style="solid", color="black", weight=3];
14[label="(++) nonnull00 (span2 isDigit (yu30 : yu31)) foldr (++) [] (map nonnull0 [])\n",fontsize=16,color="black",shape="box"];14 -> 16[label="",style="solid", color="black", weight=3];
15[label="(++) nonnull00 (span3 isDigit []) foldr (++) [] (map nonnull0 [])\n",fontsize=16,color="black",shape="box"];15 -> 17[label="",style="solid", color="black", weight=3];
16[label="(++) nonnull00 (span2Span1 isDigit yu31 isDigit yu30 yu31 (isDigit yu30)) foldr (++) [] (map nonnull0 [])\n",fontsize=16,color="black",shape="box"];16 -> 18[label="",style="solid", color="black", weight=3];
17[label="(++) nonnull00 ([],[]) foldr (++) [] (map nonnull0 [])\n",fontsize=16,color="black",shape="box"];17 -> 19[label="",style="solid", color="black", weight=3];
18 -> 25[label="",style="dashed", color="red", weight=0];
18[label="(++) nonnull00 (span2Span1 isDigit yu31 isDigit yu30 yu31 (yu30 >= Char (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))) && yu30 <= Char (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) foldr (++) [] (map nonnull0 [])\n",fontsize=16,color="magenta"];18 -> 26[label="",style="dashed", color="magenta", weight=3];
18 -> 27[label="",style="dashed", color="magenta", weight=3];
18 -> 28[label="",style="dashed", color="magenta", weight=3];
18 -> 29[label="",style="dashed", color="magenta", weight=3];
19[label="(++) [] foldr (++) [] (map nonnull0 [])\n",fontsize=16,color="black",shape="box"];19 -> 24[label="",style="solid", color="black", weight=3];
26[label="yu30\n",fontsize=16,color="green",shape="box"];27[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))\n",fontsize=16,color="green",shape="box"];28[label="yu31\n",fontsize=16,color="green",shape="box"];29[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))\n",fontsize=16,color="green",shape="box"];25[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit yu10 yu9 (yu10 >= Char (Pos (Succ yu11)) && yu10 <= Char (Pos (Succ yu12)))) foldr (++) [] (map nonnull0 [])\n",fontsize=16,color="black",shape="triangle"];25 -> 34[label="",style="solid", color="black", weight=3];
24[label="foldr (++) [] (map nonnull0 [])\n",fontsize=16,color="black",shape="triangle"];24 -> 35[label="",style="solid", color="black", weight=3];
34 -> 36[label="",style="dashed", color="red", weight=0];
34[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit yu10 yu9 (compare yu10 (Char (Pos (Succ yu11))) /= LT && yu10 <= Char (Pos (Succ yu12)))) foldr (++) [] (map nonnull0 [])\n",fontsize=16,color="magenta"];34 -> 37[label="",style="dashed", color="magenta", weight=3];
35[label="foldr (++) [] []\n",fontsize=16,color="black",shape="box"];35 -> 38[label="",style="solid", color="black", weight=3];
37 -> 24[label="",style="dashed", color="red", weight=0];
37[label="foldr (++) [] (map nonnull0 [])\n",fontsize=16,color="magenta"];36[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit yu10 yu9 (compare yu10 (Char (Pos (Succ yu11))) /= LT && yu10 <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="triangle"];36 -> 39[label="",style="solid", color="black", weight=3];
38[label="[]\n",fontsize=16,color="green",shape="box"];39[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit yu10 yu9 (not (compare yu10 (Char (Pos (Succ yu11))) == LT) && yu10 <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];39 -> 40[label="",style="solid", color="black", weight=3];
40[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit yu10 yu9 (not (primCmpChar yu10 (Char (Pos (Succ yu11))) == LT) && yu10 <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="burlywood",shape="box"];1792[label="yu10/Char yu100",fontsize=10,color="white",style="solid",shape="box"];40 -> 1792[label="",style="solid", color="burlywood", weight=9];
1792 -> 41[label="",style="solid", color="burlywood", weight=3];
41[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char yu100) yu9 (not (primCmpChar (Char yu100) (Char (Pos (Succ yu11))) == LT) && Char yu100 <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];41 -> 42[label="",style="solid", color="black", weight=3];
42[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char yu100) yu9 (not (primCmpInt yu100 (Pos (Succ yu11)) == LT) && Char yu100 <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="burlywood",shape="box"];1793[label="yu100/Pos yu1000",fontsize=10,color="white",style="solid",shape="box"];42 -> 1793[label="",style="solid", color="burlywood", weight=9];
1793 -> 43[label="",style="solid", color="burlywood", weight=3];
1794[label="yu100/Neg yu1000",fontsize=10,color="white",style="solid",shape="box"];42 -> 1794[label="",style="solid", color="burlywood", weight=9];
1794 -> 44[label="",style="solid", color="burlywood", weight=3];
43[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Pos yu1000)) yu9 (not (primCmpInt (Pos yu1000) (Pos (Succ yu11)) == LT) && Char (Pos yu1000) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="burlywood",shape="box"];1795[label="yu1000/Succ yu10000",fontsize=10,color="white",style="solid",shape="box"];43 -> 1795[label="",style="solid", color="burlywood", weight=9];
1795 -> 45[label="",style="solid", color="burlywood", weight=3];
1796[label="yu1000/Zero",fontsize=10,color="white",style="solid",shape="box"];43 -> 1796[label="",style="solid", color="burlywood", weight=9];
1796 -> 46[label="",style="solid", color="burlywood", weight=3];
44[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Neg yu1000)) yu9 (not (primCmpInt (Neg yu1000) (Pos (Succ yu11)) == LT) && Char (Neg yu1000) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="burlywood",shape="box"];1797[label="yu1000/Succ yu10000",fontsize=10,color="white",style="solid",shape="box"];44 -> 1797[label="",style="solid", color="burlywood", weight=9];
1797 -> 47[label="",style="solid", color="burlywood", weight=3];
1798[label="yu1000/Zero",fontsize=10,color="white",style="solid",shape="box"];44 -> 1798[label="",style="solid", color="burlywood", weight=9];
1798 -> 48[label="",style="solid", color="burlywood", weight=3];
45[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Pos (Succ yu10000))) yu9 (not (primCmpInt (Pos (Succ yu10000)) (Pos (Succ yu11)) == LT) && Char (Pos (Succ yu10000)) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];45 -> 49[label="",style="solid", color="black", weight=3];
46[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Pos Zero)) yu9 (not (primCmpInt (Pos Zero) (Pos (Succ yu11)) == LT) && Char (Pos Zero) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];46 -> 50[label="",style="solid", color="black", weight=3];
47[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Neg (Succ yu10000))) yu9 (not (primCmpInt (Neg (Succ yu10000)) (Pos (Succ yu11)) == LT) && Char (Neg (Succ yu10000)) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];47 -> 51[label="",style="solid", color="black", weight=3];
48[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Neg Zero)) yu9 (not (primCmpInt (Neg Zero) (Pos (Succ yu11)) == LT) && Char (Neg Zero) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];48 -> 52[label="",style="solid", color="black", weight=3];
49 -> 358[label="",style="dashed", color="red", weight=0];
49[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Pos (Succ yu10000))) yu9 (not (primCmpNat (Succ yu10000) (Succ yu11) == LT) && Char (Pos (Succ yu10000)) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="magenta"];49 -> 359[label="",style="dashed", color="magenta", weight=3];
49 -> 360[label="",style="dashed", color="magenta", weight=3];
49 -> 361[label="",style="dashed", color="magenta", weight=3];
49 -> 362[label="",style="dashed", color="magenta", weight=3];
49 -> 363[label="",style="dashed", color="magenta", weight=3];
49 -> 364[label="",style="dashed", color="magenta", weight=3];
50[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Pos Zero)) yu9 (not (primCmpNat Zero (Succ yu11) == LT) && Char (Pos Zero) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];50 -> 54[label="",style="solid", color="black", weight=3];
51[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Neg (Succ yu10000))) yu9 (not (LT == LT) && Char (Neg (Succ yu10000)) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];51 -> 55[label="",style="solid", color="black", weight=3];
52[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Neg Zero)) yu9 (not (LT == LT) && Char (Neg Zero) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];52 -> 56[label="",style="solid", color="black", weight=3];
359[label="yu10000\n",fontsize=16,color="green",shape="box"];360[label="yu9\n",fontsize=16,color="green",shape="box"];361[label="Succ yu11\n",fontsize=16,color="green",shape="box"];362[label="yu12\n",fontsize=16,color="green",shape="box"];363[label="Succ yu10000\n",fontsize=16,color="green",shape="box"];364[label="yu13\n",fontsize=16,color="green",shape="box"];358[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not (primCmpNat yu29 yu30 == LT) && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="burlywood",shape="triangle"];1800[label="yu29/Succ yu290",fontsize=10,color="white",style="solid",shape="box"];358 -> 1800[label="",style="solid", color="burlywood", weight=9];
1800 -> 419[label="",style="solid", color="burlywood", weight=3];
1801[label="yu29/Zero",fontsize=10,color="white",style="solid",shape="box"];358 -> 1801[label="",style="solid", color="burlywood", weight=9];
1801 -> 420[label="",style="solid", color="burlywood", weight=3];
54[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Pos Zero)) yu9 (not (LT == LT) && Char (Pos Zero) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];54 -> 59[label="",style="solid", color="black", weight=3];
55[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Neg (Succ yu10000))) yu9 (not True && Char (Neg (Succ yu10000)) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];55 -> 60[label="",style="solid", color="black", weight=3];
56[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Neg Zero)) yu9 (not True && Char (Neg Zero) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];56 -> 61[label="",style="solid", color="black", weight=3];
419[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not (primCmpNat (Succ yu290) yu30 == LT) && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="burlywood",shape="box"];1802[label="yu30/Succ yu300",fontsize=10,color="white",style="solid",shape="box"];419 -> 1802[label="",style="solid", color="burlywood", weight=9];
1802 -> 421[label="",style="solid", color="burlywood", weight=3];
1803[label="yu30/Zero",fontsize=10,color="white",style="solid",shape="box"];419 -> 1803[label="",style="solid", color="burlywood", weight=9];
1803 -> 422[label="",style="solid", color="burlywood", weight=3];
420[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not (primCmpNat Zero yu30 == LT) && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="burlywood",shape="box"];1804[label="yu30/Succ yu300",fontsize=10,color="white",style="solid",shape="box"];420 -> 1804[label="",style="solid", color="burlywood", weight=9];
1804 -> 423[label="",style="solid", color="burlywood", weight=3];
1805[label="yu30/Zero",fontsize=10,color="white",style="solid",shape="box"];420 -> 1805[label="",style="solid", color="burlywood", weight=9];
1805 -> 424[label="",style="solid", color="burlywood", weight=3];
59[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Pos Zero)) yu9 (not True && Char (Pos Zero) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];59 -> 66[label="",style="solid", color="black", weight=3];
60[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Neg (Succ yu10000))) yu9 (False && Char (Neg (Succ yu10000)) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];60 -> 67[label="",style="solid", color="black", weight=3];
61[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Neg Zero)) yu9 (False && Char (Neg Zero) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];61 -> 68[label="",style="solid", color="black", weight=3];
421[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not (primCmpNat (Succ yu290) (Succ yu300) == LT) && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="black",shape="box"];421 -> 425[label="",style="solid", color="black", weight=3];
422[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not (primCmpNat (Succ yu290) Zero == LT) && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="black",shape="box"];422 -> 426[label="",style="solid", color="black", weight=3];
423[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not (primCmpNat Zero (Succ yu300) == LT) && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="black",shape="box"];423 -> 427[label="",style="solid", color="black", weight=3];
424[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not (primCmpNat Zero Zero == LT) && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="black",shape="box"];424 -> 428[label="",style="solid", color="black", weight=3];
66[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Pos Zero)) yu9 (False && Char (Pos Zero) <= Char (Pos (Succ yu12)))) yu13\n",fontsize=16,color="black",shape="box"];66 -> 73[label="",style="solid", color="black", weight=3];
67[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Neg (Succ yu10000))) yu9 False) yu13\n",fontsize=16,color="black",shape="box"];67 -> 74[label="",style="solid", color="black", weight=3];
68[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Neg Zero)) yu9 False) yu13\n",fontsize=16,color="black",shape="box"];68 -> 75[label="",style="solid", color="black", weight=3];
425 -> 358[label="",style="dashed", color="red", weight=0];
425[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not (primCmpNat yu290 yu300 == LT) && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="magenta"];425 -> 429[label="",style="dashed", color="magenta", weight=3];
425 -> 430[label="",style="dashed", color="magenta", weight=3];
426[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not (GT == LT) && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="black",shape="box"];426 -> 431[label="",style="solid", color="black", weight=3];
427[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not (LT == LT) && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="black",shape="box"];427 -> 432[label="",style="solid", color="black", weight=3];
428[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not (EQ == LT) && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="black",shape="box"];428 -> 433[label="",style="solid", color="black", weight=3];
73[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Pos Zero)) yu9 False) yu13\n",fontsize=16,color="black",shape="box"];73 -> 81[label="",style="solid", color="black", weight=3];
74[label="(++) nonnull00 (span2Span0 isDigit yu9 isDigit (Char (Neg (Succ yu10000))) yu9 otherwise) yu13\n",fontsize=16,color="black",shape="box"];74 -> 82[label="",style="solid", color="black", weight=3];
75[label="(++) nonnull00 (span2Span0 isDigit yu9 isDigit (Char (Neg Zero)) yu9 otherwise) yu13\n",fontsize=16,color="black",shape="box"];75 -> 83[label="",style="solid", color="black", weight=3];
429[label="yu300\n",fontsize=16,color="green",shape="box"];430[label="yu290\n",fontsize=16,color="green",shape="box"];431[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not False && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="black",shape="triangle"];431 -> 434[label="",style="solid", color="black", weight=3];
432[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not True && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="black",shape="box"];432 -> 435[label="",style="solid", color="black", weight=3];
433 -> 431[label="",style="dashed", color="red", weight=0];
433[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not False && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="magenta"];81[label="(++) nonnull00 (span2Span0 isDigit yu9 isDigit (Char (Pos Zero)) yu9 otherwise) yu13\n",fontsize=16,color="black",shape="box"];81 -> 91[label="",style="solid", color="black", weight=3];
82[label="(++) nonnull00 (span2Span0 isDigit yu9 isDigit (Char (Neg (Succ yu10000))) yu9 True) yu13\n",fontsize=16,color="black",shape="box"];82 -> 92[label="",style="solid", color="black", weight=3];
83[label="(++) nonnull00 (span2Span0 isDigit yu9 isDigit (Char (Neg Zero)) yu9 True) yu13\n",fontsize=16,color="black",shape="box"];83 -> 93[label="",style="solid", color="black", weight=3];
434[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (True && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="black",shape="box"];434 -> 436[label="",style="solid", color="black", weight=3];
435[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (False && Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="black",shape="box"];435 -> 437[label="",style="solid", color="black", weight=3];
91[label="(++) nonnull00 (span2Span0 isDigit yu9 isDigit (Char (Pos Zero)) yu9 True) yu13\n",fontsize=16,color="black",shape="box"];91 -> 101[label="",style="solid", color="black", weight=3];
92[label="(++) nonnull00 ([],Char (Neg (Succ yu10000)) : yu9) yu13\n",fontsize=16,color="black",shape="box"];92 -> 102[label="",style="solid", color="black", weight=3];
93[label="(++) nonnull00 ([],Char (Neg Zero) : yu9) yu13\n",fontsize=16,color="black",shape="box"];93 -> 103[label="",style="solid", color="black", weight=3];
436[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (Char (Pos (Succ yu28)) <= Char (Pos (Succ yu31)))) yu32\n",fontsize=16,color="black",shape="box"];436 -> 438[label="",style="solid", color="black", weight=3];
437[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 False) yu32\n",fontsize=16,color="black",shape="triangle"];437 -> 439[label="",style="solid", color="black", weight=3];
101[label="(++) nonnull00 ([],Char (Pos Zero) : yu9) yu13\n",fontsize=16,color="black",shape="box"];101 -> 112[label="",style="solid", color="black", weight=3];
102[label="(++) [] yu13\n",fontsize=16,color="black",shape="triangle"];102 -> 113[label="",style="solid", color="black", weight=3];
103 -> 102[label="",style="dashed", color="red", weight=0];
103[label="(++) [] yu13\n",fontsize=16,color="magenta"];438[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (compare (Char (Pos (Succ yu28))) (Char (Pos (Succ yu31))) /= GT)) yu32\n",fontsize=16,color="black",shape="box"];438 -> 440[label="",style="solid", color="black", weight=3];
439[label="(++) nonnull00 (span2Span0 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 otherwise) yu32\n",fontsize=16,color="black",shape="box"];439 -> 441[label="",style="solid", color="black", weight=3];
112 -> 102[label="",style="dashed", color="red", weight=0];
112[label="(++) [] yu13\n",fontsize=16,color="magenta"];113[label="yu13\n",fontsize=16,color="green",shape="box"];440[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not (compare (Char (Pos (Succ yu28))) (Char (Pos (Succ yu31))) == GT))) yu32\n",fontsize=16,color="black",shape="box"];440 -> 442[label="",style="solid", color="black", weight=3];
441[label="(++) nonnull00 (span2Span0 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 True) yu32\n",fontsize=16,color="black",shape="box"];441 -> 443[label="",style="solid", color="black", weight=3];
442[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not (primCmpChar (Char (Pos (Succ yu28))) (Char (Pos (Succ yu31))) == GT))) yu32\n",fontsize=16,color="black",shape="box"];442 -> 444[label="",style="solid", color="black", weight=3];
443[label="(++) nonnull00 ([],Char (Pos (Succ yu28)) : yu27) yu32\n",fontsize=16,color="black",shape="box"];443 -> 445[label="",style="solid", color="black", weight=3];
444[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not (primCmpInt (Pos (Succ yu28)) (Pos (Succ yu31)) == GT))) yu32\n",fontsize=16,color="black",shape="box"];444 -> 446[label="",style="solid", color="black", weight=3];
445 -> 102[label="",style="dashed", color="red", weight=0];
445[label="(++) [] yu32\n",fontsize=16,color="magenta"];445 -> 447[label="",style="dashed", color="magenta", weight=3];
446 -> 681[label="",style="dashed", color="red", weight=0];
446[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Pos (Succ yu28))) yu27 (not (primCmpNat (Succ yu28) (Succ yu31) == GT))) yu32\n",fontsize=16,color="magenta"];446 -> 682[label="",style="dashed", color="magenta", weight=3];
446 -> 683[label="",style="dashed", color="magenta", weight=3];
446 -> 684[label="",style="dashed", color="magenta", weight=3];
446 -> 685[label="",style="dashed", color="magenta", weight=3];
446 -> 686[label="",style="dashed", color="magenta", weight=3];
447[label="yu32\n",fontsize=16,color="green",shape="box"];682[label="Succ yu31\n",fontsize=16,color="green",shape="box"];683[label="yu32\n",fontsize=16,color="green",shape="box"];684[label="yu27\n",fontsize=16,color="green",shape="box"];685[label="Succ yu28\n",fontsize=16,color="green",shape="box"];686[label="yu28\n",fontsize=16,color="green",shape="box"];681[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 (not (primCmpNat yu64 yu65 == GT))) yu66\n",fontsize=16,color="burlywood",shape="triangle"];1812[label="yu64/Succ yu640",fontsize=10,color="white",style="solid",shape="box"];681 -> 1812[label="",style="solid", color="burlywood", weight=9];
1812 -> 732[label="",style="solid", color="burlywood", weight=3];
1813[label="yu64/Zero",fontsize=10,color="white",style="solid",shape="box"];681 -> 1813[label="",style="solid", color="burlywood", weight=9];
1813 -> 733[label="",style="solid", color="burlywood", weight=3];
732[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 (not (primCmpNat (Succ yu640) yu65 == GT))) yu66\n",fontsize=16,color="burlywood",shape="box"];1814[label="yu65/Succ yu650",fontsize=10,color="white",style="solid",shape="box"];732 -> 1814[label="",style="solid", color="burlywood", weight=9];
1814 -> 734[label="",style="solid", color="burlywood", weight=3];
1815[label="yu65/Zero",fontsize=10,color="white",style="solid",shape="box"];732 -> 1815[label="",style="solid", color="burlywood", weight=9];
1815 -> 735[label="",style="solid", color="burlywood", weight=3];
733[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 (not (primCmpNat Zero yu65 == GT))) yu66\n",fontsize=16,color="burlywood",shape="box"];1816[label="yu65/Succ yu650",fontsize=10,color="white",style="solid",shape="box"];733 -> 1816[label="",style="solid", color="burlywood", weight=9];
1816 -> 736[label="",style="solid", color="burlywood", weight=3];
1817[label="yu65/Zero",fontsize=10,color="white",style="solid",shape="box"];733 -> 1817[label="",style="solid", color="burlywood", weight=9];
1817 -> 737[label="",style="solid", color="burlywood", weight=3];
734[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 (not (primCmpNat (Succ yu640) (Succ yu650) == GT))) yu66\n",fontsize=16,color="black",shape="box"];734 -> 738[label="",style="solid", color="black", weight=3];
735[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 (not (primCmpNat (Succ yu640) Zero == GT))) yu66\n",fontsize=16,color="black",shape="box"];735 -> 739[label="",style="solid", color="black", weight=3];
736[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 (not (primCmpNat Zero (Succ yu650) == GT))) yu66\n",fontsize=16,color="black",shape="box"];736 -> 740[label="",style="solid", color="black", weight=3];
737[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 (not (primCmpNat Zero Zero == GT))) yu66\n",fontsize=16,color="black",shape="box"];737 -> 741[label="",style="solid", color="black", weight=3];
738 -> 681[label="",style="dashed", color="red", weight=0];
738[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 (not (primCmpNat yu640 yu650 == GT))) yu66\n",fontsize=16,color="magenta"];738 -> 742[label="",style="dashed", color="magenta", weight=3];
738 -> 743[label="",style="dashed", color="magenta", weight=3];
739[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 (not (GT == GT))) yu66\n",fontsize=16,color="black",shape="box"];739 -> 744[label="",style="solid", color="black", weight=3];
740[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 (not (LT == GT))) yu66\n",fontsize=16,color="black",shape="box"];740 -> 745[label="",style="solid", color="black", weight=3];
741[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 (not (EQ == GT))) yu66\n",fontsize=16,color="black",shape="box"];741 -> 746[label="",style="solid", color="black", weight=3];
742[label="yu650\n",fontsize=16,color="green",shape="box"];743[label="yu640\n",fontsize=16,color="green",shape="box"];744[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 (not True)) yu66\n",fontsize=16,color="black",shape="box"];744 -> 747[label="",style="solid", color="black", weight=3];
745[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 (not False)) yu66\n",fontsize=16,color="black",shape="triangle"];745 -> 748[label="",style="solid", color="black", weight=3];
746 -> 745[label="",style="dashed", color="red", weight=0];
746[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 (not False)) yu66\n",fontsize=16,color="magenta"];747 -> 437[label="",style="dashed", color="red", weight=0];
747[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 False) yu66\n",fontsize=16,color="magenta"];747 -> 749[label="",style="dashed", color="magenta", weight=3];
747 -> 750[label="",style="dashed", color="magenta", weight=3];
747 -> 751[label="",style="dashed", color="magenta", weight=3];
748[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Pos (Succ yu63))) yu62 True) yu66\n",fontsize=16,color="black",shape="box"];748 -> 752[label="",style="solid", color="black", weight=3];
749[label="yu63\n",fontsize=16,color="green",shape="box"];750[label="yu62\n",fontsize=16,color="green",shape="box"];751[label="yu66\n",fontsize=16,color="green",shape="box"];752[label="(++) nonnull00 (Char (Pos (Succ yu63)) : span2Ys isDigit yu62,span2Zs isDigit yu62) yu66\n",fontsize=16,color="black",shape="box"];752 -> 753[label="",style="solid", color="black", weight=3];
753[label="(++) ((Char (Pos (Succ yu63)) : span2Ys isDigit yu62,span2Zs isDigit yu62) : []) yu66\n",fontsize=16,color="black",shape="box"];753 -> 754[label="",style="solid", color="black", weight=3];
754[label="(Char (Pos (Succ yu63)) : span2Ys isDigit yu62,span2Zs isDigit yu62) : [] ++ yu66\n",fontsize=16,color="green",shape="box"];754 -> 755[label="",style="dashed", color="green", weight=3];
754 -> 756[label="",style="dashed", color="green", weight=3];
754 -> 757[label="",style="dashed", color="green", weight=3];
755[label="span2Ys isDigit yu62\n",fontsize=16,color="black",shape="triangle"];755 -> 758[label="",style="solid", color="black", weight=3];
756[label="span2Zs isDigit yu62\n",fontsize=16,color="black",shape="triangle"];756 -> 759[label="",style="solid", color="black", weight=3];
757 -> 102[label="",style="dashed", color="red", weight=0];
757[label="[] ++ yu66\n",fontsize=16,color="magenta"];757 -> 760[label="",style="dashed", color="magenta", weight=3];
758[label="span2Ys0 isDigit yu62 (span2Vu43 isDigit yu62)\n",fontsize=16,color="black",shape="box"];758 -> 761[label="",style="solid", color="black", weight=3];
759[label="span2Zs0 isDigit yu62 (span2Vu43 isDigit yu62)\n",fontsize=16,color="black",shape="box"];759 -> 762[label="",style="solid", color="black", weight=3];
760[label="yu66\n",fontsize=16,color="green",shape="box"];761[label="span2Ys0 isDigit yu62 (span isDigit yu62)\n",fontsize=16,color="burlywood",shape="box"];1822[label="yu62/yu620 : yu621",fontsize=10,color="white",style="solid",shape="box"];761 -> 1822[label="",style="solid", color="burlywood", weight=9];
1822 -> 763[label="",style="solid", color="burlywood", weight=3];
1823[label="yu62/[]",fontsize=10,color="white",style="solid",shape="box"];761 -> 1823[label="",style="solid", color="burlywood", weight=9];
1823 -> 764[label="",style="solid", color="burlywood", weight=3];
762[label="span2Zs0 isDigit yu62 (span isDigit yu62)\n",fontsize=16,color="burlywood",shape="box"];1824[label="yu62/yu620 : yu621",fontsize=10,color="white",style="solid",shape="box"];762 -> 1824[label="",style="solid", color="burlywood", weight=9];
1824 -> 765[label="",style="solid", color="burlywood", weight=3];
1825[label="yu62/[]",fontsize=10,color="white",style="solid",shape="box"];762 -> 1825[label="",style="solid", color="burlywood", weight=9];
1825 -> 766[label="",style="solid", color="burlywood", weight=3];
763[label="span2Ys0 isDigit (yu620 : yu621) (span isDigit (yu620 : yu621))\n",fontsize=16,color="black",shape="box"];763 -> 767[label="",style="solid", color="black", weight=3];
764[label="span2Ys0 isDigit [] (span isDigit [])\n",fontsize=16,color="black",shape="box"];764 -> 768[label="",style="solid", color="black", weight=3];
765[label="span2Zs0 isDigit (yu620 : yu621) (span isDigit (yu620 : yu621))\n",fontsize=16,color="black",shape="box"];765 -> 769[label="",style="solid", color="black", weight=3];
766[label="span2Zs0 isDigit [] (span isDigit [])\n",fontsize=16,color="black",shape="box"];766 -> 770[label="",style="solid", color="black", weight=3];
767[label="span2Ys0 isDigit (yu620 : yu621) (span2 isDigit (yu620 : yu621))\n",fontsize=16,color="black",shape="box"];767 -> 771[label="",style="solid", color="black", weight=3];
768[label="span2Ys0 isDigit [] (span3 isDigit [])\n",fontsize=16,color="black",shape="box"];768 -> 772[label="",style="solid", color="black", weight=3];
769[label="span2Zs0 isDigit (yu620 : yu621) (span2 isDigit (yu620 : yu621))\n",fontsize=16,color="black",shape="box"];769 -> 773[label="",style="solid", color="black", weight=3];
770[label="span2Zs0 isDigit [] (span3 isDigit [])\n",fontsize=16,color="black",shape="box"];770 -> 774[label="",style="solid", color="black", weight=3];
771[label="span2Ys0 isDigit (yu620 : yu621) (span2Span1 isDigit yu621 isDigit yu620 yu621 (isDigit yu620))\n",fontsize=16,color="black",shape="box"];771 -> 775[label="",style="solid", color="black", weight=3];
772[label="span2Ys0 isDigit [] ([],[])\n",fontsize=16,color="black",shape="box"];772 -> 776[label="",style="solid", color="black", weight=3];
773[label="span2Zs0 isDigit (yu620 : yu621) (span2Span1 isDigit yu621 isDigit yu620 yu621 (isDigit yu620))\n",fontsize=16,color="black",shape="box"];773 -> 777[label="",style="solid", color="black", weight=3];
774[label="span2Zs0 isDigit [] ([],[])\n",fontsize=16,color="black",shape="box"];774 -> 778[label="",style="solid", color="black", weight=3];
775 -> 787[label="",style="dashed", color="red", weight=0];
775[label="span2Ys0 isDigit (yu620 : yu621) (span2Span1 isDigit yu621 isDigit yu620 yu621 (yu620 >= Char (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))) && yu620 <= Char (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))\n",fontsize=16,color="magenta"];775 -> 788[label="",style="dashed", color="magenta", weight=3];
775 -> 789[label="",style="dashed", color="magenta", weight=3];
775 -> 790[label="",style="dashed", color="magenta", weight=3];
775 -> 791[label="",style="dashed", color="magenta", weight=3];
776[label="[]\n",fontsize=16,color="green",shape="box"];777 -> 797[label="",style="dashed", color="red", weight=0];
777[label="span2Zs0 isDigit (yu620 : yu621) (span2Span1 isDigit yu621 isDigit yu620 yu621 (yu620 >= Char (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))) && yu620 <= Char (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))\n",fontsize=16,color="magenta"];777 -> 798[label="",style="dashed", color="magenta", weight=3];
777 -> 799[label="",style="dashed", color="magenta", weight=3];
777 -> 800[label="",style="dashed", color="magenta", weight=3];
777 -> 801[label="",style="dashed", color="magenta", weight=3];
778[label="[]\n",fontsize=16,color="green",shape="box"];788[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))\n",fontsize=16,color="green",shape="box"];789[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))\n",fontsize=16,color="green",shape="box"];790[label="yu621\n",fontsize=16,color="green",shape="box"];791[label="yu620\n",fontsize=16,color="green",shape="box"];787[label="span2Ys0 isDigit (yu76 : yu77) (span2Span1 isDigit yu77 isDigit yu76 yu77 (yu76 >= Char (Pos (Succ yu78)) && yu76 <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="triangle"];787 -> 796[label="",style="solid", color="black", weight=3];
798[label="yu620\n",fontsize=16,color="green",shape="box"];799[label="yu621\n",fontsize=16,color="green",shape="box"];800[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))\n",fontsize=16,color="green",shape="box"];801[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))\n",fontsize=16,color="green",shape="box"];797[label="span2Zs0 isDigit (yu81 : yu82) (span2Span1 isDigit yu82 isDigit yu81 yu82 (yu81 >= Char (Pos (Succ yu83)) && yu81 <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="triangle"];797 -> 806[label="",style="solid", color="black", weight=3];
796[label="span2Ys0 isDigit (yu76 : yu77) (span2Span1 isDigit yu77 isDigit yu76 yu77 (compare yu76 (Char (Pos (Succ yu78))) /= LT && yu76 <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];796 -> 807[label="",style="solid", color="black", weight=3];
806[label="span2Zs0 isDigit (yu81 : yu82) (span2Span1 isDigit yu82 isDigit yu81 yu82 (compare yu81 (Char (Pos (Succ yu83))) /= LT && yu81 <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];806 -> 808[label="",style="solid", color="black", weight=3];
807[label="span2Ys0 isDigit (yu76 : yu77) (span2Span1 isDigit yu77 isDigit yu76 yu77 (not (compare yu76 (Char (Pos (Succ yu78))) == LT) && yu76 <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];807 -> 809[label="",style="solid", color="black", weight=3];
808[label="span2Zs0 isDigit (yu81 : yu82) (span2Span1 isDigit yu82 isDigit yu81 yu82 (not (compare yu81 (Char (Pos (Succ yu83))) == LT) && yu81 <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];808 -> 810[label="",style="solid", color="black", weight=3];
809[label="span2Ys0 isDigit (yu76 : yu77) (span2Span1 isDigit yu77 isDigit yu76 yu77 (not (primCmpChar yu76 (Char (Pos (Succ yu78))) == LT) && yu76 <= Char (Pos (Succ yu79))))\n",fontsize=16,color="burlywood",shape="box"];1828[label="yu76/Char yu760",fontsize=10,color="white",style="solid",shape="box"];809 -> 1828[label="",style="solid", color="burlywood", weight=9];
1828 -> 811[label="",style="solid", color="burlywood", weight=3];
810[label="span2Zs0 isDigit (yu81 : yu82) (span2Span1 isDigit yu82 isDigit yu81 yu82 (not (primCmpChar yu81 (Char (Pos (Succ yu83))) == LT) && yu81 <= Char (Pos (Succ yu84))))\n",fontsize=16,color="burlywood",shape="box"];1829[label="yu81/Char yu810",fontsize=10,color="white",style="solid",shape="box"];810 -> 1829[label="",style="solid", color="burlywood", weight=9];
1829 -> 812[label="",style="solid", color="burlywood", weight=3];
811[label="span2Ys0 isDigit (Char yu760 : yu77) (span2Span1 isDigit yu77 isDigit (Char yu760) yu77 (not (primCmpChar (Char yu760) (Char (Pos (Succ yu78))) == LT) && Char yu760 <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];811 -> 813[label="",style="solid", color="black", weight=3];
812[label="span2Zs0 isDigit (Char yu810 : yu82) (span2Span1 isDigit yu82 isDigit (Char yu810) yu82 (not (primCmpChar (Char yu810) (Char (Pos (Succ yu83))) == LT) && Char yu810 <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];812 -> 814[label="",style="solid", color="black", weight=3];
813[label="span2Ys0 isDigit (Char yu760 : yu77) (span2Span1 isDigit yu77 isDigit (Char yu760) yu77 (not (primCmpInt yu760 (Pos (Succ yu78)) == LT) && Char yu760 <= Char (Pos (Succ yu79))))\n",fontsize=16,color="burlywood",shape="box"];1830[label="yu760/Pos yu7600",fontsize=10,color="white",style="solid",shape="box"];813 -> 1830[label="",style="solid", color="burlywood", weight=9];
1830 -> 815[label="",style="solid", color="burlywood", weight=3];
1831[label="yu760/Neg yu7600",fontsize=10,color="white",style="solid",shape="box"];813 -> 1831[label="",style="solid", color="burlywood", weight=9];
1831 -> 816[label="",style="solid", color="burlywood", weight=3];
814[label="span2Zs0 isDigit (Char yu810 : yu82) (span2Span1 isDigit yu82 isDigit (Char yu810) yu82 (not (primCmpInt yu810 (Pos (Succ yu83)) == LT) && Char yu810 <= Char (Pos (Succ yu84))))\n",fontsize=16,color="burlywood",shape="box"];1832[label="yu810/Pos yu8100",fontsize=10,color="white",style="solid",shape="box"];814 -> 1832[label="",style="solid", color="burlywood", weight=9];
1832 -> 817[label="",style="solid", color="burlywood", weight=3];
1833[label="yu810/Neg yu8100",fontsize=10,color="white",style="solid",shape="box"];814 -> 1833[label="",style="solid", color="burlywood", weight=9];
1833 -> 818[label="",style="solid", color="burlywood", weight=3];
815[label="span2Ys0 isDigit (Char (Pos yu7600) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Pos yu7600)) yu77 (not (primCmpInt (Pos yu7600) (Pos (Succ yu78)) == LT) && Char (Pos yu7600) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="burlywood",shape="box"];1834[label="yu7600/Succ yu76000",fontsize=10,color="white",style="solid",shape="box"];815 -> 1834[label="",style="solid", color="burlywood", weight=9];
1834 -> 819[label="",style="solid", color="burlywood", weight=3];
1835[label="yu7600/Zero",fontsize=10,color="white",style="solid",shape="box"];815 -> 1835[label="",style="solid", color="burlywood", weight=9];
1835 -> 820[label="",style="solid", color="burlywood", weight=3];
816[label="span2Ys0 isDigit (Char (Neg yu7600) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Neg yu7600)) yu77 (not (primCmpInt (Neg yu7600) (Pos (Succ yu78)) == LT) && Char (Neg yu7600) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="burlywood",shape="box"];1836[label="yu7600/Succ yu76000",fontsize=10,color="white",style="solid",shape="box"];816 -> 1836[label="",style="solid", color="burlywood", weight=9];
1836 -> 821[label="",style="solid", color="burlywood", weight=3];
1837[label="yu7600/Zero",fontsize=10,color="white",style="solid",shape="box"];816 -> 1837[label="",style="solid", color="burlywood", weight=9];
1837 -> 822[label="",style="solid", color="burlywood", weight=3];
817[label="span2Zs0 isDigit (Char (Pos yu8100) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Pos yu8100)) yu82 (not (primCmpInt (Pos yu8100) (Pos (Succ yu83)) == LT) && Char (Pos yu8100) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="burlywood",shape="box"];1838[label="yu8100/Succ yu81000",fontsize=10,color="white",style="solid",shape="box"];817 -> 1838[label="",style="solid", color="burlywood", weight=9];
1838 -> 823[label="",style="solid", color="burlywood", weight=3];
1839[label="yu8100/Zero",fontsize=10,color="white",style="solid",shape="box"];817 -> 1839[label="",style="solid", color="burlywood", weight=9];
1839 -> 824[label="",style="solid", color="burlywood", weight=3];
818[label="span2Zs0 isDigit (Char (Neg yu8100) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Neg yu8100)) yu82 (not (primCmpInt (Neg yu8100) (Pos (Succ yu83)) == LT) && Char (Neg yu8100) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="burlywood",shape="box"];1840[label="yu8100/Succ yu81000",fontsize=10,color="white",style="solid",shape="box"];818 -> 1840[label="",style="solid", color="burlywood", weight=9];
1840 -> 825[label="",style="solid", color="burlywood", weight=3];
1841[label="yu8100/Zero",fontsize=10,color="white",style="solid",shape="box"];818 -> 1841[label="",style="solid", color="burlywood", weight=9];
1841 -> 826[label="",style="solid", color="burlywood", weight=3];
819[label="span2Ys0 isDigit (Char (Pos (Succ yu76000)) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Pos (Succ yu76000))) yu77 (not (primCmpInt (Pos (Succ yu76000)) (Pos (Succ yu78)) == LT) && Char (Pos (Succ yu76000)) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];819 -> 827[label="",style="solid", color="black", weight=3];
820[label="span2Ys0 isDigit (Char (Pos Zero) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Pos Zero)) yu77 (not (primCmpInt (Pos Zero) (Pos (Succ yu78)) == LT) && Char (Pos Zero) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];820 -> 828[label="",style="solid", color="black", weight=3];
821[label="span2Ys0 isDigit (Char (Neg (Succ yu76000)) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Neg (Succ yu76000))) yu77 (not (primCmpInt (Neg (Succ yu76000)) (Pos (Succ yu78)) == LT) && Char (Neg (Succ yu76000)) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];821 -> 829[label="",style="solid", color="black", weight=3];
822[label="span2Ys0 isDigit (Char (Neg Zero) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Neg Zero)) yu77 (not (primCmpInt (Neg Zero) (Pos (Succ yu78)) == LT) && Char (Neg Zero) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];822 -> 830[label="",style="solid", color="black", weight=3];
823[label="span2Zs0 isDigit (Char (Pos (Succ yu81000)) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Pos (Succ yu81000))) yu82 (not (primCmpInt (Pos (Succ yu81000)) (Pos (Succ yu83)) == LT) && Char (Pos (Succ yu81000)) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];823 -> 831[label="",style="solid", color="black", weight=3];
824[label="span2Zs0 isDigit (Char (Pos Zero) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Pos Zero)) yu82 (not (primCmpInt (Pos Zero) (Pos (Succ yu83)) == LT) && Char (Pos Zero) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];824 -> 832[label="",style="solid", color="black", weight=3];
825[label="span2Zs0 isDigit (Char (Neg (Succ yu81000)) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Neg (Succ yu81000))) yu82 (not (primCmpInt (Neg (Succ yu81000)) (Pos (Succ yu83)) == LT) && Char (Neg (Succ yu81000)) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];825 -> 833[label="",style="solid", color="black", weight=3];
826[label="span2Zs0 isDigit (Char (Neg Zero) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Neg Zero)) yu82 (not (primCmpInt (Neg Zero) (Pos (Succ yu83)) == LT) && Char (Neg Zero) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];826 -> 834[label="",style="solid", color="black", weight=3];
827 -> 1107[label="",style="dashed", color="red", weight=0];
827[label="span2Ys0 isDigit (Char (Pos (Succ yu76000)) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Pos (Succ yu76000))) yu77 (not (primCmpNat (Succ yu76000) (Succ yu78) == LT) && Char (Pos (Succ yu76000)) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="magenta"];827 -> 1108[label="",style="dashed", color="magenta", weight=3];
827 -> 1109[label="",style="dashed", color="magenta", weight=3];
827 -> 1110[label="",style="dashed", color="magenta", weight=3];
827 -> 1111[label="",style="dashed", color="magenta", weight=3];
827 -> 1112[label="",style="dashed", color="magenta", weight=3];
828[label="span2Ys0 isDigit (Char (Pos Zero) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Pos Zero)) yu77 (not (primCmpNat Zero (Succ yu78) == LT) && Char (Pos Zero) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];828 -> 836[label="",style="solid", color="black", weight=3];
829[label="span2Ys0 isDigit (Char (Neg (Succ yu76000)) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Neg (Succ yu76000))) yu77 (not (LT == LT) && Char (Neg (Succ yu76000)) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];829 -> 837[label="",style="solid", color="black", weight=3];
830[label="span2Ys0 isDigit (Char (Neg Zero) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Neg Zero)) yu77 (not (LT == LT) && Char (Neg Zero) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];830 -> 838[label="",style="solid", color="black", weight=3];
831 -> 1282[label="",style="dashed", color="red", weight=0];
831[label="span2Zs0 isDigit (Char (Pos (Succ yu81000)) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Pos (Succ yu81000))) yu82 (not (primCmpNat (Succ yu81000) (Succ yu83) == LT) && Char (Pos (Succ yu81000)) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="magenta"];831 -> 1283[label="",style="dashed", color="magenta", weight=3];
831 -> 1284[label="",style="dashed", color="magenta", weight=3];
831 -> 1285[label="",style="dashed", color="magenta", weight=3];
831 -> 1286[label="",style="dashed", color="magenta", weight=3];
831 -> 1287[label="",style="dashed", color="magenta", weight=3];
832[label="span2Zs0 isDigit (Char (Pos Zero) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Pos Zero)) yu82 (not (primCmpNat Zero (Succ yu83) == LT) && Char (Pos Zero) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];832 -> 840[label="",style="solid", color="black", weight=3];
833[label="span2Zs0 isDigit (Char (Neg (Succ yu81000)) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Neg (Succ yu81000))) yu82 (not (LT == LT) && Char (Neg (Succ yu81000)) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];833 -> 841[label="",style="solid", color="black", weight=3];
834[label="span2Zs0 isDigit (Char (Neg Zero) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Neg Zero)) yu82 (not (LT == LT) && Char (Neg Zero) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];834 -> 842[label="",style="solid", color="black", weight=3];
1108[label="yu76000\n",fontsize=16,color="green",shape="box"];1109[label="Succ yu78\n",fontsize=16,color="green",shape="box"];1110[label="yu77\n",fontsize=16,color="green",shape="box"];1111[label="Succ yu76000\n",fontsize=16,color="green",shape="box"];1112[label="yu79\n",fontsize=16,color="green",shape="box"];1107[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not (primCmpNat yu88 yu89 == LT) && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="burlywood",shape="triangle"];1844[label="yu88/Succ yu880",fontsize=10,color="white",style="solid",shape="box"];1107 -> 1844[label="",style="solid", color="burlywood", weight=9];
1844 -> 1143[label="",style="solid", color="burlywood", weight=3];
1845[label="yu88/Zero",fontsize=10,color="white",style="solid",shape="box"];1107 -> 1845[label="",style="solid", color="burlywood", weight=9];
1845 -> 1144[label="",style="solid", color="burlywood", weight=3];
836[label="span2Ys0 isDigit (Char (Pos Zero) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Pos Zero)) yu77 (not (LT == LT) && Char (Pos Zero) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];836 -> 845[label="",style="solid", color="black", weight=3];
837[label="span2Ys0 isDigit (Char (Neg (Succ yu76000)) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Neg (Succ yu76000))) yu77 (not True && Char (Neg (Succ yu76000)) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];837 -> 846[label="",style="solid", color="black", weight=3];
838[label="span2Ys0 isDigit (Char (Neg Zero) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Neg Zero)) yu77 (not True && Char (Neg Zero) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];838 -> 847[label="",style="solid", color="black", weight=3];
1283[label="yu81000\n",fontsize=16,color="green",shape="box"];1284[label="Succ yu83\n",fontsize=16,color="green",shape="box"];1285[label="yu82\n",fontsize=16,color="green",shape="box"];1286[label="yu84\n",fontsize=16,color="green",shape="box"];1287[label="Succ yu81000\n",fontsize=16,color="green",shape="box"];1282[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not (primCmpNat yu106 yu107 == LT) && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="burlywood",shape="triangle"];1846[label="yu106/Succ yu1060",fontsize=10,color="white",style="solid",shape="box"];1282 -> 1846[label="",style="solid", color="burlywood", weight=9];
1846 -> 1328[label="",style="solid", color="burlywood", weight=3];
1847[label="yu106/Zero",fontsize=10,color="white",style="solid",shape="box"];1282 -> 1847[label="",style="solid", color="burlywood", weight=9];
1847 -> 1329[label="",style="solid", color="burlywood", weight=3];
840[label="span2Zs0 isDigit (Char (Pos Zero) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Pos Zero)) yu82 (not (LT == LT) && Char (Pos Zero) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];840 -> 850[label="",style="solid", color="black", weight=3];
841[label="span2Zs0 isDigit (Char (Neg (Succ yu81000)) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Neg (Succ yu81000))) yu82 (not True && Char (Neg (Succ yu81000)) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];841 -> 851[label="",style="solid", color="black", weight=3];
842[label="span2Zs0 isDigit (Char (Neg Zero) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Neg Zero)) yu82 (not True && Char (Neg Zero) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];842 -> 852[label="",style="solid", color="black", weight=3];
1143[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not (primCmpNat (Succ yu880) yu89 == LT) && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="burlywood",shape="box"];1848[label="yu89/Succ yu890",fontsize=10,color="white",style="solid",shape="box"];1143 -> 1848[label="",style="solid", color="burlywood", weight=9];
1848 -> 1164[label="",style="solid", color="burlywood", weight=3];
1849[label="yu89/Zero",fontsize=10,color="white",style="solid",shape="box"];1143 -> 1849[label="",style="solid", color="burlywood", weight=9];
1849 -> 1165[label="",style="solid", color="burlywood", weight=3];
1144[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not (primCmpNat Zero yu89 == LT) && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="burlywood",shape="box"];1850[label="yu89/Succ yu890",fontsize=10,color="white",style="solid",shape="box"];1144 -> 1850[label="",style="solid", color="burlywood", weight=9];
1850 -> 1166[label="",style="solid", color="burlywood", weight=3];
1851[label="yu89/Zero",fontsize=10,color="white",style="solid",shape="box"];1144 -> 1851[label="",style="solid", color="burlywood", weight=9];
1851 -> 1167[label="",style="solid", color="burlywood", weight=3];
845[label="span2Ys0 isDigit (Char (Pos Zero) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Pos Zero)) yu77 (not True && Char (Pos Zero) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];845 -> 857[label="",style="solid", color="black", weight=3];
846[label="span2Ys0 isDigit (Char (Neg (Succ yu76000)) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Neg (Succ yu76000))) yu77 (False && Char (Neg (Succ yu76000)) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];846 -> 858[label="",style="solid", color="black", weight=3];
847[label="span2Ys0 isDigit (Char (Neg Zero) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Neg Zero)) yu77 (False && Char (Neg Zero) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];847 -> 859[label="",style="solid", color="black", weight=3];
1328[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not (primCmpNat (Succ yu1060) yu107 == LT) && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="burlywood",shape="box"];1852[label="yu107/Succ yu1070",fontsize=10,color="white",style="solid",shape="box"];1328 -> 1852[label="",style="solid", color="burlywood", weight=9];
1852 -> 1332[label="",style="solid", color="burlywood", weight=3];
1853[label="yu107/Zero",fontsize=10,color="white",style="solid",shape="box"];1328 -> 1853[label="",style="solid", color="burlywood", weight=9];
1853 -> 1333[label="",style="solid", color="burlywood", weight=3];
1329[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not (primCmpNat Zero yu107 == LT) && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="burlywood",shape="box"];1854[label="yu107/Succ yu1070",fontsize=10,color="white",style="solid",shape="box"];1329 -> 1854[label="",style="solid", color="burlywood", weight=9];
1854 -> 1334[label="",style="solid", color="burlywood", weight=3];
1855[label="yu107/Zero",fontsize=10,color="white",style="solid",shape="box"];1329 -> 1855[label="",style="solid", color="burlywood", weight=9];
1855 -> 1335[label="",style="solid", color="burlywood", weight=3];
850[label="span2Zs0 isDigit (Char (Pos Zero) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Pos Zero)) yu82 (not True && Char (Pos Zero) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];850 -> 864[label="",style="solid", color="black", weight=3];
851[label="span2Zs0 isDigit (Char (Neg (Succ yu81000)) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Neg (Succ yu81000))) yu82 (False && Char (Neg (Succ yu81000)) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];851 -> 865[label="",style="solid", color="black", weight=3];
852[label="span2Zs0 isDigit (Char (Neg Zero) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Neg Zero)) yu82 (False && Char (Neg Zero) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];852 -> 866[label="",style="solid", color="black", weight=3];
1164[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not (primCmpNat (Succ yu880) (Succ yu890) == LT) && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="black",shape="box"];1164 -> 1180[label="",style="solid", color="black", weight=3];
1165[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not (primCmpNat (Succ yu880) Zero == LT) && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="black",shape="box"];1165 -> 1181[label="",style="solid", color="black", weight=3];
1166[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not (primCmpNat Zero (Succ yu890) == LT) && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="black",shape="box"];1166 -> 1182[label="",style="solid", color="black", weight=3];
1167[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not (primCmpNat Zero Zero == LT) && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="black",shape="box"];1167 -> 1183[label="",style="solid", color="black", weight=3];
857[label="span2Ys0 isDigit (Char (Pos Zero) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Pos Zero)) yu77 (False && Char (Pos Zero) <= Char (Pos (Succ yu79))))\n",fontsize=16,color="black",shape="box"];857 -> 871[label="",style="solid", color="black", weight=3];
858[label="span2Ys0 isDigit (Char (Neg (Succ yu76000)) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Neg (Succ yu76000))) yu77 False)\n",fontsize=16,color="black",shape="box"];858 -> 872[label="",style="solid", color="black", weight=3];
859[label="span2Ys0 isDigit (Char (Neg Zero) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Neg Zero)) yu77 False)\n",fontsize=16,color="black",shape="box"];859 -> 873[label="",style="solid", color="black", weight=3];
1332[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not (primCmpNat (Succ yu1060) (Succ yu1070) == LT) && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="black",shape="box"];1332 -> 1337[label="",style="solid", color="black", weight=3];
1333[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not (primCmpNat (Succ yu1060) Zero == LT) && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="black",shape="box"];1333 -> 1338[label="",style="solid", color="black", weight=3];
1334[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not (primCmpNat Zero (Succ yu1070) == LT) && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="black",shape="box"];1334 -> 1339[label="",style="solid", color="black", weight=3];
1335[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not (primCmpNat Zero Zero == LT) && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="black",shape="box"];1335 -> 1340[label="",style="solid", color="black", weight=3];
864[label="span2Zs0 isDigit (Char (Pos Zero) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Pos Zero)) yu82 (False && Char (Pos Zero) <= Char (Pos (Succ yu84))))\n",fontsize=16,color="black",shape="box"];864 -> 878[label="",style="solid", color="black", weight=3];
865[label="span2Zs0 isDigit (Char (Neg (Succ yu81000)) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Neg (Succ yu81000))) yu82 False)\n",fontsize=16,color="black",shape="box"];865 -> 879[label="",style="solid", color="black", weight=3];
866[label="span2Zs0 isDigit (Char (Neg Zero) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Neg Zero)) yu82 False)\n",fontsize=16,color="black",shape="box"];866 -> 880[label="",style="solid", color="black", weight=3];
1180 -> 1107[label="",style="dashed", color="red", weight=0];
1180[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not (primCmpNat yu880 yu890 == LT) && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="magenta"];1180 -> 1196[label="",style="dashed", color="magenta", weight=3];
1180 -> 1197[label="",style="dashed", color="magenta", weight=3];
1181[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not (GT == LT) && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="black",shape="box"];1181 -> 1198[label="",style="solid", color="black", weight=3];
1182[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not (LT == LT) && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="black",shape="box"];1182 -> 1199[label="",style="solid", color="black", weight=3];
1183[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not (EQ == LT) && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="black",shape="box"];1183 -> 1200[label="",style="solid", color="black", weight=3];
871[label="span2Ys0 isDigit (Char (Pos Zero) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Pos Zero)) yu77 False)\n",fontsize=16,color="black",shape="box"];871 -> 886[label="",style="solid", color="black", weight=3];
872[label="span2Ys0 isDigit (Char (Neg (Succ yu76000)) : yu77) (span2Span0 isDigit yu77 isDigit (Char (Neg (Succ yu76000))) yu77 otherwise)\n",fontsize=16,color="black",shape="box"];872 -> 887[label="",style="solid", color="black", weight=3];
873[label="span2Ys0 isDigit (Char (Neg Zero) : yu77) (span2Span0 isDigit yu77 isDigit (Char (Neg Zero)) yu77 otherwise)\n",fontsize=16,color="black",shape="box"];873 -> 888[label="",style="solid", color="black", weight=3];
1337 -> 1282[label="",style="dashed", color="red", weight=0];
1337[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not (primCmpNat yu1060 yu1070 == LT) && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="magenta"];1337 -> 1342[label="",style="dashed", color="magenta", weight=3];
1337 -> 1343[label="",style="dashed", color="magenta", weight=3];
1338[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not (GT == LT) && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="black",shape="box"];1338 -> 1344[label="",style="solid", color="black", weight=3];
1339[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not (LT == LT) && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="black",shape="box"];1339 -> 1345[label="",style="solid", color="black", weight=3];
1340[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not (EQ == LT) && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="black",shape="box"];1340 -> 1346[label="",style="solid", color="black", weight=3];
878[label="span2Zs0 isDigit (Char (Pos Zero) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Pos Zero)) yu82 False)\n",fontsize=16,color="black",shape="box"];878 -> 894[label="",style="solid", color="black", weight=3];
879[label="span2Zs0 isDigit (Char (Neg (Succ yu81000)) : yu82) (span2Span0 isDigit yu82 isDigit (Char (Neg (Succ yu81000))) yu82 otherwise)\n",fontsize=16,color="black",shape="box"];879 -> 895[label="",style="solid", color="black", weight=3];
880[label="span2Zs0 isDigit (Char (Neg Zero) : yu82) (span2Span0 isDigit yu82 isDigit (Char (Neg Zero)) yu82 otherwise)\n",fontsize=16,color="black",shape="box"];880 -> 896[label="",style="solid", color="black", weight=3];
1196[label="yu890\n",fontsize=16,color="green",shape="box"];1197[label="yu880\n",fontsize=16,color="green",shape="box"];1198[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not False && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="black",shape="triangle"];1198 -> 1211[label="",style="solid", color="black", weight=3];
1199[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not True && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="black",shape="box"];1199 -> 1212[label="",style="solid", color="black", weight=3];
1200 -> 1198[label="",style="dashed", color="red", weight=0];
1200[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not False && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="magenta"];886[label="span2Ys0 isDigit (Char (Pos Zero) : yu77) (span2Span0 isDigit yu77 isDigit (Char (Pos Zero)) yu77 otherwise)\n",fontsize=16,color="black",shape="box"];886 -> 904[label="",style="solid", color="black", weight=3];
887[label="span2Ys0 isDigit (Char (Neg (Succ yu76000)) : yu77) (span2Span0 isDigit yu77 isDigit (Char (Neg (Succ yu76000))) yu77 True)\n",fontsize=16,color="black",shape="box"];887 -> 905[label="",style="solid", color="black", weight=3];
888[label="span2Ys0 isDigit (Char (Neg Zero) : yu77) (span2Span0 isDigit yu77 isDigit (Char (Neg Zero)) yu77 True)\n",fontsize=16,color="black",shape="box"];888 -> 906[label="",style="solid", color="black", weight=3];
1342[label="yu1070\n",fontsize=16,color="green",shape="box"];1343[label="yu1060\n",fontsize=16,color="green",shape="box"];1344[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not False && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="black",shape="triangle"];1344 -> 1349[label="",style="solid", color="black", weight=3];
1345[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not True && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="black",shape="box"];1345 -> 1350[label="",style="solid", color="black", weight=3];
1346 -> 1344[label="",style="dashed", color="red", weight=0];
1346[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not False && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="magenta"];894[label="span2Zs0 isDigit (Char (Pos Zero) : yu82) (span2Span0 isDigit yu82 isDigit (Char (Pos Zero)) yu82 otherwise)\n",fontsize=16,color="black",shape="box"];894 -> 914[label="",style="solid", color="black", weight=3];
895[label="span2Zs0 isDigit (Char (Neg (Succ yu81000)) : yu82) (span2Span0 isDigit yu82 isDigit (Char (Neg (Succ yu81000))) yu82 True)\n",fontsize=16,color="black",shape="box"];895 -> 915[label="",style="solid", color="black", weight=3];
896[label="span2Zs0 isDigit (Char (Neg Zero) : yu82) (span2Span0 isDigit yu82 isDigit (Char (Neg Zero)) yu82 True)\n",fontsize=16,color="black",shape="box"];896 -> 916[label="",style="solid", color="black", weight=3];
1211[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (True && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="black",shape="box"];1211 -> 1240[label="",style="solid", color="black", weight=3];
1212[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (False && Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="black",shape="box"];1212 -> 1241[label="",style="solid", color="black", weight=3];
904[label="span2Ys0 isDigit (Char (Pos Zero) : yu77) (span2Span0 isDigit yu77 isDigit (Char (Pos Zero)) yu77 True)\n",fontsize=16,color="black",shape="box"];904 -> 924[label="",style="solid", color="black", weight=3];
905[label="span2Ys0 isDigit (Char (Neg (Succ yu76000)) : yu77) ([],Char (Neg (Succ yu76000)) : yu77)\n",fontsize=16,color="black",shape="box"];905 -> 925[label="",style="solid", color="black", weight=3];
906[label="span2Ys0 isDigit (Char (Neg Zero) : yu77) ([],Char (Neg Zero) : yu77)\n",fontsize=16,color="black",shape="box"];906 -> 926[label="",style="solid", color="black", weight=3];
1349[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (True && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="black",shape="box"];1349 -> 1355[label="",style="solid", color="black", weight=3];
1350[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (False && Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="black",shape="box"];1350 -> 1356[label="",style="solid", color="black", weight=3];
914[label="span2Zs0 isDigit (Char (Pos Zero) : yu82) (span2Span0 isDigit yu82 isDigit (Char (Pos Zero)) yu82 True)\n",fontsize=16,color="black",shape="box"];914 -> 934[label="",style="solid", color="black", weight=3];
915[label="span2Zs0 isDigit (Char (Neg (Succ yu81000)) : yu82) ([],Char (Neg (Succ yu81000)) : yu82)\n",fontsize=16,color="black",shape="box"];915 -> 935[label="",style="solid", color="black", weight=3];
916[label="span2Zs0 isDigit (Char (Neg Zero) : yu82) ([],Char (Neg Zero) : yu82)\n",fontsize=16,color="black",shape="box"];916 -> 936[label="",style="solid", color="black", weight=3];
1240[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (Char (Pos (Succ yu86)) <= Char (Pos (Succ yu90))))\n",fontsize=16,color="black",shape="box"];1240 -> 1254[label="",style="solid", color="black", weight=3];
1241[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 False)\n",fontsize=16,color="black",shape="triangle"];1241 -> 1255[label="",style="solid", color="black", weight=3];
924[label="span2Ys0 isDigit (Char (Pos Zero) : yu77) ([],Char (Pos Zero) : yu77)\n",fontsize=16,color="black",shape="box"];924 -> 945[label="",style="solid", color="black", weight=3];
925[label="[]\n",fontsize=16,color="green",shape="box"];926[label="[]\n",fontsize=16,color="green",shape="box"];1355[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (Char (Pos (Succ yu104)) <= Char (Pos (Succ yu108))))\n",fontsize=16,color="black",shape="box"];1355 -> 1361[label="",style="solid", color="black", weight=3];
1356[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 False)\n",fontsize=16,color="black",shape="triangle"];1356 -> 1362[label="",style="solid", color="black", weight=3];
934[label="span2Zs0 isDigit (Char (Pos Zero) : yu82) ([],Char (Pos Zero) : yu82)\n",fontsize=16,color="black",shape="box"];934 -> 954[label="",style="solid", color="black", weight=3];
935[label="Char (Neg (Succ yu81000)) : yu82\n",fontsize=16,color="green",shape="box"];936[label="Char (Neg Zero) : yu82\n",fontsize=16,color="green",shape="box"];1254[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (compare (Char (Pos (Succ yu86))) (Char (Pos (Succ yu90))) /= GT))\n",fontsize=16,color="black",shape="box"];1254 -> 1268[label="",style="solid", color="black", weight=3];
1255[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span0 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 otherwise)\n",fontsize=16,color="black",shape="box"];1255 -> 1269[label="",style="solid", color="black", weight=3];
945[label="[]\n",fontsize=16,color="green",shape="box"];1361[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (compare (Char (Pos (Succ yu104))) (Char (Pos (Succ yu108))) /= GT))\n",fontsize=16,color="black",shape="box"];1361 -> 1368[label="",style="solid", color="black", weight=3];
1362[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span0 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 otherwise)\n",fontsize=16,color="black",shape="box"];1362 -> 1369[label="",style="solid", color="black", weight=3];
954[label="Char (Pos Zero) : yu82\n",fontsize=16,color="green",shape="box"];1268[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not (compare (Char (Pos (Succ yu86))) (Char (Pos (Succ yu90))) == GT)))\n",fontsize=16,color="black",shape="box"];1268 -> 1280[label="",style="solid", color="black", weight=3];
1269[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span0 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 True)\n",fontsize=16,color="black",shape="box"];1269 -> 1281[label="",style="solid", color="black", weight=3];
1368[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not (compare (Char (Pos (Succ yu104))) (Char (Pos (Succ yu108))) == GT)))\n",fontsize=16,color="black",shape="box"];1368 -> 1376[label="",style="solid", color="black", weight=3];
1369[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span0 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 True)\n",fontsize=16,color="black",shape="box"];1369 -> 1377[label="",style="solid", color="black", weight=3];
1280[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not (primCmpChar (Char (Pos (Succ yu86))) (Char (Pos (Succ yu90))) == GT)))\n",fontsize=16,color="black",shape="box"];1280 -> 1330[label="",style="solid", color="black", weight=3];
1281[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) ([],Char (Pos (Succ yu86)) : yu87)\n",fontsize=16,color="black",shape="box"];1281 -> 1331[label="",style="solid", color="black", weight=3];
1376[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not (primCmpChar (Char (Pos (Succ yu104))) (Char (Pos (Succ yu108))) == GT)))\n",fontsize=16,color="black",shape="box"];1376 -> 1384[label="",style="solid", color="black", weight=3];
1377[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) ([],Char (Pos (Succ yu104)) : yu105)\n",fontsize=16,color="black",shape="box"];1377 -> 1385[label="",style="solid", color="black", weight=3];
1330[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not (primCmpInt (Pos (Succ yu86)) (Pos (Succ yu90)) == GT)))\n",fontsize=16,color="black",shape="box"];1330 -> 1336[label="",style="solid", color="black", weight=3];
1331[label="[]\n",fontsize=16,color="green",shape="box"];1384[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not (primCmpInt (Pos (Succ yu104)) (Pos (Succ yu108)) == GT)))\n",fontsize=16,color="black",shape="box"];1384 -> 1394[label="",style="solid", color="black", weight=3];
1385[label="Char (Pos (Succ yu104)) : yu105\n",fontsize=16,color="green",shape="box"];1336 -> 1709[label="",style="dashed", color="red", weight=0];
1336[label="span2Ys0 isDigit (Char (Pos (Succ yu86)) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Pos (Succ yu86))) yu87 (not (primCmpNat (Succ yu86) (Succ yu90) == GT)))\n",fontsize=16,color="magenta"];1336 -> 1710[label="",style="dashed", color="magenta", weight=3];
1336 -> 1711[label="",style="dashed", color="magenta", weight=3];
1336 -> 1712[label="",style="dashed", color="magenta", weight=3];
1336 -> 1713[label="",style="dashed", color="magenta", weight=3];
1394 -> 1650[label="",style="dashed", color="red", weight=0];
1394[label="span2Zs0 isDigit (Char (Pos (Succ yu104)) : yu105) (span2Span1 isDigit yu105 isDigit (Char (Pos (Succ yu104))) yu105 (not (primCmpNat (Succ yu104) (Succ yu108) == GT)))\n",fontsize=16,color="magenta"];1394 -> 1651[label="",style="dashed", color="magenta", weight=3];
1394 -> 1652[label="",style="dashed", color="magenta", weight=3];
1394 -> 1653[label="",style="dashed", color="magenta", weight=3];
1394 -> 1654[label="",style="dashed", color="magenta", weight=3];
1710[label="Succ yu86\n",fontsize=16,color="green",shape="box"];1711[label="yu86\n",fontsize=16,color="green",shape="box"];1712[label="yu87\n",fontsize=16,color="green",shape="box"];1713[label="Succ yu90\n",fontsize=16,color="green",shape="box"];1709[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 (not (primCmpNat yu139 yu140 == GT)))\n",fontsize=16,color="burlywood",shape="triangle"];1862[label="yu139/Succ yu1390",fontsize=10,color="white",style="solid",shape="box"];1709 -> 1862[label="",style="solid", color="burlywood", weight=9];
1862 -> 1750[label="",style="solid", color="burlywood", weight=3];
1863[label="yu139/Zero",fontsize=10,color="white",style="solid",shape="box"];1709 -> 1863[label="",style="solid", color="burlywood", weight=9];
1863 -> 1751[label="",style="solid", color="burlywood", weight=3];
1651[label="Succ yu108\n",fontsize=16,color="green",shape="box"];1652[label="Succ yu104\n",fontsize=16,color="green",shape="box"];1653[label="yu104\n",fontsize=16,color="green",shape="box"];1654[label="yu105\n",fontsize=16,color="green",shape="box"];1650[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 (not (primCmpNat yu134 yu135 == GT)))\n",fontsize=16,color="burlywood",shape="triangle"];1864[label="yu134/Succ yu1340",fontsize=10,color="white",style="solid",shape="box"];1650 -> 1864[label="",style="solid", color="burlywood", weight=9];
1864 -> 1679[label="",style="solid", color="burlywood", weight=3];
1865[label="yu134/Zero",fontsize=10,color="white",style="solid",shape="box"];1650 -> 1865[label="",style="solid", color="burlywood", weight=9];
1865 -> 1680[label="",style="solid", color="burlywood", weight=3];
1750[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 (not (primCmpNat (Succ yu1390) yu140 == GT)))\n",fontsize=16,color="burlywood",shape="box"];1866[label="yu140/Succ yu1400",fontsize=10,color="white",style="solid",shape="box"];1750 -> 1866[label="",style="solid", color="burlywood", weight=9];
1866 -> 1754[label="",style="solid", color="burlywood", weight=3];
1867[label="yu140/Zero",fontsize=10,color="white",style="solid",shape="box"];1750 -> 1867[label="",style="solid", color="burlywood", weight=9];
1867 -> 1755[label="",style="solid", color="burlywood", weight=3];
1751[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 (not (primCmpNat Zero yu140 == GT)))\n",fontsize=16,color="burlywood",shape="box"];1868[label="yu140/Succ yu1400",fontsize=10,color="white",style="solid",shape="box"];1751 -> 1868[label="",style="solid", color="burlywood", weight=9];
1868 -> 1756[label="",style="solid", color="burlywood", weight=3];
1869[label="yu140/Zero",fontsize=10,color="white",style="solid",shape="box"];1751 -> 1869[label="",style="solid", color="burlywood", weight=9];
1869 -> 1757[label="",style="solid", color="burlywood", weight=3];
1679[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 (not (primCmpNat (Succ yu1340) yu135 == GT)))\n",fontsize=16,color="burlywood",shape="box"];1870[label="yu135/Succ yu1350",fontsize=10,color="white",style="solid",shape="box"];1679 -> 1870[label="",style="solid", color="burlywood", weight=9];
1870 -> 1688[label="",style="solid", color="burlywood", weight=3];
1871[label="yu135/Zero",fontsize=10,color="white",style="solid",shape="box"];1679 -> 1871[label="",style="solid", color="burlywood", weight=9];
1871 -> 1689[label="",style="solid", color="burlywood", weight=3];
1680[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 (not (primCmpNat Zero yu135 == GT)))\n",fontsize=16,color="burlywood",shape="box"];1872[label="yu135/Succ yu1350",fontsize=10,color="white",style="solid",shape="box"];1680 -> 1872[label="",style="solid", color="burlywood", weight=9];
1872 -> 1690[label="",style="solid", color="burlywood", weight=3];
1873[label="yu135/Zero",fontsize=10,color="white",style="solid",shape="box"];1680 -> 1873[label="",style="solid", color="burlywood", weight=9];
1873 -> 1691[label="",style="solid", color="burlywood", weight=3];
1754[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 (not (primCmpNat (Succ yu1390) (Succ yu1400) == GT)))\n",fontsize=16,color="black",shape="box"];1754 -> 1761[label="",style="solid", color="black", weight=3];
1755[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 (not (primCmpNat (Succ yu1390) Zero == GT)))\n",fontsize=16,color="black",shape="box"];1755 -> 1762[label="",style="solid", color="black", weight=3];
1756[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 (not (primCmpNat Zero (Succ yu1400) == GT)))\n",fontsize=16,color="black",shape="box"];1756 -> 1763[label="",style="solid", color="black", weight=3];
1757[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 (not (primCmpNat Zero Zero == GT)))\n",fontsize=16,color="black",shape="box"];1757 -> 1764[label="",style="solid", color="black", weight=3];
1688[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 (not (primCmpNat (Succ yu1340) (Succ yu1350) == GT)))\n",fontsize=16,color="black",shape="box"];1688 -> 1696[label="",style="solid", color="black", weight=3];
1689[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 (not (primCmpNat (Succ yu1340) Zero == GT)))\n",fontsize=16,color="black",shape="box"];1689 -> 1697[label="",style="solid", color="black", weight=3];
1690[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 (not (primCmpNat Zero (Succ yu1350) == GT)))\n",fontsize=16,color="black",shape="box"];1690 -> 1698[label="",style="solid", color="black", weight=3];
1691[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 (not (primCmpNat Zero Zero == GT)))\n",fontsize=16,color="black",shape="box"];1691 -> 1699[label="",style="solid", color="black", weight=3];
1761 -> 1709[label="",style="dashed", color="red", weight=0];
1761[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 (not (primCmpNat yu1390 yu1400 == GT)))\n",fontsize=16,color="magenta"];1761 -> 1768[label="",style="dashed", color="magenta", weight=3];
1761 -> 1769[label="",style="dashed", color="magenta", weight=3];
1762[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 (not (GT == GT)))\n",fontsize=16,color="black",shape="box"];1762 -> 1770[label="",style="solid", color="black", weight=3];
1763[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 (not (LT == GT)))\n",fontsize=16,color="black",shape="box"];1763 -> 1771[label="",style="solid", color="black", weight=3];
1764[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 (not (EQ == GT)))\n",fontsize=16,color="black",shape="box"];1764 -> 1772[label="",style="solid", color="black", weight=3];
1696 -> 1650[label="",style="dashed", color="red", weight=0];
1696[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 (not (primCmpNat yu1340 yu1350 == GT)))\n",fontsize=16,color="magenta"];1696 -> 1704[label="",style="dashed", color="magenta", weight=3];
1696 -> 1705[label="",style="dashed", color="magenta", weight=3];
1697[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 (not (GT == GT)))\n",fontsize=16,color="black",shape="box"];1697 -> 1706[label="",style="solid", color="black", weight=3];
1698[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 (not (LT == GT)))\n",fontsize=16,color="black",shape="box"];1698 -> 1707[label="",style="solid", color="black", weight=3];
1699[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 (not (EQ == GT)))\n",fontsize=16,color="black",shape="box"];1699 -> 1708[label="",style="solid", color="black", weight=3];
1768[label="yu1390\n",fontsize=16,color="green",shape="box"];1769[label="yu1400\n",fontsize=16,color="green",shape="box"];1770[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 (not True))\n",fontsize=16,color="black",shape="box"];1770 -> 1776[label="",style="solid", color="black", weight=3];
1771[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 (not False))\n",fontsize=16,color="black",shape="triangle"];1771 -> 1777[label="",style="solid", color="black", weight=3];
1772 -> 1771[label="",style="dashed", color="red", weight=0];
1772[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 (not False))\n",fontsize=16,color="magenta"];1704[label="yu1350\n",fontsize=16,color="green",shape="box"];1705[label="yu1340\n",fontsize=16,color="green",shape="box"];1706[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 (not True))\n",fontsize=16,color="black",shape="box"];1706 -> 1752[label="",style="solid", color="black", weight=3];
1707[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 (not False))\n",fontsize=16,color="black",shape="triangle"];1707 -> 1753[label="",style="solid", color="black", weight=3];
1708 -> 1707[label="",style="dashed", color="red", weight=0];
1708[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 (not False))\n",fontsize=16,color="magenta"];1776 -> 1241[label="",style="dashed", color="red", weight=0];
1776[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 False)\n",fontsize=16,color="magenta"];1776 -> 1778[label="",style="dashed", color="magenta", weight=3];
1776 -> 1779[label="",style="dashed", color="magenta", weight=3];
1777[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (span2Span1 isDigit yu138 isDigit (Char (Pos (Succ yu137))) yu138 True)\n",fontsize=16,color="black",shape="box"];1777 -> 1780[label="",style="solid", color="black", weight=3];
1752 -> 1356[label="",style="dashed", color="red", weight=0];
1752[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 False)\n",fontsize=16,color="magenta"];1752 -> 1758[label="",style="dashed", color="magenta", weight=3];
1752 -> 1759[label="",style="dashed", color="magenta", weight=3];
1753[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (span2Span1 isDigit yu133 isDigit (Char (Pos (Succ yu132))) yu133 True)\n",fontsize=16,color="black",shape="box"];1753 -> 1760[label="",style="solid", color="black", weight=3];
1778[label="yu137\n",fontsize=16,color="green",shape="box"];1779[label="yu138\n",fontsize=16,color="green",shape="box"];1780 -> 1781[label="",style="dashed", color="red", weight=0];
1780[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (Char (Pos (Succ yu137)) : span2Ys isDigit yu138,span2Zs isDigit yu138)\n",fontsize=16,color="magenta"];1780 -> 1782[label="",style="dashed", color="magenta", weight=3];
1780 -> 1783[label="",style="dashed", color="magenta", weight=3];
1758[label="yu132\n",fontsize=16,color="green",shape="box"];1759[label="yu133\n",fontsize=16,color="green",shape="box"];1760 -> 1765[label="",style="dashed", color="red", weight=0];
1760[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (Char (Pos (Succ yu132)) : span2Ys isDigit yu133,span2Zs isDigit yu133)\n",fontsize=16,color="magenta"];1760 -> 1766[label="",style="dashed", color="magenta", weight=3];
1760 -> 1767[label="",style="dashed", color="magenta", weight=3];
1782 -> 756[label="",style="dashed", color="red", weight=0];
1782[label="span2Zs isDigit yu138\n",fontsize=16,color="magenta"];1782 -> 1784[label="",style="dashed", color="magenta", weight=3];
1783 -> 755[label="",style="dashed", color="red", weight=0];
1783[label="span2Ys isDigit yu138\n",fontsize=16,color="magenta"];1783 -> 1785[label="",style="dashed", color="magenta", weight=3];
1781[label="span2Ys0 isDigit (Char (Pos (Succ yu137)) : yu138) (Char (Pos (Succ yu137)) : yu144,yu143)\n",fontsize=16,color="black",shape="triangle"];1781 -> 1786[label="",style="solid", color="black", weight=3];
1766 -> 756[label="",style="dashed", color="red", weight=0];
1766[label="span2Zs isDigit yu133\n",fontsize=16,color="magenta"];1766 -> 1773[label="",style="dashed", color="magenta", weight=3];
1767 -> 755[label="",style="dashed", color="red", weight=0];
1767[label="span2Ys isDigit yu133\n",fontsize=16,color="magenta"];1767 -> 1774[label="",style="dashed", color="magenta", weight=3];
1765[label="span2Zs0 isDigit (Char (Pos (Succ yu132)) : yu133) (Char (Pos (Succ yu132)) : yu142,yu141)\n",fontsize=16,color="black",shape="triangle"];1765 -> 1775[label="",style="solid", color="black", weight=3];
1784[label="yu138\n",fontsize=16,color="green",shape="box"];1785[label="yu138\n",fontsize=16,color="green",shape="box"];1786[label="Char (Pos (Succ yu137)) : yu144\n",fontsize=16,color="green",shape="box"];1773[label="yu133\n",fontsize=16,color="green",shape="box"];1774[label="yu133\n",fontsize=16,color="green",shape="box"];1775[label="yu141\n",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

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

new_span2Zs00(yu104, yu105, Succ(yu1060), Zero, yu108) → new_span2Zs01(yu104, yu105, Succ(yu104), Succ(yu108))
new_span2Ys00(yu86, yu87, Succ(yu880), Zero, yu90) → new_span2Ys01(yu86, yu87, Succ(yu86), Succ(yu90))
new_span2Zs01(yu132, yu133, Zero, Zero) → new_span2Zs03(yu132, yu133)
new_span2Ys03(yu137, yu138) → new_span2Zs(yu138)
new_span2Zs01(yu132, yu133, Succ(yu1340), Succ(yu1350)) → new_span2Zs01(yu132, yu133, yu1340, yu1350)
new_span2Ys01(yu137, yu138, Zero, Succ(yu1400)) → new_span2Zs(yu138)
new_span2Zs01(yu132, yu133, Zero, Succ(yu1350)) → new_span2Zs(yu133)
new_span2Zs01(yu132, yu133, Zero, Succ(yu1350)) → new_span2Ys(yu133)
new_span2Zs03(yu132, yu133) → new_span2Ys(yu133)
new_span2Ys01(yu137, yu138, Succ(yu1390), Succ(yu1400)) → new_span2Ys01(yu137, yu138, yu1390, yu1400)
new_span2Ys01(yu137, yu138, Zero, Zero) → new_span2Ys03(yu137, yu138)
new_span2Zs0(Char(Pos(Succ(yu81000))), yu82, yu83, yu84) → new_span2Zs00(yu81000, yu82, Succ(yu81000), Succ(yu83), yu84)
new_span2Ys(:(yu620, yu621)) → new_span2Ys0(yu620, yu621, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Ys00(yu86, yu87, Succ(yu880), Succ(yu890), yu90) → new_span2Ys00(yu86, yu87, yu880, yu890, yu90)
new_span2Zs(:(yu620, yu621)) → new_span2Zs0(yu620, yu621, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Ys03(yu137, yu138) → new_span2Ys(yu138)
new_span2Zs02(yu104, yu105, yu108) → new_span2Zs01(yu104, yu105, Succ(yu104), Succ(yu108))
new_span2Zs00(yu104, yu105, Zero, Zero, yu108) → new_span2Zs02(yu104, yu105, yu108)
new_span2Ys00(yu86, yu87, Zero, Zero, yu90) → new_span2Ys02(yu86, yu87, yu90)
new_span2Ys0(Char(Pos(Succ(yu76000))), yu77, yu78, yu79) → new_span2Ys00(yu76000, yu77, Succ(yu76000), Succ(yu78), yu79)
new_span2Ys01(yu137, yu138, Zero, Succ(yu1400)) → new_span2Ys(yu138)
new_span2Zs00(yu104, yu105, Succ(yu1060), Succ(yu1070), yu108) → new_span2Zs00(yu104, yu105, yu1060, yu1070, yu108)
new_span2Zs03(yu132, yu133) → new_span2Zs(yu133)
new_span2Ys02(yu86, yu87, yu90) → new_span2Ys01(yu86, yu87, Succ(yu86), Succ(yu90))

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_span2Zs01(yu132, yu133, Succ(yu1340), Succ(yu1350)) → new_span2Zs01(yu132, yu133, yu1340, yu1350)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4
new_span2Zs00(yu104, yu105, Succ(yu1060), Succ(yu1070), yu108) → new_span2Zs00(yu104, yu105, yu1060, yu1070, yu108)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4, 5 >= 5
new_span2Ys01(yu137, yu138, Succ(yu1390), Succ(yu1400)) → new_span2Ys01(yu137, yu138, yu1390, yu1400)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4
new_span2Ys00(yu86, yu87, Succ(yu880), Succ(yu890), yu90) → new_span2Ys00(yu86, yu87, yu880, yu890, yu90)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4, 5 >= 5
new_span2Zs(:(yu620, yu621)) → new_span2Zs0(yu620, yu621, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
The graph contains the following edges 1 > 1, 1 > 2
new_span2Ys01(yu137, yu138, Zero, Zero) → new_span2Ys03(yu137, yu138)
The graph contains the following edges 1 >= 1, 2 >= 2
new_span2Ys(:(yu620, yu621)) → new_span2Ys0(yu620, yu621, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
The graph contains the following edges 1 > 1, 1 > 2
new_span2Zs01(yu132, yu133, Zero, Zero) → new_span2Zs03(yu132, yu133)
The graph contains the following edges 1 >= 1, 2 >= 2
new_span2Zs03(yu132, yu133) → new_span2Ys(yu133)
The graph contains the following edges 2 >= 1
new_span2Zs03(yu132, yu133) → new_span2Zs(yu133)
The graph contains the following edges 2 >= 1
new_span2Zs01(yu132, yu133, Zero, Succ(yu1350)) → new_span2Ys(yu133)
The graph contains the following edges 2 >= 1
new_span2Zs01(yu132, yu133, Zero, Succ(yu1350)) → new_span2Zs(yu133)
The graph contains the following edges 2 >= 1
new_span2Ys01(yu137, yu138, Zero, Succ(yu1400)) → new_span2Ys(yu138)
The graph contains the following edges 2 >= 1
new_span2Ys01(yu137, yu138, Zero, Succ(yu1400)) → new_span2Zs(yu138)
The graph contains the following edges 2 >= 1
new_span2Ys03(yu137, yu138) → new_span2Ys(yu138)
The graph contains the following edges 2 >= 1
new_span2Ys03(yu137, yu138) → new_span2Zs(yu138)
The graph contains the following edges 2 >= 1
new_span2Ys0(Char(Pos(Succ(yu76000))), yu77, yu78, yu79) → new_span2Ys00(yu76000, yu77, Succ(yu76000), Succ(yu78), yu79)
The graph contains the following edges 1 > 1, 2 >= 2, 1 > 3, 4 >= 5
new_span2Ys00(yu86, yu87, Succ(yu880), Zero, yu90) → new_span2Ys01(yu86, yu87, Succ(yu86), Succ(yu90))
The graph contains the following edges 1 >= 1, 2 >= 2
new_span2Ys02(yu86, yu87, yu90) → new_span2Ys01(yu86, yu87, Succ(yu86), Succ(yu90))
The graph contains the following edges 1 >= 1, 2 >= 2
new_span2Ys00(yu86, yu87, Zero, Zero, yu90) → new_span2Ys02(yu86, yu87, yu90)
The graph contains the following edges 1 >= 1, 2 >= 2, 5 >= 3
new_span2Zs0(Char(Pos(Succ(yu81000))), yu82, yu83, yu84) → new_span2Zs00(yu81000, yu82, Succ(yu81000), Succ(yu83), yu84)
The graph contains the following edges 1 > 1, 2 >= 2, 1 > 3, 4 >= 5
new_span2Zs00(yu104, yu105, Zero, Zero, yu108) → new_span2Zs02(yu104, yu105, yu108)
The graph contains the following edges 1 >= 1, 2 >= 2, 5 >= 3
new_span2Zs02(yu104, yu105, yu108) → new_span2Zs01(yu104, yu105, Succ(yu104), Succ(yu108))
The graph contains the following edges 1 >= 1, 2 >= 2
new_span2Zs00(yu104, yu105, Succ(yu1060), Zero, yu108) → new_span2Zs01(yu104, yu105, Succ(yu104), Succ(yu108))
The graph contains the following edges 1 >= 1, 2 >= 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

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

new_psPs(yu62, yu63, Succ(yu640), Succ(yu650), yu66) → new_psPs(yu62, yu63, yu640, yu650, yu66)

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

new_psPs(yu62, yu63, Succ(yu640), Succ(yu650), yu66) → new_psPs(yu62, yu63, yu640, yu650, yu66)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4, 5 >= 5

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

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

new_psPs0(yu27, yu28, Succ(yu290), Succ(yu300), yu31, yu32) → new_psPs0(yu27, yu28, yu290, yu300, yu31, yu32)

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

new_psPs0(yu27, yu28, Succ(yu290), Succ(yu300), yu31, yu32) → new_psPs0(yu27, yu28, yu290, yu300, yu31, yu32)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4, 5 >= 5, 6 >= 6

span2Span1	xy xz p wv ww True	= (wv : span2Ys xy xz,span2Zs xy xz)
span2Span1	xy xz p wv ww False	= span2Span0 xy xz p wv ww otherwise