diff --git a/analysis/definitions/demand_bound_function.v b/analysis/definitions/demand_bound_function.v
new file mode 100644
index 0000000000000000000000000000000000000000..cbde5ea37be45dae2ec60f8967884b3051f73c2b
--- /dev/null
+++ b/analysis/definitions/demand_bound_function.v
@@ -0,0 +1,22 @@
+Require Export prosa.analysis.definitions.request_bound_function.
+
+(** * Demand Bound Function (DBF) *)
+(** Here we define Baruah et al.'s classic notion of a demand bound function,
+    generalized to arbitrary arrival curves. *)
+Section DemandBoundFunction.
+  (** Consider any type of tasks. *)
+  Context {Task : TaskType}.
+
+  (** Suppose each task is characterized by a WCET, a relative deadline, and an arrival curve. *)
+  Context `{TaskCost Task} `{TaskDeadline Task} `{MaxArrivals Task}.
+
+  (** A task's DBF is its request-bound function (RBF) shifted by [task_deadline tsk - 1] time units. *)
+  Definition task_demand_bound_function (tsk : Task) (delta : duration) :=
+    let delta' := delta - (task_deadline tsk - 1) in
+      task_request_bound_function tsk delta'.
+
+  (** A task set's total demand bound function is simply the sum of each task's DBF.*)
+  Definition total_demand_bound_function (ts: seq Task) (delta : duration) :=
+    \sum_(tsk <- ts) task_demand_bound_function tsk delta.
+
+End DemandBoundFunction.
diff --git a/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v
index 52d91d547b805f82a2aa2151865fce20f0e20361..cf3621c5755fbbada044ad69af9186e4e41901d9 100644
--- a/analysis/facts/behavior/arrivals.v
+++ b/analysis/facts/behavior/arrivals.v
@@ -2,8 +2,6 @@ Require Export prosa.behavior.all.
 Require Export prosa.util.all.
 Require Export prosa.model.task.arrivals.
 
-
-
 (** * Arrival Sequence *)
 
 (** First, we relate the stronger to the weaker arrival predicates. *)
@@ -479,6 +477,34 @@ Section ArrivalSequencePrefix.
 
   End ArrivalTimes.
 
+  (** In the following section, we establish a lemma that allows splitting the arrival sequence by task. *)
+  Section ArrivalPartition.
+
+    (** If all jobs stem from tasks in a given task set [ts]... *)
+    Variable ts : seq Task.
+    Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+    (** ... then we can partition the arrival sequence by task. *)
+    Lemma arrivals_between_partitioned_by_task:
+      forall t1 t2 j,
+        (j \in arrivals_between arr_seq t1 t2)
+        = (j \in \cat_(tsk <- ts) task_arrivals_between arr_seq tsk t1 t2).
+    Proof.
+      move=> t1 t2 j.
+      rewrite /task_arrivals_between.
+      set l:= arrivals_between arr_seq t1 t2.
+      rewrite -{1}(@filter_predT _ l).
+      under eq_big_seq.
+      { move=> tsk tsk_IN.
+        rewrite (@eq_in_filter _ _ (fun j => (predT j) && (job_of_task tsk j))) => //.
+        over. }
+      apply bigcat_partitions => j' IN' pred_true.
+      apply H_all_jobs_from_taskset.
+      by apply in_arrivals_implies_arrived in IN'.
+    Qed.
+
+  End ArrivalPartition.
+
 End ArrivalSequencePrefix.
 
 (** In this section, we establish a few auxiliary facts about the
diff --git a/analysis/facts/model/dbf.v b/analysis/facts/model/dbf.v
new file mode 100644
index 0000000000000000000000000000000000000000..96830fd44c5fbc828f17b88ccfab00d59f253516
--- /dev/null
+++ b/analysis/facts/model/dbf.v
@@ -0,0 +1,175 @@
+Require Export prosa.model.task.absolute_deadline.
+Require Export prosa.analysis.definitions.demand_bound_function.
+Require Export prosa.analysis.facts.model.rbf.
+Require Export prosa.analysis.facts.model.workload.
+
+(** * Facts about the Demand Bound Function (DBF) *)
+(** In this file we establish some properties of DBFs. *)
+Section ProofDemandBoundDefinition.
+  (** Consider any type of task with relative deadlines and any type of jobs associated with such tasks. *)
+  Context {Task : TaskType} `{TaskDeadline Task}
+          {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
+
+  (** Consider a valid arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** First, we establish a relation between a task's arrivals in a given interval and
+      those arrivals that also have a deadline contained within the given interval. *)
+  Lemma task_arrivals_with_deadline_within_eq:
+    forall (tsk : Task) (t : instant) (delta : duration),
+      task_arrivals_with_deadline_within arr_seq tsk t (t + delta)
+      = task_arrivals_between arr_seq tsk t (t + (delta - (task_deadline tsk -1))).
+  Proof.
+    move=> tsk t delta.
+    rewrite /task_arrivals_with_deadline_within/job_deadline
+      /job_deadline_from_task_deadline/task_arrivals_between.
+    rewrite (@arrivals_between_cat _ _ _ (t + (delta - (task_deadline tsk - 1)))); try lia.
+    rewrite filter_cat.
+    rewrite (@eq_in_filter _ _ (fun j => job_of_task tsk j)).
+    { set nilS := [seq j <- arrivals_between arr_seq t (t + (delta - (task_deadline tsk - 1))) | job_of_task tsk j].
+      rewrite -[in RHS](@cats0 _ nilS).
+      apply /eqP; rewrite eqseq_cat => //=.
+      apply /andP; split => //=.
+      rewrite (@eq_in_filter _ _ pred0);
+        first by rewrite filter_pred0.
+      move=> j IN.
+      have [/eqP ->|] := boolP (job_of_task tsk j) => //=.
+      have GEQ: job_arrival j >= t + (delta - (task_deadline tsk - 1))
+        by apply: job_arrival_between_ge.
+      have LT := (arrivals_between_nonempty _ _ _ _ IN).
+      by lia. }
+    { move=> j IN.
+      have [/eqP ->|] := boolP (job_of_task tsk j) => //=.
+      have -> : (job_arrival j + task_deadline tsk  <= t + delta) => //.
+      have LT := (arrivals_between_nonempty _ _ _ _ IN).
+      have LTj: job_arrival j < t + (delta - (task_deadline tsk - 1))
+        by apply: job_arrival_between_lt.
+      by lia. }
+  Qed.
+
+  (** As a corollary, we also show a much more useful result that arises when we count these jobs. *)
+  Corollary num_task_arrivals_with_deadline_within_eq:
+    forall (tsk : Task) (t : instant) (delta : duration),
+      number_of_task_arrivals_with_deadline_within arr_seq tsk t (t + delta)
+      = number_of_task_arrivals arr_seq tsk t (t + (delta - (task_deadline tsk - 1))).
+  Proof.
+    move=> tsk t delta.
+    rewrite /number_of_task_arrivals_with_deadline_within
+      /number_of_task_arrivals.
+    by rewrite task_arrivals_with_deadline_within_eq.
+  Qed.
+
+  (** In the following, assume we are given a valid WCET bound for each task. *)
+  Context `{TaskCost Task} `{JobCost Job}.
+  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
+
+  (** A task's _demand_ in a given interval is the sum of the execution costs (i.e., the workload) of the task's jobs
+      that both arrive in the interval and have a deadline within it. *)
+  Definition task_demand_within (tsk :  Task) (t1 t2 : instant)  :=
+    let
+      causing_demand (j : Job) := (job_deadline j <= t2) && (job_of_task tsk j)
+    in
+      workload_of_jobs causing_demand (arrivals_between arr_seq t1 t2).
+
+  (** Consider a task set [ts]. *)
+  Variable ts : seq Task.
+
+  (** Let [max_arrivals] be any arrival curve. *)
+  Context `{MaxArrivals Task}.
+  Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
+
+  (** The task's processor demand  [task_demand_within] is upper-bounded by the task's DBF [task_demand_bound_function]. *)
+  Lemma task_demand_within_le_task_dbf:
+    forall (tsk : Task) t delta,
+      tsk \in ts ->
+      task_demand_within tsk t (t + delta) <= task_demand_bound_function tsk delta.
+  Proof.
+    move=> tsk t delta IN0.
+    have ->: task_demand_within tsk t (t + delta)
+      = task_workload_between arr_seq tsk t (t + (delta - (task_deadline tsk - 1))).
+      { rewrite /task_demand_within/task_workload_between/task_workload/workload_of_jobs.
+        under eq_bigl do rewrite andbC.
+        rewrite -big_filter.
+        move: (task_arrivals_with_deadline_within_eq tsk t delta).
+        rewrite /task_arrivals_with_deadline_within/task_arrivals_between => ->.
+        by rewrite big_filter. }
+    rewrite /task_demand_bound_function/task_workload_between/task_workload.
+    by apply workload_le_rbf.
+  Qed.
+
+  (** We also prove that [task_demand_within] is less than shifted RBF. *)
+  Corollary task_demand_within_le_task_rbf_shifted:
+    forall (tsk : Task) t delta,
+      tsk \in ts ->
+      task_demand_within tsk t (t + delta) <= task_request_bound_function tsk (delta - (task_deadline tsk - 1)).
+  Proof.
+    move=> tsk t delta IN0.
+    by apply task_demand_within_le_task_dbf.
+  Qed.
+
+  (** Next, we define the total workload of all jobs that arrives in a given interval that also have a
+      deadline within the interval. *)
+  Definition total_demand_within (t1 t2 : instant) :=
+    let
+      causing_demand (j : Job) := job_deadline j <= t2
+    in
+      workload_of_jobs causing_demand (arrivals_between arr_seq t1 t2).
+
+  (** Assume that all jobs come from the task set [ts]. *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+  (** We relate [total_demand_within] to the sum of each task's demand [task_demand_within]. *)
+  Lemma total_demand_within_le_sum_over_partitions:
+    forall (t : instant) (delta : duration),
+      total_demand_within t (t + delta) <= \sum_(tsk <- ts) task_demand_within tsk t (t + delta).
+  Proof.
+    move=> t delta.
+    rewrite /total_demand_within/task_demand_within.
+    rewrite /workload_of_jobs.
+    apply sum_over_partitions_le.
+    move=> j' IN ?.
+    apply H_all_jobs_from_taskset.
+    by apply in_arrivals_implies_arrived in IN.
+  Qed.
+
+  (** Here we prove a stronger version of the above lemma by assuming that the task set [ts] is indeed a set. *)
+  Lemma total_demand_within_partitioned_by_tasks:
+    forall (t : instant) (delta : duration),
+      uniq ts ->
+      total_demand_within t (t + delta) = \sum_(tsk <- ts) task_demand_within tsk t (t + delta).
+  Proof.
+    move=> t delta UniqTS.
+    rewrite /total_demand_within/task_demand_within.
+    rewrite /job_of_task.
+    apply workload_of_jobs_partitioned_by_tasks => //=.
+    move=> j' IN.
+    apply H_all_jobs_from_taskset.
+    by apply in_arrivals_implies_arrived in IN.
+  Qed.
+
+  (** Finally we establish that [total_demand_within] is bounded by [total_demand_bound_function]. *)
+  Lemma total_demand_within_le_total_dbf:
+    forall (t : instant) (delta : duration),
+      total_demand_within t (t + delta) <= total_demand_bound_function ts delta.
+  Proof.
+    move=> t delta.
+    apply (@leq_trans (\sum_(tsk <- ts) task_demand_within tsk t (t + delta)));
+      first by apply total_demand_within_le_sum_over_partitions.
+    rewrite /total_demand_bound_function.
+    apply leq_sum_seq => tsk' tsk_IN P_tsk.
+    by apply task_demand_within_le_task_dbf.
+  Qed.
+
+  (** As a corollary, we also note that [total_demand_within] is less than
+      the sum of each task's shifted RBF. *)
+  Corollary total_demand_within_le_sum_task_rbf_shifted:
+    forall (t : instant ) (delta : instant),
+      total_demand_within t (t + delta)
+      <= \sum_(tsk <- ts) task_request_bound_function tsk (delta - (task_deadline tsk - 1)).
+  Proof.
+    move=> t delta.
+    by apply total_demand_within_le_total_dbf.
+  Qed.
+
+End ProofDemandBoundDefinition.
diff --git a/model/task/arrivals.v b/model/task/arrivals.v
index 0ff7d557c914c56d97e807bdd547077fbe5b3c8c..63da4159bdefd707d0b65c64eecfdaffa338a462 100644
--- a/model/task/arrivals.v
+++ b/model/task/arrivals.v
@@ -22,7 +22,7 @@ Section TaskArrivals.
       in a given half-open interval <<[t1, t2)>>. *)
   Definition task_arrivals_between (t1 t2 : instant) :=
     [seq j <- arrivals_between arr_seq t1 t2 | job_of_task tsk j].
-  
+
   (** Based on that, we define the list of jobs of task [tsk] that
       arrive up to and including time [t], ... *)
   Definition task_arrivals_up_to (t : instant) :=
@@ -45,6 +45,19 @@ Section TaskArrivals.
   Definition cost_of_task_arrivals (t1 t2 : instant) :=
     \sum_(j <- task_arrivals_between t1 t2) job_cost j.
 
+  (** In the following, suppose there is a deadline associated with each job. *)
+  Context `{JobDeadline Job}.
+
+  (** We define the list of jobs of task [tsk] that arrive in
+      a given half-open interval <<[t1, t2)>> and that also have a deadline
+      within the closed interval <<[t1, t2]>>, ... *)
+  Definition task_arrivals_with_deadline_within (t1 t2 : instant) :=
+    [seq j <- arrivals_between arr_seq t1 t2 | job_of_task tsk j & job_deadline j <= t2].
+
+  (** ... and similarly define the count of such jobs. *)
+  Definition number_of_task_arrivals_with_deadline_within (t1 t2 : instant) :=
+    size (task_arrivals_with_deadline_within t1 t2).
+
 End TaskArrivals.
 
 (** In this section we introduce a few definitions
diff --git a/scripts/wordlist.pws b/scripts/wordlist.pws
index c82427c6a7a367e34ab8fcfbdec00a985e11a9b1..0d92bc2debce04c66e20d4f77184ce31b38779c2 100644
--- a/scripts/wordlist.pws
+++ b/scripts/wordlist.pws
@@ -50,6 +50,8 @@ RTAs
 IBF
 RBF
 RBFs
+DBF
+DBFs
 WCET
 WCETs
 BCET
@@ -127,4 +129,5 @@ IBFs
 boundedness
 RHS
 LHS
-subsequence
\ No newline at end of file
+subsequence
+Baruah
diff --git a/util/bigcat.v b/util/bigcat.v
index ef31c239d68ced378d019dbbd6c0cb9f3244ade9..1a6d3a2b5454975fe7928a751831ebb6cce0aeff 100644
--- a/util/bigcat.v
+++ b/util/bigcat.v
@@ -385,3 +385,48 @@ Section BigCatNestedCount.
   Qed.
 
 End BigCatNestedCount.
+
+(** In the following section we introduce a lemma that relates to partitioning.*)
+Section BigCatPartitionLemma.
+  (** Consider an item type [X] and partition type [Y] both supporting equality comparisons. *)
+  Variable X Y : eqType.
+
+  (** Consider a sequence of items of type [X] ... *)
+  Variable xs : seq X.
+  (** ... and a sequence of partitions. *)
+  Variable ys : seq Y.
+
+  (** Consider a predicate [P] on [X]. *)
+  Variable P : pred X.
+
+  (** Define a mapping from items to partitions. *)
+  Variable x_to_y : X -> Y.
+
+  (** We assume that any item in [xs] has its corresponding partition in the sequence of partitions [ys]. *)
+  Hypothesis H_no_partition_missing : forall x, x \in xs -> P x -> x_to_y x \in ys.
+
+  (** Consider a partition of [xs]. *)
+  Let partitioned_seq (y : Y) := [seq x <- xs | P x && (x_to_y x == y)].
+
+  (** We prove that any element in [xs] is also contained in the union of the partitions. *)
+  Lemma bigcat_partitions:
+    forall j,
+      (j \in [seq x <- xs | P x])
+      = (j \in \cat_(y <- ys) partitioned_seq y).
+  Proof.
+    move=> j.
+    apply /idP/idP.
+    { rewrite mem_filter => /andP [PredJ_true IN].
+      apply mem_bigcat with (x := x_to_y j).
+      { move: IN PredJ_true.
+        by apply H_no_partition_missing. }
+      rewrite mem_filter.
+      by do 2! [apply /andP; split; eauto]. }
+    { move=> /mem_bigcat_exists [x [x_IN IN]].
+      move: IN.
+      rewrite !mem_filter.
+      move=> /andP [/andP [PredJ X_to_Y_eq] IN].
+      by apply /andP. }
+  Qed.
+
+End BigCatPartitionLemma.