NuSMV source with CTL specifications defined

MODULE main VAR

sig_m : word[5];

sig_n : word[5];

sig_gcd : word[5];

172

um_euclid : mod_euclid(sig_m, sig_n, sig_gcd);

um_test_euclid : mod_test_euclid(sig_m, sig_n);

CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_0) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_7) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_8) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_9) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_10) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_11) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_12) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_13) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_14) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_15) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_16) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_17) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_18) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_19) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_20) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_21) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_22) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_23) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_24) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_25) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_26) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_27) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_28) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_29) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_30) CTLSPEC AG (sig_m = 0d5_0 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_31) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_1 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1)

173

CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_2 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_3 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2)

174

CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_4 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_5 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1)

175

CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_6 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_7) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_7) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_7) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_7) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_7) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_7 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_8) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_8) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_8) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_8)

176

CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_8 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_9) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_9) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_9) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_9) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_9 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_10) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_10) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_10) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_10) CTLSPEC AG (sig_m = 0d5_10 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1)

177

CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_11) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_11) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_11) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_11 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_12) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_12) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_12) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_12 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_13) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1)

178

CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_13) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_13) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_13 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_14) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_7) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_14) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_7) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_14) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_14 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_15) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1)

179

CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_15) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_15) CTLSPEC AG (sig_m = 0d5_15 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_16) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_8) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_16) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_8) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_16 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_17) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_17) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1)

180

CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_17 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_18) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_9) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_18) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_9) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_18 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_19) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_19) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1)

181

CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_19 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_20) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_10) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_20) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_10) CTLSPEC AG (sig_m = 0d5_20 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_21) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_7) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_7) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_21) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_7) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_21 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_22) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2)

182

CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_11) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_22) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_22 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_23) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_23) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_23 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_24) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_8) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3)

183

CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_12) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_8) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_24) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_24 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_25) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_25) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_25 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_26) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_13) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2)

184

CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_26) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_26 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_27) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_9) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_9) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_27) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_27 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_28) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_7) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_14) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_7) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1)

185

CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_4) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_28) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_28 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_29) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_29) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_29 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_30) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_10) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_15) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_10) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_6) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_5) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_2) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_30)

186

CTLSPEC AG (sig_m = 0d5_30 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_0 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_31) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_1 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_2 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_3 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_4 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_5 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_6 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_7 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_8 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_9 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_10 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_11 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_12 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_13 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_14 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_15 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_16 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_17 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_18 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_19 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_20 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_21 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_22 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_23 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_24 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_25 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_26 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_27 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_28 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_29 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_1) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_31)

CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_30 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3) CTLSPEC AG (sig_m = 0d5_31 & sig_n = 0d5_31 -> sig_gcd = 0d5_0 | sig_gcd = 0d5_3)

MODULE mod_euclid(inp_m_in, inp_n_in, out_gcd)

187

188

189

190