Stephan Merz

> Safe == > []TerminationDetected => []Terminated The algorithm even has the stronger property [](TerminationDetected => []Terminated) Stephan > On 26 Jan 2022, at 17:42, Markus Alexander Kuppe ***@***.***> wrote:...

The definition of Wakeup(i) in AsyncTerminationDetection could be changed to /\ pending[i] > 0 /\ \/ UNCHANGED active \/ ~ active[i] /\ active' = [active EXCEPT ![i] = TRUE] /\...

Ah, GitHub formatting ... maybe this works better: ```tla /\ pending[i] > 0 /\ \/ UNCHANGED active \/ ~ active[i] /\ active' = [active EXCEPT ![i] = TRUE] /\ pending'...

I think the *_theorems(_proofs) modules should also be moved to the CommunityModules so that everything is in one place and that they get better visibility. Obviously, they only need to...

TLAPS doesn't support quantification over tuples: > Quantification over tuples and set constructors using tuples are not supported > (for example { \in S \X T : ...}). Note that...

@kape1395 I fail to reproduce your results. For me, neither `simp` nor `auto` solve your theorem, but `blast` does. The reduction from `∀ e ∈ S : op (e) =...

@kape1395 Some more investigation and bisection revealed two issues in `SetTheory.thy`: (i) one elimination rule was (clearly) too general, and (ii) adding rule `bspec` to preprocessing for the simplifier also...

@kape1395 Thank you very much for investigating this further! I would have hoped the interference between bounded quantification and rewrite of `Nat` to be handled by the congruence rules `bAllCong`...

The Linux foundation requires us to sign all commits: this was not the case before. In fact, I had noticed that I had forgotten to sign and tried to amend...

I was a bit sloppy in my description of the workaround. The following proof works for me: ```tla LEMMA ASSUME NEW s \in Stream, NEW n \in Nat, s[n].seq #...