Manual changes.

theories/Core/Equivocation.v

@@ -703,11 +703,11 @@ Lemma from_send_to_from_sent_argument
   `{HasBeenSentCapability}
   (P : state vlsm -> Prop)
   (P_stable : forall s l oim s' oom,
-    input_valid_transition pre_vlsm l (s, oim) (s', oom) ->
+    input_constrained_transition vlsm l (s, oim) (s', oom) ->
     P s -> P s')
   (msg : message)
   (send_establishes_P : forall s l oim s',
-    input_valid_transition pre_vlsm l (s, oim) (s', Some msg) ->
+    input_constrained_transition vlsm l (s, oim) (s', Some msg) ->
     P s') :
   forall s,
     valid_state_prop (pre_loaded_with_all_messages_vlsm vlsm) s ->

theories/Core/Equivocation/TraceWiseEquivocation.v

@@ -221,7 +221,7 @@ Qed.
 
 Lemma transition_is_equivocating_tracewise_char
   l s om s' om'
-  (Ht : input_valid_transition PreFree l (s, om) (s', om'))
+  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s, om) (s', om'))
   (v : validator)
   : is_equivocating_tracewise_no_has_been_sent s' v ->
     is_equivocating_tracewise_no_has_been_sent s v \/
@@ -245,7 +245,7 @@ Qed.
 
 Lemma transition_receiving_no_sender_reflects_is_equivocating_tracewise
   l s om s' om'
-  (Ht : input_valid_transition PreFree l (s, om) (s', om'))
+  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s, om) (s', om'))
   (Hno_sender : option_bind _ _ sender om = None)
   (v : validator)
   : is_equivocating_tracewise_no_has_been_sent s' v -> is_equivocating_tracewise_no_has_been_sent s v.
@@ -336,7 +336,7 @@ Qed.
 
 Lemma input_valid_transition_receiving_no_sender_reflects_equivocating_validators
   l s om s' om'
-  (Ht : input_valid_transition PreFree l (s, om) (s', om'))
+  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s, om) (s', om'))
   (Hno_sender : option_bind _ _ sender om = None)
   : equivocating_validators s' ⊆ equivocating_validators s.
 Proof.
@@ -357,7 +357,7 @@ Qed.
 
 Lemma composite_transition_no_sender_equivocators_weight
   l s om s' om'
-  (Ht : input_valid_transition PreFree l (s, om) (s', om'))
+  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s, om) (s', om'))
   (Hno_sender : option_bind _ _ sender om = None)
   : (equivocation_fault s' <= equivocation_fault s)%R.
 Proof.

theories/Core/Equivocation/WitnessedEquivocation.v

@@ -168,7 +168,7 @@ Qed.
 *)
 Lemma equivocating_validators_step_update
     l s om s' om'
-    (Ht : input_valid_transition PreFree l (s, om) (s', om'))
+    (Ht : input_constrained_transition Free l (s, om) (s', om'))
     v
     : v ∈ equivocating_validators s' ->
       v ∈ equivocating_validators s \/

theories/Core/HistoryVLSM.v

@@ -111,7 +111,7 @@ Lemma composite_valid_transition_reflects_rechability :
   forall l s1 iom s2 oom,
   composite_valid_transition IM l s1 iom s2 oom ->
   valid_state_prop RFree s2 ->
-  input_valid_transition RFree l (s1, iom) (s2, oom).
+  input_constrained_transition Free l (s1, iom) (s2, oom).
 Proof.
   intros * Hnext Hs2; revert l s1 iom oom Hnext.
   induction Hs2 using valid_state_prop_ind; intros * Hnext.
@@ -140,7 +140,7 @@ Proof.
           apply f_equal with (f := fun s => s j) in Heqs'.
           by state_update_simpl.
       }
-      assert (Hss1 : input_valid_transition RFree (existT i li)
+      assert (Hss1 : input_constrained_transition Free (existT i li)
                   (state_update IM s j (s1 j), om) (s1, om')).
       {
         repeat split; [by apply IHHs2 | by apply any_message_is_valid_in_preloaded | ..]
@@ -175,7 +175,7 @@ Lemma composite_valid_transitions_from_to_reflects_reachability :
   valid_state_prop RFree s' -> finite_valid_trace_from_to RFree s s' tr.
 Proof.
   induction 1; intros; [by constructor |].
-  assert (Hitem : input_valid_transition RFree (l item) (s', input item)
+  assert (Hitem : input_constrained_transition Free (l item) (s', input item)
                           (destination item, output item))
     by (apply composite_valid_transition_reflects_rechability; done).
   eapply finite_valid_trace_from_to_app.

theories/Core/ProjectionTraces.v

@@ -201,8 +201,7 @@ Lemma pre_loaded_with_all_messages_projection_input_valid_transition_eq
   (s1 s2 : composite_state IM)
   (om1 om2 : option message)
   (l : label (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)))
-  (Ht : input_valid_transition
-          (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)) l (s1, om1) (s2, om2))
+  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s1, om1) (s2, om2))
   (Hl : projT1 l = j)
   : input_constrained_transition (IM (projT1 l))
       (projT2 l) (s1 (projT1 l), om1) (s2 (projT1 l), om2).
@@ -220,8 +219,7 @@ Lemma pre_loaded_with_all_messages_projection_input_valid_transition_neq
   [s1 s2 : composite_state IM]
   [om1 om2 : option message]
   [l : label (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM))]
-  (Ht : input_valid_transition
-          (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)) l (s1, om1) (s2, om2))
+  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s1, om1) (s2, om2))
   [i : index]
   (Hi : i <> projT1 l)
   : s1 i = s2 i.

theories/Core/SubProjectionTraces.v

@@ -1553,7 +1553,7 @@ Qed.
   Note that, in general, this is not trace-equivalent with the directly obtained
   [projection_induced_validator] of the constrained composition to the corresponding
   component, as the intermediate induced projection might generate more
-  [input_valid_transitions] to be considered as a basis for the next projection.
+  [input_valid_transition]s to be considered as a basis for the next projection.
 *)
 
 Definition sub_label_element_project

theories/Examples/Tutorial/Multiply.v

@@ -353,7 +353,7 @@ Qed.
 *)
 
 Example doubling_example_constrained_transition :
-  input_valid_transition (pre_loaded_with_all_messages_vlsm doubling_vlsm) multiply_label
+  input_constrained_transition doubling_vlsm multiply_label
    (3, Some 3) (0, Some 6).
 Proof.
   apply (finite_valid_trace_from_to_last_transition