diff --git a/model/task/arrival/example.v b/model/task/arrival/example.v
new file mode 100644
index 0000000000000000000000000000000000000000..18a08082bb84d38df087c250c7c9e52c6f260e5e
--- /dev/null
+++ b/model/task/arrival/example.v
@@ -0,0 +1,83 @@
+Require Import prosa.model.task.arrival.periodic.
+Require Import prosa.model.task.arrival.periodic_as_sporadic.
+Require Import prosa.model.task.arrival.sporadic_as_curve.
+Require Import prosa.model.task.arrival.curve_as_rbf.
+
+(** * Arrival Model Conversion
+
+  This file demonstrates the automatic conversion of arrival
+  models. In particular, we show how a set of periodic tasks can be
+  interpreted also as (1) sporadic tasks with minimum inter-arrival
+  times, (2) sporadic tasks with arrival curves, and (3) request-bound
+  functions.  *)
+
+Section AutoArrivalModelConversion.
+
+  (** Consider periodic tasks ... *)
+  Context {Task : TaskType} `{PeriodicModel Task}.
+
+  (** ... and their corresponding jobs. *)
+  Context {Job : JobType} `{JobArrival Job} `{JobTask Job Task}.
+
+  (** Given a set of such periodic tasks  ... *)
+  Variable ts : TaskSet Task.
+
+  (** ... and a valid arrival sequence, ...*)
+  Variable arr_seq : arrival_sequence Job.  Hypothesis
+  H_consistent_arrivals: consistent_arrival_times arr_seq.  Hypothesis
+  H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
+
+  (** ... if the tasks are valid periodic tasks, ...*)
+  Hypothesis H_respects : taskset_respects_periodic_task_model arr_seq ts.
+  Hypothesis H_valid_periods : valid_periods ts.
+
+  (** ... then we can automatically interpret them also as satisfying
+      other arrival models, as we demonstrate in the following. *)
+
+  (** ** Periodic Tasks as Sporadic Tasks *)
+
+  (** The tasks satisfy the sporadic validity constraint... *)
+  Goal valid_taskset_inter_arrival_times ts.
+  Proof. by rt_auto. Qed.
+
+  (** ... and arrival sequence is legal under the sporadic task
+      model. *)
+  Goal taskset_respects_sporadic_task_model ts arr_seq.
+  Proof. by rt_auto. Qed.
+
+  (** ** Periodic Tasks as Arrival Curves *)
+
+  (** The tasks satisfy the arrival-curve validity constraint... *)
+  Goal valid_taskset_arrival_curve ts max_arrivals.
+  Proof. by rt_auto. Qed.
+
+  (** ... and the arrival sequence is legal under the arrival-curve
+      model. *)
+  Goal taskset_respects_max_arrivals arr_seq ts.
+  Proof. by rt_eauto. Qed.
+
+  (** ** Periodic Tasks as RBFs *)
+
+  (** Assuming that each task has a WCET... *)
+  Context `{TaskCost Task}.
+
+  (** ... and that jobs are compliant with the WCET, ... *)
+  Context `{JobCost Job}.
+  Hypothesis H_valid_costs : jobs_have_valid_job_costs.
+
+  (** ... the tasks satisfy the RBF validity constraint... *)
+  Goal valid_taskset_request_bound_function ts (task_max_rbf max_arrivals).
+  Proof. by rt_auto. Qed.
+
+  (** ... and the arrival sequence is legal under the RBF model. *)
+  Goal taskset_respects_max_request_bound arr_seq ts.
+  Proof. by rt_eauto. Qed.
+
+  (** Thanks to type-class resolution, all conversions from more
+      restrictive to less restrictive task model happen transparently
+      and the and necessary proofs are found automatically.
+
+      Of course, it is possible to start from sporadic tasks or tasks
+      with arrival curves, too. *)
+
+End AutoArrivalModelConversion.