Update old names

Replace UIB_departure with maximal_departure

examples/case_study/arbitrary_flows.v

@@ -144,14 +144,8 @@ Section switch_1.
 Definition beta_S1 : Fup :=
   delta (hDev (alpha1 + alpha2 + alpha3)%F beta1)%:nngenum.
 
-Definition alpha1_S1 := ((alpha1 / beta_S1) + delta 0)%D.
-Definition alpha2_S1 := ((alpha2 / beta_S1) + delta 0)%D.
-Definition alpha3_S1 := ((alpha3 / beta_S1) + delta 0)%D.
-
 Definition alpha_S1 : Fup^3 := finfun_of_tuple [tuple alpha1; alpha2; alpha3].
 
-Let alpha_S1_out : Fup^3 := finfun_of_tuple [tuple alpha1_S1; alpha2_S1; alpha3_S1].
-
 Lemma min_residual_service_S1 i :
   is_min_service
     (residual_server_constr S1 i [ffun i => alpha_S1 i : F]) beta_S1.
@@ -162,6 +156,12 @@ have -> : (alpha1 + alpha2 + alpha3 = \sum_j alpha_S1 j)%F.
 exact: FIFO_delay.
 Qed.
 
+Definition alpha1_S1 := ((alpha1 / beta_S1) + delta 0)%D.
+Definition alpha2_S1 := ((alpha2 / beta_S1) + delta 0)%D.
+Definition alpha3_S1 := ((alpha3 / beta_S1) + delta 0)%D.
+
+Let alpha_S1_out : Fup^3 := finfun_of_tuple [tuple alpha1_S1; alpha2_S1; alpha3_S1].
+
 Lemma alpha_S1_correct i :
   is_maximal_arrival (finfun_of_tuple [tuple F1; F2; F3] i) (alpha_S1 i).
 Proof.
