\define TRANS (state<0> = 1 * (state<0>$NS = 1 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 )))+ state<1> = 0 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 ))+ state<1>$NS = 0 * (  p$NS = 0 * (q$NS = 1 ))))+ state<0>$NS = 0 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (  q$NS = 0)))))+ state<0> = 0 * (state<0>$NS = 1 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 )))+ state<1> = 0 * (  state<1>$NS = 0 * (  p$NS = 0 * (q$NS = 1 ))))+ state<0>$NS = 0 * (state<1>$NS = 1 * (p$NS = 1 * (  q$NS = 0)))))
\define REACH (state<0> = 1 * (state<1> = 1 * (p = 1 * (q = 1 ))+ state<1> = 0 * (  p = 0 * (q = 1 )))+ state<0> = 0 * (state<1> = 1 * (p = 1 * (  q = 0))+ state<1> = 0 * (  p = 0 * (  q = 0))))
\define REL (state<0> = 1 + state<0> = 0 * (state<0>$NS = 1 * (state<1> = 1 + state<1> = 0 * (state<1>$NS = 1 + state<1>$NS = 0 * (p = 1 + p = 0 * (q = 1 ))))+ state<0>$NS = 0))
\define new_rel (state<0> = 1 * (state<0>$NS = 1 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 )))+ state<1> = 0 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 ))+ state<1>$NS = 0 * (  p$NS = 0 * (q$NS = 1 ))))+ state<0>$NS = 0 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (  q$NS = 0)))))+ state<0> = 0 * (state<0>$NS = 1 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 )))+ state<1> = 0 * (  state<1>$NS = 0 * (p = 1 * (  p$NS = 0 * (q$NS = 1 ))+ p = 0 * (  p$NS = 0 * (q = 1 * (q$NS = 1 ))))))+ state<0>$NS = 0 * (state<1>$NS = 1 * (p$NS = 1 * (  q$NS = 0)))))