190 A.4.2 Verification output - A graphical analysis tool for hardware design

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_0) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_0)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_1) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_2) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_3) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_4) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_4)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_5) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_5)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_6) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_6)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_7) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_7)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_8) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_8)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_9) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_9)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_10) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_10)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_11) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_11)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_12) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_12)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_13) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_13)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_14) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_14)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_15) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_15)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_16) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_16)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_17) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_17)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_18) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_18)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_19) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_19)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_20) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_20)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_21) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_21)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_22) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_22)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_23) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_23)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_24) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_24)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_25) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_25)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_26) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_26)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_27) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_27)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_28) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_28)) is true

191

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_29) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_29)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_30) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_30)) is true

-- specification AG ((sig_m = 0d5_0 & sig_n = 0d5_31) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_31)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_0) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_1) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_2) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_3) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_4) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_5) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_6) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_7) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_8) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_9) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_10) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_11) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_12) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_13) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_14) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_15) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_16) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_17) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_18) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_19) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_20) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_21) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_22) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_23) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_24) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_25) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_26) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_27) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

192

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_28) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_29) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_30) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_1 & sig_n = 0d5_31) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_0) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_1) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_2) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_3) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_4) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_5) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_6) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_7) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_8) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_9) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_10) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_11) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_12) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_13) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_14) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_15) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_16) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_17) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_18) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_19) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_20) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_21) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_22) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_23) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_24) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_25) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_26) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

193

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_27) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_28) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_29) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_30) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_2 & sig_n = 0d5_31) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_0) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_1) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_2) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_3) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_4) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_5) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_6) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_7) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_8) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_9) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_10) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_11) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_12) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_13) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_14) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_15) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_16) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_17) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_18) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_19) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_20) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_21) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_22) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_23) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_24) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_25) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

194

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_26) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_27) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_28) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_29) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_30) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_3 & sig_n = 0d5_31) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_0) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_4)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_1) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_2) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_3) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_4) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_4)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_5) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_6) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_7) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_8) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_4)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_9) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_10) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_11) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_12) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_4)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_13) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_14) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_15) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_16) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_4)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_17) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_18) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_19) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_20) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_4)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_21) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_22) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_23) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_24) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_4)) is true

195

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_25) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_26) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_27) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_28) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_4)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_29) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_30) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_4 & sig_n = 0d5_31) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_0) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_5)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_1) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_2) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_3) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_4) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_5) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_5)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_6) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_7) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_8) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_9) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_10) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_5)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_11) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_12) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_13) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_14) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_15) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_5)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_16) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_17) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_18) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_19) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_20) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_5)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_21) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_22) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_23) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

196

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_24) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_25) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_5)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_26) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_27) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_28) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_29) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_30) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_5)) is true

-- specification AG ((sig_m = 0d5_5 & sig_n = 0d5_31) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_0) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_6)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_1) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_2) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_3) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_4) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_5) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_6) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_6)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_7) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_8) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_9) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_10) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_11) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_12) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_6)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_13) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_14) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_15) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_16) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_17) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_18) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_6)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_19) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_20) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_21) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_22) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

197

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_23) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_24) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_6)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_25) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_26) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_27) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_28) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_29) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_30) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_6)) is true

-- specification AG ((sig_m = 0d5_6 & sig_n = 0d5_31) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_0) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_7)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_1) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_2) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_3) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_4) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_5) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_6) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_7) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_7)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_8) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_9) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_10) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_11) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_12) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_13) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_14) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_7)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_15) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_16) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_17) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_18) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_19) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_20) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_21) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_7)) is true

198

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_22) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_23) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_24) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_25) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_26) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_27) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_28) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_7)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_29) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_30) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_7 & sig_n = 0d5_31) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_0) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_8)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_1) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_2) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_3) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_4) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_4)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_5) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_6) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_7) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_8) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_8)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_9) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_10) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_11) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_12) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_4)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_13) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_14) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_15) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_16) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_8)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_17) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_18) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_19) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_20) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_4)) is true

199

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_21) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_22) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_23) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_24) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_8)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_25) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_26) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_27) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_28) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_4)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_29) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_30) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_8 & sig_n = 0d5_31) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_0) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_9)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_1) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_2) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_3) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_4) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_5) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_6) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_7) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_8) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_9) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_9)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_10) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_11) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_12) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_13) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_14) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_15) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_16) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_17) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_18) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_9)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_19) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

200

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_20) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_21) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_22) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_23) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_24) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_25) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_26) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_27) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_9)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_28) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_29) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_30) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_3)) is true

-- specification AG ((sig_m = 0d5_9 & sig_n = 0d5_31) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_10 & sig_n = 0d5_0) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_10)) is true

-- specification AG ((sig_m = 0d5_10 & sig_n = 0d5_1) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_10 & sig_n = 0d5_2) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_10 & sig_n = 0d5_3) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_10 & sig_n = 0d5_4) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_10 & sig_n = 0d5_5) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_5)) is true

-- specification AG ((sig_m = 0d5_10 & sig_n = 0d5_6) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_10 & sig_n = 0d5_7) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_10 & sig_n = 0d5_8) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_10 & sig_n = 0d5_9) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_10 & sig_n = 0d5_10) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_10)) is true

-- specification AG ((sig_m = 0d5_10 & sig_n = 0d5_11) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_1)) is true

-- specification AG ((sig_m = 0d5_10 & sig_n = 0d5_12) -> (sig_gcd = 0d5_0 | sig_gcd = 0d5_2)) is true

-- specification AG ((sig_m = 0d5_10 & sig_n = 0d5_13) -> (sig_gcd = 0d5_0 |

In document A graphical analysis tool for hardware design (Sider 190-200)