diff --git a/restructuring/model/readiness/basic.v b/restructuring/model/readiness/basic.v
index c8125ed345595f06eed6510afc2fb4e7d88f452a..d9fd6d8602da58cc7cbae418ffcbe8a022d648bc 100644
--- a/restructuring/model/readiness/basic.v
+++ b/restructuring/model/readiness/basic.v
@@ -1,4 +1,5 @@
 From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior.facts Require Import completion.
 
 (* We define the readiness indicator function for the classic Liu & Layland
    model without jitter and no self-suspensions, where jobs are always
@@ -22,4 +23,24 @@ Section LiuAndLaylandReadiness.
     }.
   Proof. trivial. Defined.
 
+
+  (* Under this definition, a schedule satisfies that only ready jobs execute
+     as long as jobs must arrive to execute and completed jobs don't execute,
+     which we note with the following theorem. *)
+  Theorem basic_readiness_compliance:
+    forall sched,
+      jobs_must_arrive_to_execute sched ->
+      completed_jobs_dont_execute sched ->
+      jobs_must_be_ready_to_execute sched.
+  Proof.
+    move=> sched ARR COMP.
+    rewrite /jobs_must_be_ready_to_execute =>  j t SCHED.
+    rewrite /job_ready /basic_ready_instance /pending.
+    apply /andP; split.
+    - by apply ARR.
+    - rewrite -less_service_than_cost_is_incomplete.
+      by apply COMP.
+  Qed.
+
 End LiuAndLaylandReadiness.
+