Use a shorter fix proposed by @damiendoligez.

Co-authored-by: Damien Doligez <[email protected]> Signed-off-by: Karolis Petrauskas <[email protected]>
tlaplus · Dec 21, 2023 · 6c7178e · 6c7178e
1 parent c822f18
commit 6c7178e
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/test/fast/regression/setEuclid_test.tla b/test/fast/regression/setEuclid_test.tla
@@ -361,7 +361,10 @@ THEOREM Inv /\ Next => Inv'
 (*|*)   BY <3>1, <3>2
     <2>3. CorrectTermination'
       <3>1. Cardinality (S) = 1 => S = {CHOOSE t \in S : TRUE}
-        BY CardThm DEF Inv, TypeOK
+        <4> Cardinality (S) = 1 => \E x \in S : S = {x}
+          BY CardThm DEF Inv, TypeOK
+        <4> QED
+          BY Zenon
       <3>2. Cardinality (S) = 1 => GCD (S) = CHOOSE t \in S : TRUE
         BY <3>1, GCD2 DEF Inv, TypeOK
       <3> QED