\define TRANS_6 (state<0> = 1 * (  state<1> = 0 * (i = 1 ))+ state<0> = 0 * (state<0>$NS = 1 * (  state<1> = 0 * (state<1>$NS = 1 * (i = 1 )))+ state<0>$NS = 0 * (  state<1> = 0 * (i = 1 ))))
\define TRANS_6 (state<0> = 1 * (state<1> = 1 + state<1> = 0 * (  i = 0))+ state<0> = 0 * (state<0>$NS = 1 * (state<1> = 1 + state<1> = 0 * (state<1>$NS = 1 * (  i = 0)))+ state<0>$NS = 0 * (state<1> = 1 + state<1> = 0 * (  i = 0))))
\define TRANS_8 (state<0> = 1 * (state<1> = 1 * (i = 1 ))+ state<0> = 0 * (state<0>$NS = 1 * (state<1> = 1 * (i = 1 )+ state<1> = 0 * (state<1>$NS = 1 * (  i = 0)))+ state<0>$NS = 0 * (state<1> = 1 * (i = 1 )+ state<1> = 0 * (  i = 0))))
\define TRANS_8 (state<0> = 1 * (state<1> = 1 * (  i = 0)+ state<1> = 0)+ state<0> = 0 * (state<0>$NS = 1 * (state<1> = 1 * (  i = 0)+ state<1> = 0 * (state<1>$NS = 1 * (i = 1 )))+ state<0>$NS = 0 * (state<1> = 1 * (  i = 0)+ state<1> = 0 * (i = 1 ))))
\define TRANS_1 (state<0> = 1 * (state<1> = 1 * (i = 1 ))+ state<0> = 0 * (state<1> = 1 * (i = 1 )+ state<1> = 0 * (  i = 0)))
\define TRANS_1 (state<0> = 1 * (state<1> = 1 * (  i = 0)+ state<1> = 0)+ state<0> = 0 * (state<1> = 1 * (  i = 0)+ state<1> = 0 * (state<1>$NS = 1 * (i = 1 ))))
\define TRANS_3 (state<0> = 1 * (  state<1> = 0 * (i = 1 ))+ state<0> = 0 * (  state<0>$NS = 0 * (  state<1> = 0 * (i = 1 ))))
\define TRANS_3 (state<1> = 1 + state<1> = 0 * (  i = 0))