From c5e38cfbd5042d47c2e6f4b86008fb376f39bfdf Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 30 Oct 2026 05:52:45 -0700 Subject: [PATCH] CRDT: cite the induction hypothesis in the proof of OGLiveness. Step <1>2 of OGLiveness did not cite its own assumption, the induction hypothesis, so tlapm proved the step only because of soundness bug 309 that ignored the bound variable of terms under a binder. With that bug fixed, the step fails. Citing <1>2 makes the proof go through with tlapm before and after the fix. Related to Github tlapm issue #309 https://github.com/tlaplus/tlapm/issues/309 Co-authored-by: Claude Opus 5.5 Signed-off-by: Markus Alexander Kuppe --- specifications/FiniteMonotonic/CRDT_proof.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specifications/FiniteMonotonic/CRDT_proof.tla b/specifications/FiniteMonotonic/CRDT_proof.tla index 7e4d016a..6961f8d0 100644 --- a/specifications/FiniteMonotonic/CRDT_proof.tla +++ b/specifications/FiniteMonotonic/CRDT_proof.tla @@ -339,7 +339,7 @@ THEOREM OGLiveness == OGSpec => <>(\A n, o \in Node : counter[n] = counter[o]) <1>2. ASSUME NEW m \in Nat, \A k \in 0 .. (m-1) : S(k) PROVE S(m) - BY <1>1 + BY <1>1, <1>2 <1>3. \A m \in Nat : S(m) <2>. HIDE DEF S <2>. QED BY <1>2, GeneralNatInduction, Isa