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