Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
(** * Implementation of Tasks and Jobs *) (** This file provides reference implementations of the notions of "tasks" and "jobs" that can be used to meet the hypotheses on which many of the analyses in Prosa are based. Note that their use is entirely optional: clients of Prosa may choose to use these types or implement their own notions of "tasks" and "jobs". *) (** ** Implementation of a Concrete Task *) (** A task comprises of an id, a cost, an arrival bound, a deadline and a priority. *) Structure concrete_task := { task_id: nat (* for uniqueness *) ; task_cost: nat ; task_arrival: task_arrivals_bound ; task_deadline: instant ; task_priority : nat }. (** To make it compatible with ssreflect, we define a decidable equality for concrete tasks. *) Definition task_eqdef (t1 t2: concrete_task) := (task_id t1 == task_id t2) && (task_cost t1 == task_cost t2) && (task_arrival t1 == task_arrival t2) && (task_deadline t1 == task_deadline t2) && (task_priority t1 == task_priority t2). (** Next, we prove that [task_eqdef] is indeed an equality, ... *)

Equality.axiom (T:=concrete_task) task_eqdef

Equality.axiom (T:=concrete_task) task_eqdef
x, y: concrete_task

reflect (x = y) (task_eqdef x y)
x, y: concrete_task
EQ: task_eqdef x y = true

reflect (x = y) true
x, y: concrete_task
EQ: task_eqdef x y = false
reflect (x = y) false
x, y: concrete_task
EQ: task_eqdef x y = true

reflect (x = y) true
x, y: concrete_task
EQ: task_eqdef x y = true

x = y
x, y: concrete_task
EQ: (task_id x == task_id y) && (task_cost x == task_cost y) && (task_arrival x == task_arrival y) && (task_deadline x == task_deadline y) && (task_priority x == task_priority y) = true

x = y
x, y: concrete_task
ID: task_id x = task_id y
COST: task_cost x = task_cost y
PER: task_arrival x = task_arrival y
DL: task_deadline x = task_deadline y
PRIO: task_priority x = task_priority y

x = y
by destruct x, y; simpl in *; subst.
x, y: concrete_task
EQ: task_eqdef x y = false

reflect (x = y) false
x, y: concrete_task
EQ: task_eqdef x y = false

reflect (x = y) false
x, y: concrete_task
EQ: task_eqdef x y = false

x <> y
x, y: concrete_task
EQ: (task_id x == task_id y) && (task_cost x == task_cost y) && (task_arrival x == task_arrival y) && (task_deadline x == task_deadline y) && (task_priority x == task_priority y) = false
BUG: x = y

False
x, y: concrete_task
EQ: ~~ ((task_id x == task_id y) && (task_cost x == task_cost y) && (task_arrival x == task_arrival y) && (task_deadline x == task_deadline y) && (task_priority x == task_priority y))
BUG: x = y

False
x, y: concrete_task
BUG: x = y
EQ: (task_id x != task_id y) || (task_cost x != task_cost y) || (task_arrival x != task_arrival y) || (task_deadline x != task_deadline y) || (task_priority x != task_priority y)