@@ -171,7 +171,7 @@ case: i => -[| [| [|//]]] ?; rewrite !ffunE.
 - exact: Halpha3.
 Qed.
 
-Lemma UIB_departure_S1 i :
+Lemma maximal_departure_S1 i :
   is_maximal_arrival
     (finfun_of_tuple [tuple F1_S1; F2_S1; F3_S1] i)
     (alpha_S1_out i).
@@ -192,7 +192,7 @@ Section switch_2_1.
 
 Lemma Halpha1_S2 : is_maximal_arrival F1_S1 alpha1_S1.
 Proof.
-move: (UIB_departure_S1 (inord 0)).
+move: (maximal_departure_S1 (inord 0)).
 by rewrite !ffunE /inord /insubd insubT.
 Qed.
 
@@ -212,7 +212,7 @@ have {1}-> : [ffun=> alpha1_S1 : F] = [ffun i : 'I_1 => [ffun=> alpha1_S1] i : F
 by apply: FIFO_delay; [exact: FIFO_one_server|].
 Qed.
 
-Lemma UIB_departure_S2_1 : is_maximal_arrival F1_S2 alpha1_S2.
+Lemma maximal_departure_S2_1 : is_maximal_arrival F1_S2 alpha1_S2.
 Proof.
 apply: maximal_arrival_F_min; [|apply: maximal_arrival_delta_0];
 apply: output_arrival_curve_mp_Fup;
@@ -228,7 +228,7 @@ Section switch_2_2.
 
 Lemma Halpha2_S2 : is_maximal_arrival F2_S1 alpha2_S1.
 Proof.
-move: (UIB_departure_S1 (inord 1)).
+move: (maximal_departure_S1 (inord 1)).
 by rewrite !ffunE /inord /insubd insubT.
 Qed.
 
@@ -248,7 +248,7 @@ have {1}-> : [ffun=> alpha2_S1 : F] = [ffun i : 'I_1 => [ffun=> alpha2_S1] i : F
 by apply: FIFO_delay; [exact: FIFO_one_server|].
 Qed.
 
-Lemma UIB_departure_S2_2 : is_maximal_arrival F2_S2 alpha2_S2.
+Lemma maximal_departure_S2_2 : is_maximal_arrival F2_S2 alpha2_S2.
 Proof.
 apply: maximal_arrival_F_min; [|apply: maximal_arrival_delta_0];
 apply: output_arrival_curve_mp_Fup;
@@ -268,7 +268,7 @@ Definition alpha3_S2 := ((alpha3_S1 / beta_S2_3) + delta 0)%D.
 
 Lemma Halpha3_S2 : is_maximal_arrival F3_S1 alpha3_S1.
 Proof.
-move: (UIB_departure_S1 (inord 2)).
+move: (maximal_departure_S1 (inord 2)).
 by rewrite !ffunE /inord /insubd insubT.
 Qed.
 
@@ -284,7 +284,7 @@ have {1}-> : [ffun=> alpha3_S1 : F] = [ffun i : 'I_1 => [ffun=> alpha3_S1] i : F
 by apply: FIFO_delay; [exact: FIFO_one_server|].
 Qed.
 
-Lemma UIB_departure_S2_3 : is_maximal_arrival F3_S2 alpha3_S2.
+Lemma maximal_departure_S2_3 : is_maximal_arrival F3_S2 alpha3_S2.
 Proof.
 apply: maximal_arrival_F_min; [|apply: maximal_arrival_delta_0];
 apply: output_arrival_curve_mp_Fup;
@@ -319,13 +319,13 @@ Lemma alpha_S3_correct i :
   is_maximal_arrival (finfun_of_tuple [tuple F1_S2; F4] i) (alpha_S3 i).
 Proof.
 case: i => -[| [|//]] ?; rewrite !ffunE.
-- exact: UIB_departure_S2_1.
+- exact: maximal_departure_S2_1.
 - exact: Halpha4.
 Qed.
 
 Let alpha_S3_out := finfun_of_tuple [tuple alpha1_S3; alpha4_S3].
 
-Lemma UIB_departure_S3 i :
+Lemma maximal_departure_S3 i :
   is_maximal_arrival
     (finfun_of_tuple [tuple F1_S3; F4_S3] i) (alpha_S3_out i).
 Proof.
@@ -333,7 +333,7 @@ case: i => -[| [|//]] Hi; rewrite !ffunE; unfold_tnth;
 ( apply: maximal_arrival_F_min; [|apply: maximal_arrival_delta_0];
   apply: output_arrival_curve_mp_Fup;
   [|exact: (@min_residual_service_S3 (Ordinal Hi))
-   |(exact: UIB_departure_S2_1 || by [])];
+   |(exact: maximal_departure_S2_1 || by [])];
   eexists; eexists; split; [exact: H_server_S3|];
   rewrite !ffunE; split=> //; split=> // j;
   rewrite ffunE; exact: alpha_S3_correct).
@@ -364,13 +364,13 @@ Lemma alpha_S4_correct i :
   is_maximal_arrival (finfun_of_tuple [tuple F3_S2; F5] i) (alpha_S4 i).
 Proof.
 case: i => -[| [|//]] ?; rewrite !ffunE.
-- exact: UIB_departure_S2_3.
+- exact: maximal_departure_S2_3.
 - exact: Halpha5.
 Qed.
 
 Let alpha_S4_out := finfun_of_tuple [tuple alpha3_S4; alpha5_S4].
 
-Lemma UIB_departure_S4 i :
+Lemma maximal_departure_S4 i :
   is_maximal_arrival
     (finfun_of_tuple [tuple F3_S4; F5_S4] i) (alpha_S4_out i).
 Proof.
@@ -378,7 +378,7 @@ case: i => -[| [|//]] Hi; rewrite !ffunE; unfold_tnth;
 ( apply: maximal_arrival_F_min; [|apply: maximal_arrival_delta_0];
   apply: output_arrival_curve_mp_Fup;
     [|exact: (@min_residual_service_S4 (Ordinal Hi))
-     |(exact: UIB_departure_S2_3 || by [])];
+     |(exact: maximal_departure_S2_3 || by [])];
    eexists; eexists; split; [exact: H_server_S4|];
    rewrite !ffunE; split=> //; split=> // j;
    rewrite ffunE; exact: alpha_S4_correct).
@@ -390,13 +390,13 @@ Section switch_5_1.
 
 Lemma Halpha1_S5 : is_maximal_arrival F1_S3 alpha1_S3.
 Proof.
-move: (UIB_departure_S3 (inord 0)).
+move: (maximal_departure_S3 (inord 0)).
 by rewrite !ffunE /inord /insubd insubT.
 Qed.
 
 Lemma Halpha3_S5 : is_maximal_arrival F3_S4 alpha3_S4.
 Proof.
-move: (UIB_departure_S4 (inord 0)).
+move: (maximal_departure_S4 (inord 0)).
 by rewrite !ffunE /inord /insubd insubT.
 Qed.
 
@@ -421,7 +421,7 @@ Lemma alpha_S5_correct i :
 Proof.
 case: i => -[| [| [|//]]] ?; rewrite !ffunE.
 - exact: Halpha1_S5.
-- exact: UIB_departure_S2_2.
+- exact: maximal_departure_S2_2.
 - exact: Halpha3_S5.
 Qed.
 
@@ -431,7 +431,7 @@ Definition alpha3_S5 := ((alpha3_S4 / beta_S5_1) + delta 0)%D.
 
 Let alpha_S5_out := finfun_of_tuple [tuple alpha1_S5; alpha2_S5; alpha3_S5].
 
-Lemma UIB_departure_S5 i :
+Lemma maximal_departure_S5 i :
   is_maximal_arrival
     (finfun_of_tuple [tuple F1_S5; F2_S5; F3_S5] i)
     (alpha_S5_out i).
@@ -440,7 +440,7 @@ case: i => -[| [| [|//]]] Hi; rewrite !ffunE; unfold_tnth;
 ( apply: maximal_arrival_F_min; [|apply: maximal_arrival_delta_0];
   apply: output_arrival_curve_mp_Fup;
     [|exact: (@min_residual_service_S5_1 (Ordinal Hi))|]);
-    [|exact: Halpha1_S5| |exact: UIB_departure_S2_2| | exact: Halpha3_S5];
+    [|exact: Halpha1_S5| |exact: maximal_departure_S2_2| | exact: Halpha3_S5];
     (eexists; eexists; split; [exact: H_server_S5_1|];
      rewrite !ffunE; split=> //; split=> // j;
      rewrite ffunE; exact: alpha_S5_correct).
@@ -452,13 +452,13 @@ Section switch_5_2.
 
 Lemma Halpha4_S5 : is_maximal_arrival F4_S3 alpha4_S3.
 Proof.
-move: (UIB_departure_S3 (inord 1)).
+move: (maximal_departure_S3 (inord 1)).
 by rewrite !ffunE /inord /insubd insubT.
 Qed.
 
 Lemma Halpha5_S5 : is_maximal_arrival F5_S4 alpha5_S4.
 Proof.
-move: (UIB_departure_S4 (inord 1)).
+move: (maximal_departure_S4 (inord 1)).
 by rewrite !ffunE /inord /insubd insubT.
 Qed.
 
@@ -490,7 +490,7 @@ Definition alpha5_S5 := ((alpha5_S4 / beta_S5_2) + delta 0)%D.
 
 Let alpha_S5_2_out := finfun_of_tuple [tuple alpha4_S5 ; alpha5_S5].
 
-Lemma UIB_departure_S6 i :
+Lemma maximal_departure_S5_2 i :
   is_maximal_arrival
     (finfun_of_tuple [tuple F4_S5; F5_S5] i)
     (alpha_S5_2_out i).