#shared states #0 -> 0 #1 -> 1 #local states #000/0 -> 0 #001/0 -> 1 #010/0 -> 2 #011/0 -> 3 #100/0 -> 4 #101/0 -> 5 #110/0 -> 6 #111/0 -> 7 #000/1 -> 8 #001/1 -> 9 #010/1 -> 10 #011/1 -> 11 #100/1 -> 12 #101/1 -> 13 #110/1 -> 14 #111/1 -> 15 #000/2 -> 16 #001/2 -> 17 #010/2 -> 18 #011/2 -> 19 #100/2 -> 20 #101/2 -> 21 #110/2 -> 22 #111/2 -> 23 #auxiliary local states #ini -> 24 #err -> 25 #end -> 26 #nil -> 27 #init 0/24 #target 1|25,25 2 28 0 0 -> 0 8 0 ~> 0 0 ~> 4 2 ~> 27 3 ~> 27 4 ~> 0 4 ~> 4 6 ~> 27 7 ~> 27 8 ~> 8 8 ~> 12 10 ~> 27 11 ~> 27 12 ~> 8 12 ~> 12 14 ~> 27 15 ~> 27 16 ~> 16 16 ~> 20 18 ~> 27 19 ~> 27 20 ~> 16 20 ~> 20 22 ~> 27 23 ~> 27 0 0 -> 0 9 0 ~> 0 0 ~> 4 2 ~> 27 3 ~> 27 5 ~> 1 6 ~> 27 7 ~> 27 8 ~> 8 8 ~> 12 10 ~> 27 11 ~> 27 13 ~> 9 14 ~> 27 15 ~> 27 16 ~> 16 16 ~> 20 18 ~> 27 19 ~> 27 21 ~> 17 22 ~> 27 23 ~> 27 0 0 -> 0 10 0 ~> 2 0 ~> 6 1 ~> 3 2 ~> 27 3 ~> 27 4 ~> 2 4 ~> 6 5 ~> 7 6 ~> 27 7 ~> 27 8 ~> 10 8 ~> 14 9 ~> 11 10 ~> 27 11 ~> 27 12 ~> 10 12 ~> 14 13 ~> 15 14 ~> 27 15 ~> 27 16 ~> 18 16 ~> 22 17 ~> 19 18 ~> 27 19 ~> 27 20 ~> 18 20 ~> 22 21 ~> 23 22 ~> 27 23 ~> 27 0 0 -> 0 11 0 ~> 2 0 ~> 6 1 ~> 3 2 ~> 27 3 ~> 27 4 ~> 6 5 ~> 3 6 ~> 27 7 ~> 27 8 ~> 10 8 ~> 14 9 ~> 11 10 ~> 27 11 ~> 27 12 ~> 14 13 ~> 11 14 ~> 27 15 ~> 27 16 ~> 18 16 ~> 22 17 ~> 19 18 ~> 27 19 ~> 27 20 ~> 22 21 ~> 19 22 ~> 27 23 ~> 27 0 0 -> 0 12 0 ~> 0 0 ~> 4 2 ~> 27 3 ~> 27 6 ~> 27 7 ~> 27 8 ~> 8 8 ~> 12 10 ~> 27 11 ~> 27 14 ~> 27 15 ~> 27 16 ~> 16 16 ~> 20 18 ~> 27 19 ~> 27 22 ~> 27 23 ~> 27 0 0 -> 0 13 0 ~> 0 0 ~> 4 1 ~> 27 2 ~> 27 3 ~> 27 5 ~> 27 6 ~> 27 7 ~> 27 8 ~> 8 8 ~> 12 9 ~> 27 10 ~> 27 11 ~> 27 13 ~> 27 14 ~> 27 15 ~> 27 16 ~> 16 16 ~> 20 17 ~> 27 18 ~> 27 19 ~> 27 21 ~> 27 22 ~> 27 23 ~> 27 0 1 -> 0 8 1 ~> 1 1 ~> 5 2 ~> 27 3 ~> 27 4 ~> 0 4 ~> 4 5 ~> 27 6 ~> 27 7 ~> 27 9 ~> 9 9 ~> 13 10 ~> 27 11 ~> 27 12 ~> 8 12 ~> 12 13 ~> 27 14 ~> 27 15 ~> 27 17 ~> 17 17 ~> 21 18 ~> 27 19 ~> 27 20 ~> 16 20 ~> 20 21 ~> 27 22 ~> 27 23 ~> 27 0 1 -> 0 9 2 ~> 27 3 ~> 27 5 ~> 27 6 ~> 27 7 ~> 27 10 ~> 27 11 ~> 27 13 ~> 27 14 ~> 27 15 ~> 27 18 ~> 27 19 ~> 27 21 ~> 27 22 ~> 27 23 ~> 27 0 1 -> 0 10 0 ~> 2 1 ~> 3 1 ~> 7 2 ~> 27 3 ~> 27 4 ~> 2 4 ~> 6 5 ~> 27 6 ~> 27 7 ~> 27 8 ~> 10 9 ~> 11 9 ~> 15 10 ~> 27 11 ~> 27 12 ~> 10 12 ~> 14 13 ~> 27 14 ~> 27 15 ~> 27 16 ~> 18 17 ~> 19 17 ~> 23 18 ~> 27 19 ~> 27 20 ~> 18 20 ~> 22 21 ~> 27 22 ~> 27 23 ~> 27 0 1 -> 0 11 0 ~> 2 1 ~> 3 2 ~> 27 3 ~> 27 4 ~> 6 5 ~> 27 6 ~> 27 7 ~> 27 8 ~> 10 9 ~> 11 10 ~> 27 11 ~> 27 12 ~> 14 13 ~> 27 14 ~> 27 15 ~> 27 16 ~> 18 17 ~> 19 18 ~> 27 19 ~> 27 20 ~> 22 21 ~> 27 22 ~> 27 23 ~> 27 0 1 -> 0 12 1 ~> 1 1 ~> 5 2 ~> 27 3 ~> 27 5 ~> 27 6 ~> 27 7 ~> 27 9 ~> 9 9 ~> 13 10 ~> 27 11 ~> 27 13 ~> 27 14 ~> 27 15 ~> 27 17 ~> 17 17 ~> 21 18 ~> 27 19 ~> 27 21 ~> 27 22 ~> 27 23 ~> 27 0 2 -> 0 14 0 ~> 27 1 ~> 27 2 ~> 2 2 ~> 6 4 ~> 27 5 ~> 27 8 ~> 27 9 ~> 27 10 ~> 10 10 ~> 14 12 ~> 27 13 ~> 27 16 ~> 27 17 ~> 27 18 ~> 18 18 ~> 22 20 ~> 27 21 ~> 27 0 2 -> 0 15 0 ~> 27 1 ~> 27 2 ~> 2 2 ~> 6 3 ~> 27 4 ~> 27 5 ~> 27 7 ~> 27 8 ~> 27 9 ~> 27 10 ~> 10 10 ~> 14 11 ~> 27 12 ~> 27 13 ~> 27 15 ~> 27 16 ~> 27 17 ~> 27 18 ~> 18 18 ~> 22 19 ~> 27 20 ~> 27 21 ~> 27 23 ~> 27 0 3 -> 0 14 0 ~> 27 1 ~> 27 3 ~> 3 3 ~> 7 4 ~> 27 5 ~> 27 7 ~> 27 8 ~> 27 9 ~> 27 11 ~> 11 11 ~> 15 12 ~> 27 13 ~> 27 15 ~> 27 16 ~> 27 17 ~> 27 19 ~> 19 19 ~> 23 20 ~> 27 21 ~> 27 23 ~> 27 0 4 -> 0 8 2 ~> 27 3 ~> 27 4 ~> 0 4 ~> 4 6 ~> 27 7 ~> 27 10 ~> 27 11 ~> 27 12 ~> 8 12 ~> 12 14 ~> 27 15 ~> 27 18 ~> 27 19 ~> 27 20 ~> 16 20 ~> 20 22 ~> 27 23 ~> 27 0 4 -> 0 9 2 ~> 27 3 ~> 27 5 ~> 1 6 ~> 27 7 ~> 27 10 ~> 27 11 ~> 27 13 ~> 9 14 ~> 27 15 ~> 27 18 ~> 27 19 ~> 27 21 ~> 17 22 ~> 27 23 ~> 27 0 4 -> 0 10 0 ~> 2 1 ~> 3 2 ~> 27 3 ~> 27 4 ~> 2 4 ~> 6 5 ~> 7 6 ~> 27 7 ~> 27 8 ~> 10 9 ~> 11 10 ~> 27 11 ~> 27 12 ~> 10 12 ~> 14 13 ~> 15 14 ~> 27 15 ~> 27 16 ~> 18 17 ~> 19 18 ~> 27 19 ~> 27 20 ~> 18 20 ~> 22 21 ~> 23 22 ~> 27 23 ~> 27 0 4 -> 0 11 0 ~> 2 1 ~> 3 2 ~> 27 3 ~> 27 4 ~> 6 5 ~> 3 6 ~> 27 7 ~> 27 8 ~> 10 9 ~> 11 10 ~> 27 11 ~> 27 12 ~> 14 13 ~> 11 14 ~> 27 15 ~> 27 16 ~> 18 17 ~> 19 18 ~> 27 19 ~> 27 20 ~> 22 21 ~> 19 22 ~> 27 23 ~> 27 0 4 -> 0 12 2 ~> 27 3 ~> 27 6 ~> 27 7 ~> 27 10 ~> 27 11 ~> 27 14 ~> 27 15 ~> 27 18 ~> 27 19 ~> 27 22 ~> 27 23 ~> 27 0 4 -> 0 13 1 ~> 27 2 ~> 27 3 ~> 27 5 ~> 27 6 ~> 27 7 ~> 27 9 ~> 27 10 ~> 27 11 ~> 27 13 ~> 27 14 ~> 27 15 ~> 27 17 ~> 27 18 ~> 27 19 ~> 27 21 ~> 27 22 ~> 27 23 ~> 27 0 4 -> 0 14 0 ~> 2 1 ~> 3 2 ~> 27 3 ~> 27 4 ~> 6 5 ~> 7 6 ~> 27 7 ~> 27 8 ~> 10 9 ~> 11 10 ~> 27 11 ~> 27 12 ~> 14 13 ~> 15 14 ~> 27 15 ~> 27 16 ~> 18 17 ~> 19 18 ~> 27 19 ~> 27 20 ~> 22 21 ~> 23 22 ~> 27 23 ~> 27 0 4 -> 0 15 0 ~> 2 1 ~> 27 2 ~> 27 3 ~> 27 4 ~> 6 5 ~> 27 6 ~> 27 7 ~> 27 8 ~> 10 9 ~> 27 10 ~> 27 11 ~> 27 12 ~> 14 13 ~> 27 14 ~> 27 15 ~> 27 16 ~> 18 17 ~> 27 18 ~> 27 19 ~> 27 20 ~> 22 21 ~> 27 22 ~> 27 23 ~> 27 0 5 -> 0 8 1 ~> 27 2 ~> 27 3 ~> 27 4 ~> 0 4 ~> 4 5 ~> 27 6 ~> 27 7 ~> 27 9 ~> 27 10 ~> 27 11 ~> 27 12 ~> 8 12 ~> 12 13 ~> 27 14 ~> 27 15 ~> 27 17 ~> 27 18 ~> 27 19 ~> 27 20 ~> 16 20 ~> 20 21 ~> 27 22 ~> 27 23 ~> 27 0 5 -> 0 10 0 ~> 2 1 ~> 27 2 ~> 27 3 ~> 27 4 ~> 2 4 ~> 6 5 ~> 27 6 ~> 27 7 ~> 27 8 ~> 10 9 ~> 27 10 ~> 27 11 ~> 27 12 ~> 10 12 ~> 14 13 ~> 27 14 ~> 27 15 ~> 27 16 ~> 18 17 ~> 27 18 ~> 27 19 ~> 27 20 ~> 18 20 ~> 22 21 ~> 27 22 ~> 27 23 ~> 27 0 5 -> 0 12 1 ~> 27 2 ~> 27 3 ~> 27 5 ~> 27 6 ~> 27 7 ~> 27 9 ~> 27 10 ~> 27 11 ~> 27 13 ~> 27 14 ~> 27 15 ~> 27 17 ~> 27 18 ~> 27 19 ~> 27 21 ~> 27 22 ~> 27 23 ~> 27 0 5 -> 0 13 1 ~> 27 2 ~> 27 3 ~> 27 5 ~> 27 6 ~> 27 7 ~> 27 9 ~> 27 10 ~> 27 11 ~> 27 13 ~> 27 14 ~> 27 15 ~> 27 17 ~> 27 18 ~> 27 19 ~> 27 21 ~> 27 22 ~> 27 23 ~> 27 0 5 -> 0 14 0 ~> 2 1 ~> 27 2 ~> 27 3 ~> 27 4 ~> 6 5 ~> 27 6 ~> 27 7 ~> 27 8 ~> 10 9 ~> 27 10 ~> 27 11 ~> 27 12 ~> 14 13 ~> 27 14 ~> 27 15 ~> 27 16 ~> 18 17 ~> 27 18 ~> 27 19 ~> 27 20 ~> 22 21 ~> 27 22 ~> 27 23 ~> 27 0 5 -> 0 15 0 ~> 2 1 ~> 27 2 ~> 27 3 ~> 27 4 ~> 6 5 ~> 27 6 ~> 27 7 ~> 27 8 ~> 10 9 ~> 27 10 ~> 27 11 ~> 27 12 ~> 14 13 ~> 27 14 ~> 27 15 ~> 27 16 ~> 18 17 ~> 27 18 ~> 27 19 ~> 27 20 ~> 22 21 ~> 27 22 ~> 27 23 ~> 27 0 6 -> 0 14 0 ~> 27 1 ~> 27 4 ~> 27 5 ~> 27 8 ~> 27 9 ~> 27 12 ~> 27 13 ~> 27 16 ~> 27 17 ~> 27 20 ~> 27 21 ~> 27 0 6 -> 0 15 0 ~> 27 1 ~> 27 3 ~> 27 4 ~> 27 5 ~> 27 7 ~> 27 8 ~> 27 9 ~> 27 11 ~> 27 12 ~> 27 13 ~> 27 15 ~> 27 16 ~> 27 17 ~> 27 19 ~> 27 20 ~> 27 21 ~> 27 23 ~> 27 0 7 -> 0 14 0 ~> 27 1 ~> 27 3 ~> 27 4 ~> 27 5 ~> 27 7 ~> 27 8 ~> 27 9 ~> 27 11 ~> 27 12 ~> 27 13 ~> 27 15 ~> 27 16 ~> 27 17 ~> 27 19 ~> 27 20 ~> 27 21 ~> 27 23 ~> 27 0 9 -> 0 17 2 ~> 27 3 ~> 27 5 ~> 27 6 ~> 27 7 ~> 27 10 ~> 27 11 ~> 27 13 ~> 27 14 ~> 27 15 ~> 27 18 ~> 27 19 ~> 27 21 ~> 27 22 ~> 27 23 ~> 27 0 11 -> 0 19 0 ~> 27 1 ~> 27 4 ~> 27 5 ~> 27 7 ~> 27 8 ~> 27 9 ~> 27 12 ~> 27 13 ~> 27 15 ~> 27 16 ~> 27 17 ~> 27 20 ~> 27 21 ~> 27 23 ~> 27 0 13 -> 0 21 1 ~> 27 2 ~> 27 3 ~> 27 5 ~> 27 6 ~> 27 7 ~> 27 9 ~> 27 10 ~> 27 11 ~> 27 13 ~> 27 14 ~> 27 15 ~> 27 17 ~> 27 18 ~> 27 19 ~> 27 21 ~> 27 22 ~> 27 23 ~> 27 0 15 -> 0 23 0 ~> 27 1 ~> 27 3 ~> 27 4 ~> 27 5 ~> 27 7 ~> 27 8 ~> 27 9 ~> 27 11 ~> 27 12 ~> 27 13 ~> 27 15 ~> 27 16 ~> 27 17 ~> 27 19 ~> 27 20 ~> 27 21 ~> 27 23 ~> 27 0 16 -> 0 26 0 ~> 0 0 ~> 1 1 ~> 0 2 ~> 27 3 ~> 27 4 ~> 4 4 ~> 5 5 ~> 4 6 ~> 27 7 ~> 27 8 ~> 8 8 ~> 9 9 ~> 8 10 ~> 27 11 ~> 27 12 ~> 12 12 ~> 13 13 ~> 12 14 ~> 27 15 ~> 27 16 ~> 16 16 ~> 17 17 ~> 16 18 ~> 27 19 ~> 27 20 ~> 20 20 ~> 21 21 ~> 20 22 ~> 27 23 ~> 27 0 16 -> 1 25 16 ~> 25 17 ~> 25 20 ~> 25 21 ~> 25 0 17 -> 0 26 0 ~> 0 0 ~> 1 1 ~> 0 2 ~> 27 3 ~> 27 4 ~> 4 4 ~> 5 5 ~> 27 6 ~> 27 7 ~> 27 8 ~> 8 8 ~> 9 9 ~> 8 10 ~> 27 11 ~> 27 12 ~> 12 12 ~> 13 13 ~> 27 14 ~> 27 15 ~> 27 16 ~> 16 16 ~> 17 17 ~> 16 18 ~> 27 19 ~> 27 20 ~> 20 20 ~> 21 21 ~> 27 22 ~> 27 23 ~> 27 0 17 -> 1 25 16 ~> 25 17 ~> 25 20 ~> 25 0 18 -> 0 26 0 ~> 27 1 ~> 27 2 ~> 2 2 ~> 3 3 ~> 2 4 ~> 27 5 ~> 27 6 ~> 6 6 ~> 7 7 ~> 6 8 ~> 27 9 ~> 27 10 ~> 10 10 ~> 11 11 ~> 10 12 ~> 27 13 ~> 27 14 ~> 14 14 ~> 15 15 ~> 14 16 ~> 27 17 ~> 27 18 ~> 18 18 ~> 19 19 ~> 18 20 ~> 27 21 ~> 27 22 ~> 22 22 ~> 23 23 ~> 22 0 18 -> 1 25 18 ~> 25 19 ~> 25 22 ~> 25 23 ~> 25 0 19 -> 0 26 0 ~> 27 1 ~> 27 2 ~> 2 2 ~> 3 3 ~> 2 4 ~> 27 5 ~> 27 6 ~> 6 6 ~> 7 7 ~> 27 8 ~> 27 9 ~> 27 10 ~> 10 10 ~> 11 11 ~> 10 12 ~> 27 13 ~> 27 14 ~> 14 14 ~> 15 15 ~> 27 16 ~> 27 17 ~> 27 18 ~> 18 18 ~> 19 19 ~> 18 20 ~> 27 21 ~> 27 22 ~> 22 22 ~> 23 23 ~> 27 0 19 -> 1 25 18 ~> 25 19 ~> 25 22 ~> 25 0 20 -> 0 26 0 ~> 0 0 ~> 1 1 ~> 0 2 ~> 27 3 ~> 27 4 ~> 4 4 ~> 5 5 ~> 4 6 ~> 27 7 ~> 27 8 ~> 8 8 ~> 9 9 ~> 8 10 ~> 27 11 ~> 27 12 ~> 12 12 ~> 13 13 ~> 12 14 ~> 27 15 ~> 27 16 ~> 16 16 ~> 17 17 ~> 16 18 ~> 27 19 ~> 27 20 ~> 20 20 ~> 21 21 ~> 20 22 ~> 27 23 ~> 27 0 20 -> 1 25 16 ~> 25 17 ~> 25 20 ~> 25 21 ~> 25 0 21 -> 0 26 0 ~> 0 0 ~> 1 1 ~> 27 2 ~> 27 3 ~> 27 4 ~> 4 4 ~> 5 5 ~> 27 6 ~> 27 7 ~> 27 8 ~> 8 8 ~> 9 9 ~> 27 10 ~> 27 11 ~> 27 12 ~> 12 12 ~> 13 13 ~> 27 14 ~> 27 15 ~> 27 16 ~> 16 16 ~> 17 17 ~> 27 18 ~> 27 19 ~> 27 20 ~> 20 20 ~> 21 21 ~> 27 22 ~> 27 23 ~> 27 0 21 -> 1 25 16 ~> 25 20 ~> 25 0 22 -> 0 26 0 ~> 27 1 ~> 27 2 ~> 2 2 ~> 3 3 ~> 2 4 ~> 27 5 ~> 27 6 ~> 6 6 ~> 7 7 ~> 6 8 ~> 27 9 ~> 27 10 ~> 10 10 ~> 11 11 ~> 10 12 ~> 27 13 ~> 27 14 ~> 14 14 ~> 15 15 ~> 14 16 ~> 27 17 ~> 27 18 ~> 18 18 ~> 19 19 ~> 18 20 ~> 27 21 ~> 27 22 ~> 22 22 ~> 23 23 ~> 22 0 22 -> 1 25 18 ~> 25 19 ~> 25 22 ~> 25 23 ~> 25 0 23 -> 0 26 0 ~> 27 1 ~> 27 2 ~> 2 2 ~> 3 3 ~> 27 4 ~> 27 5 ~> 27 6 ~> 6 6 ~> 7 7 ~> 27 8 ~> 27 9 ~> 27 10 ~> 10 10 ~> 11 11 ~> 27 12 ~> 27 13 ~> 27 14 ~> 14 14 ~> 15 15 ~> 27 16 ~> 27 17 ~> 27 18 ~> 18 18 ~> 19 19 ~> 27 20 ~> 27 21 ~> 27 22 ~> 22 22 ~> 23 23 ~> 27 0 23 -> 1 25 18 ~> 25 22 ~> 25 0 24 -> 0 2 24 ~> 2