tdma.v

Require Export prosa.model.schedule.tdma.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Import prosa.util.all.

(** In this section, we define the properties of TDMA and prove some basic lemmas. *)
Section TDMAFacts.
  Context {Task:eqType}.

  (** Consider any task set ts... *)
  Variable ts: {set Task}.

  (** ... with a TDMA policy *)
  Context `{TDMAPolicy Task}.

  Section TimeSlotFacts.
    (** Consider any task in ts*)
    Variable task: Task.
    Hypothesis H_task_in_ts: task \in ts.

    (** Assume task_time_slot is valid time slot*)
    Hypothesis time_slot_positive:
      valid_time_slot ts.

    (** Obviously, the TDMA cycle is greater or equal than any task time slot which is
          in TDMA cycle *)
    Lemma TDMA_cycle_ge_each_time_slot:
      TDMA_cycle ts >= task_time_slot task.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
task_time_slot task <= TDMA_cycle ts
    Proof.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
task_time_slot task <= TDMA_cycle ts
      rewrite /TDMA_cycle (big_rem task) //.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
task_time_slot task <=
ssrnat_addn__canonical__Monoid_ComLaw
  (task_time_slot task)
  (\big[ssrnat_addn__canonical__Monoid_ComLaw/0]_(y <- 
   rem (T:=Task) task ts) task_time_slot y)
      apply:leq_trans; last by exact: leq_addr.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
task_time_slot task <= task_time_slot task
        by apply leqnn.
    Qed.

    (** Thus, a TDMA cycle is always positive *)
    Lemma TDMA_cycle_positive:
      TDMA_cycle ts > 0.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
0 < TDMA_cycle ts
    Proof.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
0 < TDMA_cycle ts
      move:time_slot_positive=>/(_ task H_task_in_ts)/leq_trans;apply;apply TDMA_cycle_ge_each_time_slot.
    Qed.

    (** Slot offset is less then cycle *)
    Lemma Offset_lt_cycle:
      task_slot_offset ts task < TDMA_cycle ts.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
task_slot_offset ts task < TDMA_cycle ts
    Proof.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
task_slot_offset ts task < TDMA_cycle ts
      rewrite /task_slot_offset /TDMA_cycle big_mkcond.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
\big[ssrnat_addn__canonical__Monoid_Law/0]_(i <- ts)
   (if slot_order i task && (i != task)
    then task_time_slot i
    else 0) < \sum_(tsk <- ts) task_time_slot tsk
      apply leq_ltn_trans with (n:=\sum_(prev_task <- ts )if prev_task!=task then task_time_slot prev_task else 0).Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
\big[ssrnat_addn__canonical__Monoid_Law/0]_(i <- ts)
   (if slot_order i task && (i != task)
    then task_time_slot i
    else 0) <=
\sum_(prev_task <- ts)
   (if prev_task != task
    then task_time_slot prev_task
    else 0)
Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
\sum_(prev_task <- ts)
   (if prev_task != task
    then task_time_slot prev_task
    else 0) < \sum_(tsk <- ts) task_time_slot tsk
      -Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
\big[ssrnat_addn__canonical__Monoid_Law/0]_(i <- ts)
   (if slot_order i task && (i != task)
    then task_time_slot i
    else 0) <=
\sum_(prev_task <- ts)
   (if prev_task != task
    then task_time_slot prev_task
    else 0) apply leq_sum => i T.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
i: Task
T: true
(if slot_order i task && (i != task)
 then task_time_slot i
 else 0) <=
(if i != task then task_time_slot i else 0) case (slot_order i task);auto.
      -Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
\sum_(prev_task <- ts)
   (if prev_task != task
    then task_time_slot prev_task
    else 0) < \sum_(tsk <- ts) task_time_slot tsk rewrite -big_mkcond (bigD1_seq task)?set_uniq//=.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
\sum_(i <- ts | i != task) task_time_slot i <
task_time_slot task +
\sum_(i <- ts | i != task) task_time_slot i
        by rewrite -subn_gt0 -addnBA // subnn addn0.
    Qed.

    (** For a task, the sum of its slot offset and its time slot is
          less then or equal to cycle. *)
    Lemma Offset_add_slot_leq_cycle:
      task_slot_offset ts task + task_time_slot task <= TDMA_cycle ts.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
task_slot_offset ts task + task_time_slot task <=
TDMA_cycle ts
    Proof.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
task_slot_offset ts task + task_time_slot task <=
TDMA_cycle ts
      rewrite /task_slot_offset /TDMA_cycle.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
\sum_(prev_task <- ts | slot_order prev_task task &&
                        (prev_task != task))
   task_time_slot prev_task + task_time_slot task <=
\sum_(tsk <- ts) task_time_slot tsk
      rewrite addnC (bigD1_seq task) //=; last by exact: (set_uniq ts).Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
task_time_slot task +
\sum_(prev_task <- ts | slot_order prev_task task &&
                        (prev_task != task))
   task_time_slot prev_task <=
task_time_slot task +
\sum_(i <- ts | i != task) task_time_slot i
      rewrite leq_add2l big_mkcond.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
\big[ssrnat_addn__canonical__Monoid_Law/0]_(i <- ts)
   (if slot_order i task && (i != task)
    then task_time_slot i
    else 0) <=
\sum_(i <- ts | i != task) task_time_slot i
      replace (\sum_(i <- ts | i != task) task_time_slot i)
        with (\sum_(i <- ts ) if i != task then task_time_slot i else 0).Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
\big[ssrnat_addn__canonical__Monoid_Law/0]_(i <- ts)
   (if slot_order i task && (i != task)
    then task_time_slot i
    else 0) <=
\sum_(i <- ts)
   (if i != task then task_time_slot i else 0)
Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
\sum_(i <- ts)
   (if i != task then task_time_slot i else 0) =
\sum_(i <- ts | i != task) task_time_slot i
      +Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
\big[ssrnat_addn__canonical__Monoid_Law/0]_(i <- ts)
   (if slot_order i task && (i != task)
    then task_time_slot i
    else 0) <=
\sum_(i <- ts)
   (if i != task then task_time_slot i else 0) apply leq_sum => i T; case (slot_order i task);auto.
      +Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
\sum_(i <- ts)
   (if i != task then task_time_slot i else 0) =
\sum_(i <- ts | i != task) task_time_slot i by rewrite -big_mkcond.
    Qed.
  End TimeSlotFacts.

  (** Now we prove that no two tasks share the same time slot at any time. *)
  Section TimeSlotOrderFacts.
    (** Consider any task in ts*)
    Variable task: Task.
    Hypothesis H_task_in_ts: task \in ts.

    (** Assume task_time_slot is valid time slot*)
    Hypothesis time_slot_positive:
      valid_time_slot ts.

    (** Assume that slot order is total... *)
    Hypothesis slot_order_total:
      total_slot_order ts.

    (*..., antisymmetric... *)
    Hypothesis slot_order_antisymmetric:
      antisymmetric_slot_order ts.

    (*... and transitive. *)
    Hypothesis slot_order_transitive:
      transitive_slot_order.

    (** Then, we can prove that the difference value between two offsets is
        at least a slot *)
    Lemma relation_offset:
      forall tsk1 tsk2, tsk1 \in ts ->
                                 tsk2 \in ts ->
                                          slot_order tsk1 tsk2 ->
                                          tsk1 != tsk2 ->
                                          task_slot_offset ts tsk2 >=
                                          task_slot_offset ts tsk1 + task_time_slot tsk1 .Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
forall tsk1 tsk2 : Task,
tsk1 \in ts ->
tsk2 \in ts ->
slot_order tsk1 tsk2 ->
tsk1 != tsk2 ->
task_slot_offset ts tsk1 + task_time_slot tsk1 <=
task_slot_offset ts tsk2
    Proof.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
forall tsk1 tsk2 : Task,
tsk1 \in ts ->
tsk2 \in ts ->
slot_order tsk1 tsk2 ->
tsk1 != tsk2 ->
task_slot_offset ts tsk1 + task_time_slot tsk1 <=
task_slot_offset ts tsk2
      move=> tsk1 tsk2 IN1 IN2 ORDER NEQ.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
task_slot_offset ts tsk1 + task_time_slot tsk1 <=
task_slot_offset ts tsk2
      rewrite /task_slot_offset big_mkcond addnC/=.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
task_time_slot tsk1 +
\sum_(i <- ts)
   (if slot_order i tsk1 && (i != tsk1)
    then task_time_slot i
    else 0) <=
\sum_(prev_task <- ts | slot_order prev_task tsk2 &&
                        (prev_task != tsk2))
   task_time_slot prev_task
      replace (\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk)
        with (task_time_slot tsk1 + \sum_(tsk <- ts )if slot_order tsk tsk2 && (tsk != tsk1) && (tsk!=tsk2) then task_time_slot tsk else O).Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
task_time_slot tsk1 +
\sum_(i <- ts)
   (if slot_order i tsk1 && (i != tsk1)
    then task_time_slot i
    else 0) <=
task_time_slot tsk1 +
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0)
Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
task_time_slot tsk1 +
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2))
   task_time_slot tsk
      -Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
task_time_slot tsk1 +
\sum_(i <- ts)
   (if slot_order i tsk1 && (i != tsk1)
    then task_time_slot i
    else 0) <=
task_time_slot tsk1 +
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0) rewrite leq_add2l.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
\sum_(i <- ts)
   (if slot_order i tsk1 && (i != tsk1)
    then task_time_slot i
    else 0) <=
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0) apply leq_sum_seq => i IN T.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
i: Task
IN: i \in ts
T: true
(if slot_order i tsk1 && (i != tsk1)
 then task_time_slot i
 else 0) <=
(if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
 then task_time_slot i
 else 0)
        case (slot_order i tsk1)eqn:SI2;auto.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
i: Task
IN: i \in ts
T: true
SI2: slot_order i tsk1 = true
(if true && (i != tsk1) then task_time_slot i else 0) <=
(if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
 then task_time_slot i
 else 0) case (i==tsk1)eqn:IT2;auto;simpl.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
i: Task
IN: i \in ts
T: true
SI2: slot_order i tsk1 = true
IT2: (i == tsk1) = false
task_time_slot i <=
(if slot_order i tsk2 && true && (i != tsk2)
 then task_time_slot i
 else 0)
        case (i==tsk2)eqn:IT1;simpl;auto.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
i: Task
IN: i \in ts
T: true
SI2: slot_order i tsk1 = true
IT2: (i == tsk1) = false
IT1: (i == tsk2) = true
task_time_slot i <=
(if slot_order i tsk2 && true && false
 then task_time_slot i
 else 0)
Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
i: Task
IN: i \in ts
T: true
SI2: slot_order i tsk1 = true
IT2: (i == tsk1) = false
IT1: (i == tsk2) = false
task_time_slot i <=
(if slot_order i tsk2 && true && true
 then task_time_slot i
 else 0)
        +Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
i: Task
IN: i \in ts
T: true
SI2: slot_order i tsk1 = true
IT2: (i == tsk1) = false
IT1: (i == tsk2) = true
task_time_slot i <=
(if slot_order i tsk2 && true && false
 then task_time_slot i
 else 0) by move/eqP in IT1;rewrite IT1 in SI2;apply slot_order_antisymmetric in ORDER;auto;apply ORDER in SI2;move/eqP in NEQ.
        +Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
i: Task
IN: i \in ts
T: true
SI2: slot_order i tsk1 = true
IT2: (i == tsk1) = false
IT1: (i == tsk2) = false
task_time_slot i <=
(if slot_order i tsk2 && true && true
 then task_time_slot i
 else 0) by rewrite (slot_order_transitive _ _ _ SI2 ORDER).
      -Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
task_time_slot tsk1 +
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0) =
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2))
   task_time_slot tsk symmetry.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2))
   task_time_slot tsk =
task_time_slot tsk1 +
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0) rewrite big_mkcond /=.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
\sum_(i <- ts)
   (if slot_order i tsk2 && (i != tsk2)
    then task_time_slot i
    else 0) =
task_time_slot tsk1 +
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0) rewrite->bigD1_seq with (j:=tsk1);auto;last by apply (set_uniq ts).Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2
NEQ: tsk1 != tsk2
ssrnat_addn__canonical__SemiGroup_ComLaw
  (if slot_order tsk1 tsk2 && (tsk1 != tsk2)
   then task_time_slot tsk1
   else 0)
  (\big[ssrnat_addn__canonical__SemiGroup_ComLaw/0]_(i <- ts | 
   i != tsk1)
      (if slot_order i tsk2 && (i != tsk2)
       then task_time_slot i
       else 0)) =
task_time_slot tsk1 +
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0)
        move/eqP /eqP in ORDER.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
NEQ: tsk1 != tsk2
ORDER: slot_order tsk1 tsk2 = true
ssrnat_addn__canonical__SemiGroup_ComLaw
  (if slot_order tsk1 tsk2 && (tsk1 != tsk2)
   then task_time_slot tsk1
   else 0)
  (\big[ssrnat_addn__canonical__SemiGroup_ComLaw/0]_(i <- ts | 
   i != tsk1)
      (if slot_order i tsk2 && (i != tsk2)
       then task_time_slot i
       else 0)) =
task_time_slot tsk1 +
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0) move/eqP in NEQ.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2 = true
NEQ: tsk1 <> tsk2
ssrnat_addn__canonical__SemiGroup_ComLaw
  (if slot_order tsk1 tsk2 && (tsk1 != tsk2)
   then task_time_slot tsk1
   else 0)
  (\big[ssrnat_addn__canonical__SemiGroup_ComLaw/0]_(i <- ts | 
   i != tsk1)
      (if slot_order i tsk2 && (i != tsk2)
       then task_time_slot i
       else 0)) =
task_time_slot tsk1 +
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0) rewrite ORDER //=.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2 = true
NEQ: tsk1 <> tsk2
(if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
\sum_(i <- ts | i != tsk1)
   (if slot_order i tsk2 && (i != tsk2)
    then task_time_slot i
    else 0) =
task_time_slot tsk1 +
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0) apply /eqP.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2 = true
NEQ: tsk1 <> tsk2
(if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
\sum_(i <- ts | i != tsk1)
   (if slot_order i tsk2 && (i != tsk2)
    then task_time_slot i
    else 0) ==
task_time_slot tsk1 +
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0)
        have TS2: (tsk1 != tsk2) = true .Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2 = true
NEQ: tsk1 <> tsk2
(tsk1 != tsk2) = true
Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2 = true
NEQ: tsk1 <> tsk2
TS2: (tsk1 != tsk2) = true
(if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
\sum_(i <- ts | i != tsk1)
   (if slot_order i tsk2 && (i != tsk2)
    then task_time_slot i
    else 0) ==
task_time_slot tsk1 +
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0)
        +Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2 = true
NEQ: tsk1 <> tsk2
(tsk1 != tsk2) = true exact /eqP.
        +Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2 = true
NEQ: tsk1 <> tsk2
TS2: (tsk1 != tsk2) = true
(if tsk1 != tsk2 then task_time_slot tsk1 else 0) +
\sum_(i <- ts | i != tsk1)
   (if slot_order i tsk2 && (i != tsk2)
    then task_time_slot i
    else 0) ==
task_time_slot tsk1 +
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0) rewrite TS2.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2 = true
NEQ: tsk1 <> tsk2
TS2: (tsk1 != tsk2) = true
task_time_slot tsk1 +
\sum_(i <- ts | i != tsk1)
   (if slot_order i tsk2 && (i != tsk2)
    then task_time_slot i
    else 0) ==
task_time_slot tsk1 +
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0)
          rewrite eqn_add2l.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2 = true
NEQ: tsk1 <> tsk2
TS2: (tsk1 != tsk2) = true
\sum_(i <- ts | i != tsk1)
   (if slot_order i tsk2 && (i != tsk2)
    then task_time_slot i
    else 0) ==
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0)
          rewrite big_mkcond.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2 = true
NEQ: tsk1 <> tsk2
TS2: (tsk1 != tsk2) = true
\big[ssrnat_addn__canonical__Monoid_Law/0]_(i <- ts)
   (if i != tsk1
    then
     if slot_order i tsk2 && (i != tsk2)
     then task_time_slot i
     else 0
    else 0) ==
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0)
          apply/eqP.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2 = true
NEQ: tsk1 <> tsk2
TS2: (tsk1 != tsk2) = true
\big[ssrnat_addn__canonical__Monoid_Law/0]_(i <- ts)
   (if i != tsk1
    then
     if slot_order i tsk2 && (i != tsk2)
     then task_time_slot i
     else 0
    else 0) =
\sum_(tsk <- ts)
   (if
     slot_order tsk tsk2 && (tsk != tsk1) &&
     (tsk != tsk2)
    then task_time_slot tsk
    else 0)
          apply eq_bigr;auto => i T.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
IN1: tsk1 \in ts
IN2: tsk2 \in ts
ORDER: slot_order tsk1 tsk2 = true
NEQ: tsk1 <> tsk2
TS2: (tsk1 != tsk2) = true
i: Task
T: true
(if i != tsk1
 then
  if slot_order i tsk2 && (i != tsk2)
  then task_time_slot i
  else 0
 else 0) =
(if slot_order i tsk2 && (i != tsk1) && (i != tsk2)
 then task_time_slot i
 else 0)
          by case(i!=tsk1); case (slot_order i tsk2); case (i!=tsk2); auto.
    Qed.

    (** Then, we proved that no two tasks share the same time slot at any time. *)
    Lemma task_in_time_slot_uniq:
      forall tsk1 tsk2 t,
        tsk1 \in ts -> task_time_slot tsk1 > 0 ->
        tsk2 \in ts -> task_time_slot tsk2 > 0 ->
        task_in_time_slot ts tsk1 t ->
        task_in_time_slot ts tsk2 t ->
        tsk1 = tsk2.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
forall (tsk1 tsk2 : Task) (t : instant),
tsk1 \in ts ->
0 < task_time_slot tsk1 ->
tsk2 \in ts ->
0 < task_time_slot tsk2 ->
task_in_time_slot ts tsk1 t ->
task_in_time_slot ts tsk2 t -> tsk1 = tsk2
    Proof.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
forall (tsk1 tsk2 : Task) (t : instant),
tsk1 \in ts ->
0 < task_time_slot tsk1 ->
tsk2 \in ts ->
0 < task_time_slot tsk2 ->
task_in_time_slot ts tsk1 t ->
task_in_time_slot ts tsk2 t -> tsk1 = tsk2
      intros tsk1 tsk2 t IN1 SLOT1 IN2 SLOT2.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
task_in_time_slot ts tsk1 t ->
task_in_time_slot ts tsk2 t -> tsk1 = tsk2
      rewrite /task_in_time_slot.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
(t + TDMA_cycle ts -
 task_slot_offset ts tsk1 %% TDMA_cycle ts)
%% TDMA_cycle ts < task_time_slot tsk1 ->
(t + TDMA_cycle ts -
 task_slot_offset ts tsk2 %% TDMA_cycle ts)
%% TDMA_cycle ts < task_time_slot tsk2 -> tsk1 = tsk2
      set cycle := TDMA_cycle ts.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
(t + cycle - task_slot_offset ts tsk1 %% cycle)
%% cycle < task_time_slot tsk1 ->
(t + cycle - task_slot_offset ts tsk2 %% cycle)
%% cycle < task_time_slot tsk2 -> tsk1 = tsk2
      set O1 := task_slot_offset ts tsk1.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
O1:= task_slot_offset ts tsk1: nat
(t + cycle - O1 %% cycle) %% cycle <
task_time_slot tsk1 ->
(t + cycle - task_slot_offset ts tsk2 %% cycle)
%% cycle < task_time_slot tsk2 -> tsk1 = tsk2
      set O2 := task_slot_offset ts tsk2.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
O1:= task_slot_offset ts tsk1: nat
O2:= task_slot_offset ts tsk2: nat
(t + cycle - O1 %% cycle) %% cycle <
task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle <
task_time_slot tsk2 -> tsk1 = tsk2
      have CO1 : O1 < cycle by apply Offset_lt_cycle.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
O1:= task_slot_offset ts tsk1: nat
O2:= task_slot_offset ts tsk2: nat
CO1: O1 < cycle
(t + cycle - O1 %% cycle) %% cycle <
task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle <
task_time_slot tsk2 -> tsk1 = tsk2
      have CO2 : O2 < cycle by apply Offset_lt_cycle.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
O1:= task_slot_offset ts tsk1: nat
O2:= task_slot_offset ts tsk2: nat
CO1: O1 < cycle
CO2: O2 < cycle
(t + cycle - O1 %% cycle) %% cycle <
task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle <
task_time_slot tsk2 -> tsk1 = tsk2
      have C : cycle > 0 by apply (TDMA_cycle_positive tsk1).Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
O1:= task_slot_offset ts tsk1: nat
O2:= task_slot_offset ts tsk2: nat
CO1: O1 < cycle
CO2: O2 < cycle
C: 0 < cycle
(t + cycle - O1 %% cycle) %% cycle <
task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle <
task_time_slot tsk2 -> tsk1 = tsk2
      have -> : O1 %% cycle = O1 by apply modn_small, Offset_lt_cycle.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
O1:= task_slot_offset ts tsk1: nat
O2:= task_slot_offset ts tsk2: nat
CO1: O1 < cycle
CO2: O2 < cycle
C: 0 < cycle
(t + cycle - O1) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2 %% cycle) %% cycle <
task_time_slot tsk2 -> tsk1 = tsk2
      have -> : O2 %% cycle = O2 by apply modn_small, Offset_lt_cycle.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
O1:= task_slot_offset ts tsk1: nat
O2:= task_slot_offset ts tsk2: nat
CO1: O1 < cycle
CO2: O2 < cycle
C: 0 < cycle
(t + cycle - O1) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2) %% cycle < task_time_slot tsk2 ->
tsk1 = tsk2
      have SO1 : O1 + task_time_slot tsk1 <= cycle by apply (Offset_add_slot_leq_cycle tsk1).Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
O1:= task_slot_offset ts tsk1: nat
O2:= task_slot_offset ts tsk2: nat
CO1: O1 < cycle
CO2: O2 < cycle
C: 0 < cycle
SO1: O1 + task_time_slot tsk1 <= cycle
(t + cycle - O1) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2) %% cycle < task_time_slot tsk2 ->
tsk1 = tsk2
      have SO2 : O2 + task_time_slot tsk2 <= cycle by apply (Offset_add_slot_leq_cycle tsk2).Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
O1:= task_slot_offset ts tsk1: nat
O2:= task_slot_offset ts tsk2: nat
CO1: O1 < cycle
CO2: O2 < cycle
C: 0 < cycle
SO1: O1 + task_time_slot tsk1 <= cycle
SO2: O2 + task_time_slot tsk2 <= cycle
(t + cycle - O1) %% cycle < task_time_slot tsk1 ->
(t + cycle - O2) %% cycle < task_time_slot tsk2 ->
tsk1 = tsk2
      repeat rewrite mod_elim; auto.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
O1:= task_slot_offset ts tsk1: nat
O2:= task_slot_offset ts tsk2: nat
CO1: O1 < cycle
CO2: O2 < cycle
C: 0 < cycle
SO1: O1 + task_time_slot tsk1 <= cycle
SO2: O2 + task_time_slot tsk2 <= cycle
(if O1 <= t %% cycle
 then t %% cycle - O1
 else t %% cycle + cycle - O1) < task_time_slot tsk1 ->
(if O2 <= t %% cycle
 then t %% cycle - O2
 else t %% cycle + cycle - O2) < task_time_slot tsk2 ->
tsk1 = tsk2
      case (O1 <= t %% cycle) eqn:O1T; case (O2 <= t %% cycle) eqn:O2T; intros G1 G2; try lia.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
O1:= task_slot_offset ts tsk1: nat
O2:= task_slot_offset ts tsk2: nat
CO1: O1 < cycle
CO2: O2 < cycle
C: 0 < cycle
SO1: O1 + task_time_slot tsk1 <= cycle
SO2: O2 + task_time_slot tsk2 <= cycle
O1T: (O1 <= t %% cycle) = true
O2T: (O2 <= t %% cycle) = true
G1: t %% cycle - O1 < task_time_slot tsk1
G2: t %% cycle - O2 < task_time_slot tsk2
tsk1 = tsk2
      rewrite ltn_subLR // in G1; rewrite ltn_subLR // in G2.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
O1:= task_slot_offset ts tsk1: nat
O2:= task_slot_offset ts tsk2: nat
CO1: O1 < cycle
CO2: O2 < cycle
C: 0 < cycle
SO1: O1 + task_time_slot tsk1 <= cycle
SO2: O2 + task_time_slot tsk2 <= cycle
O1T: (O1 <= t %% cycle) = true
O2T: (O2 <= t %% cycle) = true
G1: t %% cycle < O1 + task_time_slot tsk1
G2: t %% cycle < O2 + task_time_slot tsk2
tsk1 = tsk2
      case (tsk1 == tsk2) eqn:NEQ; move/eqP in NEQ; auto.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
O1:= task_slot_offset ts tsk1: nat
O2:= task_slot_offset ts tsk2: nat
CO1: O1 < cycle
CO2: O2 < cycle
C: 0 < cycle
SO1: O1 + task_time_slot tsk1 <= cycle
SO2: O2 + task_time_slot tsk2 <= cycle
O1T: (O1 <= t %% cycle) = true
O2T: (O2 <= t %% cycle) = true
G1: t %% cycle < O1 + task_time_slot tsk1
G2: t %% cycle < O2 + task_time_slot tsk2
NEQ: tsk1 <> tsk2
tsk1 = tsk2
      destruct (slot_order_total tsk1 tsk2) as [order | order]; auto.Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
O1:= task_slot_offset ts tsk1: nat
O2:= task_slot_offset ts tsk2: nat
CO1: O1 < cycle
CO2: O2 < cycle
C: 0 < cycle
SO1: O1 + task_time_slot tsk1 <= cycle
SO2: O2 + task_time_slot tsk2 <= cycle
O1T: (O1 <= t %% cycle) = true
O2T: (O2 <= t %% cycle) = true
G1: t %% cycle < O1 + task_time_slot tsk1
G2: t %% cycle < O2 + task_time_slot tsk2
NEQ: tsk1 <> tsk2
order: slot_order tsk1 tsk2
tsk1 = tsk2
Task: eqType
ts: {setTask}
H: TDMAPolicy Task
task: Task
H_task_in_ts: task \in ts
time_slot_positive: valid_time_slot ts
slot_order_total: total_slot_order ts
slot_order_antisymmetric: antisymmetric_slot_order ts
slot_order_transitive: transitive_slot_order
tsk1, tsk2: Task
t: instant
IN1: tsk1 \in ts
SLOT1: 0 < task_time_slot tsk1
IN2: tsk2 \in ts
SLOT2: 0 < task_time_slot tsk2
cycle:= TDMA_cycle ts: nat
O1:= task_slot_offset ts tsk1: nat
O2:= task_slot_offset ts tsk2: nat
CO1: O1 < cycle
CO2: O2 < cycle
C: 0 < cycle
SO1: O1 + task_time_slot tsk1 <= cycle
SO2: O2 + task_time_slot tsk2 <= cycle
O1T: (O1 <= t %% cycle) = true
O2T: (O2 <= t %% cycle) = true
G1: t %% cycle < O1 + task_time_slot tsk1
G2: t %% cycle < O2 + task_time_slot tsk2
NEQ: tsk1 <> tsk2
order: slot_order tsk2 tsk1
tsk1 = tsk2
      all: by apply relation_offset in order; fold O1 O2 in order; try lia; auto; apply/eqP; auto.
    Qed.

  End TimeSlotOrderFacts.

End TDMAFacts.