Merge pull request #98 from tlaplus/fix-setEuclid

fixed bogus proof in setEuclid_test.tla
tlaplus · Dec 21, 2023 · a0ae986 · a0ae986
2 parents fe954fc + 6c7178e
commit a0ae986
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