// Parikh automata intersection problem, generated by OSTRICH+

counter int R0, R1, R103, R104, R105, R106, R107, R108, R109, R110, R111, R112, R113, R114, R115, R116, R117, R118, R119, R120, R121, R122, R123, R124, R125, R126, R127, R128, R129, R13, R130, R131, R132, R133, R134, R135, R136, R137, R138, R139, R14, R140, R141, R142, R143, R144, R145, R146, R147, R148, R149, R150, R151, R152, R153, R154, R155, R156, R2, R3, R4, R5, R6, R7, R8, R9;

synchronised { // Automata constraining P62

automaton P62_0 {

init s0;

s0 -> s1 [118, 118];

accepting s1;

};

};

synchronised { // Automata constraining value1

automaton value1_0 {

init s0;

s0 -> s0 [0, 43];

s0 -> s0 [45, 60];

s0 -> s1 [61, 61];

s0 -> s0 [62, 65535];

s1 -> s1 [0, 43];

s1 -> s1 [45, 65535];

accepting s1;

};

automaton value1_1 {

init s0;

s0 -> s0 [0, 65535] { R3 += 1 };

accepting s0;

};

automaton value1_2 {

init s0;

s0 -> s1 [0, 60] { R14 += 1 };

s0 -> s0 [0, 65535] { R13 += 1, R14 += 1 };

s0 -> s2 [61, 61];

s0 -> s1 [62, 65535] { R14 += 1 };

s1 -> s1 [0, 60] { R14 += 1 };

s1 -> s2 [61, 61];

s1 -> s1 [62, 65535] { R14 += 1 };

s2 -> s2 [0, 65535];

accepting s2;

};

automaton value1_3 {

init s0;

s0 -> s1 [0, 65535] { R122 += 1, R0 += 1 };

s0 -> s0 [0, 65535] { R121 += 1, R122 += 1 };

s1 -> s1 [0, 65535] { R122 += 1, R0 += 1 };

s1 -> s2 [0, 65535];

s2 -> s2 [0, 65535];

accepting s0, s1, s2;

};

automaton value1_4 {

init s0;

s0 -> s1 [0, 64] { R134 += 1 };

s0 -> s0 [0, 65535] { R133 += 1, R134 += 1 };

s0 -> s2 [86, 86] { R134 += 1 };

s0 -> s1 [87, 65535] { R134 += 1 };

s1 -> s1 [0, 64] { R134 += 1 };

s1 -> s2 [86, 86] { R134 += 1 };

s1 -> s1 [87, 65535] { R134 += 1 };

s2 -> s2 [0, 64] { R134 += 1 };

s2 -> s2 [0, 65535];

s2 -> s2 [86, 65535] { R134 += 1 };

accepting s2;

};

automaton value1_5 {

init s0;

s0 -> s1 [0, 65535] { R136 += 1, R2 += 1 };

s0 -> s0 [0, 65535] { R135 += 1, R136 += 1 };

s1 -> s1 [0, 65535] { R136 += 1, R2 += 1 };

s1 -> s2 [0, 65535];

s2 -> s2 [0, 65535];

accepting s0, s1, s2;

};

automaton value1_6 {

init s0;

s0 -> s1 [0, 85] { R138 += 1 };

s0 -> s0 [0, 65535] { R137 += 1, R138 += 1 };

s0 -> s2 [0, 65535] { R138 += 1, R9 += 1 };

s0 -> s3 [86, 86] { R138 += 1 };

s0 -> s1 [87, 65535] { R138 += 1 };

s1 -> s1 [0, 85] { R138 += 1 };

s1 -> s1 [0, 65535];

s1 -> s3 [86, 86] { R138 += 1 };

s1 -> s1 [87, 65535] { R138 += 1 };

s2 -> s1 [0, 85] { R138 += 1 };

s2 -> s4 [0, 65535];

s2 -> s2 [0, 65535] { R138 += 1, R9 += 1 };

s2 -> s3 [86, 86] { R138 += 1 };

s2 -> s1 [87, 65535] { R138 += 1 };

s3 -> s3 [0, 65535] { R138 += 1 };

s4 -> s4 [0, 65535];

accepting s0, s1, s2, s4;

};

automaton value1_7 {

init s0;

s0 -> s1 [0, 8] { R140 += 1, R114 += 1 };

s0 -> s2 [0, 65535] { R140 += 1, R113 += 1, R114 += 1 };

s0 -> s0 [0, 65535] { R139 += 1, R140 += 1 };

s0 -> s3 [9, 13] { R140 += 1, R114 += 1 };

s0 -> s1 [14, 31] { R140 += 1, R114 += 1 };

s0 -> s3 [32, 32] { R140 += 1, R114 += 1 };

s0 -> s1 [33, 65535] { R140 += 1, R114 += 1 };

s1 -> s1 [0, 65535] { R140 += 1, R114 += 1 };

s1 -> s4 [0, 65535];

s1 -> s5 [0, 65535] { R140 += 1 };

s2 -> s1 [0, 8] { R140 += 1, R114 += 1 };

s2 -> s2 [0, 65535] { R140 += 1, R113 += 1, R114 += 1 };

s2 -> s4 [0, 65535];

s2 -> s3 [9, 13] { R140 += 1, R114 += 1 };

s2 -> s1 [14, 31] { R140 += 1, R114 += 1 };

s2 -> s3 [32, 32] { R140 += 1, R114 += 1 };

s2 -> s1 [33, 65535] { R140 += 1, R114 += 1 };

s3 -> s1 [0, 65535] { R140 += 1, R114 += 1 };

s4 -> s4 [0, 65535];

s5 -> s4 [0, 65535];

s5 -> s5 [0, 65535] { R140 += 1 };

accepting s4, s5, s2, s1, s0;

};

automaton value1_8 {

init s0;

s0 -> s1 [0, 65535] { R142 += 1, R115 += 1, R116 += 1 };

s0 -> s2 [0, 65535] { R142 += 1, R116 += 1, R6 += 1 };

s0 -> s0 [0, 65535] { R141 += 1, R142 += 1 };

s1 -> s1 [0, 65535] { R142 += 1, R115 += 1, R116 += 1 };

s1 -> s2 [0, 65535] { R142 += 1, R116 += 1, R6 += 1 };

s1 -> s4 [0, 65535];

s2 -> s2 [0, 65535] { R142 += 1, R116 += 1, R6 += 1 };

s2 -> s3 [0, 65535] { R142 += 1 };

s2 -> s4 [0, 65535];

s3 -> s3 [0, 65535] { R142 += 1 };

s3 -> s4 [0, 65535];

s4 -> s4 [0, 65535];

accepting s3, s4, s2, s1, s0;

};

automaton value1_9 {

init s0;

s0 -> s1 [0, 8] { R144 += 1, R118 += 1 };

s0 -> s2 [0, 65535] { R144 += 1, R117 += 1, R118 += 1 };

s0 -> s0 [0, 65535] { R143 += 1, R144 += 1 };

s0 -> s3 [9, 13] { R144 += 1, R118 += 1 };

s0 -> s1 [14, 31] { R144 += 1, R118 += 1 };

s0 -> s3 [32, 32] { R144 += 1, R118 += 1 };

s0 -> s1 [33, 65535] { R144 += 1, R118 += 1 };

s1 -> s1 [0, 65535] { R144 += 1, R118 += 1 };

s1 -> s5 [0, 65535] { R144 += 1 };

s1 -> s4 [0, 65535];

s2 -> s1 [0, 8] { R144 += 1, R118 += 1 };

s2 -> s2 [0, 65535] { R144 += 1, R117 += 1, R118 += 1 };

s2 -> s4 [0, 65535];

s2 -> s3 [9, 13] { R144 += 1, R118 += 1 };

s2 -> s1 [14, 31] { R144 += 1, R118 += 1 };

s2 -> s3 [32, 32] { R144 += 1, R118 += 1 };

s2 -> s1 [33, 65535] { R144 += 1, R118 += 1 };

s3 -> s1 [0, 65535] { R144 += 1, R118 += 1 };

s4 -> s4 [0, 65535];

s5 -> s5 [0, 65535] { R144 += 1 };

s5 -> s4 [0, 65535];

accepting s4, s5, s2, s1, s0;

};

automaton value1_10 {

init s0;

s0 -> s0 [0, 65535] { R145 += 1, R146 += 1 };

s0 -> s1 [0, 65535] { R146 += 1, R120 += 1, R7 += 1 };

s0 -> s2 [0, 65535] { R146 += 1, R119 += 1, R120 += 1 };

s1 -> s1 [0, 65535] { R146 += 1, R120 += 1, R7 += 1 };

s1 -> s3 [0, 65535];

s1 -> s4 [0, 65535] { R146 += 1 };

s2 -> s1 [0, 65535] { R146 += 1, R120 += 1, R7 += 1 };

s2 -> s2 [0, 65535] { R146 += 1, R119 += 1, R120 += 1 };

s2 -> s3 [0, 65535];

s3 -> s3 [0, 65535];

s4 -> s3 [0, 65535];

s4 -> s4 [0, 65535] { R146 += 1 };

accepting s3, s4, s2, s1, s0;

};

automaton value1_11 {

init s0;

s0 -> s1 [0, 85] { R148 += 1, R124 += 1 };

s0 -> s0 [0, 65535] { R147 += 1, R148 += 1 };

s0 -> s2 [0, 65535] { R148 += 1, R123 += 1, R124 += 1 };

s0 -> s1 [87, 65535] { R148 += 1, R124 += 1 };

s1 -> s1 [0, 85] { R148 += 1, R124 += 1 };

s1 -> s3 [0, 65535];

s1 -> s1 [0, 65535] { R148 += 1 };

s1 -> s1 [87, 65535] { R148 += 1, R124 += 1 };

s2 -> s1 [0, 85] { R148 += 1, R124 += 1 };

s2 -> s3 [0, 65535];

s2 -> s2 [0, 65535] { R148 += 1, R123 += 1, R124 += 1 };

s2 -> s1 [87, 65535] { R148 += 1, R124 += 1 };

s3 -> s3 [0, 65535];

accepting s0, s1, s2, s3;

};

automaton value1_12 {

init s0;

s0 -> s0 [0, 65535] { R149 += 1, R150 += 1 };

s0 -> s1 [0, 65535] { R150 += 1, R126 += 1, R103 += 1 };

s0 -> s2 [0, 65535] { R150 += 1, R125 += 1, R126 += 1 };

s1 -> s4 [0, 65535] { R150 += 1 };

s1 -> s3 [0, 65535];

s1 -> s1 [0, 65535] { R150 += 1, R126 += 1, R103 += 1 };

s2 -> s3 [0, 65535];

s2 -> s1 [0, 65535] { R150 += 1, R126 += 1, R103 += 1 };

s2 -> s2 [0, 65535] { R150 += 1, R125 += 1, R126 += 1 };

s3 -> s3 [0, 65535];

s4 -> s4 [0, 65535] { R150 += 1 };

s4 -> s3 [0, 65535];

accepting s3, s4, s2, s1, s0;

};

automaton value1_13 {

init s0;

s0 -> s1 [0, 86] { R152 += 1, R128 += 1 };

s0 -> s2 [0, 65535] { R152 += 1, R127 += 1, R128 += 1 };

s0 -> s0 [0, 65535] { R151 += 1, R152 += 1 };

s0 -> s3 [87, 87] { R152 += 1, R128 += 1 };

s0 -> s1 [88, 65535] { R152 += 1, R128 += 1 };

s1 -> s1 [0, 86] { R152 += 1, R128 += 1 };

s1 -> s3 [87, 87] { R152 += 1, R128 += 1 };

s1 -> s1 [88, 65535] { R152 += 1, R128 += 1 };

s2 -> s1 [0, 86] { R152 += 1, R128 += 1 };

s2 -> s2 [0, 65535] { R152 += 1, R127 += 1, R128 += 1 };

s2 -> s3 [87, 87] { R152 += 1, R128 += 1 };

s2 -> s1 [88, 65535] { R152 += 1, R128 += 1 };

s3 -> s4 [0, 65535];

s3 -> s3 [0, 65535] { R152 += 1, R128 += 1 };

s3 -> s5 [0, 65535] { R152 += 1 };

s4 -> s4 [0, 65535];

s5 -> s4 [0, 65535];

s5 -> s5 [0, 65535] { R152 += 1 };

accepting s3, s4, s5;

};

automaton value1_14 {

init s0;

s0 -> s1 [0, 65535] { R154 += 1, R130 += 1, R104 += 1 };

s0 -> s0 [0, 65535] { R153 += 1, R154 += 1 };

s0 -> s2 [0, 65535] { R154 += 1, R129 += 1, R130 += 1 };

s1 -> s1 [0, 65535] { R154 += 1, R130 += 1, R104 += 1 };

s1 -> s3 [0, 65535];

s1 -> s4 [0, 65535] { R154 += 1 };

s2 -> s1 [0, 65535] { R154 += 1, R130 += 1, R104 += 1 };

s2 -> s3 [0, 65535];

s2 -> s2 [0, 65535] { R154 += 1, R129 += 1, R130 += 1 };

s3 -> s3 [0, 65535];

s4 -> s3 [0, 65535];

s4 -> s4 [0, 65535] { R154 += 1 };

accepting s3, s4, s2, s1, s0;

};

automaton value1_15 {

init s0;

s0 -> s1 [0, 85] { R156 += 1, R132 += 1 };

s0 -> s0 [0, 65535] { R155 += 1, R156 += 1 };

s0 -> s2 [0, 65535] { R156 += 1, R131 += 1, R132 += 1 };

s0 -> s3 [86, 86] { R156 += 1, R132 += 1 };

s0 -> s4 [86, 86] { R156 += 1, R132 += 1 };

s0 -> s1 [88, 65535] { R156 += 1, R132 += 1 };

s1 -> s1 [0, 85] { R156 += 1, R132 += 1 };

s1 -> s1 [0, 65535] { R156 += 1 };

s1 -> s5 [0, 65535];

s1 -> s3 [86, 86] { R156 += 1, R132 += 1 };

s1 -> s4 [86, 86] { R156 += 1, R132 += 1 };

s1 -> s1 [88, 65535] { R156 += 1, R132 += 1 };

s2 -> s1 [0, 85] { R156 += 1, R132 += 1 };

s2 -> s2 [0, 65535] { R156 += 1, R131 += 1, R132 += 1 };

s2 -> s5 [0, 65535];

s2 -> s3 [86, 86] { R156 += 1, R132 += 1 };

s2 -> s4 [86, 86] { R156 += 1, R132 += 1 };

s2 -> s1 [88, 65535] { R156 += 1, R132 += 1 };

s3 -> s3 [0, 86] { R156 += 1, R132 += 1 };

s3 -> s3 [0, 65535] { R156 += 1 };

s3 -> s5 [0, 65535];

s3 -> s3 [88, 65535] { R156 += 1, R132 += 1 };

s4 -> s5 [0, 65535];

s4 -> s4 [0, 65535] { R156 += 1 };

s5 -> s5 [0, 65535];

accepting s3, s4, s5, s2, s1, s0;

};

};

