Name the previously-anonymous ASSUMEs in PaxosCommit and EWD687a

TLAPS' backends sometimes fail to find facts contributed by an
unnamed ASSUME, so two of the proofs in this branch had been
working around that by re-stating the spec's anonymous ASSUME under
a fresh name inside the proof file (PaxosCommitAssumptions in
transaction_commit/PaxosCommit_proof.tla and EdgeFacts in
ewd687a/EWD687a_proof.tla).

Move each name into the spec itself and drop the duplicates from
the proof files.  The conjuncts of each ASSUME are unchanged; only
a name is attached.  The named-ASSUME pattern is already used by
sibling specs such as Paxos/Voting.tla and ewd840/EWD840.tla.

Affected pairs:

  specifications/transaction_commit/PaxosCommit.tla
    + ASSUME PaxosCommitAssumptions == ...
  specifications/transaction_commit/PaxosCommit_proof.tla
    - duplicate restatement removed; existing references unchanged.

  specifications/ewd687a/EWD687a.tla
    + ASSUME EdgeFacts == ...
  specifications/ewd687a/EWD687a_proof.tla
    - duplicate restatement removed.

(The third anonymous ASSUME in this branch -- in
PaxosHowToWinATuringAward/Voting.tla -- is named in its own
introducing commit.  The auxiliary ASSUME ProcsFinite == IsFiniteSet(Procs)
in EWD687a_proof.tla is *not* a restatement -- it is a genuinely new
hypothesis added by the proof for the chain-of-upEdges argument --
and stays in the proof file.)

Both proofs re-checked with TLAPS:
  - PaxosCommit_proof.tla:    5  obligations
  - EWD687a_proof.tla:        642 obligations

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

Author: lemmy

specifications/ewd687a/EWD687a.tla

@@ -123,7 +123,8 @@ OutEdges(p) == {e \in Edges : e[1] = p}
 (* something that was not stated explicitly: that a process can't send     *)
 (* messages to itself, so an edge joins two different processes.           *)
 (***************************************************************************)
-ASSUME  /\ \* Every edge is a pair of distinct processes
+ASSUME EdgeFacts ==
+        /\ \* Every edge is a pair of distinct processes
            \A e \in Edges :
              /\ (e \in Procs \X Procs)
              /\ (e[1] # e[2])

specifications/ewd687a/EWD687a_proof.tla

@@ -4,17 +4,6 @@
 (***************************************************************************)
 EXTENDS EWD687a, NaturalsInduction, FiniteSetTheorems, TLAPS
 
------------------------------------------------------------------------------
-(***************************************************************************)
-(* Re-state the (unnamed) ASSUME from EWD687a as a named assumption so we  *)
-(* can refer to it by name in proofs.  TLAPS does not currently expose     *)
-(* unnamed ASSUMEs to backends.                                            *)
-(***************************************************************************)
-ASSUME EdgeFacts ==
-        /\ \A e \in Edges : (e \in Procs \X Procs) /\ (e[1] # e[2])
-        /\ Leader \in Procs
-        /\ InEdges(Leader) = {}
-
 -----------------------------------------------------------------------------
 (***************************************************************************)
 (* Theorem 1: Spec => CountersConsistent                                   *)

specifications/transaction_commit/PaxosCommit.tla

@@ -44,7 +44,8 @@ CONSTANT RM,             \* The set of resource managers.
          Majority,       \* The set of majorities of acceptors
          Ballot          \* The set of ballot numbers
 
-ASSUME  \* We assume these properties of the declared constants.
+ASSUME PaxosCommitAssumptions ==
+  \* We assume these properties of the declared constants.
   /\ Ballot \subseteq Nat
   /\ 0 \in Ballot
   /\ Majority \subseteq SUBSET Acceptor

specifications/transaction_commit/PaxosCommit_proof.tla

@@ -14,15 +14,6 @@
 (***************************************************************************)
 EXTENDS PaxosCommit, TLAPS
 
-(***************************************************************************)
-(* Pull the relevant facts out of the unnamed ASSUME in PaxosCommit.tla.   *)
-(***************************************************************************)
-ASSUME PaxosCommitAssumptions ==
-  /\ Ballot \subseteq Nat
-  /\ 0 \in Ballot
-  /\ Majority \subseteq SUBSET Acceptor
-  /\ \A MS1, MS2 \in Majority : MS1 \cap MS2 # {}
-
 THEOREM TypeOK_Init == PCSpec => PCTypeOK
 <1>1. PCInit => PCTypeOK
   BY PaxosCommitAssumptions DEF PCInit, PCTypeOK