# [tlaplus] The Euclid algorithm and TLAPS 1.4.5

Hi,

I have just upgraded TLAPS from v1.4.3 to v1.4.5. I use TLA+ Toolbox v1.7.0 on Ubuntu.

And unfortunately TLAPS is not able to prove the following part of the Euclid algorithm:

THEOREM GCDProperty3 == ASSUME
NEW p \in Number,
NEW q \in Number,
q > p
PROVE GCD(p, q) = GCD(p, q - p)
<1> USE DEF Divisors, |
<1>1 \A d \in Number: d | p /\ d | q => d | (q - p)
BY DEF Number
<1>2 \A d \in Number: d | p /\ d | (q - p) => d | q
BY DEF Number
<1> QED
BY <1>1, <1>2 DEF GCD

More precisely, it cannot prove <1>1 and <1>2. I can see timeout after 30 seconds or something.

Downgrading to v1.4.3 solves the issue.

Has anybody encountered a similar issue? Or maybe somebody managed to prove the Euclid algorithm with TLAPS v1.4.5?

Best Regards,
Pawel

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.