// This script verifies that Every length-n integer x,
// where n >= 8, AND n is even, AND x is even,
// is the sum of EXACTLY 7 numbers:
//        -  6 palindromes of length n-3
//        and
//        - 2^i for 1 <= i <= n

NestedWordAutomaton palCheckerSIX = (
callAlphabet = { a b },
internalAlphabet = { c d },
returnAlphabet = { e f },
states = { 
f_0_ZERO f_0_ONE f_0_TWO f_0_THREE f_0_FOUR f_0_FIVE f_0_SIX 
f_1_ZERO f_1_ONE f_1_TWO f_1_THREE f_1_FOUR f_1_FIVE f_1_SIX 
f_2_ZERO f_2_ONE f_2_TWO f_2_THREE f_2_FOUR f_2_FIVE f_2_SIX 
f_3_ZERO f_3_ONE f_3_TWO f_3_THREE f_3_FOUR f_3_FIVE f_3_SIX 
f_4_ZERO f_4_ONE f_4_TWO f_4_THREE f_4_FOUR f_4_FIVE f_4_SIX 
f_5_ZERO f_5_ONE f_5_TWO f_5_THREE f_5_FOUR f_5_FIVE f_5_SIX 
g_0_ZERO g_0_ONE g_0_TWO g_0_THREE g_0_FOUR g_0_FIVE g_0_SIX 
g_1_ZERO g_1_ONE g_1_TWO g_1_THREE g_1_FOUR g_1_FIVE g_1_SIX 
g_2_ZERO g_2_ONE g_2_TWO g_2_THREE g_2_FOUR g_2_FIVE g_2_SIX 
g_3_ZERO g_3_ONE g_3_TWO g_3_THREE g_3_FOUR g_3_FIVE g_3_SIX 
g_4_ZERO g_4_ONE g_4_TWO g_4_THREE g_4_FOUR g_4_FIVE g_4_SIX 
g_5_ZERO g_5_ONE g_5_TWO g_5_THREE g_5_FOUR g_5_FIVE g_5_SIX 
g_6_ZERO g_6_ONE g_6_TWO g_6_THREE g_6_FOUR g_6_FIVE g_6_SIX 
t0 t1 t2 t3 t4 t5 t6 s0 s1 s2 s3 s4 s5 s6 q n0 n1 m0 l1 l2 acc},
initialStates = {f_0_SIX},
finalStates = {acc},
callTransitions = {
(f_0_ZERO a f_0_ZERO)
(f_0_ZERO a f_0_ONE)
(f_0_ZERO a f_0_TWO)
(f_0_ZERO a f_0_THREE)
(f_0_ZERO a f_0_FOUR)
(f_0_ZERO a f_0_FIVE)
(f_0_ZERO a f_0_SIX)

(f_0_ONE b f_0_ZERO)
(f_0_ONE b f_0_ONE)
(f_0_ONE b f_0_TWO)
(f_0_ONE b f_0_THREE)
(f_0_ONE b f_0_FOUR)
(f_0_ONE b f_0_FIVE)
(f_0_ONE b f_0_SIX)

(f_0_TWO a f_1_ZERO)
(f_0_TWO a f_1_ONE)
(f_0_TWO a f_1_TWO)
(f_0_TWO a f_1_THREE)
(f_0_TWO a f_1_FOUR)
(f_0_TWO a f_1_FIVE)
(f_0_TWO a f_1_SIX)

(f_0_THREE b f_1_ZERO)
(f_0_THREE b f_1_ONE)
(f_0_THREE b f_1_TWO)
(f_0_THREE b f_1_THREE)
(f_0_THREE b f_1_FOUR)
(f_0_THREE b f_1_FIVE)
(f_0_THREE b f_1_SIX)

(f_0_FOUR a f_2_ZERO)
(f_0_FOUR a f_2_ONE)
(f_0_FOUR a f_2_TWO)
(f_0_FOUR a f_2_THREE)
(f_0_FOUR a f_2_FOUR)
(f_0_FOUR a f_2_FIVE)
(f_0_FOUR a f_2_SIX)

(f_0_FIVE b f_2_ZERO)
(f_0_FIVE b f_2_ONE)
(f_0_FIVE b f_2_TWO)
(f_0_FIVE b f_2_THREE)
(f_0_FIVE b f_2_FOUR)
(f_0_FIVE b f_2_FIVE)
(f_0_FIVE b f_2_SIX)

(f_0_SIX a f_3_ZERO)
(f_0_SIX a f_3_ONE)
(f_0_SIX a f_3_TWO)
(f_0_SIX a f_3_THREE)
(f_0_SIX a f_3_FOUR)
(f_0_SIX a f_3_FIVE)
(f_0_SIX a f_3_SIX)

(f_1_ZERO b f_0_ZERO)
(f_1_ZERO b f_0_ONE)
(f_1_ZERO b f_0_TWO)
(f_1_ZERO b f_0_THREE)
(f_1_ZERO b f_0_FOUR)
(f_1_ZERO b f_0_FIVE)
(f_1_ZERO b f_0_SIX)

(f_1_ONE a f_1_ZERO)
(f_1_ONE a f_1_ONE)
(f_1_ONE a f_1_TWO)
(f_1_ONE a f_1_THREE)
(f_1_ONE a f_1_FOUR)
(f_1_ONE a f_1_FIVE)
(f_1_ONE a f_1_SIX)

(f_1_TWO b f_1_ZERO)
(f_1_TWO b f_1_ONE)
(f_1_TWO b f_1_TWO)
(f_1_TWO b f_1_THREE)
(f_1_TWO b f_1_FOUR)
(f_1_TWO b f_1_FIVE)
(f_1_TWO b f_1_SIX)

(f_1_THREE a f_2_ZERO)
(f_1_THREE a f_2_ONE)
(f_1_THREE a f_2_TWO)
(f_1_THREE a f_2_THREE)
(f_1_THREE a f_2_FOUR)
(f_1_THREE a f_2_FIVE)
(f_1_THREE a f_2_SIX)

(f_1_FOUR b f_2_ZERO)
(f_1_FOUR b f_2_ONE)
(f_1_FOUR b f_2_TWO)
(f_1_FOUR b f_2_THREE)
(f_1_FOUR b f_2_FOUR)
(f_1_FOUR b f_2_FIVE)
(f_1_FOUR b f_2_SIX)

(f_1_FIVE a f_3_ZERO)
(f_1_FIVE a f_3_ONE)
(f_1_FIVE a f_3_TWO)
(f_1_FIVE a f_3_THREE)
(f_1_FIVE a f_3_FOUR)
(f_1_FIVE a f_3_FIVE)
(f_1_FIVE a f_3_SIX)

(f_1_SIX b f_3_ZERO)
(f_1_SIX b f_3_ONE)
(f_1_SIX b f_3_TWO)
(f_1_SIX b f_3_THREE)
(f_1_SIX b f_3_FOUR)
(f_1_SIX b f_3_FIVE)
(f_1_SIX b f_3_SIX)

(f_2_ZERO a f_1_ZERO)
(f_2_ZERO a f_1_ONE)
(f_2_ZERO a f_1_TWO)
(f_2_ZERO a f_1_THREE)
(f_2_ZERO a f_1_FOUR)
(f_2_ZERO a f_1_FIVE)
(f_2_ZERO a f_1_SIX)

(f_2_ONE b f_1_ZERO)
(f_2_ONE b f_1_ONE)
(f_2_ONE b f_1_TWO)
(f_2_ONE b f_1_THREE)
(f_2_ONE b f_1_FOUR)
(f_2_ONE b f_1_FIVE)
(f_2_ONE b f_1_SIX)

(f_2_TWO a f_2_ZERO)
(f_2_TWO a f_2_ONE)
(f_2_TWO a f_2_TWO)
(f_2_TWO a f_2_THREE)
(f_2_TWO a f_2_FOUR)
(f_2_TWO a f_2_FIVE)
(f_2_TWO a f_2_SIX)

(f_2_THREE b f_2_ZERO)
(f_2_THREE b f_2_ONE)
(f_2_THREE b f_2_TWO)
(f_2_THREE b f_2_THREE)
(f_2_THREE b f_2_FOUR)
(f_2_THREE b f_2_FIVE)
(f_2_THREE b f_2_SIX)

(f_2_FOUR a f_3_ZERO)
(f_2_FOUR a f_3_ONE)
(f_2_FOUR a f_3_TWO)
(f_2_FOUR a f_3_THREE)
(f_2_FOUR a f_3_FOUR)
(f_2_FOUR a f_3_FIVE)
(f_2_FOUR a f_3_SIX)

(f_2_FIVE b f_3_ZERO)
(f_2_FIVE b f_3_ONE)
(f_2_FIVE b f_3_TWO)
(f_2_FIVE b f_3_THREE)
(f_2_FIVE b f_3_FOUR)
(f_2_FIVE b f_3_FIVE)
(f_2_FIVE b f_3_SIX)

(f_2_SIX a f_4_ZERO)
(f_2_SIX a f_4_ONE)
(f_2_SIX a f_4_TWO)
(f_2_SIX a f_4_THREE)
(f_2_SIX a f_4_FOUR)
(f_2_SIX a f_4_FIVE)
(f_2_SIX a f_4_SIX)

(f_3_ZERO b f_1_ZERO)
(f_3_ZERO b f_1_ONE)
(f_3_ZERO b f_1_TWO)
(f_3_ZERO b f_1_THREE)
(f_3_ZERO b f_1_FOUR)
(f_3_ZERO b f_1_FIVE)
(f_3_ZERO b f_1_SIX)

(f_3_ONE a f_2_ZERO)
(f_3_ONE a f_2_ONE)
(f_3_ONE a f_2_TWO)
(f_3_ONE a f_2_THREE)
(f_3_ONE a f_2_FOUR)
(f_3_ONE a f_2_FIVE)
(f_3_ONE a f_2_SIX)

(f_3_TWO b f_2_ZERO)
(f_3_TWO b f_2_ONE)
(f_3_TWO b f_2_TWO)
(f_3_TWO b f_2_THREE)
(f_3_TWO b f_2_FOUR)
(f_3_TWO b f_2_FIVE)
(f_3_TWO b f_2_SIX)

(f_3_THREE a f_3_ZERO)
(f_3_THREE a f_3_ONE)
(f_3_THREE a f_3_TWO)
(f_3_THREE a f_3_THREE)
(f_3_THREE a f_3_FOUR)
(f_3_THREE a f_3_FIVE)
(f_3_THREE a f_3_SIX)

(f_3_FOUR b f_3_ZERO)
(f_3_FOUR b f_3_ONE)
(f_3_FOUR b f_3_TWO)
(f_3_FOUR b f_3_THREE)
(f_3_FOUR b f_3_FOUR)
(f_3_FOUR b f_3_FIVE)
(f_3_FOUR b f_3_SIX)

(f_3_FIVE a f_4_ZERO)
(f_3_FIVE a f_4_ONE)
(f_3_FIVE a f_4_TWO)
(f_3_FIVE a f_4_THREE)
(f_3_FIVE a f_4_FOUR)
(f_3_FIVE a f_4_FIVE)
(f_3_FIVE a f_4_SIX)

(f_3_SIX b f_4_ZERO)
(f_3_SIX b f_4_ONE)
(f_3_SIX b f_4_TWO)
(f_3_SIX b f_4_THREE)
(f_3_SIX b f_4_FOUR)
(f_3_SIX b f_4_FIVE)
(f_3_SIX b f_4_SIX)

(f_4_ZERO a f_2_ZERO)
(f_4_ZERO a f_2_ONE)
(f_4_ZERO a f_2_TWO)
(f_4_ZERO a f_2_THREE)
(f_4_ZERO a f_2_FOUR)
(f_4_ZERO a f_2_FIVE)
(f_4_ZERO a f_2_SIX)

(f_4_ONE b f_2_ZERO)
(f_4_ONE b f_2_ONE)
(f_4_ONE b f_2_TWO)
(f_4_ONE b f_2_THREE)
(f_4_ONE b f_2_FOUR)
(f_4_ONE b f_2_FIVE)
(f_4_ONE b f_2_SIX)

(f_4_TWO a f_3_ZERO)
(f_4_TWO a f_3_ONE)
(f_4_TWO a f_3_TWO)
(f_4_TWO a f_3_THREE)
(f_4_TWO a f_3_FOUR)
(f_4_TWO a f_3_FIVE)
(f_4_TWO a f_3_SIX)

(f_4_THREE b f_3_ZERO)
(f_4_THREE b f_3_ONE)
(f_4_THREE b f_3_TWO)
(f_4_THREE b f_3_THREE)
(f_4_THREE b f_3_FOUR)
(f_4_THREE b f_3_FIVE)
(f_4_THREE b f_3_SIX)

(f_4_FOUR a f_4_ZERO)
(f_4_FOUR a f_4_ONE)
(f_4_FOUR a f_4_TWO)
(f_4_FOUR a f_4_THREE)
(f_4_FOUR a f_4_FOUR)
(f_4_FOUR a f_4_FIVE)
(f_4_FOUR a f_4_SIX)

(f_4_FIVE b f_4_ZERO)
(f_4_FIVE b f_4_ONE)
(f_4_FIVE b f_4_TWO)
(f_4_FIVE b f_4_THREE)
(f_4_FIVE b f_4_FOUR)
(f_4_FIVE b f_4_FIVE)
(f_4_FIVE b f_4_SIX)

(f_4_SIX a f_5_ZERO)
(f_4_SIX a f_5_ONE)
(f_4_SIX a f_5_TWO)
(f_4_SIX a f_5_THREE)
(f_4_SIX a f_5_FOUR)
(f_4_SIX a f_5_FIVE)
(f_4_SIX a f_5_SIX)

(f_5_ZERO b f_2_ZERO)
(f_5_ZERO b f_2_ONE)
(f_5_ZERO b f_2_TWO)
(f_5_ZERO b f_2_THREE)
(f_5_ZERO b f_2_FOUR)
(f_5_ZERO b f_2_FIVE)
(f_5_ZERO b f_2_SIX)

(f_5_ONE a f_3_ZERO)
(f_5_ONE a f_3_ONE)
(f_5_ONE a f_3_TWO)
(f_5_ONE a f_3_THREE)
(f_5_ONE a f_3_FOUR)
(f_5_ONE a f_3_FIVE)
(f_5_ONE a f_3_SIX)

(f_5_TWO b f_3_ZERO)
(f_5_TWO b f_3_ONE)
(f_5_TWO b f_3_TWO)
(f_5_TWO b f_3_THREE)
(f_5_TWO b f_3_FOUR)
(f_5_TWO b f_3_FIVE)
(f_5_TWO b f_3_SIX)

(f_5_THREE a f_4_ZERO)
(f_5_THREE a f_4_ONE)
(f_5_THREE a f_4_TWO)
(f_5_THREE a f_4_THREE)
(f_5_THREE a f_4_FOUR)
(f_5_THREE a f_4_FIVE)
(f_5_THREE a f_4_SIX)

(f_5_FOUR b f_4_ZERO)
(f_5_FOUR b f_4_ONE)
(f_5_FOUR b f_4_TWO)
(f_5_FOUR b f_4_THREE)
(f_5_FOUR b f_4_FOUR)
(f_5_FOUR b f_4_FIVE)
(f_5_FOUR b f_4_SIX)

(f_5_FIVE a f_5_ZERO)
(f_5_FIVE a f_5_ONE)
(f_5_FIVE a f_5_TWO)
(f_5_FIVE a f_5_THREE)
(f_5_FIVE a f_5_FOUR)
(f_5_FIVE a f_5_FIVE)
(f_5_FIVE a f_5_SIX)

(f_5_SIX b f_5_ZERO)
(f_5_SIX b f_5_ONE)
(f_5_SIX b f_5_TWO)
(f_5_SIX b f_5_THREE)
(f_5_SIX b f_5_FOUR)
(f_5_SIX b f_5_FIVE)
(f_5_SIX b f_5_SIX)


(g_0_ZERO a g_0_ZERO)
(g_0_ZERO a g_0_ONE)
(g_0_ZERO a g_0_TWO)
(g_0_ZERO a g_0_THREE)
(g_0_ZERO a g_0_FOUR)
(g_0_ZERO a g_0_FIVE)
(g_0_ZERO a g_0_SIX)

(g_0_ONE b g_0_ZERO)
(g_0_ONE b g_0_ONE)
(g_0_ONE b g_0_TWO)
(g_0_ONE b g_0_THREE)
(g_0_ONE b g_0_FOUR)
(g_0_ONE b g_0_FIVE)
(g_0_ONE b g_0_SIX)

(g_0_TWO a g_1_ZERO)
(g_0_TWO a g_1_ONE)
(g_0_TWO a g_1_TWO)
(g_0_TWO a g_1_THREE)
(g_0_TWO a g_1_FOUR)
(g_0_TWO a g_1_FIVE)
(g_0_TWO a g_1_SIX)

(g_0_THREE b g_1_ZERO)
(g_0_THREE b g_1_ONE)
(g_0_THREE b g_1_TWO)
(g_0_THREE b g_1_THREE)
(g_0_THREE b g_1_FOUR)
(g_0_THREE b g_1_FIVE)
(g_0_THREE b g_1_SIX)

(g_0_FOUR a g_2_ZERO)
(g_0_FOUR a g_2_ONE)
(g_0_FOUR a g_2_TWO)
(g_0_FOUR a g_2_THREE)
(g_0_FOUR a g_2_FOUR)
(g_0_FOUR a g_2_FIVE)
(g_0_FOUR a g_2_SIX)

(g_0_FIVE b g_2_ZERO)
(g_0_FIVE b g_2_ONE)
(g_0_FIVE b g_2_TWO)
(g_0_FIVE b g_2_THREE)
(g_0_FIVE b g_2_FOUR)
(g_0_FIVE b g_2_FIVE)
(g_0_FIVE b g_2_SIX)

(g_0_SIX a g_3_ZERO)
(g_0_SIX a g_3_ONE)
(g_0_SIX a g_3_TWO)
(g_0_SIX a g_3_THREE)
(g_0_SIX a g_3_FOUR)
(g_0_SIX a g_3_FIVE)
(g_0_SIX a g_3_SIX)

(g_1_ZERO b g_0_ZERO)
(g_1_ZERO b g_0_ONE)
(g_1_ZERO b g_0_TWO)
(g_1_ZERO b g_0_THREE)
(g_1_ZERO b g_0_FOUR)
(g_1_ZERO b g_0_FIVE)
(g_1_ZERO b g_0_SIX)

(g_1_ONE a g_1_ZERO)
(g_1_ONE a g_1_ONE)
(g_1_ONE a g_1_TWO)
(g_1_ONE a g_1_THREE)
(g_1_ONE a g_1_FOUR)
(g_1_ONE a g_1_FIVE)
(g_1_ONE a g_1_SIX)

(g_1_TWO b g_1_ZERO)
(g_1_TWO b g_1_ONE)
(g_1_TWO b g_1_TWO)
(g_1_TWO b g_1_THREE)
(g_1_TWO b g_1_FOUR)
(g_1_TWO b g_1_FIVE)
(g_1_TWO b g_1_SIX)

(g_1_THREE a g_2_ZERO)
(g_1_THREE a g_2_ONE)
(g_1_THREE a g_2_TWO)
(g_1_THREE a g_2_THREE)
(g_1_THREE a g_2_FOUR)
(g_1_THREE a g_2_FIVE)
(g_1_THREE a g_2_SIX)

(g_1_FOUR b g_2_ZERO)
(g_1_FOUR b g_2_ONE)
(g_1_FOUR b g_2_TWO)
(g_1_FOUR b g_2_THREE)
(g_1_FOUR b g_2_FOUR)
(g_1_FOUR b g_2_FIVE)
(g_1_FOUR b g_2_SIX)

(g_1_FIVE a g_3_ZERO)
(g_1_FIVE a g_3_ONE)
(g_1_FIVE a g_3_TWO)
(g_1_FIVE a g_3_THREE)
(g_1_FIVE a g_3_FOUR)
(g_1_FIVE a g_3_FIVE)
(g_1_FIVE a g_3_SIX)

(g_1_SIX b g_3_ZERO)
(g_1_SIX b g_3_ONE)
(g_1_SIX b g_3_TWO)
(g_1_SIX b g_3_THREE)
(g_1_SIX b g_3_FOUR)
(g_1_SIX b g_3_FIVE)
(g_1_SIX b g_3_SIX)

(g_2_ZERO a g_1_ZERO)
(g_2_ZERO a g_1_ONE)
(g_2_ZERO a g_1_TWO)
(g_2_ZERO a g_1_THREE)
(g_2_ZERO a g_1_FOUR)
(g_2_ZERO a g_1_FIVE)
(g_2_ZERO a g_1_SIX)

(g_2_ONE b g_1_ZERO)
(g_2_ONE b g_1_ONE)
(g_2_ONE b g_1_TWO)
(g_2_ONE b g_1_THREE)
(g_2_ONE b g_1_FOUR)
(g_2_ONE b g_1_FIVE)
(g_2_ONE b g_1_SIX)

(g_2_TWO a g_2_ZERO)
(g_2_TWO a g_2_ONE)
(g_2_TWO a g_2_TWO)
(g_2_TWO a g_2_THREE)
(g_2_TWO a g_2_FOUR)
(g_2_TWO a g_2_FIVE)
(g_2_TWO a g_2_SIX)

(g_2_THREE b g_2_ZERO)
(g_2_THREE b g_2_ONE)
(g_2_THREE b g_2_TWO)
(g_2_THREE b g_2_THREE)
(g_2_THREE b g_2_FOUR)
(g_2_THREE b g_2_FIVE)
(g_2_THREE b g_2_SIX)

(g_2_FOUR a g_3_ZERO)
(g_2_FOUR a g_3_ONE)
(g_2_FOUR a g_3_TWO)
(g_2_FOUR a g_3_THREE)
(g_2_FOUR a g_3_FOUR)
(g_2_FOUR a g_3_FIVE)
(g_2_FOUR a g_3_SIX)

(g_2_FIVE b g_3_ZERO)
(g_2_FIVE b g_3_ONE)
(g_2_FIVE b g_3_TWO)
(g_2_FIVE b g_3_THREE)
(g_2_FIVE b g_3_FOUR)
(g_2_FIVE b g_3_FIVE)
(g_2_FIVE b g_3_SIX)

(g_2_SIX a g_4_ZERO)
(g_2_SIX a g_4_ONE)
(g_2_SIX a g_4_TWO)
(g_2_SIX a g_4_THREE)
(g_2_SIX a g_4_FOUR)
(g_2_SIX a g_4_FIVE)
(g_2_SIX a g_4_SIX)

(g_3_ZERO b g_1_ZERO)
(g_3_ZERO b g_1_ONE)
(g_3_ZERO b g_1_TWO)
(g_3_ZERO b g_1_THREE)
(g_3_ZERO b g_1_FOUR)
(g_3_ZERO b g_1_FIVE)
(g_3_ZERO b g_1_SIX)

(g_3_ONE a g_2_ZERO)
(g_3_ONE a g_2_ONE)
(g_3_ONE a g_2_TWO)
(g_3_ONE a g_2_THREE)
(g_3_ONE a g_2_FOUR)
(g_3_ONE a g_2_FIVE)
(g_3_ONE a g_2_SIX)

(g_3_TWO b g_2_ZERO)
(g_3_TWO b g_2_ONE)
(g_3_TWO b g_2_TWO)
(g_3_TWO b g_2_THREE)
(g_3_TWO b g_2_FOUR)
(g_3_TWO b g_2_FIVE)
(g_3_TWO b g_2_SIX)

(g_3_THREE a g_3_ZERO)
(g_3_THREE a g_3_ONE)
(g_3_THREE a g_3_TWO)
(g_3_THREE a g_3_THREE)
(g_3_THREE a g_3_FOUR)
(g_3_THREE a g_3_FIVE)
(g_3_THREE a g_3_SIX)

(g_3_FOUR b g_3_ZERO)
(g_3_FOUR b g_3_ONE)
(g_3_FOUR b g_3_TWO)
(g_3_FOUR b g_3_THREE)
(g_3_FOUR b g_3_FOUR)
(g_3_FOUR b g_3_FIVE)
(g_3_FOUR b g_3_SIX)

(g_3_FIVE a g_4_ZERO)
(g_3_FIVE a g_4_ONE)
(g_3_FIVE a g_4_TWO)
(g_3_FIVE a g_4_THREE)
(g_3_FIVE a g_4_FOUR)
(g_3_FIVE a g_4_FIVE)
(g_3_FIVE a g_4_SIX)

(g_3_SIX b g_4_ZERO)
(g_3_SIX b g_4_ONE)
(g_3_SIX b g_4_TWO)
(g_3_SIX b g_4_THREE)
(g_3_SIX b g_4_FOUR)
(g_3_SIX b g_4_FIVE)
(g_3_SIX b g_4_SIX)

(g_4_ZERO a g_2_ZERO)
(g_4_ZERO a g_2_ONE)
(g_4_ZERO a g_2_TWO)
(g_4_ZERO a g_2_THREE)
(g_4_ZERO a g_2_FOUR)
(g_4_ZERO a g_2_FIVE)
(g_4_ZERO a g_2_SIX)

(g_4_ONE b g_2_ZERO)
(g_4_ONE b g_2_ONE)
(g_4_ONE b g_2_TWO)
(g_4_ONE b g_2_THREE)
(g_4_ONE b g_2_FOUR)
(g_4_ONE b g_2_FIVE)
(g_4_ONE b g_2_SIX)

(g_4_TWO a g_3_ZERO)
(g_4_TWO a g_3_ONE)
(g_4_TWO a g_3_TWO)
(g_4_TWO a g_3_THREE)
(g_4_TWO a g_3_FOUR)
(g_4_TWO a g_3_FIVE)
(g_4_TWO a g_3_SIX)

(g_4_THREE b g_3_ZERO)
(g_4_THREE b g_3_ONE)
(g_4_THREE b g_3_TWO)
(g_4_THREE b g_3_THREE)
(g_4_THREE b g_3_FOUR)
(g_4_THREE b g_3_FIVE)
(g_4_THREE b g_3_SIX)

(g_4_FOUR a g_4_ZERO)
(g_4_FOUR a g_4_ONE)
(g_4_FOUR a g_4_TWO)
(g_4_FOUR a g_4_THREE)
(g_4_FOUR a g_4_FOUR)
(g_4_FOUR a g_4_FIVE)
(g_4_FOUR a g_4_SIX)

(g_4_FIVE b g_4_ZERO)
(g_4_FIVE b g_4_ONE)
(g_4_FIVE b g_4_TWO)
(g_4_FIVE b g_4_THREE)
(g_4_FIVE b g_4_FOUR)
(g_4_FIVE b g_4_FIVE)
(g_4_FIVE b g_4_SIX)

(g_4_SIX a g_5_ZERO)
(g_4_SIX a g_5_ONE)
(g_4_SIX a g_5_TWO)
(g_4_SIX a g_5_THREE)
(g_4_SIX a g_5_FOUR)
(g_4_SIX a g_5_FIVE)
(g_4_SIX a g_5_SIX)

(g_5_ZERO b g_2_ZERO)
(g_5_ZERO b g_2_ONE)
(g_5_ZERO b g_2_TWO)
(g_5_ZERO b g_2_THREE)
(g_5_ZERO b g_2_FOUR)
(g_5_ZERO b g_2_FIVE)
(g_5_ZERO b g_2_SIX)

(g_5_ONE a g_3_ZERO)
(g_5_ONE a g_3_ONE)
(g_5_ONE a g_3_TWO)
(g_5_ONE a g_3_THREE)
(g_5_ONE a g_3_FOUR)
(g_5_ONE a g_3_FIVE)
(g_5_ONE a g_3_SIX)

(g_5_TWO b g_3_ZERO)
(g_5_TWO b g_3_ONE)
(g_5_TWO b g_3_TWO)
(g_5_TWO b g_3_THREE)
(g_5_TWO b g_3_FOUR)
(g_5_TWO b g_3_FIVE)
(g_5_TWO b g_3_SIX)

(g_5_THREE a g_4_ZERO)
(g_5_THREE a g_4_ONE)
(g_5_THREE a g_4_TWO)
(g_5_THREE a g_4_THREE)
(g_5_THREE a g_4_FOUR)
(g_5_THREE a g_4_FIVE)
(g_5_THREE a g_4_SIX)

(g_5_FOUR b g_4_ZERO)
(g_5_FOUR b g_4_ONE)
(g_5_FOUR b g_4_TWO)
(g_5_FOUR b g_4_THREE)
(g_5_FOUR b g_4_FOUR)
(g_5_FOUR b g_4_FIVE)
(g_5_FOUR b g_4_SIX)

(g_5_FIVE a g_5_ZERO)
(g_5_FIVE a g_5_ONE)
(g_5_FIVE a g_5_TWO)
(g_5_FIVE a g_5_THREE)
(g_5_FIVE a g_5_FOUR)
(g_5_FIVE a g_5_FIVE)
(g_5_FIVE a g_5_SIX)

(g_5_SIX b g_5_ZERO)
(g_5_SIX b g_5_ONE)
(g_5_SIX b g_5_TWO)
(g_5_SIX b g_5_THREE)
(g_5_SIX b g_5_FOUR)
(g_5_SIX b g_5_FIVE)
(g_5_SIX b g_5_SIX)

(g_6_ZERO a g_3_ZERO)
(g_6_ZERO a g_3_ONE)
(g_6_ZERO a g_3_TWO)
(g_6_ZERO a g_3_THREE)
(g_6_ZERO a g_3_FOUR)
(g_6_ZERO a g_3_FIVE)
(g_6_ZERO a g_3_SIX)

(g_6_ONE b g_3_ZERO)
(g_6_ONE b g_3_ONE)
(g_6_ONE b g_3_TWO)
(g_6_ONE b g_3_THREE)
(g_6_ONE b g_3_FOUR)
(g_6_ONE b g_3_FIVE)
(g_6_ONE b g_3_SIX)

(g_6_TWO a g_4_ZERO)
(g_6_TWO a g_4_ONE)
(g_6_TWO a g_4_TWO)
(g_6_TWO a g_4_THREE)
(g_6_TWO a g_4_FOUR)
(g_6_TWO a g_4_FIVE)
(g_6_TWO a g_4_SIX)

(g_6_THREE b g_4_ZERO)
(g_6_THREE b g_4_ONE)
(g_6_THREE b g_4_TWO)
(g_6_THREE b g_4_THREE)
(g_6_THREE b g_4_FOUR)
(g_6_THREE b g_4_FIVE)
(g_6_THREE b g_4_SIX)

(g_6_FOUR a g_5_ZERO)
(g_6_FOUR a g_5_ONE)
(g_6_FOUR a g_5_TWO)
(g_6_FOUR a g_5_THREE)
(g_6_FOUR a g_5_FOUR)
(g_6_FOUR a g_5_FIVE)
(g_6_FOUR a g_5_SIX)

(g_6_FIVE b g_5_ZERO)
(g_6_FIVE b g_5_ONE)
(g_6_FIVE b g_5_TWO)
(g_6_FIVE b g_5_THREE)
(g_6_FIVE b g_5_FOUR)
(g_6_FIVE b g_5_FIVE)
(g_6_FIVE b g_5_SIX)

(g_6_SIX a g_6_ZERO)
(g_6_SIX a g_6_ONE)
(g_6_SIX a g_6_TWO)
(g_6_SIX a g_6_THREE)
(g_6_SIX a g_6_FOUR)
(g_6_SIX a g_6_FIVE)
(g_6_SIX a g_6_SIX)




(f_0_ZERO b g_0_ZERO)
(f_0_ZERO b g_0_ONE)
(f_0_ZERO b g_0_TWO)
(f_0_ZERO b g_0_THREE)
(f_0_ZERO b g_0_FOUR)
(f_0_ZERO b g_0_FIVE)
(f_0_ZERO b g_0_SIX)

(f_0_ONE a g_1_ZERO)
(f_0_ONE a g_1_ONE)
(f_0_ONE a g_1_TWO)
(f_0_ONE a g_1_THREE)
(f_0_ONE a g_1_FOUR)
(f_0_ONE a g_1_FIVE)
(f_0_ONE a g_1_SIX)

(f_0_TWO b g_1_ZERO)
(f_0_TWO b g_1_ONE)
(f_0_TWO b g_1_TWO)
(f_0_TWO b g_1_THREE)
(f_0_TWO b g_1_FOUR)
(f_0_TWO b g_1_FIVE)
(f_0_TWO b g_1_SIX)

(f_0_THREE a g_2_ZERO)
(f_0_THREE a g_2_ONE)
(f_0_THREE a g_2_TWO)
(f_0_THREE a g_2_THREE)
(f_0_THREE a g_2_FOUR)
(f_0_THREE a g_2_FIVE)
(f_0_THREE a g_2_SIX)

(f_0_FOUR b g_2_ZERO)
(f_0_FOUR b g_2_ONE)
(f_0_FOUR b g_2_TWO)
(f_0_FOUR b g_2_THREE)
(f_0_FOUR b g_2_FOUR)
(f_0_FOUR b g_2_FIVE)
(f_0_FOUR b g_2_SIX)

(f_0_FIVE a g_3_ZERO)
(f_0_FIVE a g_3_ONE)
(f_0_FIVE a g_3_TWO)
(f_0_FIVE a g_3_THREE)
(f_0_FIVE a g_3_FOUR)
(f_0_FIVE a g_3_FIVE)
(f_0_FIVE a g_3_SIX)

(f_0_SIX b g_3_ZERO)
(f_0_SIX b g_3_ONE)
(f_0_SIX b g_3_TWO)
(f_0_SIX b g_3_THREE)
(f_0_SIX b g_3_FOUR)
(f_0_SIX b g_3_FIVE)
(f_0_SIX b g_3_SIX)

(f_1_ZERO a g_1_ZERO)
(f_1_ZERO a g_1_ONE)
(f_1_ZERO a g_1_TWO)
(f_1_ZERO a g_1_THREE)
(f_1_ZERO a g_1_FOUR)
(f_1_ZERO a g_1_FIVE)
(f_1_ZERO a g_1_SIX)

(f_1_ONE b g_1_ZERO)
(f_1_ONE b g_1_ONE)
(f_1_ONE b g_1_TWO)
(f_1_ONE b g_1_THREE)
(f_1_ONE b g_1_FOUR)
(f_1_ONE b g_1_FIVE)
(f_1_ONE b g_1_SIX)

(f_1_TWO a g_2_ZERO)
(f_1_TWO a g_2_ONE)
(f_1_TWO a g_2_TWO)
(f_1_TWO a g_2_THREE)
(f_1_TWO a g_2_FOUR)
(f_1_TWO a g_2_FIVE)
(f_1_TWO a g_2_SIX)

(f_1_THREE b g_2_ZERO)
(f_1_THREE b g_2_ONE)
(f_1_THREE b g_2_TWO)
(f_1_THREE b g_2_THREE)
(f_1_THREE b g_2_FOUR)
(f_1_THREE b g_2_FIVE)
(f_1_THREE b g_2_SIX)

(f_1_FOUR a g_3_ZERO)
(f_1_FOUR a g_3_ONE)
(f_1_FOUR a g_3_TWO)
(f_1_FOUR a g_3_THREE)
(f_1_FOUR a g_3_FOUR)
(f_1_FOUR a g_3_FIVE)
(f_1_FOUR a g_3_SIX)

(f_1_FIVE b g_3_ZERO)
(f_1_FIVE b g_3_ONE)
(f_1_FIVE b g_3_TWO)
(f_1_FIVE b g_3_THREE)
(f_1_FIVE b g_3_FOUR)
(f_1_FIVE b g_3_FIVE)
(f_1_FIVE b g_3_SIX)

(f_1_SIX a g_4_ZERO)
(f_1_SIX a g_4_ONE)
(f_1_SIX a g_4_TWO)
(f_1_SIX a g_4_THREE)
(f_1_SIX a g_4_FOUR)
(f_1_SIX a g_4_FIVE)
(f_1_SIX a g_4_SIX)

(f_2_ZERO b g_1_ZERO)
(f_2_ZERO b g_1_ONE)
(f_2_ZERO b g_1_TWO)
(f_2_ZERO b g_1_THREE)
(f_2_ZERO b g_1_FOUR)
(f_2_ZERO b g_1_FIVE)
(f_2_ZERO b g_1_SIX)

(f_2_ONE a g_2_ZERO)
(f_2_ONE a g_2_ONE)
(f_2_ONE a g_2_TWO)
(f_2_ONE a g_2_THREE)
(f_2_ONE a g_2_FOUR)
(f_2_ONE a g_2_FIVE)
(f_2_ONE a g_2_SIX)

(f_2_TWO b g_2_ZERO)
(f_2_TWO b g_2_ONE)
(f_2_TWO b g_2_TWO)
(f_2_TWO b g_2_THREE)
(f_2_TWO b g_2_FOUR)
(f_2_TWO b g_2_FIVE)
(f_2_TWO b g_2_SIX)

(f_2_THREE a g_3_ZERO)
(f_2_THREE a g_3_ONE)
(f_2_THREE a g_3_TWO)
(f_2_THREE a g_3_THREE)
(f_2_THREE a g_3_FOUR)
(f_2_THREE a g_3_FIVE)
(f_2_THREE a g_3_SIX)

(f_2_FOUR b g_3_ZERO)
(f_2_FOUR b g_3_ONE)
(f_2_FOUR b g_3_TWO)
(f_2_FOUR b g_3_THREE)
(f_2_FOUR b g_3_FOUR)
(f_2_FOUR b g_3_FIVE)
(f_2_FOUR b g_3_SIX)

(f_2_FIVE a g_4_ZERO)
(f_2_FIVE a g_4_ONE)
(f_2_FIVE a g_4_TWO)
(f_2_FIVE a g_4_THREE)
(f_2_FIVE a g_4_FOUR)
(f_2_FIVE a g_4_FIVE)
(f_2_FIVE a g_4_SIX)

(f_2_SIX b g_4_ZERO)
(f_2_SIX b g_4_ONE)
(f_2_SIX b g_4_TWO)
(f_2_SIX b g_4_THREE)
(f_2_SIX b g_4_FOUR)
(f_2_SIX b g_4_FIVE)
(f_2_SIX b g_4_SIX)

(f_3_ZERO a g_2_ZERO)
(f_3_ZERO a g_2_ONE)
(f_3_ZERO a g_2_TWO)
(f_3_ZERO a g_2_THREE)
(f_3_ZERO a g_2_FOUR)
(f_3_ZERO a g_2_FIVE)
(f_3_ZERO a g_2_SIX)

(f_3_ONE b g_2_ZERO)
(f_3_ONE b g_2_ONE)
(f_3_ONE b g_2_TWO)
(f_3_ONE b g_2_THREE)
(f_3_ONE b g_2_FOUR)
(f_3_ONE b g_2_FIVE)
(f_3_ONE b g_2_SIX)

(f_3_TWO a g_3_ZERO)
(f_3_TWO a g_3_ONE)
(f_3_TWO a g_3_TWO)
(f_3_TWO a g_3_THREE)
(f_3_TWO a g_3_FOUR)
(f_3_TWO a g_3_FIVE)
(f_3_TWO a g_3_SIX)

(f_3_THREE b g_3_ZERO)
(f_3_THREE b g_3_ONE)
(f_3_THREE b g_3_TWO)
(f_3_THREE b g_3_THREE)
(f_3_THREE b g_3_FOUR)
(f_3_THREE b g_3_FIVE)
(f_3_THREE b g_3_SIX)

(f_3_FOUR a g_4_ZERO)
(f_3_FOUR a g_4_ONE)
(f_3_FOUR a g_4_TWO)
(f_3_FOUR a g_4_THREE)
(f_3_FOUR a g_4_FOUR)
(f_3_FOUR a g_4_FIVE)
(f_3_FOUR a g_4_SIX)

(f_3_FIVE b g_4_ZERO)
(f_3_FIVE b g_4_ONE)
(f_3_FIVE b g_4_TWO)
(f_3_FIVE b g_4_THREE)
(f_3_FIVE b g_4_FOUR)
(f_3_FIVE b g_4_FIVE)
(f_3_FIVE b g_4_SIX)

(f_3_SIX a g_5_ZERO)
(f_3_SIX a g_5_ONE)
(f_3_SIX a g_5_TWO)
(f_3_SIX a g_5_THREE)
(f_3_SIX a g_5_FOUR)
(f_3_SIX a g_5_FIVE)
(f_3_SIX a g_5_SIX)

(f_4_ZERO b g_2_ZERO)
(f_4_ZERO b g_2_ONE)
(f_4_ZERO b g_2_TWO)
(f_4_ZERO b g_2_THREE)
(f_4_ZERO b g_2_FOUR)
(f_4_ZERO b g_2_FIVE)
(f_4_ZERO b g_2_SIX)

(f_4_ONE a g_3_ZERO)
(f_4_ONE a g_3_ONE)
(f_4_ONE a g_3_TWO)
(f_4_ONE a g_3_THREE)
(f_4_ONE a g_3_FOUR)
(f_4_ONE a g_3_FIVE)
(f_4_ONE a g_3_SIX)

(f_4_TWO b g_3_ZERO)
(f_4_TWO b g_3_ONE)
(f_4_TWO b g_3_TWO)
(f_4_TWO b g_3_THREE)
(f_4_TWO b g_3_FOUR)
(f_4_TWO b g_3_FIVE)
(f_4_TWO b g_3_SIX)

(f_4_THREE a g_4_ZERO)
(f_4_THREE a g_4_ONE)
(f_4_THREE a g_4_TWO)
(f_4_THREE a g_4_THREE)
(f_4_THREE a g_4_FOUR)
(f_4_THREE a g_4_FIVE)
(f_4_THREE a g_4_SIX)

(f_4_FOUR b g_4_ZERO)
(f_4_FOUR b g_4_ONE)
(f_4_FOUR b g_4_TWO)
(f_4_FOUR b g_4_THREE)
(f_4_FOUR b g_4_FOUR)
(f_4_FOUR b g_4_FIVE)
(f_4_FOUR b g_4_SIX)

(f_4_FIVE a g_5_ZERO)
(f_4_FIVE a g_5_ONE)
(f_4_FIVE a g_5_TWO)
(f_4_FIVE a g_5_THREE)
(f_4_FIVE a g_5_FOUR)
(f_4_FIVE a g_5_FIVE)
(f_4_FIVE a g_5_SIX)

(f_4_SIX b g_5_ZERO)
(f_4_SIX b g_5_ONE)
(f_4_SIX b g_5_TWO)
(f_4_SIX b g_5_THREE)
(f_4_SIX b g_5_FOUR)
(f_4_SIX b g_5_FIVE)
(f_4_SIX b g_5_SIX)

(f_5_ZERO a g_3_ZERO)
(f_5_ZERO a g_3_ONE)
(f_5_ZERO a g_3_TWO)
(f_5_ZERO a g_3_THREE)
(f_5_ZERO a g_3_FOUR)
(f_5_ZERO a g_3_FIVE)
(f_5_ZERO a g_3_SIX)

(f_5_ONE b g_3_ZERO)
(f_5_ONE b g_3_ONE)
(f_5_ONE b g_3_TWO)
(f_5_ONE b g_3_THREE)
(f_5_ONE b g_3_FOUR)
(f_5_ONE b g_3_FIVE)
(f_5_ONE b g_3_SIX)

(f_5_TWO a g_4_ZERO)
(f_5_TWO a g_4_ONE)
(f_5_TWO a g_4_TWO)
(f_5_TWO a g_4_THREE)
(f_5_TWO a g_4_FOUR)
(f_5_TWO a g_4_FIVE)
(f_5_TWO a g_4_SIX)

(f_5_THREE b g_4_ZERO)
(f_5_THREE b g_4_ONE)
(f_5_THREE b g_4_TWO)
(f_5_THREE b g_4_THREE)
(f_5_THREE b g_4_FOUR)
(f_5_THREE b g_4_FIVE)
(f_5_THREE b g_4_SIX)

(f_5_FOUR a g_5_ZERO)
(f_5_FOUR a g_5_ONE)
(f_5_FOUR a g_5_TWO)
(f_5_FOUR a g_5_THREE)
(f_5_FOUR a g_5_FOUR)
(f_5_FOUR a g_5_FIVE)
(f_5_FOUR a g_5_SIX)

(f_5_FIVE b g_5_ZERO)
(f_5_FIVE b g_5_ONE)
(f_5_FIVE b g_5_TWO)
(f_5_FIVE b g_5_THREE)
(f_5_FIVE b g_5_FOUR)
(f_5_FIVE b g_5_FIVE)
(f_5_FIVE b g_5_SIX)

(f_5_SIX a g_6_ZERO)
(f_5_SIX a g_6_ONE)
(f_5_SIX a g_6_TWO)
(f_5_SIX a g_6_THREE)
(f_5_SIX a g_6_FOUR)
(f_5_SIX a g_6_FIVE)
(f_5_SIX a g_6_SIX)


},
internalTransitions = {

(t4 c n0)
(t5 d n0)
(t6 c n1)
(n0 c q)
(n1 d q)
(q d acc)

(s3 c n0)
(s4 d n0)
(s5 c n1)

(s3 d l1)
(s4 c l2)
(s5 d l2)

(l1 c q)
(l2 d q)

(l1 d q)

(f_0_ZERO c s0)
(f_0_ONE c s0)
(f_0_TWO c s0)
(f_0_THREE c s0)
(f_0_FOUR c s0)
(f_0_FIVE c s0)
(f_0_SIX c s0)

(f_0_ZERO d s0)
(f_0_ONE d s0)
(f_0_TWO d s0)
(f_0_THREE d s0)
(f_0_FOUR d s0)
(f_0_FIVE d s0)
(f_0_SIX d s0)

(f_0_ZERO c s1)
(f_0_ONE c s1)
(f_0_TWO c s1)
(f_0_THREE c s1)
(f_0_FOUR c s1)
(f_0_FIVE c s1)
(f_0_SIX c s1)

(f_0_ZERO d s1)
(f_0_ONE d s1)
(f_0_TWO d s1)
(f_0_THREE d s1)
(f_0_FOUR d s1)
(f_0_FIVE d s1)
(f_0_SIX d s1)

(f_0_ZERO c s2)
(f_0_ONE c s2)
(f_0_TWO c s2)
(f_0_THREE c s2)
(f_0_FOUR c s2)
(f_0_FIVE c s2)
(f_0_SIX c s2)

(f_0_ZERO d s2)
(f_0_ONE d s2)
(f_0_TWO d s2)
(f_0_THREE d s2)
(f_0_FOUR d s2)
(f_0_FIVE d s2)
(f_0_SIX d s2)

(f_0_ZERO c s3)
(f_0_ONE c s3)
(f_0_TWO c s3)
(f_0_THREE c s3)
(f_0_FOUR c s3)
(f_0_FIVE c s3)
(f_0_SIX c s3)

(f_1_ZERO d s0)
(f_1_ONE d s0)
(f_1_TWO d s0)
(f_1_THREE d s0)
(f_1_FOUR d s0)
(f_1_FIVE d s0)
(f_1_SIX d s0)

(f_1_ZERO c s1)
(f_1_ONE c s1)
(f_1_TWO c s1)
(f_1_THREE c s1)
(f_1_FOUR c s1)
(f_1_FIVE c s1)
(f_1_SIX c s1)

(f_1_ZERO d s1)
(f_1_ONE d s1)
(f_1_TWO d s1)
(f_1_THREE d s1)
(f_1_FOUR d s1)
(f_1_FIVE d s1)
(f_1_SIX d s1)

(f_1_ZERO c s2)
(f_1_ONE c s2)
(f_1_TWO c s2)
(f_1_THREE c s2)
(f_1_FOUR c s2)
(f_1_FIVE c s2)
(f_1_SIX c s2)

(f_1_ZERO d s2)
(f_1_ONE d s2)
(f_1_TWO d s2)
(f_1_THREE d s2)
(f_1_FOUR d s2)
(f_1_FIVE d s2)
(f_1_SIX d s2)

(f_1_ZERO c s3)
(f_1_ONE c s3)
(f_1_TWO c s3)
(f_1_THREE c s3)
(f_1_FOUR c s3)
(f_1_FIVE c s3)
(f_1_SIX c s3)

(f_1_ZERO d s3)
(f_1_ONE d s3)
(f_1_TWO d s3)
(f_1_THREE d s3)
(f_1_FOUR d s3)
(f_1_FIVE d s3)
(f_1_SIX d s3)

(f_2_ZERO c s1)
(f_2_ONE c s1)
(f_2_TWO c s1)
(f_2_THREE c s1)
(f_2_FOUR c s1)
(f_2_FIVE c s1)
(f_2_SIX c s1)

(f_2_ZERO d s1)
(f_2_ONE d s1)
(f_2_TWO d s1)
(f_2_THREE d s1)
(f_2_FOUR d s1)
(f_2_FIVE d s1)
(f_2_SIX d s1)

(f_2_ZERO c s2)
(f_2_ONE c s2)
(f_2_TWO c s2)
(f_2_THREE c s2)
(f_2_FOUR c s2)
(f_2_FIVE c s2)
(f_2_SIX c s2)

(f_2_ZERO d s2)
(f_2_ONE d s2)
(f_2_TWO d s2)
(f_2_THREE d s2)
(f_2_FOUR d s2)
(f_2_FIVE d s2)
(f_2_SIX d s2)

(f_2_ZERO c s3)
(f_2_ONE c s3)
(f_2_TWO c s3)
(f_2_THREE c s3)
(f_2_FOUR c s3)
(f_2_FIVE c s3)
(f_2_SIX c s3)

(f_2_ZERO d s3)
(f_2_ONE d s3)
(f_2_TWO d s3)
(f_2_THREE d s3)
(f_2_FOUR d s3)
(f_2_FIVE d s3)
(f_2_SIX d s3)

(f_2_ZERO c s4)
(f_2_ONE c s4)
(f_2_TWO c s4)
(f_2_THREE c s4)
(f_2_FOUR c s4)
(f_2_FIVE c s4)
(f_2_SIX c s4)

(f_3_ZERO d s1)
(f_3_ONE d s1)
(f_3_TWO d s1)
(f_3_THREE d s1)
(f_3_FOUR d s1)
(f_3_FIVE d s1)
(f_3_SIX d s1)

(f_3_ZERO c s2)
(f_3_ONE c s2)
(f_3_TWO c s2)
(f_3_THREE c s2)
(f_3_FOUR c s2)
(f_3_FIVE c s2)
(f_3_SIX c s2)

(f_3_ZERO d s2)
(f_3_ONE d s2)
(f_3_TWO d s2)
(f_3_THREE d s2)
(f_3_FOUR d s2)
(f_3_FIVE d s2)
(f_3_SIX d s2)

(f_3_ZERO c s3)
(f_3_ONE c s3)
(f_3_TWO c s3)
(f_3_THREE c s3)
(f_3_FOUR c s3)
(f_3_FIVE c s3)
(f_3_SIX c s3)

(f_3_ZERO d s3)
(f_3_ONE d s3)
(f_3_TWO d s3)
(f_3_THREE d s3)
(f_3_FOUR d s3)
(f_3_FIVE d s3)
(f_3_SIX d s3)

(f_3_ZERO c s4)
(f_3_ONE c s4)
(f_3_TWO c s4)
(f_3_THREE c s4)
(f_3_FOUR c s4)
(f_3_FIVE c s4)
(f_3_SIX c s4)

(f_3_ZERO d s4)
(f_3_ONE d s4)
(f_3_TWO d s4)
(f_3_THREE d s4)
(f_3_FOUR d s4)
(f_3_FIVE d s4)
(f_3_SIX d s4)

(f_4_ZERO c s2)
(f_4_ONE c s2)
(f_4_TWO c s2)
(f_4_THREE c s2)
(f_4_FOUR c s2)
(f_4_FIVE c s2)
(f_4_SIX c s2)

(f_4_ZERO d s2)
(f_4_ONE d s2)
(f_4_TWO d s2)
(f_4_THREE d s2)
(f_4_FOUR d s2)
(f_4_FIVE d s2)
(f_4_SIX d s2)

(f_4_ZERO c s3)
(f_4_ONE c s3)
(f_4_TWO c s3)
(f_4_THREE c s3)
(f_4_FOUR c s3)
(f_4_FIVE c s3)
(f_4_SIX c s3)

(f_4_ZERO d s3)
(f_4_ONE d s3)
(f_4_TWO d s3)
(f_4_THREE d s3)
(f_4_FOUR d s3)
(f_4_FIVE d s3)
(f_4_SIX d s3)

(f_4_ZERO c s4)
(f_4_ONE c s4)
(f_4_TWO c s4)
(f_4_THREE c s4)
(f_4_FOUR c s4)
(f_4_FIVE c s4)
(f_4_SIX c s4)

(f_4_ZERO d s4)
(f_4_ONE d s4)
(f_4_TWO d s4)
(f_4_THREE d s4)
(f_4_FOUR d s4)
(f_4_FIVE d s4)
(f_4_SIX d s4)

(f_4_ZERO c s5)
(f_4_ONE c s5)
(f_4_TWO c s5)
(f_4_THREE c s5)
(f_4_FOUR c s5)
(f_4_FIVE c s5)
(f_4_SIX c s5)

(f_5_ZERO d s2)
(f_5_ONE d s2)
(f_5_TWO d s2)
(f_5_THREE d s2)
(f_5_FOUR d s2)
(f_5_FIVE d s2)
(f_5_SIX d s2)

(f_5_ZERO c s3)
(f_5_ONE c s3)
(f_5_TWO c s3)
(f_5_THREE c s3)
(f_5_FOUR c s3)
(f_5_FIVE c s3)
(f_5_SIX c s3)

(f_5_ZERO d s3)
(f_5_ONE d s3)
(f_5_TWO d s3)
(f_5_THREE d s3)
(f_5_FOUR d s3)
(f_5_FIVE d s3)
(f_5_SIX d s3)

(f_5_ZERO c s4)
(f_5_ONE c s4)
(f_5_TWO c s4)
(f_5_THREE c s4)
(f_5_FOUR c s4)
(f_5_FIVE c s4)
(f_5_SIX c s4)

(f_5_ZERO d s4)
(f_5_ONE d s4)
(f_5_TWO d s4)
(f_5_THREE d s4)
(f_5_FOUR d s4)
(f_5_FIVE d s4)
(f_5_SIX d s4)

(f_5_ZERO c s5)
(f_5_ONE c s5)
(f_5_TWO c s5)
(f_5_THREE c s5)
(f_5_FOUR c s5)
(f_5_FIVE c s5)
(f_5_SIX c s5)

(f_5_ZERO d s5)
(f_5_ONE d s5)
(f_5_TWO d s5)
(f_5_THREE d s5)
(f_5_FOUR d s5)
(f_5_FIVE d s5)
(f_5_SIX d s5)

(g_0_ZERO c t0)
(g_0_ONE c t0)
(g_0_TWO c t0)
(g_0_THREE c t0)
(g_0_FOUR c t0)
(g_0_FIVE c t0)
(g_0_SIX c t0)

(g_0_ZERO d t0)
(g_0_ONE d t0)
(g_0_TWO d t0)
(g_0_THREE d t0)
(g_0_FOUR d t0)
(g_0_FIVE d t0)
(g_0_SIX d t0)

(g_0_ZERO c t1)
(g_0_ONE c t1)
(g_0_TWO c t1)
(g_0_THREE c t1)
(g_0_FOUR c t1)
(g_0_FIVE c t1)
(g_0_SIX c t1)

(g_0_ZERO d t1)
(g_0_ONE d t1)
(g_0_TWO d t1)
(g_0_THREE d t1)
(g_0_FOUR d t1)
(g_0_FIVE d t1)
(g_0_SIX d t1)

(g_0_ZERO c t2)
(g_0_ONE c t2)
(g_0_TWO c t2)
(g_0_THREE c t2)
(g_0_FOUR c t2)
(g_0_FIVE c t2)
(g_0_SIX c t2)

(g_0_ZERO d t2)
(g_0_ONE d t2)
(g_0_TWO d t2)
(g_0_THREE d t2)
(g_0_FOUR d t2)
(g_0_FIVE d t2)
(g_0_SIX d t2)

(g_0_ZERO c t3)
(g_0_ONE c t3)
(g_0_TWO c t3)
(g_0_THREE c t3)
(g_0_FOUR c t3)
(g_0_FIVE c t3)
(g_0_SIX c t3)

(g_1_ZERO d t0)
(g_1_ONE d t0)
(g_1_TWO d t0)
(g_1_THREE d t0)
(g_1_FOUR d t0)
(g_1_FIVE d t0)
(g_1_SIX d t0)

(g_1_ZERO c t1)
(g_1_ONE c t1)
(g_1_TWO c t1)
(g_1_THREE c t1)
(g_1_FOUR c t1)
(g_1_FIVE c t1)
(g_1_SIX c t1)

(g_1_ZERO d t1)
(g_1_ONE d t1)
(g_1_TWO d t1)
(g_1_THREE d t1)
(g_1_FOUR d t1)
(g_1_FIVE d t1)
(g_1_SIX d t1)

(g_1_ZERO c t2)
(g_1_ONE c t2)
(g_1_TWO c t2)
(g_1_THREE c t2)
(g_1_FOUR c t2)
(g_1_FIVE c t2)
(g_1_SIX c t2)

(g_1_ZERO d t2)
(g_1_ONE d t2)
(g_1_TWO d t2)
(g_1_THREE d t2)
(g_1_FOUR d t2)
(g_1_FIVE d t2)
(g_1_SIX d t2)

(g_1_ZERO c t3)
(g_1_ONE c t3)
(g_1_TWO c t3)
(g_1_THREE c t3)
(g_1_FOUR c t3)
(g_1_FIVE c t3)
(g_1_SIX c t3)

(g_1_ZERO d t3)
(g_1_ONE d t3)
(g_1_TWO d t3)
(g_1_THREE d t3)
(g_1_FOUR d t3)
(g_1_FIVE d t3)
(g_1_SIX d t3)

(g_2_ZERO c t1)
(g_2_ONE c t1)
(g_2_TWO c t1)
(g_2_THREE c t1)
(g_2_FOUR c t1)
(g_2_FIVE c t1)
(g_2_SIX c t1)

(g_2_ZERO d t1)
(g_2_ONE d t1)
(g_2_TWO d t1)
(g_2_THREE d t1)
(g_2_FOUR d t1)
(g_2_FIVE d t1)
(g_2_SIX d t1)

(g_2_ZERO c t2)
(g_2_ONE c t2)
(g_2_TWO c t2)
(g_2_THREE c t2)
(g_2_FOUR c t2)
(g_2_FIVE c t2)
(g_2_SIX c t2)

(g_2_ZERO d t2)
(g_2_ONE d t2)
(g_2_TWO d t2)
(g_2_THREE d t2)
(g_2_FOUR d t2)
(g_2_FIVE d t2)
(g_2_SIX d t2)

(g_2_ZERO c t3)
(g_2_ONE c t3)
(g_2_TWO c t3)
(g_2_THREE c t3)
(g_2_FOUR c t3)
(g_2_FIVE c t3)
(g_2_SIX c t3)

(g_2_ZERO d t3)
(g_2_ONE d t3)
(g_2_TWO d t3)
(g_2_THREE d t3)
(g_2_FOUR d t3)
(g_2_FIVE d t3)
(g_2_SIX d t3)

(g_2_ZERO c t4)
(g_2_ONE c t4)
(g_2_TWO c t4)
(g_2_THREE c t4)
(g_2_FOUR c t4)
(g_2_FIVE c t4)
(g_2_SIX c t4)

(g_3_ZERO d t1)
(g_3_ONE d t1)
(g_3_TWO d t1)
(g_3_THREE d t1)
(g_3_FOUR d t1)
(g_3_FIVE d t1)
(g_3_SIX d t1)

(g_3_ZERO c t2)
(g_3_ONE c t2)
(g_3_TWO c t2)
(g_3_THREE c t2)
(g_3_FOUR c t2)
(g_3_FIVE c t2)
(g_3_SIX c t2)

(g_3_ZERO d t2)
(g_3_ONE d t2)
(g_3_TWO d t2)
(g_3_THREE d t2)
(g_3_FOUR d t2)
(g_3_FIVE d t2)
(g_3_SIX d t2)

(g_3_ZERO c t3)
(g_3_ONE c t3)
(g_3_TWO c t3)
(g_3_THREE c t3)
(g_3_FOUR c t3)
(g_3_FIVE c t3)
(g_3_SIX c t3)

(g_3_ZERO d t3)
(g_3_ONE d t3)
(g_3_TWO d t3)
(g_3_THREE d t3)
(g_3_FOUR d t3)
(g_3_FIVE d t3)
(g_3_SIX d t3)

(g_3_ZERO c t4)
(g_3_ONE c t4)
(g_3_TWO c t4)
(g_3_THREE c t4)
(g_3_FOUR c t4)
(g_3_FIVE c t4)
(g_3_SIX c t4)

(g_3_ZERO d t4)
(g_3_ONE d t4)
(g_3_TWO d t4)
(g_3_THREE d t4)
(g_3_FOUR d t4)
(g_3_FIVE d t4)
(g_3_SIX d t4)

(g_4_ZERO c t2)
(g_4_ONE c t2)
(g_4_TWO c t2)
(g_4_THREE c t2)
(g_4_FOUR c t2)
(g_4_FIVE c t2)
(g_4_SIX c t2)

(g_4_ZERO d t2)
(g_4_ONE d t2)
(g_4_TWO d t2)
(g_4_THREE d t2)
(g_4_FOUR d t2)
(g_4_FIVE d t2)
(g_4_SIX d t2)

(g_4_ZERO c t3)
(g_4_ONE c t3)
(g_4_TWO c t3)
(g_4_THREE c t3)
(g_4_FOUR c t3)
(g_4_FIVE c t3)
(g_4_SIX c t3)

(g_4_ZERO d t3)
(g_4_ONE d t3)
(g_4_TWO d t3)
(g_4_THREE d t3)
(g_4_FOUR d t3)
(g_4_FIVE d t3)
(g_4_SIX d t3)

(g_4_ZERO c t4)
(g_4_ONE c t4)
(g_4_TWO c t4)
(g_4_THREE c t4)
(g_4_FOUR c t4)
(g_4_FIVE c t4)
(g_4_SIX c t4)

(g_4_ZERO d t4)
(g_4_ONE d t4)
(g_4_TWO d t4)
(g_4_THREE d t4)
(g_4_FOUR d t4)
(g_4_FIVE d t4)
(g_4_SIX d t4)

(g_4_ZERO c t5)
(g_4_ONE c t5)
(g_4_TWO c t5)
(g_4_THREE c t5)
(g_4_FOUR c t5)
(g_4_FIVE c t5)
(g_4_SIX c t5)

(g_5_ZERO d t2)
(g_5_ONE d t2)
(g_5_TWO d t2)
(g_5_THREE d t2)
(g_5_FOUR d t2)
(g_5_FIVE d t2)
(g_5_SIX d t2)

(g_5_ZERO c t3)
(g_5_ONE c t3)
(g_5_TWO c t3)
(g_5_THREE c t3)
(g_5_FOUR c t3)
(g_5_FIVE c t3)
(g_5_SIX c t3)

(g_5_ZERO d t3)
(g_5_ONE d t3)
(g_5_TWO d t3)
(g_5_THREE d t3)
(g_5_FOUR d t3)
(g_5_FIVE d t3)
(g_5_SIX d t3)

(g_5_ZERO c t4)
(g_5_ONE c t4)
(g_5_TWO c t4)
(g_5_THREE c t4)
(g_5_FOUR c t4)
(g_5_FIVE c t4)
(g_5_SIX c t4)

(g_5_ZERO d t4)
(g_5_ONE d t4)
(g_5_TWO d t4)
(g_5_THREE d t4)
(g_5_FOUR d t4)
(g_5_FIVE d t4)
(g_5_SIX d t4)

(g_5_ZERO c t5)
(g_5_ONE c t5)
(g_5_TWO c t5)
(g_5_THREE c t5)
(g_5_FOUR c t5)
(g_5_FIVE c t5)
(g_5_SIX c t5)

(g_5_ZERO d t5)
(g_5_ONE d t5)
(g_5_TWO d t5)
(g_5_THREE d t5)
(g_5_FOUR d t5)
(g_5_FIVE d t5)
(g_5_SIX d t5)

},
returnTransitions = {
(s0 f_0_ZERO e s0)
(s0 f_1_ZERO e s0)
(s0 f_2_ZERO e s0)
(s0 f_3_ZERO e s0)
(s0 f_4_ZERO e s0)
(s0 f_5_ZERO e s0)

(s0 f_0_TWO e s1)
(s0 f_1_TWO e s1)
(s0 f_2_TWO e s1)
(s0 f_3_TWO e s1)
(s0 f_4_TWO e s1)
(s0 f_5_TWO e s1)

(s0 f_0_FOUR e s2)
(s0 f_1_FOUR e s2)
(s0 f_2_FOUR e s2)
(s0 f_3_FOUR e s2)
(s0 f_4_FOUR e s2)
(s0 f_5_FOUR e s2)

(s0 f_0_SIX e s3)
(s0 f_1_SIX e s3)
(s0 f_2_SIX e s3)
(s0 f_3_SIX e s3)
(s0 f_4_SIX e s3)
(s0 f_5_SIX e s3)

(s0 f_0_ONE f s0)
(s0 f_1_ONE f s0)
(s0 f_2_ONE f s0)
(s0 f_3_ONE f s0)
(s0 f_4_ONE f s0)
(s0 f_5_ONE f s0)

(s0 f_0_THREE f s1)
(s0 f_1_THREE f s1)
(s0 f_2_THREE f s1)
(s0 f_3_THREE f s1)
(s0 f_4_THREE f s1)
(s0 f_5_THREE f s1)

(s0 f_0_FIVE f s2)
(s0 f_1_FIVE f s2)
(s0 f_2_FIVE f s2)
(s0 f_3_FIVE f s2)
(s0 f_4_FIVE f s2)
(s0 f_5_FIVE f s2)


(s1 f_0_ZERO f s0)
(s1 f_1_ZERO f s0)
(s1 f_2_ZERO f s0)
(s1 f_3_ZERO f s0)
(s1 f_4_ZERO f s0)
(s1 f_5_ZERO f s0)

(s1 f_0_TWO f s1)
(s1 f_1_TWO f s1)
(s1 f_2_TWO f s1)
(s1 f_3_TWO f s1)
(s1 f_4_TWO f s1)
(s1 f_5_TWO f s1)

(s1 f_0_FOUR f s2)
(s1 f_1_FOUR f s2)
(s1 f_2_FOUR f s2)
(s1 f_3_FOUR f s2)
(s1 f_4_FOUR f s2)
(s1 f_5_FOUR f s2)

(s1 f_0_SIX f s3)
(s1 f_1_SIX f s3)
(s1 f_2_SIX f s3)
(s1 f_3_SIX f s3)
(s1 f_4_SIX f s3)
(s1 f_5_SIX f s3)

(s1 f_0_ONE e s1)
(s1 f_1_ONE e s1)
(s1 f_2_ONE e s1)
(s1 f_3_ONE e s1)
(s1 f_4_ONE e s1)
(s1 f_5_ONE e s1)

(s1 f_0_THREE e s2)
(s1 f_1_THREE e s2)
(s1 f_2_THREE e s2)
(s1 f_3_THREE e s2)
(s1 f_4_THREE e s2)
(s1 f_5_THREE e s2)

(s1 f_0_FIVE e s3)
(s1 f_1_FIVE e s3)
(s1 f_2_FIVE e s3)
(s1 f_3_FIVE e s3)
(s1 f_4_FIVE e s3)
(s1 f_5_FIVE e s3)


(s2 f_0_ZERO e s1)
(s2 f_1_ZERO e s1)
(s2 f_2_ZERO e s1)
(s2 f_3_ZERO e s1)
(s2 f_4_ZERO e s1)
(s2 f_5_ZERO e s1)

(s2 f_0_TWO e s2)
(s2 f_1_TWO e s2)
(s2 f_2_TWO e s2)
(s2 f_3_TWO e s2)
(s2 f_4_TWO e s2)
(s2 f_5_TWO e s2)

(s2 f_0_FOUR e s3)
(s2 f_1_FOUR e s3)
(s2 f_2_FOUR e s3)
(s2 f_3_FOUR e s3)
(s2 f_4_FOUR e s3)
(s2 f_5_FOUR e s3)

(s2 f_0_SIX e s4)
(s2 f_1_SIX e s4)
(s2 f_2_SIX e s4)
(s2 f_3_SIX e s4)
(s2 f_4_SIX e s4)
(s2 f_5_SIX e s4)

(s2 f_0_ONE f s1)
(s2 f_1_ONE f s1)
(s2 f_2_ONE f s1)
(s2 f_3_ONE f s1)
(s2 f_4_ONE f s1)
(s2 f_5_ONE f s1)

(s2 f_0_THREE f s2)
(s2 f_1_THREE f s2)
(s2 f_2_THREE f s2)
(s2 f_3_THREE f s2)
(s2 f_4_THREE f s2)
(s2 f_5_THREE f s2)

(s2 f_0_FIVE f s3)
(s2 f_1_FIVE f s3)
(s2 f_2_FIVE f s3)
(s2 f_3_FIVE f s3)
(s2 f_4_FIVE f s3)
(s2 f_5_FIVE f s3)


(s3 f_0_ZERO f s1)
(s3 f_1_ZERO f s1)
(s3 f_2_ZERO f s1)
(s3 f_3_ZERO f s1)
(s3 f_4_ZERO f s1)
(s3 f_5_ZERO f s1)

(s3 f_0_TWO f s2)
(s3 f_1_TWO f s2)
(s3 f_2_TWO f s2)
(s3 f_3_TWO f s2)
(s3 f_4_TWO f s2)
(s3 f_5_TWO f s2)

(s3 f_0_FOUR f s3)
(s3 f_1_FOUR f s3)
(s3 f_2_FOUR f s3)
(s3 f_3_FOUR f s3)
(s3 f_4_FOUR f s3)
(s3 f_5_FOUR f s3)

(s3 f_0_SIX f s4)
(s3 f_1_SIX f s4)
(s3 f_2_SIX f s4)
(s3 f_3_SIX f s4)
(s3 f_4_SIX f s4)
(s3 f_5_SIX f s4)

(s3 f_0_ONE e s2)
(s3 f_1_ONE e s2)
(s3 f_2_ONE e s2)
(s3 f_3_ONE e s2)
(s3 f_4_ONE e s2)
(s3 f_5_ONE e s2)

(s3 f_0_THREE e s3)
(s3 f_1_THREE e s3)
(s3 f_2_THREE e s3)
(s3 f_3_THREE e s3)
(s3 f_4_THREE e s3)
(s3 f_5_THREE e s3)

(s3 f_0_FIVE e s4)
(s3 f_1_FIVE e s4)
(s3 f_2_FIVE e s4)
(s3 f_3_FIVE e s4)
(s3 f_4_FIVE e s4)
(s3 f_5_FIVE e s4)


(s4 f_0_ZERO e s2)
(s4 f_1_ZERO e s2)
(s4 f_2_ZERO e s2)
(s4 f_3_ZERO e s2)
(s4 f_4_ZERO e s2)
(s4 f_5_ZERO e s2)

(s4 f_0_TWO e s3)
(s4 f_1_TWO e s3)
(s4 f_2_TWO e s3)
(s4 f_3_TWO e s3)
(s4 f_4_TWO e s3)
(s4 f_5_TWO e s3)

(s4 f_0_FOUR e s4)
(s4 f_1_FOUR e s4)
(s4 f_2_FOUR e s4)
(s4 f_3_FOUR e s4)
(s4 f_4_FOUR e s4)
(s4 f_5_FOUR e s4)

(s4 f_0_SIX e s5)
(s4 f_1_SIX e s5)
(s4 f_2_SIX e s5)
(s4 f_3_SIX e s5)
(s4 f_4_SIX e s5)
(s4 f_5_SIX e s5)

(s4 f_0_ONE f s2)
(s4 f_1_ONE f s2)
(s4 f_2_ONE f s2)
(s4 f_3_ONE f s2)
(s4 f_4_ONE f s2)
(s4 f_5_ONE f s2)

(s4 f_0_THREE f s3)
(s4 f_1_THREE f s3)
(s4 f_2_THREE f s3)
(s4 f_3_THREE f s3)
(s4 f_4_THREE f s3)
(s4 f_5_THREE f s3)

(s4 f_0_FIVE f s4)
(s4 f_1_FIVE f s4)
(s4 f_2_FIVE f s4)
(s4 f_3_FIVE f s4)
(s4 f_4_FIVE f s4)
(s4 f_5_FIVE f s4)


(s5 f_0_ZERO f s2)
(s5 f_1_ZERO f s2)
(s5 f_2_ZERO f s2)
(s5 f_3_ZERO f s2)
(s5 f_4_ZERO f s2)
(s5 f_5_ZERO f s2)

(s5 f_0_TWO f s3)
(s5 f_1_TWO f s3)
(s5 f_2_TWO f s3)
(s5 f_3_TWO f s3)
(s5 f_4_TWO f s3)
(s5 f_5_TWO f s3)

(s5 f_0_FOUR f s4)
(s5 f_1_FOUR f s4)
(s5 f_2_FOUR f s4)
(s5 f_3_FOUR f s4)
(s5 f_4_FOUR f s4)
(s5 f_5_FOUR f s4)

(s5 f_0_SIX f s5)
(s5 f_1_SIX f s5)
(s5 f_2_SIX f s5)
(s5 f_3_SIX f s5)
(s5 f_4_SIX f s5)
(s5 f_5_SIX f s5)

(s5 f_0_ONE e s3)
(s5 f_1_ONE e s3)
(s5 f_2_ONE e s3)
(s5 f_3_ONE e s3)
(s5 f_4_ONE e s3)
(s5 f_5_ONE e s3)

(s5 f_0_THREE e s4)
(s5 f_1_THREE e s4)
(s5 f_2_THREE e s4)
(s5 f_3_THREE e s4)
(s5 f_4_THREE e s4)
(s5 f_5_THREE e s4)

(s5 f_0_FIVE e s5)
(s5 f_1_FIVE e s5)
(s5 f_2_FIVE e s5)
(s5 f_3_FIVE e s5)
(s5 f_4_FIVE e s5)
(s5 f_5_FIVE e s5)

(t0 g_0_ZERO e t0)
(t0 g_1_ZERO e t0)
(t0 g_2_ZERO e t0)
(t0 g_3_ZERO e t0)
(t0 g_4_ZERO e t0)
(t0 g_5_ZERO e t0)

(t0 g_0_TWO e t1)
(t0 g_1_TWO e t1)
(t0 g_2_TWO e t1)
(t0 g_3_TWO e t1)
(t0 g_4_TWO e t1)
(t0 g_5_TWO e t1)

(t0 g_0_FOUR e t2)
(t0 g_1_FOUR e t2)
(t0 g_2_FOUR e t2)
(t0 g_3_FOUR e t2)
(t0 g_4_FOUR e t2)
(t0 g_5_FOUR e t2)

(t0 g_0_SIX e t3)
(t0 g_1_SIX e t3)
(t0 g_2_SIX e t3)
(t0 g_3_SIX e t3)
(t0 g_4_SIX e t3)
(t0 g_5_SIX e t3)

(t0 g_0_ONE f t0)
(t0 g_1_ONE f t0)
(t0 g_2_ONE f t0)
(t0 g_3_ONE f t0)
(t0 g_4_ONE f t0)
(t0 g_5_ONE f t0)

(t0 g_0_THREE f t1)
(t0 g_1_THREE f t1)
(t0 g_2_THREE f t1)
(t0 g_3_THREE f t1)
(t0 g_4_THREE f t1)
(t0 g_5_THREE f t1)

(t0 g_0_FIVE f t2)
(t0 g_1_FIVE f t2)
(t0 g_2_FIVE f t2)
(t0 g_3_FIVE f t2)
(t0 g_4_FIVE f t2)
(t0 g_5_FIVE f t2)


(t1 g_0_ZERO f t0)
(t1 g_1_ZERO f t0)
(t1 g_2_ZERO f t0)
(t1 g_3_ZERO f t0)
(t1 g_4_ZERO f t0)
(t1 g_5_ZERO f t0)

(t1 g_0_TWO f t1)
(t1 g_1_TWO f t1)
(t1 g_2_TWO f t1)
(t1 g_3_TWO f t1)
(t1 g_4_TWO f t1)
(t1 g_5_TWO f t1)

(t1 g_0_FOUR f t2)
(t1 g_1_FOUR f t2)
(t1 g_2_FOUR f t2)
(t1 g_3_FOUR f t2)
(t1 g_4_FOUR f t2)
(t1 g_5_FOUR f t2)

(t1 g_0_SIX f t3)
(t1 g_1_SIX f t3)
(t1 g_2_SIX f t3)
(t1 g_3_SIX f t3)
(t1 g_4_SIX f t3)
(t1 g_5_SIX f t3)

(t1 g_0_ONE e t1)
(t1 g_1_ONE e t1)
(t1 g_2_ONE e t1)
(t1 g_3_ONE e t1)
(t1 g_4_ONE e t1)
(t1 g_5_ONE e t1)

(t1 g_0_THREE e t2)
(t1 g_1_THREE e t2)
(t1 g_2_THREE e t2)
(t1 g_3_THREE e t2)
(t1 g_4_THREE e t2)
(t1 g_5_THREE e t2)

(t1 g_0_FIVE e t3)
(t1 g_1_FIVE e t3)
(t1 g_2_FIVE e t3)
(t1 g_3_FIVE e t3)
(t1 g_4_FIVE e t3)
(t1 g_5_FIVE e t3)


(t2 g_0_ZERO e t1)
(t2 g_1_ZERO e t1)
(t2 g_2_ZERO e t1)
(t2 g_3_ZERO e t1)
(t2 g_4_ZERO e t1)
(t2 g_5_ZERO e t1)

(t2 g_0_TWO e t2)
(t2 g_1_TWO e t2)
(t2 g_2_TWO e t2)
(t2 g_3_TWO e t2)
(t2 g_4_TWO e t2)
(t2 g_5_TWO e t2)

(t2 g_0_FOUR e t3)
(t2 g_1_FOUR e t3)
(t2 g_2_FOUR e t3)
(t2 g_3_FOUR e t3)
(t2 g_4_FOUR e t3)
(t2 g_5_FOUR e t3)

(t2 g_0_SIX e t4)
(t2 g_1_SIX e t4)
(t2 g_2_SIX e t4)
(t2 g_3_SIX e t4)
(t2 g_4_SIX e t4)
(t2 g_5_SIX e t4)

(t2 g_0_ONE f t1)
(t2 g_1_ONE f t1)
(t2 g_2_ONE f t1)
(t2 g_3_ONE f t1)
(t2 g_4_ONE f t1)
(t2 g_5_ONE f t1)

(t2 g_0_THREE f t2)
(t2 g_1_THREE f t2)
(t2 g_2_THREE f t2)
(t2 g_3_THREE f t2)
(t2 g_4_THREE f t2)
(t2 g_5_THREE f t2)

(t2 g_0_FIVE f t3)
(t2 g_1_FIVE f t3)
(t2 g_2_FIVE f t3)
(t2 g_3_FIVE f t3)
(t2 g_4_FIVE f t3)
(t2 g_5_FIVE f t3)


(t3 g_0_ZERO f t1)
(t3 g_1_ZERO f t1)
(t3 g_2_ZERO f t1)
(t3 g_3_ZERO f t1)
(t3 g_4_ZERO f t1)
(t3 g_5_ZERO f t1)

(t3 g_0_TWO f t2)
(t3 g_1_TWO f t2)
(t3 g_2_TWO f t2)
(t3 g_3_TWO f t2)
(t3 g_4_TWO f t2)
(t3 g_5_TWO f t2)

(t3 g_0_FOUR f t3)
(t3 g_1_FOUR f t3)
(t3 g_2_FOUR f t3)
(t3 g_3_FOUR f t3)
(t3 g_4_FOUR f t3)
(t3 g_5_FOUR f t3)

(t3 g_0_SIX f t4)
(t3 g_1_SIX f t4)
(t3 g_2_SIX f t4)
(t3 g_3_SIX f t4)
(t3 g_4_SIX f t4)
(t3 g_5_SIX f t4)

(t3 g_0_ONE e t2)
(t3 g_1_ONE e t2)
(t3 g_2_ONE e t2)
(t3 g_3_ONE e t2)
(t3 g_4_ONE e t2)
(t3 g_5_ONE e t2)

(t3 g_0_THREE e t3)
(t3 g_1_THREE e t3)
(t3 g_2_THREE e t3)
(t3 g_3_THREE e t3)
(t3 g_4_THREE e t3)
(t3 g_5_THREE e t3)

(t3 g_0_FIVE e t4)
(t3 g_1_FIVE e t4)
(t3 g_2_FIVE e t4)
(t3 g_3_FIVE e t4)
(t3 g_4_FIVE e t4)
(t3 g_5_FIVE e t4)


(t4 g_0_ZERO e t2)
(t4 g_1_ZERO e t2)
(t4 g_2_ZERO e t2)
(t4 g_3_ZERO e t2)
(t4 g_4_ZERO e t2)
(t4 g_5_ZERO e t2)

(t4 g_0_TWO e t3)
(t4 g_1_TWO e t3)
(t4 g_2_TWO e t3)
(t4 g_3_TWO e t3)
(t4 g_4_TWO e t3)
(t4 g_5_TWO e t3)

(t4 g_0_FOUR e t4)
(t4 g_1_FOUR e t4)
(t4 g_2_FOUR e t4)
(t4 g_3_FOUR e t4)
(t4 g_4_FOUR e t4)
(t4 g_5_FOUR e t4)

(t4 g_0_SIX e t5)
(t4 g_1_SIX e t5)
(t4 g_2_SIX e t5)
(t4 g_3_SIX e t5)
(t4 g_4_SIX e t5)
(t4 g_5_SIX e t5)

(t4 g_0_ONE f t2)
(t4 g_1_ONE f t2)
(t4 g_2_ONE f t2)
(t4 g_3_ONE f t2)
(t4 g_4_ONE f t2)
(t4 g_5_ONE f t2)

(t4 g_0_THREE f t3)
(t4 g_1_THREE f t3)
(t4 g_2_THREE f t3)
(t4 g_3_THREE f t3)
(t4 g_4_THREE f t3)
(t4 g_5_THREE f t3)

(t4 g_0_FIVE f t4)
(t4 g_1_FIVE f t4)
(t4 g_2_FIVE f t4)
(t4 g_3_FIVE f t4)
(t4 g_4_FIVE f t4)
(t4 g_5_FIVE f t4)


(t5 g_0_ZERO f t2)
(t5 g_1_ZERO f t2)
(t5 g_2_ZERO f t2)
(t5 g_3_ZERO f t2)
(t5 g_4_ZERO f t2)
(t5 g_5_ZERO f t2)

(t5 g_0_TWO f t3)
(t5 g_1_TWO f t3)
(t5 g_2_TWO f t3)
(t5 g_3_TWO f t3)
(t5 g_4_TWO f t3)
(t5 g_5_TWO f t3)

(t5 g_0_FOUR f t4)
(t5 g_1_FOUR f t4)
(t5 g_2_FOUR f t4)
(t5 g_3_FOUR f t4)
(t5 g_4_FOUR f t4)
(t5 g_5_FOUR f t4)

(t5 g_0_SIX f t5)
(t5 g_1_SIX f t5)
(t5 g_2_SIX f t5)
(t5 g_3_SIX f t5)
(t5 g_4_SIX f t5)
(t5 g_5_SIX f t5)

(t5 g_0_ONE e t3)
(t5 g_1_ONE e t3)
(t5 g_2_ONE e t3)
(t5 g_3_ONE e t3)
(t5 g_4_ONE e t3)
(t5 g_5_ONE e t3)

(t5 g_0_THREE e t4)
(t5 g_1_THREE e t4)
(t5 g_2_THREE e t4)
(t5 g_3_THREE e t4)
(t5 g_4_THREE e t4)
(t5 g_5_THREE e t4)

(t5 g_0_FIVE e t5)
(t5 g_1_FIVE e t5)
(t5 g_2_FIVE e t5)
(t5 g_3_FIVE e t5)
(t5 g_4_FIVE e t5)
(t5 g_5_FIVE e t5)

(t6 g_0_ZERO e t3)
(t6 g_1_ZERO e t3)
(t6 g_2_ZERO e t3)
(t6 g_3_ZERO e t3)
(t6 g_4_ZERO e t3)
(t6 g_5_ZERO e t3)

(t6 g_0_TWO e t4)
(t6 g_1_TWO e t4)
(t6 g_2_TWO e t4)
(t6 g_3_TWO e t4)
(t6 g_4_TWO e t4)
(t6 g_5_TWO e t4)

(t6 g_0_FOUR e t5)
(t6 g_1_FOUR e t5)
(t6 g_2_FOUR e t5)
(t6 g_3_FOUR e t5)
(t6 g_4_FOUR e t5)
(t6 g_5_FOUR e t5)

(t6 g_0_SIX e t6)
(t6 g_1_SIX e t6)
(t6 g_2_SIX e t6)
(t6 g_3_SIX e t6)
(t6 g_4_SIX e t6)
(t6 g_5_SIX e t6)

(t6 g_0_ONE f t3)
(t6 g_1_ONE f t3)
(t6 g_2_ONE f t3)
(t6 g_3_ONE f t3)
(t6 g_4_ONE f t3)
(t6 g_5_ONE f t3)

(t6 g_0_THREE f t4)
(t6 g_1_THREE f t4)
(t6 g_2_THREE f t4)
(t6 g_3_THREE f t4)
(t6 g_4_THREE f t4)
(t6 g_5_THREE f t4)

(t6 g_0_FIVE f t5)
(t6 g_1_FIVE f t5)
(t6 g_2_FIVE f t5)
(t6 g_3_FIVE f t5)
(t6 g_4_FIVE f t5)
(t6 g_5_FIVE f t5)

(s0 f_0_ZERO f t0)
(s0 f_1_ZERO f t0)
(s0 f_2_ZERO f t0)
(s0 f_3_ZERO f t0)
(s0 f_4_ZERO f t0)
(s0 f_5_ZERO f t0)

(s0 f_0_TWO f t1)
(s0 f_1_TWO f t1)
(s0 f_2_TWO f t1)
(s0 f_3_TWO f t1)
(s0 f_4_TWO f t1)
(s0 f_5_TWO f t1)

(s0 f_0_FOUR f t2)
(s0 f_1_FOUR f t2)
(s0 f_2_FOUR f t2)
(s0 f_3_FOUR f t2)
(s0 f_4_FOUR f t2)
(s0 f_5_FOUR f t2)

(s0 f_0_SIX f t3)
(s0 f_1_SIX f t3)
(s0 f_2_SIX f t3)
(s0 f_3_SIX f t3)
(s0 f_4_SIX f t3)
(s0 f_5_SIX f t3)

(s0 f_0_ONE e t1)
(s0 f_1_ONE e t1)
(s0 f_2_ONE e t1)
(s0 f_3_ONE e t1)
(s0 f_4_ONE e t1)
(s0 f_5_ONE e t1)

(s0 f_0_THREE e t2)
(s0 f_1_THREE e t2)
(s0 f_2_THREE e t2)
(s0 f_3_THREE e t2)
(s0 f_4_THREE e t2)
(s0 f_5_THREE e t2)

(s0 f_0_FIVE e t3)
(s0 f_1_FIVE e t3)
(s0 f_2_FIVE e t3)
(s0 f_3_FIVE e t3)
(s0 f_4_FIVE e t3)
(s0 f_5_FIVE e t3)

(s1 f_0_ZERO e t1)
(s1 f_1_ZERO e t1)
(s1 f_2_ZERO e t1)
(s1 f_3_ZERO e t1)
(s1 f_4_ZERO e t1)
(s1 f_5_ZERO e t1)

(s1 f_0_TWO e t2)
(s1 f_1_TWO e t2)
(s1 f_2_TWO e t2)
(s1 f_3_TWO e t2)
(s1 f_4_TWO e t2)
(s1 f_5_TWO e t2)

(s1 f_0_FOUR e t3)
(s1 f_1_FOUR e t3)
(s1 f_2_FOUR e t3)
(s1 f_3_FOUR e t3)
(s1 f_4_FOUR e t3)
(s1 f_5_FOUR e t3)

(s1 f_0_SIX e t4)
(s1 f_1_SIX e t4)
(s1 f_2_SIX e t4)
(s1 f_3_SIX e t4)
(s1 f_4_SIX e t4)
(s1 f_5_SIX e t4)

(s1 f_0_ONE f t1)
(s1 f_1_ONE f t1)
(s1 f_2_ONE f t1)
(s1 f_3_ONE f t1)
(s1 f_4_ONE f t1)
(s1 f_5_ONE f t1)

(s1 f_0_THREE f t2)
(s1 f_1_THREE f t2)
(s1 f_2_THREE f t2)
(s1 f_3_THREE f t2)
(s1 f_4_THREE f t2)
(s1 f_5_THREE f t2)

(s1 f_0_FIVE f t3)
(s1 f_1_FIVE f t3)
(s1 f_2_FIVE f t3)
(s1 f_3_FIVE f t3)
(s1 f_4_FIVE f t3)
(s1 f_5_FIVE f t3)


(s2 f_0_ZERO f t1)
(s2 f_1_ZERO f t1)
(s2 f_2_ZERO f t1)
(s2 f_3_ZERO f t1)
(s2 f_4_ZERO f t1)
(s2 f_5_ZERO f t1)

(s2 f_0_TWO f t2)
(s2 f_1_TWO f t2)
(s2 f_2_TWO f t2)
(s2 f_3_TWO f t2)
(s2 f_4_TWO f t2)
(s2 f_5_TWO f t2)

(s2 f_0_FOUR f t3)
(s2 f_1_FOUR f t3)
(s2 f_2_FOUR f t3)
(s2 f_3_FOUR f t3)
(s2 f_4_FOUR f t3)
(s2 f_5_FOUR f t3)

(s2 f_0_SIX f t4)
(s2 f_1_SIX f t4)
(s2 f_2_SIX f t4)
(s2 f_3_SIX f t4)
(s2 f_4_SIX f t4)
(s2 f_5_SIX f t4)

(s2 f_0_ONE e t2)
(s2 f_1_ONE e t2)
(s2 f_2_ONE e t2)
(s2 f_3_ONE e t2)
(s2 f_4_ONE e t2)
(s2 f_5_ONE e t2)

(s2 f_0_THREE e t3)
(s2 f_1_THREE e t3)
(s2 f_2_THREE e t3)
(s2 f_3_THREE e t3)
(s2 f_4_THREE e t3)
(s2 f_5_THREE e t3)

(s2 f_0_FIVE e t4)
(s2 f_1_FIVE e t4)
(s2 f_2_FIVE e t4)
(s2 f_3_FIVE e t4)
(s2 f_4_FIVE e t4)
(s2 f_5_FIVE e t4)


(s3 f_0_ZERO e t2)
(s3 f_1_ZERO e t2)
(s3 f_2_ZERO e t2)
(s3 f_3_ZERO e t2)
(s3 f_4_ZERO e t2)
(s3 f_5_ZERO e t2)

(s3 f_0_TWO e t3)
(s3 f_1_TWO e t3)
(s3 f_2_TWO e t3)
(s3 f_3_TWO e t3)
(s3 f_4_TWO e t3)
(s3 f_5_TWO e t3)

(s3 f_0_FOUR e t4)
(s3 f_1_FOUR e t4)
(s3 f_2_FOUR e t4)
(s3 f_3_FOUR e t4)
(s3 f_4_FOUR e t4)
(s3 f_5_FOUR e t4)

(s3 f_0_SIX e t5)
(s3 f_1_SIX e t5)
(s3 f_2_SIX e t5)
(s3 f_3_SIX e t5)
(s3 f_4_SIX e t5)
(s3 f_5_SIX e t5)

(s3 f_0_ONE f t2)
(s3 f_1_ONE f t2)
(s3 f_2_ONE f t2)
(s3 f_3_ONE f t2)
(s3 f_4_ONE f t2)
(s3 f_5_ONE f t2)

(s3 f_0_THREE f t3)
(s3 f_1_THREE f t3)
(s3 f_2_THREE f t3)
(s3 f_3_THREE f t3)
(s3 f_4_THREE f t3)
(s3 f_5_THREE f t3)

(s3 f_0_FIVE f t4)
(s3 f_1_FIVE f t4)
(s3 f_2_FIVE f t4)
(s3 f_3_FIVE f t4)
(s3 f_4_FIVE f t4)
(s3 f_5_FIVE f t4)


(s4 f_0_ZERO f t2)
(s4 f_1_ZERO f t2)
(s4 f_2_ZERO f t2)
(s4 f_3_ZERO f t2)
(s4 f_4_ZERO f t2)
(s4 f_5_ZERO f t2)

(s4 f_0_TWO f t3)
(s4 f_1_TWO f t3)
(s4 f_2_TWO f t3)
(s4 f_3_TWO f t3)
(s4 f_4_TWO f t3)
(s4 f_5_TWO f t3)

(s4 f_0_FOUR f t4)
(s4 f_1_FOUR f t4)
(s4 f_2_FOUR f t4)
(s4 f_3_FOUR f t4)
(s4 f_4_FOUR f t4)
(s4 f_5_FOUR f t4)

(s4 f_0_SIX f t5)
(s4 f_1_SIX f t5)
(s4 f_2_SIX f t5)
(s4 f_3_SIX f t5)
(s4 f_4_SIX f t5)
(s4 f_5_SIX f t5)

(s4 f_0_ONE e t3)
(s4 f_1_ONE e t3)
(s4 f_2_ONE e t3)
(s4 f_3_ONE e t3)
(s4 f_4_ONE e t3)
(s4 f_5_ONE e t3)

(s4 f_0_THREE e t4)
(s4 f_1_THREE e t4)
(s4 f_2_THREE e t4)
(s4 f_3_THREE e t4)
(s4 f_4_THREE e t4)
(s4 f_5_THREE e t4)

(s4 f_0_FIVE e t5)
(s4 f_1_FIVE e t5)
(s4 f_2_FIVE e t5)
(s4 f_3_FIVE e t5)
(s4 f_4_FIVE e t5)
(s4 f_5_FIVE e t5)


(s5 f_0_ZERO e t3)
(s5 f_1_ZERO e t3)
(s5 f_2_ZERO e t3)
(s5 f_3_ZERO e t3)
(s5 f_4_ZERO e t3)
(s5 f_5_ZERO e t3)

(s5 f_0_TWO e t4)
(s5 f_1_TWO e t4)
(s5 f_2_TWO e t4)
(s5 f_3_TWO e t4)
(s5 f_4_TWO e t4)
(s5 f_5_TWO e t4)

(s5 f_0_FOUR e t5)
(s5 f_1_FOUR e t5)
(s5 f_2_FOUR e t5)
(s5 f_3_FOUR e t5)
(s5 f_4_FOUR e t5)
(s5 f_5_FOUR e t5)

(s5 f_0_SIX e t6)
(s5 f_1_SIX e t6)
(s5 f_2_SIX e t6)
(s5 f_3_SIX e t6)
(s5 f_4_SIX e t6)
(s5 f_5_SIX e t6)

(s5 f_0_ONE f t3)
(s5 f_1_ONE f t3)
(s5 f_2_ONE f t3)
(s5 f_3_ONE f t3)
(s5 f_4_ONE f t3)
(s5 f_5_ONE f t3)

(s5 f_0_THREE f t4)
(s5 f_1_THREE f t4)
(s5 f_2_THREE f t4)
(s5 f_3_THREE f t4)
(s5 f_4_THREE f t4)
(s5 f_5_THREE f t4)

(s5 f_0_FIVE f t5)
(s5 f_1_FIVE f t5)
(s5 f_2_FIVE f t5)
(s5 f_3_FIVE f t5)
(s5 f_4_FIVE f t5)
(s5 f_5_FIVE f t5)

(t0 f_0_ZERO e t0)
(t0 f_1_ZERO e t0)
(t0 f_2_ZERO e t0)
(t0 f_3_ZERO e t0)
(t0 f_4_ZERO e t0)
(t0 f_5_ZERO e t0)

(t0 f_0_TWO e t1)
(t0 f_1_TWO e t1)
(t0 f_2_TWO e t1)
(t0 f_3_TWO e t1)
(t0 f_4_TWO e t1)
(t0 f_5_TWO e t1)

(t0 f_0_FOUR e t2)
(t0 f_1_FOUR e t2)
(t0 f_2_FOUR e t2)
(t0 f_3_FOUR e t2)
(t0 f_4_FOUR e t2)
(t0 f_5_FOUR e t2)

(t0 f_0_SIX e t3)
(t0 f_1_SIX e t3)
(t0 f_2_SIX e t3)
(t0 f_3_SIX e t3)
(t0 f_4_SIX e t3)
(t0 f_5_SIX e t3)

(t0 f_0_ONE f t0)
(t0 f_1_ONE f t0)
(t0 f_2_ONE f t0)
(t0 f_3_ONE f t0)
(t0 f_4_ONE f t0)
(t0 f_5_ONE f t0)

(t0 f_0_THREE f t1)
(t0 f_1_THREE f t1)
(t0 f_2_THREE f t1)
(t0 f_3_THREE f t1)
(t0 f_4_THREE f t1)
(t0 f_5_THREE f t1)

(t0 f_0_FIVE f t2)
(t0 f_1_FIVE f t2)
(t0 f_2_FIVE f t2)
(t0 f_3_FIVE f t2)
(t0 f_4_FIVE f t2)
(t0 f_5_FIVE f t2)


(t1 f_0_ZERO f t0)
(t1 f_1_ZERO f t0)
(t1 f_2_ZERO f t0)
(t1 f_3_ZERO f t0)
(t1 f_4_ZERO f t0)
(t1 f_5_ZERO f t0)

(t1 f_0_TWO f t1)
(t1 f_1_TWO f t1)
(t1 f_2_TWO f t1)
(t1 f_3_TWO f t1)
(t1 f_4_TWO f t1)
(t1 f_5_TWO f t1)

(t1 f_0_FOUR f t2)
(t1 f_1_FOUR f t2)
(t1 f_2_FOUR f t2)
(t1 f_3_FOUR f t2)
(t1 f_4_FOUR f t2)
(t1 f_5_FOUR f t2)

(t1 f_0_SIX f t3)
(t1 f_1_SIX f t3)
(t1 f_2_SIX f t3)
(t1 f_3_SIX f t3)
(t1 f_4_SIX f t3)
(t1 f_5_SIX f t3)

(t1 f_0_ONE e t1)
(t1 f_1_ONE e t1)
(t1 f_2_ONE e t1)
(t1 f_3_ONE e t1)
(t1 f_4_ONE e t1)
(t1 f_5_ONE e t1)

(t1 f_0_THREE e t2)
(t1 f_1_THREE e t2)
(t1 f_2_THREE e t2)
(t1 f_3_THREE e t2)
(t1 f_4_THREE e t2)
(t1 f_5_THREE e t2)

(t1 f_0_FIVE e t3)
(t1 f_1_FIVE e t3)
(t1 f_2_FIVE e t3)
(t1 f_3_FIVE e t3)
(t1 f_4_FIVE e t3)
(t1 f_5_FIVE e t3)


(t2 f_0_ZERO e t1)
(t2 f_1_ZERO e t1)
(t2 f_2_ZERO e t1)
(t2 f_3_ZERO e t1)
(t2 f_4_ZERO e t1)
(t2 f_5_ZERO e t1)

(t2 f_0_TWO e t2)
(t2 f_1_TWO e t2)
(t2 f_2_TWO e t2)
(t2 f_3_TWO e t2)
(t2 f_4_TWO e t2)
(t2 f_5_TWO e t2)

(t2 f_0_FOUR e t3)
(t2 f_1_FOUR e t3)
(t2 f_2_FOUR e t3)
(t2 f_3_FOUR e t3)
(t2 f_4_FOUR e t3)
(t2 f_5_FOUR e t3)

(t2 f_0_SIX e t4)
(t2 f_1_SIX e t4)
(t2 f_2_SIX e t4)
(t2 f_3_SIX e t4)
(t2 f_4_SIX e t4)
(t2 f_5_SIX e t4)

(t2 f_0_ONE f t1)
(t2 f_1_ONE f t1)
(t2 f_2_ONE f t1)
(t2 f_3_ONE f t1)
(t2 f_4_ONE f t1)
(t2 f_5_ONE f t1)

(t2 f_0_THREE f t2)
(t2 f_1_THREE f t2)
(t2 f_2_THREE f t2)
(t2 f_3_THREE f t2)
(t2 f_4_THREE f t2)
(t2 f_5_THREE f t2)

(t2 f_0_FIVE f t3)
(t2 f_1_FIVE f t3)
(t2 f_2_FIVE f t3)
(t2 f_3_FIVE f t3)
(t2 f_4_FIVE f t3)
(t2 f_5_FIVE f t3)


(t3 f_0_ZERO f t1)
(t3 f_1_ZERO f t1)
(t3 f_2_ZERO f t1)
(t3 f_3_ZERO f t1)
(t3 f_4_ZERO f t1)
(t3 f_5_ZERO f t1)

(t3 f_0_TWO f t2)
(t3 f_1_TWO f t2)
(t3 f_2_TWO f t2)
(t3 f_3_TWO f t2)
(t3 f_4_TWO f t2)
(t3 f_5_TWO f t2)

(t3 f_0_FOUR f t3)
(t3 f_1_FOUR f t3)
(t3 f_2_FOUR f t3)
(t3 f_3_FOUR f t3)
(t3 f_4_FOUR f t3)
(t3 f_5_FOUR f t3)

(t3 f_0_SIX f t4)
(t3 f_1_SIX f t4)
(t3 f_2_SIX f t4)
(t3 f_3_SIX f t4)
(t3 f_4_SIX f t4)
(t3 f_5_SIX f t4)

(t3 f_0_ONE e t2)
(t3 f_1_ONE e t2)
(t3 f_2_ONE e t2)
(t3 f_3_ONE e t2)
(t3 f_4_ONE e t2)
(t3 f_5_ONE e t2)

(t3 f_0_THREE e t3)
(t3 f_1_THREE e t3)
(t3 f_2_THREE e t3)
(t3 f_3_THREE e t3)
(t3 f_4_THREE e t3)
(t3 f_5_THREE e t3)

(t3 f_0_FIVE e t4)
(t3 f_1_FIVE e t4)
(t3 f_2_FIVE e t4)
(t3 f_3_FIVE e t4)
(t3 f_4_FIVE e t4)
(t3 f_5_FIVE e t4)


(t4 f_0_ZERO e t2)
(t4 f_1_ZERO e t2)
(t4 f_2_ZERO e t2)
(t4 f_3_ZERO e t2)
(t4 f_4_ZERO e t2)
(t4 f_5_ZERO e t2)

(t4 f_0_TWO e t3)
(t4 f_1_TWO e t3)
(t4 f_2_TWO e t3)
(t4 f_3_TWO e t3)
(t4 f_4_TWO e t3)
(t4 f_5_TWO e t3)

(t4 f_0_FOUR e t4)
(t4 f_1_FOUR e t4)
(t4 f_2_FOUR e t4)
(t4 f_3_FOUR e t4)
(t4 f_4_FOUR e t4)
(t4 f_5_FOUR e t4)

(t4 f_0_SIX e t5)
(t4 f_1_SIX e t5)
(t4 f_2_SIX e t5)
(t4 f_3_SIX e t5)
(t4 f_4_SIX e t5)
(t4 f_5_SIX e t5)

(t4 f_0_ONE f t2)
(t4 f_1_ONE f t2)
(t4 f_2_ONE f t2)
(t4 f_3_ONE f t2)
(t4 f_4_ONE f t2)
(t4 f_5_ONE f t2)

(t4 f_0_THREE f t3)
(t4 f_1_THREE f t3)
(t4 f_2_THREE f t3)
(t4 f_3_THREE f t3)
(t4 f_4_THREE f t3)
(t4 f_5_THREE f t3)

(t4 f_0_FIVE f t4)
(t4 f_1_FIVE f t4)
(t4 f_2_FIVE f t4)
(t4 f_3_FIVE f t4)
(t4 f_4_FIVE f t4)
(t4 f_5_FIVE f t4)


(t5 f_0_ZERO f t2)
(t5 f_1_ZERO f t2)
(t5 f_2_ZERO f t2)
(t5 f_3_ZERO f t2)
(t5 f_4_ZERO f t2)
(t5 f_5_ZERO f t2)

(t5 f_0_TWO f t3)
(t5 f_1_TWO f t3)
(t5 f_2_TWO f t3)
(t5 f_3_TWO f t3)
(t5 f_4_TWO f t3)
(t5 f_5_TWO f t3)

(t5 f_0_FOUR f t4)
(t5 f_1_FOUR f t4)
(t5 f_2_FOUR f t4)
(t5 f_3_FOUR f t4)
(t5 f_4_FOUR f t4)
(t5 f_5_FOUR f t4)

(t5 f_0_SIX f t5)
(t5 f_1_SIX f t5)
(t5 f_2_SIX f t5)
(t5 f_3_SIX f t5)
(t5 f_4_SIX f t5)
(t5 f_5_SIX f t5)

(t5 f_0_ONE e t3)
(t5 f_1_ONE e t3)
(t5 f_2_ONE e t3)
(t5 f_3_ONE e t3)
(t5 f_4_ONE e t3)
(t5 f_5_ONE e t3)

(t5 f_0_THREE e t4)
(t5 f_1_THREE e t4)
(t5 f_2_THREE e t4)
(t5 f_3_THREE e t4)
(t5 f_4_THREE e t4)
(t5 f_5_THREE e t4)

(t5 f_0_FIVE e t5)
(t5 f_1_FIVE e t5)
(t5 f_2_FIVE e t5)
(t5 f_3_FIVE e t5)
(t5 f_4_FIVE e t5)
(t5 f_5_FIVE e t5)

(t6 f_0_ZERO e t3)
(t6 f_1_ZERO e t3)
(t6 f_2_ZERO e t3)
(t6 f_3_ZERO e t3)
(t6 f_4_ZERO e t3)
(t6 f_5_ZERO e t3)

(t6 f_0_TWO e t4)
(t6 f_1_TWO e t4)
(t6 f_2_TWO e t4)
(t6 f_3_TWO e t4)
(t6 f_4_TWO e t4)
(t6 f_5_TWO e t4)

(t6 f_0_FOUR e t5)
(t6 f_1_FOUR e t5)
(t6 f_2_FOUR e t5)
(t6 f_3_FOUR e t5)
(t6 f_4_FOUR e t5)
(t6 f_5_FOUR e t5)

(t6 f_0_SIX e t6)
(t6 f_1_SIX e t6)
(t6 f_2_SIX e t6)
(t6 f_3_SIX e t6)
(t6 f_4_SIX e t6)
(t6 f_5_SIX e t6)

(t6 f_0_ONE f t3)
(t6 f_1_ONE f t3)
(t6 f_2_ONE f t3)
(t6 f_3_ONE f t3)
(t6 f_4_ONE f t3)
(t6 f_5_ONE f t3)

(t6 f_0_THREE f t4)
(t6 f_1_THREE f t4)
(t6 f_2_THREE f t4)
(t6 f_3_THREE f t4)
(t6 f_4_THREE f t4)
(t6 f_5_THREE f t4)

(t6 f_0_FIVE f t5)
(t6 f_1_FIVE f t5)
(t6 f_2_FIVE f t5)
(t6 f_3_FIVE f t5)
(t6 f_4_FIVE f t5)
(t6 f_5_FIVE f t5)
}
);

print(numberOfStates(determinize(palCheckerSIX)));

NestedWordAutomaton syntaxChecker = (
	callAlphabet = { a b },
	internalAlphabet = { c d },
	returnAlphabet = { e f },
	states = {q0 q1 q2 q3 q4 q5 q6 q7 q8 q9},
	initialStates = {q0},
	finalStates = {q9},
	callTransitions = {
		(q0 a q1)

		(q1 a q2)
		(q1 b q2)

		(q2 a q3)
		(q2 b q3)

		(q3 a q3)
		(q3 b q3)
	},
	internalTransitions = {
		(q3 c q4)
		(q3 d q4)

		(q6 c q7)
		(q6 d q7)
		(q7 c q8)
		(q7 d q8)
		(q8 d q9)
	},
	returnTransitions = {
		(q4 q2 e q4)
		(q4 q2 f q4)

		(q4 q1 e q5)
		(q4 q1 f q5)

		(q5 q0 e q6)
		(q5 q0 f q6)
	}
);

//print(getAcceptedWord(Difference(syntaxChecker, palCheckerSIX)));
assert(IsIncluded(syntaxChecker, palCheckerSIX));