Replace Functions and FunctionTheorems with Fork variants

tlaplus/tlapm#239
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

.github/scripts/check_manifest_features.py

@@ -96,9 +96,10 @@ def get_module_features(examples_root, path, parser, queries):
 tlaps_modules = {
     'BagsTheorems',
     'FiniteSetTheorems',
-    'FunctionTheorems',
+    'FunctionForkTheorems',
+    'FunctionsFork',
     'NaturalsInduction',
-    'SequencesExtTheorems',
+    'SequencesExtForkTheorems',
     'SequenceTheorems',
     'TLAPS',
     'WellFoundedInduction'

specifications/LoopInvariance/SumSequence.tla

@@ -9,7 +9,7 @@
 (*                                                                         *)
 (*    http://lamport.azurewebsites.net/tla/proving-safety.pdf              *)
 (***************************************************************************)
-EXTENDS Integers, SequenceTheorems, SequencesExtTheorems, NaturalsInduction, TLAPS
+EXTENDS Integers, SequenceTheorems, SequencesExtForkTheorems, NaturalsInduction, TLAPS
 
 (***************************************************************************)
 (* To facilitate model checking, we assume that the sequence to be summed  *)
@@ -55,9 +55,9 @@ with the variable sum equal to the sum of the elements of seq.
 }
 ***************************************************************************)
 \* BEGIN TRANSLATION
-VARIABLES seq, sum, n, pc
+VARIABLES pc, seq, sum, n
 
-vars == << seq, sum, n, pc >>
+vars == << pc, seq, sum, n >>
 
 Init == (* Global variables *)
         /\ seq \in Seq(Values)

specifications/bcastByz/bcastByz.tla

@@ -34,8 +34,8 @@
 
 EXTENDS Naturals, 
         FiniteSets,
-        Functions,
-        FunctionTheorems, 
+        FunctionsFork,
+        FunctionForkTheorems, 
         FiniteSetTheorems,
         NaturalsInduction,
         SequenceTheorems,