False
task_id0, task_cost0: nat
task_arrival0: task_arrivals_bound
task_deadline0: instant
task_priority0, task_id1, task_cost1: nat
task_arrival1: task_arrivals_bound
task_deadline1: instant
task_priority1: nat
BUG: {| task_id := task_id0; task_cost := task_cost0; task_arrival := task_arrival0; task_deadline := task_deadline0; task_priority := task_priority0 |} = {| task_id := task_id1; task_cost := task_cost1; task_arrival := task_arrival1; task_deadline := task_deadline1; task_priority := task_priority1 |}
EQ: (task_id {| task_id := task_id0; task_cost := task_cost0; task_arrival := task_arrival0; task_deadline := task_deadline0; task_priority := task_priority0 |} != task_id {| task_id := task_id1; task_cost := task_cost1; task_arrival := task_arrival1; task_deadline := task_deadline1; task_priority := task_priority1 |}) || (task_cost {| task_id := task_id0; task_cost := task_cost0; task_arrival := task_arrival0; task_deadline := task_deadline0; task_priority := task_priority0 |} != task_cost {| task_id := task_id1; task_cost := task_cost1; task_arrival := task_arrival1; task_deadline := task_deadline1; task_priority := task_priority1 |}) || (task_arrival {| task_id := task_id0; task_cost := task_cost0; task_arrival := task_arrival0; task_deadline := task_deadline0; task_priority := task_priority0 |} != task_arrival {| task_id := task_id1; task_cost := task_cost1; task_arrival := task_arrival1; task_deadline := task_deadline1; task_priority := task_priority1 |}) || (task_deadline {| task_id := task_id0; task_cost := task_cost0; task_arrival := task_arrival0; task_deadline := task_deadline0; task_priority := task_priority0 |} != task_deadline {| task_id := task_id1; task_cost := task_cost1; task_arrival := task_arrival1; task_deadline := task_deadline1; task_priority := task_priority1 |}) || (task_priority {| task_id := task_id0; task_cost := task_cost0; task_arrival := task_arrival0; task_deadline := task_deadline0; task_priority := task_priority0 |} != task_priority {| task_id := task_id1; task_cost := task_cost1; task_arrival := task_arrival1; task_deadline := task_deadline1; task_priority := task_priority1 |})

False
task_id0, task_cost0: nat
task_arrival0: task_arrivals_bound
task_deadline0: instant
task_priority0, task_id1, task_cost1: nat
task_arrival1: task_arrivals_bound
task_deadline1: instant
task_priority1: nat
EQ: (task_id {| task_id := task_id0; task_cost := task_cost0; task_arrival := task_arrival0; task_deadline := task_deadline0; task_priority := task_priority0 |} != task_id {| task_id := task_id1; task_cost := task_cost1; task_arrival := task_arrival1; task_deadline := task_deadline1; task_priority := task_priority1 |}) || (task_cost {| task_id := task_id0; task_cost := task_cost0; task_arrival := task_arrival0; task_deadline := task_deadline0; task_priority := task_priority0 |} != task_cost {| task_id := task_id1; task_cost := task_cost1; task_arrival := task_arrival1; task_deadline := task_deadline1; task_priority := task_priority1 |}) || (task_arrival {| task_id := task_id0; task_cost := task_cost0; task_arrival := task_arrival0; task_deadline := task_deadline0; task_priority := task_priority0 |} != task_arrival {| task_id := task_id1; task_cost := task_cost1; task_arrival := task_arrival1; task_deadline := task_deadline1; task_priority := task_priority1 |}) || (task_deadline {| task_id := task_id0; task_cost := task_cost0; task_arrival := task_arrival0; task_deadline := task_deadline0; task_priority := task_priority0 |} != task_deadline {| task_id := task_id1; task_cost := task_cost1; task_arrival := task_arrival1; task_deadline := task_deadline1; task_priority := task_priority1 |}) || (task_priority {| task_id := task_id0; task_cost := task_cost0; task_arrival := task_arrival0; task_deadline := task_deadline0; task_priority := task_priority0 |} != task_priority {| task_id := task_id1; task_cost := task_cost1; task_arrival := task_arrival1; task_deadline := task_deadline1; task_priority := task_priority1 |})
ID: task_id0 = task_id1
COST: task_cost0 = task_cost1
PER: task_arrival0 = task_arrival1
DL: task_deadline0 = task_deadline1
PRIO: task_priority0 = task_priority1

