EWD840_proof: do not rely on instantiation distributing over WF.

Instantiation does not distribute over ENABLED, and hence not over WF.
The proof of Spec => TD!Spec relied on WF_TD!vars(TD!DetectTermination)
matching the fairness conjunct of TD!Spec, which tlapm#321 no longer
allows. SyncTerminationDetection now names its fairness condition Fair,
and the proof derives TD!Fair from the new lemma
SyncTerminationDetection_proof!Fairness, as suggested by Stephan Merz.

tlaplus/tlapm#69
tlaplus/tlapm#321

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

specifications/ewd840/EWD840_proof.tla

@@ -281,8 +281,10 @@ BY Live, TypeCorrect, Invariant, PTL DEF Spec
 (* Note that the parameters of the module SyncTerminationDetection are     *)
 (* instantiated by the symbols of the same name in the present module.     *)
 (***************************************************************************)
+TDP == INSTANCE SyncTerminationDetection_proof
+
 THEOREM Spec => TD!Spec
-<1>. USE DEF Node, TD!Node
+<1>. USE DEF Node, TD!Node, TDP!Node
 <1>1. Init => TD!Init
   BY DEF Init, TD!Init, terminationDetected
 <1>2. TypeOK /\ Inv /\ [Next]_vars => [TD!Next]_TD!vars
@@ -299,18 +301,19 @@ THEOREM Spec => TD!Spec
     BY <2>4 DEF Deactivate, TD!Next, TD!Terminate, TD!terminated
   <2>. QED  BY <2>1, <2>2, <2>3, <2>4 DEF Next, System, Environment
 <1>3. []TypeOK /\ []Inv /\ [][Next]_vars /\ WF_vars(System)
-      => WF_TD!vars(TD!DetectTermination)
+      => TDP!Fair
   <2>. SUFFICES /\ []TypeOK /\ []Inv /\ [][Next]_vars /\ WF_vars(System)
-                /\ []ENABLED <<TD!DetectTermination>>_TD!vars
+                /\ <>[](TDP!terminated /\ ~terminationDetected)
                 => FALSE 
-    BY PTL
-  <2>1. TypeOK /\ ENABLED <<TD!DetectTermination>>_TD!vars
-        => terminated /\ ~terminationDetected
-    BY ExpandENABLED 
-       DEF TypeOK, TD!DetectTermination, TD!vars, terminated, TD!terminated, terminationDetected
+    <3>. TypeOK => TDP!TypeOK
+      BY DEF TypeOK, TDP!TypeOK, terminationDetected
+    <3>. QED  BY TDP!Fairness, PTL
+  <2>1. TDP!terminated => terminated
+    BY DEF TDP!terminated, terminated
   <2>. QED BY <2>1, Live, PTL DEF Liveness
 <1>. QED  
-  BY <1>1, <1>2, <1>3, TypeCorrect, Invariant, PTL DEF Spec, TD!Spec
+  BY <1>1, <1>2, <1>3, TypeCorrect, Invariant, PTL DEF Spec, TD!Spec, TD!Fair, TDP!Fair, 
+     TD!vars, TDP!vars, TD!DetectTermination, TDP!DetectTermination, TD!terminated, TDP!terminated
 =============================================================================
 \* Modification History
 \* Created Mon Sep 09 11:33:10 CEST 2013 by merz

specifications/ewd840/SyncTerminationDetection.tla

@@ -50,7 +50,8 @@ Next ==
   \/ DetectTermination
 
 vars == <<active, terminationDetected>>
-Spec == Init /\ [][Next]_vars /\ WF_vars(DetectTermination)
+Fair == WF_vars(DetectTermination)
+Spec == Init /\ [][Next]_vars /\ Fair
 
 ------------------------------------------------------------------------------
 (* Correctness properties *)

specifications/ewd840/SyncTerminationDetection_proof.tla

@@ -39,6 +39,11 @@ LEMMA Enabled_ST ==
     PROVE (ENABLED <<DetectTermination>>_vars) <=> terminated /\ ~terminationDetected
 BY ExpandENABLED DEF TypeOK, DetectTermination, terminated, vars
 
+LEMMA Fairness ==
+    ASSUME []TypeOK
+    PROVE  Fair <=> (<>[](terminated /\ ~terminationDetected) => []<><<DetectTermination>>_vars)
+BY Enabled_ST, PTL DEF Fair
+
 (****************************************************************************)
 (* Proving liveness is easy since a single occurrence of the helpful action *)
 (* DetectTermination leads to the desired state.                            *)
@@ -52,6 +57,6 @@ THEOREM Live == Spec => Liveness
   BY DEF TypeOK, DetectTermination
 <1>3. TypeOK /\ P => ENABLED <<DetectTermination>>_vars
   BY Enabled_ST
-<1>. QED  BY <1>1, <1>2, <1>3, TypeCorrect, PTL DEF Spec, Liveness
+<1>. QED  BY <1>1, <1>2, <1>3, TypeCorrect, PTL DEF Spec, Fair, Liveness
 
 =============================================================================