[Agda] slow file with many constructors

Aaron Stump aaron-stump at uiowa.edu
Fri Jan 24 21:51:06 CET 2014


Dear Agda list,

Over winter break, I wrote a parser generator which targets Agda! Yes, 
it is exciting, I know.  It's not quite ready for release, partly 
because I am getting really slow checking times for some of the 
generated files.  Attached is a standalone Agda file of 1500 lines which 
takes about 30 seconds to check on my machine, with the 2.3.2 release of 
Agda.  This was generated from a tiny expression grammar, and I have 
found that Agda is taking too long and way too much memory (many GB) on 
bigger generated files from more interesting grammars.

I talked to Nils Anders at PLPV, and he was speculating that perhaps the 
rather large number of constructors in a datatype representing a set of 
states (grep for s183) could perhaps be exposing a quadratic-time 
algorithm somewhere in the implementation.  So I am sending in this 
file, in case there is such a bug, or for any advice on how to speed up 
checking time.  The "len-dec-rewrite" function towards the end of the 
file will induce some reduction; in particular, normalizing some calls 
to the list length function on some particular lists (of length maybe 12 
or 15 max).  Otherwise, it's almost just simply typed, so one would hope 
it would check much more quickly.

Thanks,
Aaron
-------------- next part --------------
module exampleSlow where

----------------------------------------------------------------------
-- levels
----------------------------------------------------------------------

infixl 6 _?_

postulate
  level : Set
  lzero  : level
  lsuc   : level ? level
  _?_   : level ? level ? level

lone : level
lone = lsuc lzero