False
task_id0, task_cost0: nat
task_arrival0: task_arrivals_bound
task_deadline0: instant
task_priority0, task_id1, task_cost1: nat
task_arrival1: task_arrivals_bound
task_deadline1: instant
task_priority1: nat
ID: task_id0 = task_id1
COST: task_cost0 = task_cost1
PER: task_arrival0 = task_arrival1
DL: task_deadline0 = task_deadline1
PRIO: task_priority0 = task_priority1
EQ: (task_id1 != task_id1) || (task_cost1 != task_cost1) || (task_arrival1 != task_arrival1) || (task_deadline1 != task_deadline1) || (task_priority1 != task_priority1)

False
by subst; rewrite !eq_refl in EQ. } Qed. (** ..., which allows instantiating the canonical structure for [[eqType of concrete_task]]. *) Canonical concrete_task_eqMixin := EqMixin eqn_task. Canonical concrete_task_eqType := Eval hnf in EqType concrete_task concrete_task_eqMixin. (** ** Implementation of a Concrete Job *) (** A job comprises of an id, an arrival time, a cost, a deadline and the task it belongs to. *) Record concrete_job := { job_id: nat ; job_arrival: instant ; job_cost: nat ; job_deadline: instant ; job_task: [eqType of concrete_task] }. (** For convenience, we define a function that converts each possible arrival bound (periodic, sporadic, and arrival-curve prefix) into an arrival-curve prefix... *) Definition get_arrival_curve_prefix tsk := match task_arrival tsk with | Periodic p => inter_arrival_to_prefix p | Sporadic m => inter_arrival_to_prefix m | ArrivalPrefix steps => steps end. (** ... and define the "arrival bound" concept for concrete tasks. *) Definition concrete_max_arrivals tsk Δ := extrapolated_arrival_curve (get_arrival_curve_prefix tsk) Δ. (** To make it compatible with ssreflect, we define a decidable equality for concrete jobs. *) Definition job_eqdef (j1 j2: concrete_job) := (job_id j1 == job_id j2) && (job_arrival j1 == job_arrival j2) && (job_cost j1 == job_cost j2) && (job_deadline j1 == job_deadline j2) && (job_task j1 == job_task j2). (** Next, we prove that [job_eqdef] is indeed an equality, ... *)

Equality.axiom (T:=concrete_job) job_eqdef

Equality.axiom (T:=concrete_job) job_eqdef
x, y: concrete_job

reflect (x = y) (job_eqdef x y)
x, y: concrete_job
EQ: job_eqdef x y = true

reflect (x = y) true
x, y: concrete_job
EQ: job_eqdef x y = false
reflect (x = y) false
x, y: concrete_job
EQ: job_eqdef x y = true

reflect (x = y) true
x, y: concrete_job
EQ: (job_id x == job_id y) && (job_arrival x == job_arrival y) && (job_cost x == job_cost y) && (job_deadline x == job_deadline y) && (job_task x == job_task y) = true

x = y
x, y: concrete_job
ID: job_id x = job_id y
ARR: job_arrival x = job_arrival y
COST: job_cost x = job_cost y
DL: job_deadline x = job_deadline y
TASK: job_task x = job_task y

x = y
by destruct x, y; simpl in *; subst.
x, y: concrete_job
EQ: job_eqdef x y = false

reflect (x = y) false
x, y: concrete_job
EQ: job_eqdef x y = false

reflect (x = y) false
x, y: concrete_job
EQ: job_eqdef x y = false

x <> y
x, y: concrete_job
EQ: (job_id x == job_id y) && (job_arrival x == job_arrival y) && (job_cost x == job_cost y) && (job_deadline x == job_deadline y) && (job_task x == job_task y) = false
BUG: x = y