synchronised { // Automata constraining value2

automaton value2_0 {

init s0;

s0 -> s0 [0, 43];

s0 -> s0 [45, 64];

s0 -> s0 [91, 65535];

accepting s0;

};

automaton value2_1 {

init s0;

s0 -> s0 [0, 65535] { R1 += 1 };

accepting s0;

};

automaton value2_2 {

init s0;

s0 -> s1 [0, 60];

s0 -> s0 [0, 65535] { R8 += 1 };

s0 -> s2 [61, 61];

s0 -> s1 [62, 65535];

s1 -> s1 [0, 60];

s1 -> s2 [61, 61];

s1 -> s1 [62, 65535];

s2 -> s2 [0, 65535];

accepting s0, s1;

};

automaton value2_3 {

init s0;

s0 -> s1 [0, 8] { R106 += 1 };

s0 -> s0 [0, 65535] { R105 += 1, R106 += 1 };

s0 -> s2 [9, 13] { R106 += 1 };

s0 -> s1 [14, 31] { R106 += 1 };

s0 -> s2 [32, 32] { R106 += 1 };

s0 -> s1 [33, 65535] { R106 += 1 };

s1 -> s1 [0, 65535] { R106 += 1 };

s1 -> s3 [0, 65535];

s2 -> s1 [0, 65535] { R106 += 1 };

s3 -> s3 [0, 65535];

accepting s0, s1, s3;

};

automaton value2_4 {

init s0;

s0 -> s1 [0, 65535] { R108 += 1, R4 += 1 };

s0 -> s0 [0, 65535] { R107 += 1, R108 += 1 };

s1 -> s1 [0, 65535] { R108 += 1, R4 += 1 };

s1 -> s2 [0, 65535];

s2 -> s2 [0, 65535];

accepting s0, s1, s2;

};

automaton value2_5 {

init s0;

s0 -> s1 [0, 8] { R110 += 1 };

s0 -> s0 [0, 65535] { R109 += 1, R110 += 1 };

s0 -> s2 [9, 13] { R110 += 1 };

s0 -> s1 [14, 31] { R110 += 1 };

s0 -> s2 [32, 32] { R110 += 1 };

s0 -> s1 [33, 65535] { R110 += 1 };

s1 -> s1 [0, 65535] { R110 += 1 };

s1 -> s3 [0, 65535];

s2 -> s1 [0, 65535] { R110 += 1 };

s3 -> s3 [0, 65535];

accepting s0, s1, s3;

};

automaton value2_6 {

init s0;

s0 -> s1 [0, 65535] { R112 += 1, R5 += 1 };

s0 -> s0 [0, 65535] { R111 += 1, R112 += 1 };

s1 -> s2 [0, 65535];

s1 -> s1 [0, 65535] { R112 += 1, R5 += 1 };

s2 -> s2 [0, 65535];

accepting s0, s1, s2;

};

};