{-# COMPILED_TYPE level ()     #-}
{-# COMPILED lzero ()           #-}
{-# COMPILED lsuc  (\_ -> ())   #-}
{-# COMPILED _?_  (\_ _ -> ()) #-}

{-# BUILTIN LEVEL     level #-}
{-# BUILTIN LEVELZERO lzero  #-}
{-# BUILTIN LEVELSUC  lsuc   #-}
{-# BUILTIN LEVELMAX  _?_   #-}

----------------------------------------------------------------------
-- equality
----------------------------------------------------------------------

data _?_ {?} {A : Set ?} (x : A) : A ? Set ? where
  refl : x ? x

{-# BUILTIN EQUALITY _?_ #-}
{-# BUILTIN REFL refl #-}

infix 4 _?_ 

----------------------------------------------------------------------
-- booleans
----------------------------------------------------------------------

data ? : Set where
 tt : ?
 ff : ?

{-# BUILTIN BOOL  ?  #-}
{-# BUILTIN TRUE  tt  #-}
{-# BUILTIN FALSE ff #-}

{-# COMPILED_DATA ? Bool True False #-}

infixr 5 _||_ 

_||_ : ? ? ? ? ?
tt || b = tt
ff || b = b

----------------------------------------------------------------------
-- products and sums
----------------------------------------------------------------------

infixr 1 _?_ _?_

data ? {? ?'} (A : Set ?) (B : A ? Set ?') : Set (? ? ?') where
  _,_ : (a : A) ? (b : B a) ? ? A B

data _?_ {? ?'} (A : Set ?) (B : Set ?') : Set (? ? ?') where
  inj? : (x : A) ? A ? B
  inj? : (y : B) ? A ? B

_?_ = _?_

----------------------------------------------------------------------
-- natural numbers
----------------------------------------------------------------------

data ? : Set where
  zero : ?
  suc : ? ? ?

{-# BUILTIN NATURAL ?    #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

infixl 8 _<_ _=?_ _?_

_=?_ : ? ? ? ? ?
0 =? 0 = tt
suc x =? suc y = x =? y
_ =? _ = ff

_<_ : ? ? ? ? ?
0 < 0 = ff
0 < (suc y) = tt
(suc x) < (suc y) = x < y
(suc x) < 0 = ff

_?_ : ? ? ? ? ?
x ? y = (x < y) || x =? y

----------------------------------------------------------------------
-- lists
----------------------------------------------------------------------

data ? {?} (A : Set ?) : Set ? where
  [] : ? A
  _::_ : (x : A) (xs : ? A) ? ? A

{-# BUILTIN LIST ? #-}
{-# BUILTIN NIL  []   #-}
{-# BUILTIN CONS _::_  #-}


infixr 6 _::_ _++_

[_] : ? {?} {A : Set ?} ? A ? ? A
[ x ] = x :: []

_++_ : ? {?} {A : Set ?} ? ? A ? ? A ? ? A
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

length : ?{?}{A : Set ?} ? ? A ? ?
length [] = 0
length (x :: xs) = suc (length xs)

----------------------------------------------------------------------
-- nonempty trees
----------------------------------------------------------------------

data ? {?} (A : Set ?) : Set ? where
  node : A ? ? (? A) ? ? A

leaf : ? {?}{A : Set ?} ? A ? ? A
leaf a = node a []

----------------------------------------------------------------------
-- characters
----------------------------------------------------------------------

postulate
  char : Set

{-# BUILTIN CHAR char #-}
{-# COMPILED_TYPE char Char #-}

----------------------------------------------------------------------
-- strings
----------------------------------------------------------------------

postulate
  string : Set

{-# BUILTIN STRING string #-}
{-# COMPILED_TYPE string String #-}

private
 primitive
  primStringAppend   : string ? string ? string
  primStringFromList : ? char ? string

infixr 6 _^_ 

_^_ : string ? string ? string
_^_ = primStringAppend

fromList : ? char ? string
fromList = primStringFromList

charToString : char ? string
charToString c = fromList [ c ]

string-append-t : ? ? Set
string-append-t 0 = string ? string 
string-append-t (suc n) = string ? (string-append-t n)

string-append-h : (n : ?) ? string ? string-append-t n
string-append-h 0 ret = ? x ? ret ^ x
string-append-h (suc n) ret = ? x ? (string-append-h n (ret ^ x))

string-append : (n : ?) ? string-append-t n
string-append n = string-append-h n ""

----------------------------------------------------------------------
-- maybe type
----------------------------------------------------------------------
data maybe {?}(A : Set ?) : Set ? where
  just : A ? maybe A
  nothing : maybe A

_?=maybe_ : ? {?}{A B : Set ?} ? maybe A ? (A ? maybe B) ? maybe B
nothing ?=maybe f = nothing
(just x) ?=maybe f = f x

return-maybe : ? {?}{A : Set ?} ? A ? maybe A
return-maybe a = just a

----------------------------------------------------------------------
-- theorems
----------------------------------------------------------------------

?-contra : ff ? tt ? ? {P : Set} ? P
?-contra ()

||-split : ? {b b' : ?} ? b || b' ? tt ? b ? tt ? b' ? tt
||-split{tt}{tt} p = inj? refl
||-split{tt}{ff} p = inj? refl
||-split{ff}{tt} p = inj? refl
||-split{ff}{ff} ()

||-tt : ? (b : ?) ? b || tt ? tt
||-tt tt = refl
||-tt ff = refl

--------------------------------------------------
-- basic properties of <, ?, and =?
--------------------------------------------------

<-0 : ? (x : ?) ? x < 0 ? ff
<-0 0 = refl
<-0 (suc y) = refl

0-? : ? (x : ?) ? 0 ? x ? tt
0-? 0 = refl
0-? (suc x) = refl

<-drop : ? {x y : ?} ? x < (suc y) ? tt ? x ? y ? x < y ? tt
<-drop {0} {0} p = inj? refl
<-drop {suc x} {0} p rewrite <-0 x = ?-contra p
<-drop {0} {suc y} p = inj? refl
<-drop {suc x} {suc y} p with <-drop {x} {y} p 
... | inj? u rewrite u = inj? refl
... | inj? u = inj? u

=?-refl : ? (x : ?) ? (x =? x) ? tt
=?-refl 0 = refl
=?-refl (suc x) rewrite (=?-refl x) = refl

=?-suc : ? (x : ?) ? suc x =? x ? ff
=?-suc 0 = refl
=?-suc (suc x) = =?-suc x

=?-to-? : ? {x y : ?} ? x =? y ? tt ? x ? y
=?-to-? {0} {0} u = refl
=?-to-? {suc x} {0} ()
=?-to-? {0} {suc y} ()
=?-to-? {suc x} {suc y} u rewrite =?-to-? {x} {y} u = refl

=?-from-? : ? {x y : ?} ? x ? y ? x =? y ? tt
=?-from-? {x} {y} u rewrite u = =?-refl y

<-suc : ? (n : ?) ? n < suc n ? tt
<-suc 0 = refl
<-suc (suc n) rewrite <-suc n = refl

<-suc2 : ? (n : ?) ? suc n < n ? ff
<-suc2 0 = refl
<-suc2 (suc n) = <-suc2 n

?-suc : ? (n : ?) ? n ? suc n ? tt
?-suc n rewrite <-suc n = refl

?-suc2 : ? (n : ?) ? suc n ? n ? ff
?-suc2 n rewrite <-suc2 n | =?-suc n = refl

<-push : ? {x y : ?} ? (suc x) < y ? tt ? ? ? (? y' ? y ? (suc y'))
<-push {x} {0} ()
<-push {0} {suc y} p = (y , refl)
<-push {suc x} {suc y} p with <-push {x} {y} p 
... | ( y' , p' ) rewrite p' = (suc y' , refl)

suc-inj : ? {n m : ?} ? suc n ? suc m ? n ? m
suc-inj {n} {m} p rewrite (=?-to-?{n} (=?-from-? p)) = refl

--------------------------------------------------
-- ordering properties of < and ??
--------------------------------------------------

<-irrefl : ? (n : ?) ? n < n ? ff
<-irrefl 0 = refl
<-irrefl (suc n) = <-irrefl n

<-asym : ? {x y : ?} ? x < y ? tt ? y < x ? ff
<-asym {0} {0} _ = refl
<-asym {0} {suc y} p = refl
<-asym {suc x}{0} ()
<-asym {suc x}{suc y} p = <-asym {x} {y} p

?ff : ? {x y : ?} ? x ? y ? ff ? y < x ? tt
?ff{0}{0} ()
?ff{0}{suc y} ()
?ff{suc x}{0} _ = refl
?ff{suc x}{suc y} p rewrite ?ff {x}{y} p = refl

?-trichotomy? : ? (n m : ?) ? n < m || n =? m || m < n ? tt
?-trichotomy? 0 0 = refl
?-trichotomy? 0 (suc m) = refl
?-trichotomy? (suc n) 0 = refl
?-trichotomy? (suc n) (suc m) = ?-trichotomy? n m

?-trichotomy : ? (n m : ?) ? (n < m ? tt) ? (n =? m ? tt) ? (m < n ? tt)
?-trichotomy n m with ||-split{n < m} (?-trichotomy? n m)
... | inj? p = inj? p
... | inj? p with ||-split{n =? m} p
... | inj? p' = inj? (inj? p')
... | inj? p' = inj? (inj? p')

<-trans : ? {x y z : ?} ? x < y ? tt ? y < z ? tt ? x < z ? tt
<-trans {x} {0} p1 p2 rewrite <-0 x = ?-contra p1
<-trans {0} {suc y} {0} p1 () 
<-trans {0} {suc y} {suc z} p1 p2 = refl
<-trans {suc x} {suc y} {0} p1 () 
<-trans {suc x} {suc y} {suc z} p1 p2 = <-trans {x} {y} {z} p1 p2

<?-trans : ? {x y z : ?} ? x < y ? tt ? y ? z ? tt ? x < z ? tt
<?-trans {x} {y} {z} p1 p2 with ||-split p2
... | inj? p' = <-trans{x}  p1 p'
... | inj? p' rewrite =?-to-? {y} {z} p' = p1

?<-trans : ? {x y z : ?} ? x ? y ? tt ? y < z ? tt ? x < z ? tt
?<-trans {x} {y} {z} p1 p2 with ||-split p1
... | inj? p' = <-trans{x} p' p2
... | inj? p' rewrite =?-to-? {x} {y} p' = p2

?-refl : ? (x : ?) ? x ? x ? tt
?-refl 0 = refl
?-refl (suc x) = ?-refl x

?-trans : ? {x y z : ?} ? x ? y ? tt ? y ? z ? tt ? x ? z ? tt
?-trans {x} {y} {z} p1 p2 with ||-split p1 | ||-split p2
... | inj? p' | inj? p'' rewrite <-trans {x} p' p'' = refl
... | inj? p' | inj? p'' rewrite =?-to-? {x} p'  | p'' = refl
... | inj? p' | inj? p'' rewrite =?-to-? {y} p'' | p' = refl
... | inj? p' | inj? p'' rewrite =?-to-? {x} p'  | =?-to-? {y} p'' | =?-refl z | ||-tt (z < z) = refl

<-suc-trans : ? {x y : ?} ? x < y ? tt ? x < suc y ? tt
<-suc-trans{x}{y} p with ?-trichotomy x (suc y)
... | inj? p' = p'
... | inj? (inj? p'') rewrite (=?-to-? {x}  p'') | <-suc2 y = ?-contra p
... | inj? (inj? p'') with <-irrefl x | <-trans {x} {y} {x} p (<-trans{y}  (<-suc y) p'')
... | p1 | p2 rewrite p1 = ?-contra p2

<-iter-suc-trans-t-h : (n : ?) ? (x : ?) ? (accum : ?) ? Set
<-iter-suc-trans-t-h 0 x accum = x < accum ? tt
<-iter-suc-trans-t-h (suc n) x accum = <-iter-suc-trans-t-h n x (suc accum)

<-iter-suc-trans-t : (n : ?) ? (x : ?) ? Set
<-iter-suc-trans-t n x = <-iter-suc-trans-t-h n x (suc x)

<-iter-suc-trans-h : ? (n : ?) ? (x : ?) ? (accum : ?) ? x < accum ? tt ? <-iter-suc-trans-t-h n x accum
<-iter-suc-trans-h 0 x accum p = p
<-iter-suc-trans-h (suc n) x accum p = <-iter-suc-trans-h n x (suc accum) (<-suc-trans{x} p)

<-iter-suc-trans : ? (n : ?) ? (x : ?) ? <-iter-suc-trans-t n x
<-iter-suc-trans n x = <-iter-suc-trans-h n x (suc x) (<-suc x)

----------------------------------------------------------------------
-- automata and parse tree records
----------------------------------------------------------------------

record automaton : Set lone where
  field
    state : Set
    state-to-string : state ? string
    start : state
    is-final : state ? ?
    next : state ? char ? maybe state
    eps : state ? ? (? state)

record ParseTreeRec : Set lone where
  field
    ParseTreeT : Set
    ParseTreeToString : ParseTreeT ? string

----------------------------------------------------------------------
-- ASTs
----------------------------------------------------------------------

num-range-1 = string
num-plus-2 = string
num = string
id-range-3 = string
id-plus-4 = string
id = string

mutual

  data expr : Set where 
    Id : id ? expr
    Num : num ? expr
    Parens : expr ? expr
    Plus : expr ? expr ? expr
    Times : expr ? expr ? expr

data ParseTreeT : Set where
  parsed-expr : expr ? ParseTreeT
  parsed-num-range-1 : num-range-1 ? ParseTreeT
  parsed-num-plus-2 : num-plus-2 ? ParseTreeT
  parsed-num : num ? ParseTreeT
  parsed-id-range-3 : id-range-3 ? ParseTreeT
  parsed-id-plus-4 : id-plus-4 ? ParseTreeT
  parsed-id : id ? ParseTreeT

-- dummy version of this function
norm-expr : expr ? expr
norm-expr x = x

------------------------------------------
-- Parse tree printing functions
------------------------------------------

num-range-1ToString : num-range-1 ? string
num-range-1ToString x = "(num-range-1 " ^ x ^ ")"
num-plus-2ToString : num-plus-2 ? string
num-plus-2ToString x = "(num-plus-2 " ^ x ^ ")"
numToString : num ? string
numToString x = "(num " ^ x ^ ")"
id-range-3ToString : id-range-3 ? string
id-range-3ToString x = "(id-range-3 " ^ x ^ ")"
id-plus-4ToString : id-plus-4 ? string
id-plus-4ToString x = "(id-plus-4 " ^ x ^ ")"
idToString : id ? string
idToString x = "(id " ^ x ^ ")"

mutual
  exprToString : expr ? string
  exprToString (Id x0) = "(Id" ^ " " ^ (idToString x0) ^ ")"
  exprToString (Num x0) = "(Num" ^ " " ^ (numToString x0) ^ ")"
  exprToString (Parens x0) = "(Parens" ^ " " ^ (exprToString x0) ^ ")"
  exprToString (Plus x0 x1) = "(Plus" ^ " " ^ (exprToString x0) ^ " " ^ (exprToString x1) ^ ")"
  exprToString (Times x0 x1) = "(Times" ^ " " ^ (exprToString x0) ^ " " ^ (exprToString x1) ^ ")"

ParseTreeToString : ParseTreeT ? string
ParseTreeToString (parsed-expr t) = exprToString t
ParseTreeToString (parsed-num-range-1 t) = num-range-1ToString t
ParseTreeToString (parsed-num-plus-2 t) = num-plus-2ToString t
ParseTreeToString (parsed-num t) = numToString t
ParseTreeToString (parsed-id-range-3 t) = id-range-3ToString t
ParseTreeToString (parsed-id-plus-4 t) = id-plus-4ToString t
ParseTreeToString (parsed-id t) = idToString t



----------------------------------------------------------------------------------
-- Automaton
----------------------------------------------------------------------------------

------------------------------------------
-- states
------------------------------------------

data state : Set where
  s0 {-  -} : state
  s1 {-  -} : state
  s2 {- start expr from  -} : state
  s3 {- end expr from  -} : state
  s4 {- Times 0 from  -} : state
  s5 {- Times 1 from  -} : state
  s6 {- Times 2 from  -} : state
  s7 {- Plus 0 from  -} : state
  s8 {- Plus 1 from  -} : state
  s9 {- Plus 2 from  -} : state
  s10 {- Parens 0 from  -} : state
  s11 {- Parens 1 from  -} : state
  s12 {- Parens 2 from  -} : state
  s13 {- Parens 3 from  -} : state
  s14 {- Num 0 from  -} : state
  s15 {- start num from Num 1 ;  -} : state
  s16 {- end num from Num 1 ;  -} : state
  s17 {- P12 0 from Num 1 ;  -} : state
  s18 {- start num-plus-2 from P12 1 ; Num 1 ;  -} : state
  s19 {- end num-plus-2 from P12 1 ; Num 1 ;  -} : state
  s20 {- P11 0 from P12 1 ; Num 1 ;  -} : state
  s21 {- start num-range-1 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s22 {- end num-range-1 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s23 {- P9 0 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s24 {- P9 1 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s25 {- P8 0 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s26 {- P8 1 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s27 {- P7 0 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s28 {- P7 1 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s29 {- P6 0 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s30 {- P6 1 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s31 {- P5 0 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s32 {- P5 1 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s33 {- P4 0 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s34 {- P4 1 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s35 {- P3 0 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s36 {- P3 1 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s37 {- P2 0 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s38 {- P2 1 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s39 {- P1 0 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s40 {- P1 1 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s41 {- P0 0 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s42 {- P0 1 from P11 1 ; P12 1 ; Num 1 ;  -} : state
  s43 {- P11 1 from P12 1 ; Num 1 ;  -} : state
  s44 {- P10 0 from P12 1 ; Num 1 ;  -} : state
  s45 {- start num-range-1 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s46 {- end num-range-1 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s47 {- P9 0 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s48 {- P9 1 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s49 {- P8 0 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s50 {- P8 1 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s51 {- P7 0 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s52 {- P7 1 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s53 {- P6 0 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s54 {- P6 1 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s55 {- P5 0 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s56 {- P5 1 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s57 {- P4 0 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s58 {- P4 1 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s59 {- P3 0 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s60 {- P3 1 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s61 {- P2 0 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s62 {- P2 1 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s63 {- P1 0 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s64 {- P1 1 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s65 {- P0 0 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s66 {- P0 1 from P10 1 ; P12 1 ; Num 1 ;  -} : state
  s67 {- Id 0 from  -} : state
  s68 {- start id from Id 1 ;  -} : state
  s69 {- end id from Id 1 ;  -} : state
  s70 {- P41 0 from Id 1 ;  -} : state
  s71 {- start id-plus-4 from P41 1 ; Id 1 ;  -} : state
  s72 {- end id-plus-4 from P41 1 ; Id 1 ;  -} : state
  s73 {- P40 0 from P41 1 ; Id 1 ;  -} : state
  s74 {- start id-range-3 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s75 {- end id-range-3 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s76 {- P38 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s77 {- P38 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s78 {- P37 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s79 {- P37 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s80 {- P36 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s81 {- P36 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s82 {- P35 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s83 {- P35 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s84 {- P34 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s85 {- P34 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s86 {- P33 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s87 {- P33 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s88 {- P32 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s89 {- P32 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s90 {- P31 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s91 {- P31 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s92 {- P30 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s93 {- P30 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s94 {- P29 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s95 {- P29 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s96 {- P28 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s97 {- P28 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s98 {- P27 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s99 {- P27 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s100 {- P26 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s101 {- P26 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s102 {- P25 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s103 {- P25 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s104 {- P24 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s105 {- P24 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s106 {- P23 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s107 {- P23 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s108 {- P22 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s109 {- P22 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s110 {- P21 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s111 {- P21 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s112 {- P20 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s113 {- P20 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s114 {- P19 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s115 {- P19 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s116 {- P18 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s117 {- P18 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s118 {- P17 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s119 {- P17 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s120 {- P16 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s121 {- P16 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s122 {- P15 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s123 {- P15 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s124 {- P14 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s125 {- P14 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s126 {- P13 0 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s127 {- P13 1 from P40 1 ; P41 1 ; Id 1 ;  -} : state
  s128 {- P40 1 from P41 1 ; Id 1 ;  -} : state
  s129 {- P39 0 from P41 1 ; Id 1 ;  -} : state
  s130 {- start id-range-3 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s131 {- end id-range-3 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s132 {- P38 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s133 {- P38 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s134 {- P37 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s135 {- P37 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s136 {- P36 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s137 {- P36 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s138 {- P35 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s139 {- P35 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s140 {- P34 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s141 {- P34 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s142 {- P33 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s143 {- P33 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s144 {- P32 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s145 {- P32 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s146 {- P31 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s147 {- P31 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s148 {- P30 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s149 {- P30 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s150 {- P29 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s151 {- P29 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s152 {- P28 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s153 {- P28 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s154 {- P27 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s155 {- P27 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s156 {- P26 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s157 {- P26 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s158 {- P25 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s159 {- P25 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s160 {- P24 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s161 {- P24 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s162 {- P23 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s163 {- P23 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s164 {- P22 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s165 {- P22 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s166 {- P21 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s167 {- P21 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s168 {- P20 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s169 {- P20 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s170 {- P19 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s171 {- P19 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s172 {- P18 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s173 {- P18 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s174 {- P17 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s175 {- P17 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s176 {- P16 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s177 {- P16 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s178 {- P15 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s179 {- P15 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s180 {- P14 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s181 {- P14 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s182 {- P13 0 from P39 1 ; P41 1 ; Id 1 ;  -} : state
  s183 {- P13 1 from P39 1 ; P41 1 ; Id 1 ;  -} : state

------------------------------------------
-- state to string
------------------------------------------

state-to-string : state ? string
state-to-string s0 = "0"
state-to-string s1 = "1"
state-to-string s2 = "2"
state-to-string s3 = "3"
state-to-string s4 = "4"
state-to-string s5 = "5"
state-to-string s6 = "6"
state-to-string s7 = "7"
state-to-string s8 = "8"
state-to-string s9 = "9"
state-to-string s10 = "10"
state-to-string s11 = "11"
state-to-string s12 = "12"
state-to-string s13 = "13"
state-to-string s14 = "14"
state-to-string s15 = "15"
state-to-string s16 = "16"
state-to-string s17 = "17"
state-to-string s18 = "18"
state-to-string s19 = "19"
state-to-string s20 = "20"
state-to-string s21 = "21"
state-to-string s22 = "22"
state-to-string s23 = "23"
state-to-string s24 = "24"
state-to-string s25 = "25"
state-to-string s26 = "26"
state-to-string s27 = "27"
state-to-string s28 = "28"
state-to-string s29 = "29"
state-to-string s30 = "30"
state-to-string s31 = "31"
state-to-string s32 = "32"
state-to-string s33 = "33"
state-to-string s34 = "34"
state-to-string s35 = "35"
state-to-string s36 = "36"
state-to-string s37 = "37"
state-to-string s38 = "38"
state-to-string s39 = "39"
state-to-string s40 = "40"
state-to-string s41 = "41"
state-to-string s42 = "42"
state-to-string s43 = "43"
state-to-string s44 = "44"
state-to-string s45 = "45"
state-to-string s46 = "46"
state-to-string s47 = "47"
state-to-string s48 = "48"
state-to-string s49 = "49"
state-to-string s50 = "50"
state-to-string s51 = "51"
state-to-string s52 = "52"
state-to-string s53 = "53"
state-to-string s54 = "54"
state-to-string s55 = "55"
state-to-string s56 = "56"
state-to-string s57 = "57"
state-to-string s58 = "58"
state-to-string s59 = "59"
state-to-string s60 = "60"
state-to-string s61 = "61"
state-to-string s62 = "62"
state-to-string s63 = "63"
state-to-string s64 = "64"
state-to-string s65 = "65"
state-to-string s66 = "66"
state-to-string s67 = "67"
state-to-string s68 = "68"
state-to-string s69 = "69"
state-to-string s70 = "70"
state-to-string s71 = "71"
state-to-string s72 = "72"
state-to-string s73 = "73"
state-to-string s74 = "74"
state-to-string s75 = "75"
state-to-string s76 = "76"
state-to-string s77 = "77"
state-to-string s78 = "78"
state-to-string s79 = "79"
state-to-string s80 = "80"
state-to-string s81 = "81"
state-to-string s82 = "82"
state-to-string s83 = "83"
state-to-string s84 = "84"
state-to-string s85 = "85"
state-to-string s86 = "86"
state-to-string s87 = "87"
state-to-string s88 = "88"
state-to-string s89 = "89"
state-to-string s90 = "90"
state-to-string s91 = "91"
state-to-string s92 = "92"
state-to-string s93 = "93"
state-to-string s94 = "94"
state-to-string s95 = "95"
state-to-string s96 = "96"
state-to-string s97 = "97"
state-to-string s98 = "98"
state-to-string s99 = "99"
state-to-string s100 = "100"
state-to-string s101 = "101"
state-to-string s102 = "102"
state-to-string s103 = "103"
state-to-string s104 = "104"
state-to-string s105 = "105"
state-to-string s106 = "106"
state-to-string s107 = "107"
state-to-string s108 = "108"
state-to-string s109 = "109"
state-to-string s110 = "110"
state-to-string s111 = "111"
state-to-string s112 = "112"
state-to-string s113 = "113"
state-to-string s114 = "114"
state-to-string s115 = "115"
state-to-string s116 = "116"
state-to-string s117 = "117"
state-to-string s118 = "118"
state-to-string s119 = "119"
state-to-string s120 = "120"
state-to-string s121 = "121"
state-to-string s122 = "122"
state-to-string s123 = "123"
state-to-string s124 = "124"
state-to-string s125 = "125"
state-to-string s126 = "126"
state-to-string s127 = "127"
state-to-string s128 = "128"
state-to-string s129 = "129"
state-to-string s130 = "130"
state-to-string s131 = "131"
state-to-string s132 = "132"
state-to-string s133 = "133"
state-to-string s134 = "134"
state-to-string s135 = "135"
state-to-string s136 = "136"
state-to-string s137 = "137"
state-to-string s138 = "138"
state-to-string s139 = "139"
state-to-string s140 = "140"
state-to-string s141 = "141"
state-to-string s142 = "142"
state-to-string s143 = "143"
state-to-string s144 = "144"
state-to-string s145 = "145"
state-to-string s146 = "146"
state-to-string s147 = "147"
state-to-string s148 = "148"
state-to-string s149 = "149"
state-to-string s150 = "150"
state-to-string s151 = "151"
state-to-string s152 = "152"
state-to-string s153 = "153"
state-to-string s154 = "154"
state-to-string s155 = "155"
state-to-string s156 = "156"
state-to-string s157 = "157"
state-to-string s158 = "158"
state-to-string s159 = "159"
state-to-string s160 = "160"
state-to-string s161 = "161"
state-to-string s162 = "162"
state-to-string s163 = "163"
state-to-string s164 = "164"
state-to-string s165 = "165"
state-to-string s166 = "166"
state-to-string s167 = "167"
state-to-string s168 = "168"
state-to-string s169 = "169"
state-to-string s170 = "170"
state-to-string s171 = "171"
state-to-string s172 = "172"
state-to-string s173 = "173"
state-to-string s174 = "174"
state-to-string s175 = "175"
state-to-string s176 = "176"
state-to-string s177 = "177"
state-to-string s178 = "178"
state-to-string s179 = "179"
state-to-string s180 = "180"
state-to-string s181 = "181"
state-to-string s182 = "182"
state-to-string s183 = "183"

------------------------------------------
-- labeled transitions
------------------------------------------

next : state ? char ? maybe state
next s5 {- Times 1 from  -} '*' = just s6 {- Times 2 from  -}
next s8 {- Plus 1 from  -} '+' = just s9 {- Plus 2 from  -}
next s10 {- Parens 0 from  -} '(' = just s11 {- Parens 1 from  -}
next s12 {- Parens 2 from  -} ')' = just s13 {- Parens 3 from  -}
next s23 {- P9 0 from P11 1 ; P12 1 ; Num 1 ;  -} '9' = just s24 {- P9 1 from P11 1 ; P12 1 ; Num 1 ;  -}
next s25 {- P8 0 from P11 1 ; P12 1 ; Num 1 ;  -} '8' = just s26 {- P8 1 from P11 1 ; P12 1 ; Num 1 ;  -}
next s27 {- P7 0 from P11 1 ; P12 1 ; Num 1 ;  -} '7' = just s28 {- P7 1 from P11 1 ; P12 1 ; Num 1 ;  -}
next s29 {- P6 0 from P11 1 ; P12 1 ; Num 1 ;  -} '6' = just s30 {- P6 1 from P11 1 ; P12 1 ; Num 1 ;  -}
next s31 {- P5 0 from P11 1 ; P12 1 ; Num 1 ;  -} '5' = just s32 {- P5 1 from P11 1 ; P12 1 ; Num 1 ;  -}
next s33 {- P4 0 from P11 1 ; P12 1 ; Num 1 ;  -} '4' = just s34 {- P4 1 from P11 1 ; P12 1 ; Num 1 ;  -}
next s35 {- P3 0 from P11 1 ; P12 1 ; Num 1 ;  -} '3' = just s36 {- P3 1 from P11 1 ; P12 1 ; Num 1 ;  -}
next s37 {- P2 0 from P11 1 ; P12 1 ; Num 1 ;  -} '2' = just s38 {- P2 1 from P11 1 ; P12 1 ; Num 1 ;  -}
next s39 {- P1 0 from P11 1 ; P12 1 ; Num 1 ;  -} '1' = just s40 {- P1 1 from P11 1 ; P12 1 ; Num 1 ;  -}
next s41 {- P0 0 from P11 1 ; P12 1 ; Num 1 ;  -} '0' = just s42 {- P0 1 from P11 1 ; P12 1 ; Num 1 ;  -}
next s47 {- P9 0 from P10 1 ; P12 1 ; Num 1 ;  -} '9' = just s48 {- P9 1 from P10 1 ; P12 1 ; Num 1 ;  -}
next s49 {- P8 0 from P10 1 ; P12 1 ; Num 1 ;  -} '8' = just s50 {- P8 1 from P10 1 ; P12 1 ; Num 1 ;  -}
next s51 {- P7 0 from P10 1 ; P12 1 ; Num 1 ;  -} '7' = just s52 {- P7 1 from P10 1 ; P12 1 ; Num 1 ;  -}
next s53 {- P6 0 from P10 1 ; P12 1 ; Num 1 ;  -} '6' = just s54 {- P6 1 from P10 1 ; P12 1 ; Num 1 ;  -}
next s55 {- P5 0 from P10 1 ; P12 1 ; Num 1 ;  -} '5' = just s56 {- P5 1 from P10 1 ; P12 1 ; Num 1 ;  -}
next s57 {- P4 0 from P10 1 ; P12 1 ; Num 1 ;  -} '4' = just s58 {- P4 1 from P10 1 ; P12 1 ; Num 1 ;  -}
next s59 {- P3 0 from P10 1 ; P12 1 ; Num 1 ;  -} '3' = just s60 {- P3 1 from P10 1 ; P12 1 ; Num 1 ;  -}
next s61 {- P2 0 from P10 1 ; P12 1 ; Num 1 ;  -} '2' = just s62 {- P2 1 from P10 1 ; P12 1 ; Num 1 ;  -}
next s63 {- P1 0 from P10 1 ; P12 1 ; Num 1 ;  -} '1' = just s64 {- P1 1 from P10 1 ; P12 1 ; Num 1 ;  -}
next s65 {- P0 0 from P10 1 ; P12 1 ; Num 1 ;  -} '0' = just s66 {- P0 1 from P10 1 ; P12 1 ; Num 1 ;  -}
next s76 {- P38 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'z' = just s77 {- P38 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s78 {- P37 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'y' = just s79 {- P37 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s80 {- P36 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'x' = just s81 {- P36 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s82 {- P35 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'w' = just s83 {- P35 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s84 {- P34 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'v' = just s85 {- P34 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s86 {- P33 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'u' = just s87 {- P33 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s88 {- P32 0 from P40 1 ; P41 1 ; Id 1 ;  -} 't' = just s89 {- P32 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s90 {- P31 0 from P40 1 ; P41 1 ; Id 1 ;  -} 's' = just s91 {- P31 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s92 {- P30 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'r' = just s93 {- P30 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s94 {- P29 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'q' = just s95 {- P29 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s96 {- P28 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'p' = just s97 {- P28 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s98 {- P27 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'o' = just s99 {- P27 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s100 {- P26 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'n' = just s101 {- P26 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s102 {- P25 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'm' = just s103 {- P25 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s104 {- P24 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'l' = just s105 {- P24 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s106 {- P23 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'k' = just s107 {- P23 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s108 {- P22 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'j' = just s109 {- P22 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s110 {- P21 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'i' = just s111 {- P21 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s112 {- P20 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'h' = just s113 {- P20 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s114 {- P19 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'g' = just s115 {- P19 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s116 {- P18 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'f' = just s117 {- P18 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s118 {- P17 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'e' = just s119 {- P17 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s120 {- P16 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'd' = just s121 {- P16 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s122 {- P15 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'c' = just s123 {- P15 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s124 {- P14 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'b' = just s125 {- P14 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s126 {- P13 0 from P40 1 ; P41 1 ; Id 1 ;  -} 'a' = just s127 {- P13 1 from P40 1 ; P41 1 ; Id 1 ;  -}
next s132 {- P38 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'z' = just s133 {- P38 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s134 {- P37 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'y' = just s135 {- P37 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s136 {- P36 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'x' = just s137 {- P36 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s138 {- P35 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'w' = just s139 {- P35 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s140 {- P34 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'v' = just s141 {- P34 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s142 {- P33 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'u' = just s143 {- P33 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s144 {- P32 0 from P39 1 ; P41 1 ; Id 1 ;  -} 't' = just s145 {- P32 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s146 {- P31 0 from P39 1 ; P41 1 ; Id 1 ;  -} 's' = just s147 {- P31 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s148 {- P30 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'r' = just s149 {- P30 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s150 {- P29 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'q' = just s151 {- P29 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s152 {- P28 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'p' = just s153 {- P28 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s154 {- P27 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'o' = just s155 {- P27 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s156 {- P26 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'n' = just s157 {- P26 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s158 {- P25 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'm' = just s159 {- P25 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s160 {- P24 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'l' = just s161 {- P24 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s162 {- P23 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'k' = just s163 {- P23 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s164 {- P22 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'j' = just s165 {- P22 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s166 {- P21 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'i' = just s167 {- P21 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s168 {- P20 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'h' = just s169 {- P20 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s170 {- P19 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'g' = just s171 {- P19 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s172 {- P18 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'f' = just s173 {- P18 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s174 {- P17 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'e' = just s175 {- P17 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s176 {- P16 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'd' = just s177 {- P16 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s178 {- P15 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'c' = just s179 {- P15 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s180 {- P14 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'b' = just s181 {- P14 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next s182 {- P13 0 from P39 1 ; P41 1 ; Id 1 ;  -} 'a' = just s183 {- P13 1 from P39 1 ; P41 1 ; Id 1 ;  -}
next x c = nothing

------------------------------------------
-- unlabeled (epsilon) transitions
------------------------------------------

eps : state ? ? (? state)
eps s0 {-  -} =
  (
   (node s2 ((node s10 []) :: (node s14 ((node s15 ((node s17 ((node s18 ((node s20 ((node s21 ((node s23 []) :: (node s25 []) :: (node s27 []) :: (node s29 []) :: (node s31 []) :: (node s33 []) :: (node s35 []) :: (node s37 []) :: (node s39 []) :: (node s41 []) :: [])) :: [])) :: (node s44 ((node s45 ((node s47 []) :: (node s49 []) :: (node s51 []) :: (node s53 []) :: (node s55 []) :: (node s57 []) :: (node s59 []) :: (node s61 []) :: (node s63 []) :: (node s65 []) :: [])) :: [])) :: [])) :: [])) :: [])) :: [])) :: (node s67 ((node s68 ((node s70 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s6 {- Times 2 from  -} =
  (
   (node s2 ((node s10 []) :: (node s14 ((node s15 ((node s17 ((node s18 ((node s20 ((node s21 ((node s23 []) :: (node s25 []) :: (node s27 []) :: (node s29 []) :: (node s31 []) :: (node s33 []) :: (node s35 []) :: (node s37 []) :: (node s39 []) :: (node s41 []) :: [])) :: [])) :: (node s44 ((node s45 ((node s47 []) :: (node s49 []) :: (node s51 []) :: (node s53 []) :: (node s55 []) :: (node s57 []) :: (node s59 []) :: (node s61 []) :: (node s63 []) :: (node s65 []) :: [])) :: [])) :: [])) :: [])) :: [])) :: [])) :: (node s67 ((node s68 ((node s70 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s9 {- Plus 2 from  -} =
  (
   (node s2 ((node s10 []) :: (node s14 ((node s15 ((node s17 ((node s18 ((node s20 ((node s21 ((node s23 []) :: (node s25 []) :: (node s27 []) :: (node s29 []) :: (node s31 []) :: (node s33 []) :: (node s35 []) :: (node s37 []) :: (node s39 []) :: (node s41 []) :: [])) :: [])) :: (node s44 ((node s45 ((node s47 []) :: (node s49 []) :: (node s51 []) :: (node s53 []) :: (node s55 []) :: (node s57 []) :: (node s59 []) :: (node s61 []) :: (node s63 []) :: (node s65 []) :: [])) :: [])) :: [])) :: [])) :: [])) :: [])) :: (node s67 ((node s68 ((node s70 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s11 {- Parens 1 from  -} =
  (
   (node s2 ((node s10 []) :: (node s14 ((node s15 ((node s17 ((node s18 ((node s20 ((node s21 ((node s23 []) :: (node s25 []) :: (node s27 []) :: (node s29 []) :: (node s31 []) :: (node s33 []) :: (node s35 []) :: (node s37 []) :: (node s39 []) :: (node s41 []) :: [])) :: [])) :: (node s44 ((node s45 ((node s47 []) :: (node s49 []) :: (node s51 []) :: (node s53 []) :: (node s55 []) :: (node s57 []) :: (node s59 []) :: (node s61 []) :: (node s63 []) :: (node s65 []) :: [])) :: [])) :: [])) :: [])) :: [])) :: [])) :: (node s67 ((node s68 ((node s70 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s13 {- Parens 3 from  -} =
  (
   (node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: []))
   :: 
   [])
eps s24 {- P9 1 from P11 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s22 ((node s43 ((node s18 ((node s20 ((node s21 ((node s23 []) :: (node s25 []) :: (node s27 []) :: (node s29 []) :: (node s31 []) :: (node s33 []) :: (node s35 []) :: (node s37 []) :: (node s39 []) :: (node s41 []) :: [])) :: [])) :: (node s44 ((node s45 ((node s47 []) :: (node s49 []) :: (node s51 []) :: (node s53 []) :: (node s55 []) :: (node s57 []) :: (node s59 []) :: (node s61 []) :: (node s63 []) :: (node s65 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s26 {- P8 1 from P11 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s22 ((node s43 ((node s18 ((node s20 ((node s21 ((node s23 []) :: (node s25 []) :: (node s27 []) :: (node s29 []) :: (node s31 []) :: (node s33 []) :: (node s35 []) :: (node s37 []) :: (node s39 []) :: (node s41 []) :: [])) :: [])) :: (node s44 ((node s45 ((node s47 []) :: (node s49 []) :: (node s51 []) :: (node s53 []) :: (node s55 []) :: (node s57 []) :: (node s59 []) :: (node s61 []) :: (node s63 []) :: (node s65 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s28 {- P7 1 from P11 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s22 ((node s43 ((node s18 ((node s20 ((node s21 ((node s23 []) :: (node s25 []) :: (node s27 []) :: (node s29 []) :: (node s31 []) :: (node s33 []) :: (node s35 []) :: (node s37 []) :: (node s39 []) :: (node s41 []) :: [])) :: [])) :: (node s44 ((node s45 ((node s47 []) :: (node s49 []) :: (node s51 []) :: (node s53 []) :: (node s55 []) :: (node s57 []) :: (node s59 []) :: (node s61 []) :: (node s63 []) :: (node s65 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s30 {- P6 1 from P11 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s22 ((node s43 ((node s18 ((node s20 ((node s21 ((node s23 []) :: (node s25 []) :: (node s27 []) :: (node s29 []) :: (node s31 []) :: (node s33 []) :: (node s35 []) :: (node s37 []) :: (node s39 []) :: (node s41 []) :: [])) :: [])) :: (node s44 ((node s45 ((node s47 []) :: (node s49 []) :: (node s51 []) :: (node s53 []) :: (node s55 []) :: (node s57 []) :: (node s59 []) :: (node s61 []) :: (node s63 []) :: (node s65 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s32 {- P5 1 from P11 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s22 ((node s43 ((node s18 ((node s20 ((node s21 ((node s23 []) :: (node s25 []) :: (node s27 []) :: (node s29 []) :: (node s31 []) :: (node s33 []) :: (node s35 []) :: (node s37 []) :: (node s39 []) :: (node s41 []) :: [])) :: [])) :: (node s44 ((node s45 ((node s47 []) :: (node s49 []) :: (node s51 []) :: (node s53 []) :: (node s55 []) :: (node s57 []) :: (node s59 []) :: (node s61 []) :: (node s63 []) :: (node s65 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s34 {- P4 1 from P11 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s22 ((node s43 ((node s18 ((node s20 ((node s21 ((node s23 []) :: (node s25 []) :: (node s27 []) :: (node s29 []) :: (node s31 []) :: (node s33 []) :: (node s35 []) :: (node s37 []) :: (node s39 []) :: (node s41 []) :: [])) :: [])) :: (node s44 ((node s45 ((node s47 []) :: (node s49 []) :: (node s51 []) :: (node s53 []) :: (node s55 []) :: (node s57 []) :: (node s59 []) :: (node s61 []) :: (node s63 []) :: (node s65 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s36 {- P3 1 from P11 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s22 ((node s43 ((node s18 ((node s20 ((node s21 ((node s23 []) :: (node s25 []) :: (node s27 []) :: (node s29 []) :: (node s31 []) :: (node s33 []) :: (node s35 []) :: (node s37 []) :: (node s39 []) :: (node s41 []) :: [])) :: [])) :: (node s44 ((node s45 ((node s47 []) :: (node s49 []) :: (node s51 []) :: (node s53 []) :: (node s55 []) :: (node s57 []) :: (node s59 []) :: (node s61 []) :: (node s63 []) :: (node s65 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s38 {- P2 1 from P11 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s22 ((node s43 ((node s18 ((node s20 ((node s21 ((node s23 []) :: (node s25 []) :: (node s27 []) :: (node s29 []) :: (node s31 []) :: (node s33 []) :: (node s35 []) :: (node s37 []) :: (node s39 []) :: (node s41 []) :: [])) :: [])) :: (node s44 ((node s45 ((node s47 []) :: (node s49 []) :: (node s51 []) :: (node s53 []) :: (node s55 []) :: (node s57 []) :: (node s59 []) :: (node s61 []) :: (node s63 []) :: (node s65 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s40 {- P1 1 from P11 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s22 ((node s43 ((node s18 ((node s20 ((node s21 ((node s23 []) :: (node s25 []) :: (node s27 []) :: (node s29 []) :: (node s31 []) :: (node s33 []) :: (node s35 []) :: (node s37 []) :: (node s39 []) :: (node s41 []) :: [])) :: [])) :: (node s44 ((node s45 ((node s47 []) :: (node s49 []) :: (node s51 []) :: (node s53 []) :: (node s55 []) :: (node s57 []) :: (node s59 []) :: (node s61 []) :: (node s63 []) :: (node s65 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s42 {- P0 1 from P11 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s22 ((node s43 ((node s18 ((node s20 ((node s21 ((node s23 []) :: (node s25 []) :: (node s27 []) :: (node s29 []) :: (node s31 []) :: (node s33 []) :: (node s35 []) :: (node s37 []) :: (node s39 []) :: (node s41 []) :: [])) :: [])) :: (node s44 ((node s45 ((node s47 []) :: (node s49 []) :: (node s51 []) :: (node s53 []) :: (node s55 []) :: (node s57 []) :: (node s59 []) :: (node s61 []) :: (node s63 []) :: (node s65 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s48 {- P9 1 from P10 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s46 ((node s19 ((node s16 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s50 {- P8 1 from P10 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s46 ((node s19 ((node s16 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s52 {- P7 1 from P10 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s46 ((node s19 ((node s16 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s54 {- P6 1 from P10 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s46 ((node s19 ((node s16 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s56 {- P5 1 from P10 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s46 ((node s19 ((node s16 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s58 {- P4 1 from P10 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s46 ((node s19 ((node s16 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s60 {- P3 1 from P10 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s46 ((node s19 ((node s16 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s62 {- P2 1 from P10 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s46 ((node s19 ((node s16 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s64 {- P1 1 from P10 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s46 ((node s19 ((node s16 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s66 {- P0 1 from P10 1 ; P12 1 ; Num 1 ;  -} =
  (
   (node s46 ((node s19 ((node s16 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s77 {- P38 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s79 {- P37 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s81 {- P36 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s83 {- P35 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s85 {- P34 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s87 {- P33 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s89 {- P32 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s91 {- P31 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s93 {- P30 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s95 {- P29 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s97 {- P28 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s99 {- P27 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s101 {- P26 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s103 {- P25 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s105 {- P24 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s107 {- P23 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s109 {- P22 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s111 {- P21 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s113 {- P20 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s115 {- P19 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s117 {- P18 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s119 {- P17 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s121 {- P16 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s123 {- P15 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s125 {- P14 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s127 {- P13 1 from P40 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s75 ((node s128 ((node s71 ((node s73 ((node s74 ((node s76 []) :: (node s78 []) :: (node s80 []) :: (node s82 []) :: (node s84 []) :: (node s86 []) :: (node s88 []) :: (node s90 []) :: (node s92 []) :: (node s94 []) :: (node s96 []) :: (node s98 []) :: (node s100 []) :: (node s102 []) :: (node s104 []) :: (node s106 []) :: (node s108 []) :: (node s110 []) :: (node s112 []) :: (node s114 []) :: (node s116 []) :: (node s118 []) :: (node s120 []) :: (node s122 []) :: (node s124 []) :: (node s126 []) :: [])) :: [])) :: (node s129 ((node s130 ((node s132 []) :: (node s134 []) :: (node s136 []) :: (node s138 []) :: (node s140 []) :: (node s142 []) :: (node s144 []) :: (node s146 []) :: (node s148 []) :: (node s150 []) :: (node s152 []) :: (node s154 []) :: (node s156 []) :: (node s158 []) :: (node s160 []) :: (node s162 []) :: (node s164 []) :: (node s166 []) :: (node s168 []) :: (node s170 []) :: (node s172 []) :: (node s174 []) :: (node s176 []) :: (node s178 []) :: (node s180 []) :: (node s182 []) :: [])) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s133 {- P38 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s135 {- P37 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s137 {- P36 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s139 {- P35 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s141 {- P34 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s143 {- P33 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s145 {- P32 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s147 {- P31 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s149 {- P30 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s151 {- P29 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s153 {- P28 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s155 {- P27 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s157 {- P26 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s159 {- P25 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s161 {- P24 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s163 {- P23 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s165 {- P22 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s167 {- P21 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s169 {- P20 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s171 {- P19 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s173 {- P18 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s175 {- P17 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s177 {- P16 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s179 {- P15 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s181 {- P14 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps s183 {- P13 1 from P39 1 ; P41 1 ; Id 1 ;  -} =
  (
   (node s131 ((node s72 ((node s69 ((node s3 ((node s1 []) :: (node s5 []) :: (node s8 []) :: (node s12 []) :: [])) :: [])) :: [])) :: []))
   :: 
   [])
eps x = []

------------------------------------------
-- final automaton record
------------------------------------------

is-final : state ? ?
is-final s1 = tt
is-final x = ff

aut : automaton
aut = record { state = state ; state-to-string = state-to-string; start = s0; is-final = is-final; next = next ; eps = eps}

ptr : ParseTreeRec
ptr = record { ParseTreeT = ParseTreeT ; ParseTreeToString = ParseTreeToString }

----------------------------------------------------------------------------------
-- Run-rewriting rules
----------------------------------------------------------------------------------

data RunElement : Set where
  State : state ? RunElement 
  InputChar : char ? RunElement 
  ParseTree : ParseTreeT ? RunElement 

Run : Set
Run = ? RunElement

RunElement-to-string : RunElement ? string
RunElement-to-string (State s) = state-to-string s
RunElement-to-string (InputChar c) = "#" ^ (charToString c)
RunElement-to-string (ParseTree t) = (ParseTreeToString t)

Run-to-string : Run ? string
Run-to-string [] = "\n"
Run-to-string (e :: r) = (RunElement-to-string e) ^ " " ^ (Run-to-string r)

record rewriteRules : Set where
  field
    eps-rewrite : state ? state ? maybe ParseTreeT
    unit-rewrite : (r : Run) ? maybe (? Run (? r' ? length r' =? length r ? tt))
    unit-rewrite-iters : ? -- the number of times to try performing a unit rewrite at the same position
    len-dec-rewrite : (r : Run) ? maybe (? Run (? r' ? length r' < length r ? tt))

------------------------------------------
-- Epsilon rules
------------------------------------------

eps-rewrite : state ? state ? maybe ParseTreeT
eps-rewrite x y = nothing
------------------------------------------
-- Unit rules
------------------------------------------

unit-rewrite : (r : Run) ? maybe (? Run (? r' ? length r' =? length r ? tt))
unit-rewrite x = nothing

------------------------------------------
-- Length-decreasing rules
------------------------------------------

len-dec-rewrite : (r : Run) ? maybe (? Run (? r' ? length r' < length r ? tt))
len-dec-rewrite {- Id-} ((State s2) :: (State s67) :: (State s68) :: (ParseTree (parsed-id x0)) :: (State s69) :: (State s3) :: rest) = just (((State s2) :: (ParseTree (parsed-expr (norm-expr (Id x0)))) :: (State s3) :: rest)
 , <-iter-suc-trans 2 (length rest))
len-dec-rewrite {- P41-} ((State s68) :: (State s70) :: (State s71) :: (ParseTree (parsed-id-plus-4 x0)) :: (State s72) :: (State s69) :: rest) = just (((State s68) :: (ParseTree (parsed-id (string-append 0 x0))) :: (State s69) :: rest)
 , <-iter-suc-trans 2 (length rest))
len-dec-rewrite {- P39-} ((State s71) :: (State s129) :: (State s130) :: (ParseTree (parsed-id-range-3 x0)) :: (State s131) :: (State s72) :: rest) = just (((State s71) :: (ParseTree (parsed-id-plus-4 (string-append 0 x0))) :: (State s72) :: rest)
 , <-iter-suc-trans 2 (length rest))
len-dec-rewrite {- P13-} ((State s130) :: (State s182) :: (InputChar 'a') :: (State s183) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'a')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P14-} ((State s130) :: (State s180) :: (InputChar 'b') :: (State s181) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'b')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P15-} ((State s130) :: (State s178) :: (InputChar 'c') :: (State s179) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'c')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P16-} ((State s130) :: (State s176) :: (InputChar 'd') :: (State s177) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'd')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P17-} ((State s130) :: (State s174) :: (InputChar 'e') :: (State s175) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'e')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P18-} ((State s130) :: (State s172) :: (InputChar 'f') :: (State s173) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'f')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P19-} ((State s130) :: (State s170) :: (InputChar 'g') :: (State s171) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'g')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P20-} ((State s130) :: (State s168) :: (InputChar 'h') :: (State s169) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'h')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P21-} ((State s130) :: (State s166) :: (InputChar 'i') :: (State s167) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'i')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P22-} ((State s130) :: (State s164) :: (InputChar 'j') :: (State s165) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'j')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P23-} ((State s130) :: (State s162) :: (InputChar 'k') :: (State s163) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'k')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P24-} ((State s130) :: (State s160) :: (InputChar 'l') :: (State s161) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'l')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P25-} ((State s130) :: (State s158) :: (InputChar 'm') :: (State s159) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'm')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P26-} ((State s130) :: (State s156) :: (InputChar 'n') :: (State s157) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'n')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P27-} ((State s130) :: (State s154) :: (InputChar 'o') :: (State s155) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'o')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P28-} ((State s130) :: (State s152) :: (InputChar 'p') :: (State s153) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'p')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P29-} ((State s130) :: (State s150) :: (InputChar 'q') :: (State s151) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'q')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P30-} ((State s130) :: (State s148) :: (InputChar 'r') :: (State s149) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'r')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P31-} ((State s130) :: (State s146) :: (InputChar 's') :: (State s147) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 's')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P32-} ((State s130) :: (State s144) :: (InputChar 't') :: (State s145) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 't')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P33-} ((State s130) :: (State s142) :: (InputChar 'u') :: (State s143) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'u')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P34-} ((State s130) :: (State s140) :: (InputChar 'v') :: (State s141) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'v')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P35-} ((State s130) :: (State s138) :: (InputChar 'w') :: (State s139) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'w')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P36-} ((State s130) :: (State s136) :: (InputChar 'x') :: (State s137) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'x')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P37-} ((State s130) :: (State s134) :: (InputChar 'y') :: (State s135) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'y')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P38-} ((State s130) :: (State s132) :: (InputChar 'z') :: (State s133) :: (State s131) :: rest) = just (((State s130) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'z')))) :: (State s131) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P40-} ((State s71) :: (State s73) :: (State s74) :: (ParseTree (parsed-id-range-3 x0)) :: (State s75) :: (State s128) :: (State s71) :: (ParseTree (parsed-id-plus-4 x1)) :: (State s72) :: rest) = just (((State s71) :: (ParseTree (parsed-id-plus-4 (string-append 1 x0 x1))) :: (State s72) :: rest)
 , <-iter-suc-trans 5 (length rest))
len-dec-rewrite {- P13-} ((State s74) :: (State s126) :: (InputChar 'a') :: (State s127) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'a')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P14-} ((State s74) :: (State s124) :: (InputChar 'b') :: (State s125) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'b')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P15-} ((State s74) :: (State s122) :: (InputChar 'c') :: (State s123) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'c')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P16-} ((State s74) :: (State s120) :: (InputChar 'd') :: (State s121) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'd')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P17-} ((State s74) :: (State s118) :: (InputChar 'e') :: (State s119) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'e')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P18-} ((State s74) :: (State s116) :: (InputChar 'f') :: (State s117) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'f')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P19-} ((State s74) :: (State s114) :: (InputChar 'g') :: (State s115) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'g')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P20-} ((State s74) :: (State s112) :: (InputChar 'h') :: (State s113) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'h')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P21-} ((State s74) :: (State s110) :: (InputChar 'i') :: (State s111) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'i')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P22-} ((State s74) :: (State s108) :: (InputChar 'j') :: (State s109) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'j')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P23-} ((State s74) :: (State s106) :: (InputChar 'k') :: (State s107) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'k')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P24-} ((State s74) :: (State s104) :: (InputChar 'l') :: (State s105) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'l')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P25-} ((State s74) :: (State s102) :: (InputChar 'm') :: (State s103) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'm')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P26-} ((State s74) :: (State s100) :: (InputChar 'n') :: (State s101) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'n')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P27-} ((State s74) :: (State s98) :: (InputChar 'o') :: (State s99) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'o')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P28-} ((State s74) :: (State s96) :: (InputChar 'p') :: (State s97) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'p')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P29-} ((State s74) :: (State s94) :: (InputChar 'q') :: (State s95) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'q')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P30-} ((State s74) :: (State s92) :: (InputChar 'r') :: (State s93) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'r')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P31-} ((State s74) :: (State s90) :: (InputChar 's') :: (State s91) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 's')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P32-} ((State s74) :: (State s88) :: (InputChar 't') :: (State s89) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 't')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P33-} ((State s74) :: (State s86) :: (InputChar 'u') :: (State s87) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'u')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P34-} ((State s74) :: (State s84) :: (InputChar 'v') :: (State s85) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'v')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P35-} ((State s74) :: (State s82) :: (InputChar 'w') :: (State s83) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'w')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P36-} ((State s74) :: (State s80) :: (InputChar 'x') :: (State s81) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'x')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P37-} ((State s74) :: (State s78) :: (InputChar 'y') :: (State s79) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'y')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P38-} ((State s74) :: (State s76) :: (InputChar 'z') :: (State s77) :: (State s75) :: rest) = just (((State s74) :: (ParseTree (parsed-id-range-3 (string-append 0 (charToString 'z')))) :: (State s75) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- Num-} ((State s2) :: (State s14) :: (State s15) :: (ParseTree (parsed-num x0)) :: (State s16) :: (State s3) :: rest) = just (((State s2) :: (ParseTree (parsed-expr (norm-expr (Num x0)))) :: (State s3) :: rest)
 , <-iter-suc-trans 2 (length rest))
len-dec-rewrite {- P12-} ((State s15) :: (State s17) :: (State s18) :: (ParseTree (parsed-num-plus-2 x0)) :: (State s19) :: (State s16) :: rest) = just (((State s15) :: (ParseTree (parsed-num (string-append 0 x0))) :: (State s16) :: rest)
 , <-iter-suc-trans 2 (length rest))
len-dec-rewrite {- P10-} ((State s18) :: (State s44) :: (State s45) :: (ParseTree (parsed-num-range-1 x0)) :: (State s46) :: (State s19) :: rest) = just (((State s18) :: (ParseTree (parsed-num-plus-2 (string-append 0 x0))) :: (State s19) :: rest)
 , <-iter-suc-trans 2 (length rest))
len-dec-rewrite {- P0-} ((State s45) :: (State s65) :: (InputChar '0') :: (State s66) :: (State s46) :: rest) = just (((State s45) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '0')))) :: (State s46) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P1-} ((State s45) :: (State s63) :: (InputChar '1') :: (State s64) :: (State s46) :: rest) = just (((State s45) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '1')))) :: (State s46) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P2-} ((State s45) :: (State s61) :: (InputChar '2') :: (State s62) :: (State s46) :: rest) = just (((State s45) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '2')))) :: (State s46) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P3-} ((State s45) :: (State s59) :: (InputChar '3') :: (State s60) :: (State s46) :: rest) = just (((State s45) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '3')))) :: (State s46) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P4-} ((State s45) :: (State s57) :: (InputChar '4') :: (State s58) :: (State s46) :: rest) = just (((State s45) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '4')))) :: (State s46) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P5-} ((State s45) :: (State s55) :: (InputChar '5') :: (State s56) :: (State s46) :: rest) = just (((State s45) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '5')))) :: (State s46) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P6-} ((State s45) :: (State s53) :: (InputChar '6') :: (State s54) :: (State s46) :: rest) = just (((State s45) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '6')))) :: (State s46) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P7-} ((State s45) :: (State s51) :: (InputChar '7') :: (State s52) :: (State s46) :: rest) = just (((State s45) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '7')))) :: (State s46) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P8-} ((State s45) :: (State s49) :: (InputChar '8') :: (State s50) :: (State s46) :: rest) = just (((State s45) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '8')))) :: (State s46) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P9-} ((State s45) :: (State s47) :: (InputChar '9') :: (State s48) :: (State s46) :: rest) = just (((State s45) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '9')))) :: (State s46) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P11-} ((State s18) :: (State s20) :: (State s21) :: (ParseTree (parsed-num-range-1 x0)) :: (State s22) :: (State s43) :: (State s18) :: (ParseTree (parsed-num-plus-2 x1)) :: (State s19) :: rest) = just (((State s18) :: (ParseTree (parsed-num-plus-2 (string-append 1 x0 x1))) :: (State s19) :: rest)
 , <-iter-suc-trans 5 (length rest))
len-dec-rewrite {- P0-} ((State s21) :: (State s41) :: (InputChar '0') :: (State s42) :: (State s22) :: rest) = just (((State s21) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '0')))) :: (State s22) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P1-} ((State s21) :: (State s39) :: (InputChar '1') :: (State s40) :: (State s22) :: rest) = just (((State s21) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '1')))) :: (State s22) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P2-} ((State s21) :: (State s37) :: (InputChar '2') :: (State s38) :: (State s22) :: rest) = just (((State s21) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '2')))) :: (State s22) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P3-} ((State s21) :: (State s35) :: (InputChar '3') :: (State s36) :: (State s22) :: rest) = just (((State s21) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '3')))) :: (State s22) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P4-} ((State s21) :: (State s33) :: (InputChar '4') :: (State s34) :: (State s22) :: rest) = just (((State s21) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '4')))) :: (State s22) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P5-} ((State s21) :: (State s31) :: (InputChar '5') :: (State s32) :: (State s22) :: rest) = just (((State s21) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '5')))) :: (State s22) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P6-} ((State s21) :: (State s29) :: (InputChar '6') :: (State s30) :: (State s22) :: rest) = just (((State s21) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '6')))) :: (State s22) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P7-} ((State s21) :: (State s27) :: (InputChar '7') :: (State s28) :: (State s22) :: rest) = just (((State s21) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '7')))) :: (State s22) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P8-} ((State s21) :: (State s25) :: (InputChar '8') :: (State s26) :: (State s22) :: rest) = just (((State s21) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '8')))) :: (State s22) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- P9-} ((State s21) :: (State s23) :: (InputChar '9') :: (State s24) :: (State s22) :: rest) = just (((State s21) :: (ParseTree (parsed-num-range-1 (string-append 0 (charToString '9')))) :: (State s22) :: rest)
 , <-iter-suc-trans 1 (length rest))
len-dec-rewrite {- Parens-} ((State s2) :: (State s10) :: (InputChar '(') :: (State s11) :: (State s2) :: (ParseTree (parsed-expr x0)) :: (State s3) :: (State s12) :: (InputChar ')') :: (State s13) :: (State s3) :: rest) = just (((State s2) :: (ParseTree (parsed-expr (norm-expr (Parens x0)))) :: (State s3) :: rest)
 , <-iter-suc-trans 7 (length rest))
len-dec-rewrite {- Plus-} ((State s2) :: (ParseTree (parsed-expr x0)) :: (State s3) :: (State s8) :: (InputChar '+') :: (State s9) :: (State s2) :: (ParseTree (parsed-expr x1)) :: (State s3) :: rest) = just (((State s2) :: (ParseTree (parsed-expr (norm-expr (Plus x0 x1)))) :: (State s3) :: rest)
 , <-iter-suc-trans 5 (length rest))
len-dec-rewrite {- Times-} ((State s2) :: (ParseTree (parsed-expr x0)) :: (State s3) :: (State s5) :: (InputChar '*') :: (State s6) :: (State s2) :: (ParseTree (parsed-expr x1)) :: (State s3) :: rest) = just (((State s2) :: (ParseTree (parsed-expr (norm-expr (Times x0 x1)))) :: (State s3) :: rest)
 , <-iter-suc-trans 5 (length rest))
len-dec-rewrite x = nothing

rrs : rewriteRules
rrs = record { eps-rewrite = eps-rewrite ; unit-rewrite = unit-rewrite ; unit-rewrite-iters = 0 ; len-dec-rewrite = len-dec-rewrite}


More information about the Agda mailing list