False
x, y: concrete_job
BUG: x = y
EQ: ~~ ((job_id x == job_id y) && (job_arrival x == job_arrival y) && (job_cost x == job_cost y) && (job_deadline x == job_deadline y)) || (job_task x != job_task y)

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
EQ: ~~ ((job_id {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_id {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}) && (job_arrival {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_arrival {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}) && (job_cost {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_cost {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}) && (job_deadline {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_deadline {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |})) || (job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} != job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |})

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
EQ: ~~ ((job_id {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_id {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}) && (job_arrival {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_arrival {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}) && (job_cost {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_cost {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |})) || (job_deadline {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} != job_deadline {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}) || (job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} != job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |})

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
EQ: ~~ ((job_id {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_id {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}) && (job_arrival {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_arrival {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}) && (job_cost {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_cost {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |})) || (job_deadline {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} != job_deadline {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |})

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
TASK: job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
EQ: ~~ ((job_id {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_id {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}) && (job_arrival {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_arrival {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}) && (job_cost {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_cost {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}))

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
DL: job_deadline {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_deadline {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
TASK: job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
EQ: ~~ ((job_id {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_id {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}) && (job_arrival {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_arrival {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |})) || (job_cost {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} != job_cost {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |})

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
DL: job_deadline {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_deadline {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
TASK: job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
EQ: ~~ ((job_id {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_id {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}) && (job_arrival {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} == job_arrival {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}))

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
COST: job_cost {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_cost {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
DL: job_deadline {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_deadline {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
TASK: job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
EQ: (job_id {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} != job_id {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}) || (job_arrival {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} != job_arrival {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |})

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
COST: job_cost {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_cost {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
DL: job_deadline {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_deadline {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
TASK: job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
ID: job_id {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_id {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
ARR: job_arrival {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_arrival {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
COST: job_cost {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_cost {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
DL: job_deadline {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_deadline {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
TASK: job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
ID: job_id {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_id {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
ARR: job_arrival {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_arrival {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
COST: job_cost {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_cost {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
DL: job_deadline {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_deadline {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
TASK: job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
ARR: job_arrival {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_arrival {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
COST: job_cost {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_cost {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
DL: job_deadline {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_deadline {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
TASK: job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
ARR: job_arrival {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_arrival {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
COST: job_cost {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_cost {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
DL: job_deadline {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_deadline {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
TASK: job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
COST: job_cost {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_cost {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
DL: job_deadline {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_deadline {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
TASK: job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
COST: job_cost {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_cost {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
DL: job_deadline {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_deadline {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
TASK: job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
DL: job_deadline {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_deadline {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
TASK: job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
DL: job_deadline {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_deadline {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
TASK: job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
TASK: job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}

False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: [eqType of concrete_task]
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: [eqType of concrete_task]
BUG: {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} = {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}
TASK: job_task {| job_id := job_id0; job_arrival := job_arrival0; job_cost := job_cost0; job_deadline := job_deadline0; job_task := job_task0 |} <> job_task {| job_id := job_id1; job_arrival := job_arrival1; job_cost := job_cost1; job_deadline := job_deadline1; job_task := job_task1 |}

False
by apply TASK; inversion BUG. } Qed. (** ... which allows instantiating the canonical structure for [[eqType of concrete_job]].*) Canonical concrete_job_eqMixin := EqMixin eqn_job. Canonical concrete_job_eqType := Eval hnf in EqType concrete_job concrete_job_eqMixin. (** ** Instances for Concrete Jobs and Tasks. *) (** In the following, we connect the concrete task and job types defined above to the generic Prosa interfaces for task and job parameters. *) Section Parameters. (** First, we connect the above definition of tasks with the generic Prosa task-parameter interfaces. *) Let Task := [eqType of concrete_task]. #[global,program] Instance TaskCost : TaskCost Task := task_cost. #[global,program] Instance TaskPriority : TaskPriority Task := task_priority. #[global,program] Instance TaskDeadline : TaskDeadline Task := task_deadline. #[global,program] Instance ConcreteMaxArrivals : MaxArrivals Task := concrete_max_arrivals. (** Second, we do the same for the above definition of job. *) Let Job := [eqType of concrete_job]. #[global,program] Instance JobTask : JobTask Job Task := job_task. #[global,program] Instance JobArrival : JobArrival Job := job_arrival. #[global,program] Instance JobCost : JobCost Job := job_cost. End Parameters.