diff --git a/coq/Arbiter.v b/coq/Arbiter.v
index 60a9e9d26919f9cf017329a35881063d86fa6e88..45d58648bc816bd12fe13f00a31ee521650beace 100644
--- a/coq/Arbiter.v
+++ b/coq/Arbiter.v
@@ -25,7 +25,7 @@ Section Arbiter.
     Arbitrate : Trace_t;
 
     (* All Requests must handled *)
-    Req_handled : forall req,  req \in Requests -> exists cmd : Command_t, cmd \in Arbitrate.(Commands) ->
-                    Match req cmd
+    Req_handled : forall req,  req \in Requests -> 
+                  exists cmd : Command_t, (cmd \in Arbitrate.(Commands)) && ((Match req cmd))
   }.
 End Arbiter.
diff --git a/coq/Commands.v b/coq/Commands.v
index 96bd4e1bc82b068ae4ad527f5810c0a326e4fd7a..232708b756f953bed4e308e2a9ae43cafc12e580 100644
--- a/coq/Commands.v
+++ b/coq/Commands.v
@@ -76,7 +76,7 @@ Section Commands.
 
   Definition isPRE (cmd : Command_t) :=
     cmd.(CKind) == PRE.
-
+    
   Definition PRE_of_req req t :=
     mkCmd t PRE req.
 
diff --git a/coq/FIFO.v b/coq/FIFO.v
index 451e4633e29dd00e9a3b63cc1accb9cd04c915fe..6e484177adea71b96eb026fa2e4178cda4dcd5cb 100644
--- a/coq/FIFO.v
+++ b/coq/FIFO.v
@@ -244,20 +244,72 @@ Section FIFO.
     - by apply (IHReqs' a b) in Ia.
   Qed.
 
+  Lemma Between_cons req Reqs a b: 
+    a \in (FIFO_trace Reqs).(Cmds) -> b \in (FIFO_trace Reqs).(Cmds) ->
+    Between ((FIFO_trace Reqs).(Cmds)) a b =
+    Between (FIFO_trace (req :: Reqs)).(Cmds) a b.
+  Proof.
+  Admitted.
+
+  Lemma FIFO_trace_Cmds_PRE_ok Reqs :
+    forall a b, a \in (FIFO_trace Reqs).(Cmds) -> b \in (FIFO_trace Reqs).(Cmds) ->
+                  PRE_to_PRE a b -> Same_Bank a b -> Before a b -> 
+                  exists c : Command_t, isACT c /\ Same_Bank a c /\ c \in Between (FIFO_trace Reqs).(Cmds) a b.
+  Proof.
+    intros a b a_cmds b_cmds ab_PRE ab_BANK a_not_b.
+    evar (req_date : nat). 
+    evar (t : nat).
+    evar (req_kind : Request_kind_t).
+    set (req := mkReq req_date req_kind a.(Request).(Bank)).
+    exists (ACT_of_req req t).
+    split.
+    - auto.
+    - split.
+      - by unfold ACT_of_req, Same_Bank.
+      - induction Reqs.
+          - auto.
+          - simpl in a_cmds.
+            move : a_cmds => /orP [ /eqP a_eq | /orP [ /eqP a_eq  | /orP [ /eqP a_eq | Ia]] ];
+            move : b_cmds => /orP [ /eqP b_eq | /orP [ /eqP b_eq  | /orP [ /eqP b_eq | Ib]] ].
+            - admit.
+            - admit.
+            - admit.
+            - admit.
+            - admit.
+            - admit.
+            - admit.
+            - admit.
+            - admit.
+            - admit.
+            - (*they are the same*) admit.
+            - (*easy due to order*) admit.
+            - admit.
+            - admit.
+            - (* interesting - induction on Reqs until find request of A until I find my ACT cmd (?)*) admit.
+            - rewrite <- Between_cons. apply IHReqs in Ia. apply Ia. all : auto.
+  Admitted.
+
   Program Definition FIFO_arbitrate :=
     let State := FIFO_trace Requests in
-      mkTrace State.(Cmds) State.(Time) _ (FIFO_trace_time_ok Requests) (FIFO_trace_T_RC_ok Requests) (FIFO_trace_T_RP_ok Requests).
+      mkTrace State.(Cmds) State.(Time) _ (FIFO_trace_time_ok Requests) _ (FIFO_trace_T_RC_ok Requests).
+  Admit Obligations.
+
+  (*
   Next Obligation.
-    induction Requests; auto.
-    by apply (FIFO_trace_uniq a) in IHl.
-  Qed.
+    induction Requests.
+    - auto. 
+    - by apply (FIFO_trace_uniq a) in IHl.
+  *)
 
   Lemma FIFO_arbiter_handled req:
-    req \in Requests -> exists cmd : Command_t, cmd \in FIFO_arbitrate.(Commands) ->
-                    Match req cmd.
-  Proof. 
+    req \in Requests -> exists cmd : Command_t, (cmd \in FIFO_arbitrate.(Commands)) /\
+                    ((cmd \in FIFO_arbitrate.(Commands)) -> Match req cmd).
+  Proof.
     intros.
     exists (Cmd_of_req req 5).
+    split.
+    - admit.
+    -
     unfold FIFO_arbitrate in *. simpl in *.
     induction Requests.
     - by rewrite in_nil in H.
diff --git a/coq/Trace.v b/coq/Trace.v
index 2c339933e5417103882193cb9252402729232553..40fa9cddba3ec3751ba286305600f17a4a485f80 100644
--- a/coq/Trace.v
+++ b/coq/Trace.v
@@ -8,17 +8,28 @@ Section Trace.
   Definition Same_Bank (a b : Command_t) :=
     a.(Request).(Bank) == b.(Request).(Bank).
 
+  Definition Same_Bank_3 (a b c : Command_t) :=
+    Same_Bank a b && Same_Bank a c.
+
   Definition ACT_to_ACT (a b : Command_t) :=
     isACT a && isACT b.
 
   Definition PRE_to_ACT (a b : Command_t) :=
     isPRE a && isACT b.
+  
+  Definition PRE_to_PRE (a b : Command_t) :=
+    isPRE a && isPRE b.
 
   Definition Before (a b : Command_t) :=
     a.(CDate) < b.(CDate).
 
   Definition Apart (a b : Command_t) t :=
     a.(CDate) + t < b.(CDate).
+  
+  Definition Between (l : Commands_t) (a b : Command_t) : Commands_t :=
+    [seq cmds <- l | (cmds.(CDate) > a.(CDate)) && (cmds.(CDate) < b.(CDate))].
+  
+  Check Between. 
 
   Record Trace_t := mkTrace
   {
@@ -31,6 +42,11 @@ Section Trace.
     (* All commands have to occur before the current time instant *)
     Cmds_time_ok : forall cmd, cmd \in Commands -> cmd.(CDate) <= Time;
 
+    (* Between any two PREs to the same bank, there has to be an ACT to the same bank in between *)
+    Cmds_PRE_ok : forall a b, a \in Commands -> b \in Commands ->
+                  PRE_to_PRE a b -> Same_Bank a b -> a != b -> 
+                  exists c : Command_t, isACT c /\ Same_Bank a c /\ c \in Between Commands a b;
+
     (* Ensure that the time between two ACT commands respects T_RC *)
     Cmds_T_RC_ok : forall a b, a \in Commands -> b \in Commands ->
                     ACT_to_ACT a b -> Same_Bank a b -> Before a b ->