constraint R2 = R128 && R3 = R122 && R13 = 0 && R14 = R156 && R113 - R128 = -1 && R114 = R128 && R115 - R128 = -1 && R116 = R128 && R117 = 0 && R118 = 1 && R119 = 0 && R120 = 1 && R121 - R156 = 1 && R123 = 0 && R124 = R128 && R125 = 0 && R126 = R128 && R127 = 0 && R133 = 0 && R134 = R156 && R135 = 0 && R136 = R156 && R137 = 0 && R138 = R156 && R139 = 0 && R140 = R156 && R141 = 0 && R142 = R156 && R143 = 0 && R144 = R156 && R145 = 0 && R146 = R156 && R147 = 0 && R148 = R156 && R149 = 0 && R150 = R156 && R151 = 0 && R152 = R156 && R153 = 0 && R154 = R156 && R155 = 0 && R0 != 0 && R1 != 0 && R8 < 1 && R9 < 1 && R156 < R122 && 0 < R128 && -1 < R156 && (R4 != 0 || ((R1 != R106 || R105 - R106 = -1 || R106 < 0) && (R1 = R106 || R1 < 1))) && (R4 != 0 || ((R1 != R108 || R107 - R108 = -1 || R108 < 0) && (R1 = R108 || R1 < 1))) && (R109 != 0 || ((R5 != 0 || ((R1 != R110 || R110 = 1 || R110 < 0) && (R1 = R110 || R110 = 1 || R1 < 1))) && (R5 = 0 || ((R1 != R110 || R110 = 1 || R110 < 0) && (R110 != 1 || -1 < R1) && (R1 = R110 || R110 = 1))))) && (R111 != 0 || ((R5 != 0 || ((R1 != R112 || R112 = 1 || R112 < 0) && (R1 = R112 || R112 = 1 || R1 < 1))) && (R5 = 0 || ((R1 != R112 || R112 = 1 || R112 < 0) && (R112 != 1 || -1 < R1) && (R1 = R112 || R112 = 1))))) && (R4 = 0 || (R1 = R106 && R105 - R106 = -1)) && (R4 = 0 || (R1 = R108 && R107 - R108 = -1)) && (R104 = 0 || (R129 = 0 && R130 = 0)) && (R104 = 0 || (R131 = 0 && R132 = 0)) && (R109 = 0 || (R5 = 0 && R1 < 0)) && (R111 = 0 || (R5 = 0 && R1 < 0));

// End of Parikh automata intersection problem