(AND/IF_1.0 (NFA (NAME Mixer) (SYMBOLS (r0 INPUT) (a0 OUTPUT) (r1 INPUT) (a1 OUTPUT) (r OUTPUT) (a INPUT) ) (STATES (0 INITIAL BOX) (1 TRANSIENT) (2 TRANSIENT) (3 TRANSIENT) (4 BOX) (5 BOX) (6 BOX) (7 TRANSIENT) (8 TRANSIENT) (9 TRANSIENT) (10 TRANSIENT) (11 TRANSIENT) ) (TRANSITIONS (0 1 r0) (0 2 r1) (1 3 r1) (1 4 r) (2 3 r0) (2 5 r) (3 6 r) (4 6 r1) (4 7 a) (5 6 r0) (5 8 a) (6 9 a) (7 0 a0) (7 9 r1) (8 9 r0) (8 0 a1) (9 2 a0) (9 1 a1) (9 10 r) (10 5 a0) (10 4 a1) (10 11 a) (11 8 a0) (11 7 a1) ) ) )