diff --git a/_CoqProject b/_CoqProject
index 619240c9868996a2a89282c338e89e3bfe3a1b7b..1fd7ee3119b3eae601e10513f2b41f06400e8fad 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -15,5 +15,6 @@ propagation.v
fifo.v
static_priority.v
examples/case_study/arbitrary_flows.v
+examples/case_study/case.v
COQDOCFLAGS = "-g -interpolate -utf8 --external https://math-comp.github.io/htmldoc/ mathcomp -R . NCCoq"
diff --git a/examples/case_study/CaseStudy.nc b/examples/case_study/CaseStudy.nc
index 78d8277be19d042054965c0efebff03b769c4231..63e2cc8d0ee50cb62c819e538389ad16e73a458f 100644
--- a/examples/case_study/CaseStudy.nc
+++ b/examples/case_study/CaseStudy.nc
@@ -174,7 +174,7 @@ f3_E2E_delay
###################################
### f4
-f4_E2E_service:= beta_S3 * beta_S5_1
+f4_E2E_service:= beta_S3 * beta_S5_2
f4_E2E_service
f4_E2E_delay:= hdev(alpha4, f4_E2E_service)
@@ -183,7 +183,7 @@ f4_E2E_delay
###################################
### f5
-f5_E2E_service:= beta_S4 * beta_S5_1
+f5_E2E_service:= beta_S4 * beta_S5_2
f5_E2E_delay:= hdev(alpha5, f5_E2E_service)
f5_E2E_delay
diff --git a/examples/case_study/case.v b/examples/case_study/case.v
new file mode 100644
index 0000000000000000000000000000000000000000..424e04b36cd1472091a885fc6aa850386612ed07
--- /dev/null
+++ b/examples/case_study/case.v
@@ -0,0 +1,504 @@
+From mathcomp Require Import all_ssreflect.
+From minerve Require Import tactic.
+
+Definition d0 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 0;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (0, +oo%E))) ] |}%bigQ.
+
+(* Contrainte *)
+
+Definition alpha1 := F_of_sequpp {|
+ sequpp_T := 2;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (20_000, 8_000%:E)))] |}%bigQ.
+
+Definition alpha2 := alpha1.
+Definition alpha3 := alpha1.
+Definition alpha4 := alpha1.
+Definition alpha5 := alpha1.
+
+Definition beta1 := F_of_sequpp {|
+ sequpp_T := 0;
+ sequpp_d := 1;
+ sequpp_c := 100_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (100_000, 0%:E)))] |}%bigQ.
+
+Definition beta2 := beta1.
+Definition beta3 := beta1.
+Definition beta4 := beta1.
+Definition beta5 := beta1.
+
+(***********************************************)
+(* Serveur S1 *)
+(***********************************************)
+
+Definition alpha_S1 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 60_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (60_000, 24_000%:E)))] |}%bigQ.
+
+(* alpha_S1:= alpha1 + alpha2 + alpha3 *)
+Goal alpha_S1 = alpha1 + alpha2 + alpha3.
+Proof. nccoq. Qed.
+
+(* beta_S1_delay:= hdev(alpha_S1, beta1) *)
+Goal hDev_bounded alpha_S1 beta1 (6/25).
+Proof. nccoq. Qed.
+
+(* beta_S1:= delay( beta_S1_delay ) *)
+Definition beta_S1 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 0;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (0, 0%:E)));
+ (6/25, (0%:E, (0, +oo%E)))
+ ] |}%bigQ.
+
+(* alpha1_S1':= alpha1 / beta_S1 *)
+Definition alpha1_S1' := F_of_sequpp {|
+ sequpp_T := 0;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (12_800%:E, (20_000, 12_800%:E))) ] |}%bigQ.
+
+Goal alpha1 / beta_S1 <= alpha1_S1'.
+Proof. nccoq. Qed.
+
+(* alpha1_S1:= alpha1_S1 /\ d0 *)
+Definition alpha1_S1 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (20_000, 12_800%:E))) ] |}%bigQ.
+
+Goal F_min alpha1_S1' d0 = alpha1_S1.
+Proof. nccoq. Qed.
+
+(* Pareil pour alpha2 et alpha3 *)
+Definition alpha2_S1 := alpha1_S1.
+Definition alpha3_S1 := alpha1_S1.
+
+(***********************************************)
+(* Serveur S2 1 *)
+(***********************************************)
+
+(* beta_S2_1_delay:= hdev( alpha1_S1, beta2 ) *)
+Goal hDev_bounded alpha1_S1 beta2 (16/125)%bigQ.
+Proof. nccoq. Qed.
+
+(* beta_S2_1:= delay( beta_S2_1_delay ) *)
+Definition beta_S2_1 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 0;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (0, 0%:E)));
+ (16/125, (0%:E, (0, +oo%E)))
+ ] |}%bigQ.
+
+(* alpha1_S2' := ( alpha1_S1 / beta_S2_1 ) *)
+Definition alpha1_S2' := F_of_sequpp {|
+ sequpp_T := 0;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (15_360%:E, (20_000, 15_360%:E))) ] |}%bigQ.
+
+Goal alpha1_S1 / beta_S2_1 <= alpha1_S2'.
+Proof. nccoq. Qed.
+
+(* alpha1_S2 := alpha1_S2' /\ d0 *)
+Definition alpha1_S2 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (20_000, 15_360%:E))) ] |}%bigQ.
+
+Goal F_min alpha1_S2' d0 = alpha1_S2.
+Proof. nccoq. Qed.
+
+(***********************************************)
+(* Serveur S2 1 *)
+(***********************************************)
+
+(* beta_S2_2_delay:= hdev( alpha2_S1, beta2 ) *)
+Goal hDev_bounded alpha2_S1 beta2 (16/125)%bigQ.
+Proof. nccoq. Qed.
+
+(* beta_S2_2:= delay( beta_S2_2_delay ) *)
+Definition beta_S2_2 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 0;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (0, 0%:E)));
+ (16/125, (0%:E, (0, +oo%E)))
+ ] |}%bigQ.
+
+(* alpha2_S2' := ( alpha1_S1 / beta_S2_1 ) *)
+Definition alpha2_S2' := F_of_sequpp {|
+ sequpp_T := 0;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (15_360%:E, (20_000, 15_360%:E))) ] |}%bigQ.
+
+Goal alpha2_S1 / beta_S2_2 <= alpha2_S2'.
+Proof. nccoq. Qed.
+
+(* alpha2_S2 := alpha2_S2' /\ d0 *)
+Definition alpha2_S2 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (20_000, 15_360%:E))) ] |}%bigQ.
+
+Goal F_min alpha2_S2' d0 = alpha2_S2.
+Proof. nccoq. Qed.
+
+(***********************************************)
+(* Serveur S2 3 *)
+(***********************************************)
+
+(* beta_S2_3_delay:= hdev( alpha1_S1, beta2 ) *)
+Goal hDev_bounded alpha1_S1 beta2 (16/125)%bigQ.
+Proof. nccoq. Qed.
+
+(* beta_S2_3:= delay( beta_S2_3_delay ) *)
+Definition beta_S2_3 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 0;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (0, 0%:E)));
+ (16/125, (0%:E, (0, +oo%E)))
+ ] |}%bigQ.
+
+(* alpha1_S2' := ( alpha1_S1 / beta_S2_3 ) *)
+Definition alpha3_S2' := F_of_sequpp {|
+ sequpp_T := 0;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (15_360%:E, (20_000, 15_360%:E))) ] |}%bigQ.
+
+Goal alpha3_S1 / beta_S2_3 <= alpha3_S2'.
+Proof. nccoq. Qed.
+
+(* alpha1_S2 := alpha1_S2' /\ d0 *)
+Definition alpha3_S2 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (20_000, 15_360%:E))) ] |}%bigQ.
+
+Goal F_min alpha3_S2' d0 = alpha3_S2.
+Proof. nccoq. Qed.
+
+(***********************************************)
+(* Serveur S3 *)
+(***********************************************)
+
+(* alpha_S3 := alpha1_S2 + alpha4 *)
+Definition alpha_S3 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 40_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (40_000, 23_360%:E)))] |}%bigQ.
+
+(* beta_S3_delay:= hdev( alpha_S3 , beta2 ) *)
+Goal hDev_bounded alpha_S3 beta2 (146/625)%bigQ.
+Proof. nccoq. Qed.
+
+(* beta_S3 := delay( beta_S3_delay ) *)
+Definition beta_S3 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 0;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (0, 0%:E)));
+ (146/625, (0%:E, (0, +oo%E)))
+ ] |}%bigQ.
+
+(* alpha1_S3':= (alpha1_S2 / beta_S3 ) *)
+Definition alpha1_S3' := F_of_sequpp {|
+ sequpp_T := 0;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (20_032%:E, (20_000, 20_032%:E))) ] |}%bigQ.
+
+Goal alpha1_S2 / beta_S3 <= alpha1_S3'.
+Proof. nccoq. Qed.
+
+(* alpha4_S3':= (alpha4 / beta_S3 ) *)
+Definition alpha4_S3' := F_of_sequpp {|
+ sequpp_T := 0;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (12_672%:E, (20_000, 12_672%:E))) ] |}%bigQ.
+
+Goal alpha4 / beta_S3 <= alpha4_S3'.
+Proof. nccoq. Qed.
+
+(* alpha1_S3 := alpha1_S3' /\ d0 *)
+Definition alpha1_S3 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (20_000, 20_032%:E))) ] |}%bigQ.
+
+Goal F_min alpha1_S3' d0 = alpha1_S3.
+Proof. nccoq. Qed.
+
+(* alpha4_S3 := alpha4_S3' /\ d0 *)
+Definition alpha4_S3 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (20_000, 12_672%:E))) ] |}%bigQ.
+
+Goal F_min alpha4_S3' d0 = alpha4_S3.
+Proof. nccoq. Qed.
+
+(***********************************************)
+(* Serveur S4 *)
+(***********************************************)
+
+(* alpha_S4 := alpha3_S2 + alpha5 *)
+Definition alpha_S4 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 40_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (40_000, 23_360%:E)))] |}%bigQ.
+
+(* beta_S4_delay:= hdev( alpha_S4 , beta4 ) *)
+Goal hDev_bounded alpha_S4 beta4 (146/625)%bigQ.
+Proof. nccoq. Qed.
+
+(* beta_S4 := delay( beta_S4_delay ) *)
+Definition beta_S4 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 0;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (0, 0%:E)));
+ (146/625, (0%:E, (0, +oo%E)))
+ ] |}%bigQ.
+
+(* alpha1_S4':= (alpha3_S2 / beta_S4 ) *)
+Definition alpha3_S4' := F_of_sequpp {|
+ sequpp_T := 0;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (20_032%:E, (20_000, 20_032%:E))) ] |}%bigQ.
+
+Goal alpha3_S2 / beta_S4 <= alpha3_S4'.
+Proof. nccoq. Qed.
+
+(* alpha5_S4':= (alpha5 / beta_S4 ) *)
+Definition alpha5_S4' := F_of_sequpp {|
+ sequpp_T := 0;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (12_672%:E, (20_000, 12_672%:E))) ] |}%bigQ.
+
+Goal alpha5 / beta_S4 <= alpha5_S4'.
+Proof. nccoq. Qed.
+
+(* alpha3_S4:= alpha3_S4 /\ d0 *)
+Definition alpha3_S4 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (20_000, 20_032%:E))) ] |}%bigQ.
+
+Goal F_min alpha3_S4' d0 = alpha3_S4.
+Proof. nccoq. Qed.
+
+(* alpha5_S4:= alpha5_S4 /\ d0 *)
+Definition alpha5_S4 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 20_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (20_000, 12_672%:E))) ] |}%bigQ.
+
+Goal F_min alpha5_S4' d0 = alpha5_S4.
+Proof. nccoq. Qed.
+
+(***********************************************)
+(* Serveur S5_1 *)
+(***********************************************)
+
+(* alpha_S5_1:= alpha1_S3 + alpha2_S2 + alpha3_S4 *)
+Definition alpha_S5_1 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 60_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (60_000, 55424%:E)))] |}%bigQ.
+
+(* beta_S5_1_delay:= hdev( alpha_S5_1 , beta5 ) *)
+Goal hDev_bounded alpha_S5_1 beta5 (1732/3125)%bigQ.
+Proof. nccoq. Qed.
+
+(* beta_S5_1 := delay( beta_S5_1_delay ) *)
+Definition beta_S5_1 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 0;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (0, 0%:E)));
+ (1732/3125, (0%:E, (0, +oo%E)))
+ ] |}%bigQ.
+
+(***********************************************)
+(* Serveur S5_2 *)
+(***********************************************)
+
+(* alpha_S5_2:= alpha4_S3 + alpha5_S4 *)
+Definition alpha_S5_2 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 40_000;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (40_000, 25344%:E)))] |}%bigQ.
+
+(* beta_S5_2_delay:= hdev( alpha_S5_2 , beta5 ) *)
+Goal hDev_bounded alpha_S5_2 beta5 (792/3125)%bigQ.
+Proof. nccoq. Qed.
+
+(* beta_S5_2 := delay( beta_S5_2_delay ) *)
+Definition beta_S5_2 := F_of_sequpp {|
+ sequpp_T := 1;
+ sequpp_d := 1;
+ sequpp_c := 0;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (0, 0%:E)));
+ (792/3125, (0%:E, (0, +oo%E)))
+ ] |}%bigQ.
+
+
+(******************************************************)
+(* End to end delay *)
+(******************************************************)
+
+(* f1 *)
+
+(* beta1_E2E:= ( beta_S1 * beta_S2_1 * beta_S3 * beta_S5_1 *)
+Definition beta1_E2E := F_of_sequpp {|
+ sequpp_T := 2;
+ sequpp_d := 1;
+ sequpp_c := 0;
+ sequpp_js := (* list of (x, (y, (rho, sigma))) *)
+ [:: (0, (0%:E, (0, 0%:E)));
+ (3612/3125, (0%:E, (0, +oo%E)))
+ ] |}%bigQ.
+
+Goal beta1_E2E = (beta_S1 * beta_S2_1 * beta_S3 * beta_S5_1).
+Proof. nccoq. Qed.
+
+(* f1_E2E_delay:= hdev(alpha1, f1_E2E_service) *)
+Goal hDev_bounded alpha1 beta1_E2E (3612/3125)%bigQ.
+Proof.
+nccoq.
+Qed.
+
+(* f2 *)
+
+(* beta2_E2E:= (beta_S1 * beta_S2_2 * beta_S5_1 *)
+Definition beta2_E2E := F_of_sequpp {|
+ sequpp_T := 2;
+ sequpp_d := 1;
+ sequpp_c := 0;
+ sequpp_js := [:: (0, (0%:E, (0, 0%:E)));
+ (2882/3125, (0%:E, (0, +oo%E))) ] |}%bigQ.
+
+Goal beta2_E2E = (beta_S1 * beta_S2_2 * beta_S5_1).
+Proof. nccoq. Qed.
+
+(* f2_E2E_delay:= hdev(alpha2, f2_E2E_service) *)
+Goal hDev_bounded alpha2 beta2_E2E (2882/3125)%bigQ.
+Proof.
+nccoq.
+Qed.
+
+(* f3 *)
+
+(* beta3_E2E:= ( beta_S1 * beta_S2_3 * beta_S4 * beta_S5_1 *)
+Definition beta3_E2E := F_of_sequpp {|
+ sequpp_T := 2;
+ sequpp_d := 1;
+ sequpp_c := 0;
+ sequpp_js := [:: (0, (0%:E, (0, 0%:E)));
+ (3612/3125, (0%:E, (0, +oo%E))) ] |}%bigQ.
+
+Goal beta3_E2E = (beta_S1 * beta_S2_3 * beta_S4 * beta_S5_1).
+Proof. nccoq. Qed.
+
+(* f3_E2E_delay:= hdev(alpha3, f3_E2E_service) *)
+Goal hDev_bounded alpha3 beta3_E2E (3612/3125)%bigQ.
+Proof.
+nccoq.
+Qed.
+
+(* f4 *)
+
+(* beta4_E2E:= ( beta_S3 * beta_S5_2 *)
+Definition beta4_E2E := F_of_sequpp {|
+ sequpp_T := 2;
+ sequpp_d := 1;
+ sequpp_c := 0;
+ sequpp_js := [:: (0, (0%:E, (0, 0%:E)));
+ (1522/3125, (0%:E, (0, +oo%E))) ] |}%bigQ.
+
+Goal beta4_E2E = (beta_S3 * beta_S5_2).
+Proof. nccoq. Qed.
+
+(* f4_E2E_delay:= hdev(alpha4, f4_E2E_service) *)
+Goal hDev_bounded alpha4 beta4_E2E (1522/3125)%bigQ.
+Proof.
+nccoq.
+Qed.
+
+(* f5 *)
+
+(* beta5_E2E:= ( beta_S4 * beta_S5_2 *)
+Definition beta5_E2E := F_of_sequpp {|
+ sequpp_T := 2;
+ sequpp_d := 1;
+ sequpp_c := 0;
+ sequpp_js := [:: (0, (0%:E, (0, 0%:E)));
+ (1522/3125, (0%:E, (0, +oo%E))) ] |}%bigQ.
+
+Goal beta5_E2E = (beta_S4 * beta_S5_2).
+Proof. nccoq. Qed.
+
+(* f5_E2E_delay:= hdev(alpha4, f4_E2E_service) *)
+Goal hDev_bounded alpha5 beta5_E2E (1522/3125)%bigQ.
+Proof.
+nccoq.
+Qed.