diff --git a/cs3234/labs/question-for-Yadunand.v b/cs3234/labs/question-for-Yadunand.v
new file mode 100644
index 0000000..e73daa1
--- /dev/null
+++ b/cs3234/labs/question-for-Yadunand.v
@@ -0,0 +1,621 @@
+(* question-for-Yadunand.v *)
+(* CS3234 oral exam *)
+(* Sun 05 May 2024 *)
+
+(* ********** *)
+
+(* Your oral exam is about primitive recursion for Peano numbers. *)
+
+(* ********** *)
+
+Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
+
+Require Import Arith Bool List.
+
+(* ********** *)
+
+(* Reminder:
+   Any function that is expressible as an instance of nat_fold_right is said to be "primitive iterative". *)
+
+Fixpoint nat_fold_right (V : Type) (zero_case : V) (succ_case : V -> V) (n : nat) : V :=
+  match n with
+    O =>
+    zero_case
+  | S n' =>
+    succ_case (nat_fold_right V zero_case succ_case n')
+  end.
+
+(* Definition:
+   Any function that is expressible as an instance of nat_parafold_right is said to be "primitive recursive". *)
+
+Fixpoint nat_parafold_right (V : Type) (zero_case : V) (succ_case : nat -> V -> V) (n : nat) : V := match n with
+    O =>
+    zero_case
+  | S n' =>
+    succ_case n' (nat_parafold_right V zero_case succ_case n')
+  end.
+
+Lemma fold_unfold_nat_parafold_right_O :
+  forall (V : Type)
+         (zero_case : V)
+         (succ_case : nat -> V -> V),
+    nat_parafold_right V zero_case succ_case 0 =
+    zero_case.
+Proof.
+  fold_unfold_tactic nat_parafold_right.
+Qed.
+
+Lemma fold_unfold_nat_parafold_right_S :
+  forall (V : Type)
+         (zero_case : V)
+         (succ_case : nat -> V -> V)
+         (n' : nat),
+    nat_parafold_right V zero_case succ_case (S n') =
+    succ_case n' (nat_parafold_right V zero_case succ_case n').
+Proof.
+  fold_unfold_tactic nat_parafold_right.
+Qed.
+
+(* ***** *)
+
+Fixpoint nat_parafold_left (V : Type) (zero_case : V) (succ_case : nat -> V -> V) (n : nat) : V :=
+  match n with
+    O =>
+    zero_case
+  | S n' =>
+    nat_parafold_left V (succ_case n' zero_case) succ_case n'    
+  end.
+
+Lemma fold_unfold_nat_parafold_left_O :
+  forall (V : Type)
+         (zero_case : V)
+         (succ_case : nat -> V -> V),
+    nat_parafold_left V zero_case succ_case 0 =
+    zero_case.
+Proof.
+  fold_unfold_tactic nat_parafold_left.
+Qed.
+
+Lemma fold_unfold_nat_parafold_left_S :
+  forall (V : Type)
+         (zero_case : V)
+         (succ_case : nat -> V -> V)
+         (n' : nat),
+    nat_parafold_left V zero_case succ_case (S n') =
+    nat_parafold_left V (succ_case n' zero_case) succ_case n'.
+Proof.
+  fold_unfold_tactic nat_parafold_left.
+Qed.
+
+(* ********** *)
+
+Definition test_fac (candidate: nat -> nat) : bool :=
+  (Nat.eqb (candidate 0) 1)
+  &&
+  (Nat.eqb (candidate 5) 120).
+
+(* ***** *)
+
+(* Recursive implementation of the factorial function: *)
+
+Fixpoint r_fac (n : nat) : nat :=
+  match n with
+    O =>
+    1
+  | S n' =>
+    S n' * r_fac n'
+  end.
+
+Compute (test_fac r_fac).
+
+(* 1.a Implement r_fac as an instance of nat_parafold_right: *)
+
+Definition r_fac_right (n : nat) : nat :=
+  nat_parafold_right nat 1 (fun n' ih => (S n') * ih) n.
+
+(* 1.b Test your implementation. *)
+Compute (test_fac r_fac).
+
+(* 1.c Prove that r_fac and r_fac_right are equivalent. *)
+
+Lemma fold_unfold_r_fac_O :
+  r_fac 0 = 1.
+Proof.
+  fold_unfold_tactic r_fac.
+Qed.
+Lemma fold_unfold_r_fac_S :
+  forall (n' : nat),
+    r_fac (S n') = S n' * r_fac n'.
+Proof.
+  fold_unfold_tactic r_fac.
+Qed.
+
+Lemma about_r_fac_and_r_fac_right :
+  forall (n : nat),
+    r_fac n = nat_parafold_right nat 1 (fun n' ih : nat => S n' * ih) n.
+Proof.
+  intro n.
+  induction n as [ | n' IHn' ].
+  - rewrite -> fold_unfold_r_fac_O.
+    rewrite -> fold_unfold_nat_parafold_right_O.
+    reflexivity.
+  - rewrite -> fold_unfold_r_fac_S.
+    rewrite -> fold_unfold_nat_parafold_right_S.
+    rewrite <- IHn'.
+    reflexivity.
+Qed.
+
+Theorem r_fac_and_r_fac_right_are_equivalent :
+  forall (n : nat),
+    r_fac n = r_fac_right n.
+Proof.
+  intro n.
+  unfold r_fac_right.
+  exact (about_r_fac_and_r_fac_right n).
+Qed.
+
+(* ***** *)
+
+(* Tail-recursive implementation of the factorial function: *)
+
+Fixpoint tr_fac_acc (n a : nat) : nat :=
+  match n with
+    O =>
+    a
+  | S n' =>
+    tr_fac_acc n' (S n' * a)
+  end.
+
+Lemma fold_unfold_tr_fac_acc_O :
+  forall (a : nat),
+  tr_fac_acc 0 a = a.
+Proof.
+  fold_unfold_tactic r_fac.
+Qed.
+
+Lemma fold_unfold_tr_fac_acc_S :
+  forall (n' a : nat),
+    tr_fac_acc (S n') a = tr_fac_acc n' (S n' * a).
+Proof.
+  fold_unfold_tactic r_fac.
+Qed.
+
+Definition tr_fac (n : nat) : nat :=
+  tr_fac_acc n 1.
+
+Compute (test_fac tr_fac).
+
+(* 2.a Implement tr_fac as an instance of nat_parafold_left: *)
+
+Definition tr_fac_left (n : nat) : nat :=
+  nat_parafold_left nat 1 (fun n' a => S n' * a) n.
+
+(* 2.b Test your implementation. *)
+
+Compute (test_fac tr_fac_left).
+
+(* 2.c Prove that tr_fac and tr_fac_left are equivalent. *)
+(* Lemma about_tr_fac_acc : *)
+(*   forall (n a : nat), *)
+(*     tr_fac_acc n a = (tr_fac_acc n 1) * a. *)
+(* Proof. *)
+(*   intros n. *)
+(*   induction n as [ | n' IHn' ]. *)
+(*   - intro a. *)
+(*     rewrite -> fold_unfold_tr_fac_acc_O. *)
+(*     rewrite -> fold_unfold_tr_fac_acc_O. *)
+(*     rewrite -> Nat.mul_1_l. *)
+(*     reflexivity. *)
+(*   - intro a. *)
+(*     rewrite -> fold_unfold_tr_fac_acc_S. *)
+(*     rewrite -> (IHn' (S (S n') * a)). *)
+(*     rewrite ->  *)
+
+
+Lemma about_tr_fac_and_tr_fac_left :
+  forall (n : nat),
+    tr_fac_acc n 1 = nat_parafold_left nat 1 (fun n' a : nat => S n' * a) n.
+  Proof.
+    intro n.
+    induction n as [ | n' IHn' ].
+    - rewrite -> fold_unfold_tr_fac_acc_O.
+      rewrite -> fold_unfold_nat_parafold_left_O.
+      reflexivity.
+    - rewrite -> fold_unfold_tr_fac_acc_S.
+      rewrite -> fold_unfold_nat_parafold_left_S.
+      rewrite -> Nat.mul_1_r.
+    Abort.
+
+Lemma about_tr_fac_and_tr_fac_left :
+  forall (n a: nat),
+    tr_fac_acc n a = nat_parafold_left nat a (fun n' a : nat => S n' * a) n.
+Proof.
+  intro n.
+  induction n as [ | n' IHn' ].
+  - intro a.
+    rewrite -> fold_unfold_tr_fac_acc_O.
+    rewrite -> fold_unfold_nat_parafold_left_O.
+    reflexivity.
+  - intro a.
+    rewrite -> fold_unfold_tr_fac_acc_S.
+    rewrite -> fold_unfold_nat_parafold_left_S.
+    exact (IHn' (S n' * a)).
+Qed.
+
+Theorem tr_fac_and_tr_fac_left_are_equivalent :
+  forall (n : nat),
+    tr_fac n = tr_fac_left n.
+Proof.
+  intro n.
+  unfold tr_fac.
+  unfold tr_fac_left.
+  exact (about_tr_fac_and_tr_fac_left n 1).
+Qed.
+
+
+(* ********** *)
+
+Definition test_Sigma (candidate: nat -> (nat -> nat) -> nat) : bool :=
+  (Nat.eqb (candidate 0 (fun n => S (2 * n))) 1)
+  &&
+  (Nat.eqb (candidate 1 (fun n => S (2 * n))) 4)
+  &&
+  (Nat.eqb (candidate 2 (fun n => S (2 * n))) 9)
+  &&
+  (Nat.eqb (candidate 3 (fun n => S (2 * n))) 16).
+
+(* ***** *)
+
+(* Recursive implementation of the summation function: *)
+
+Fixpoint r_Sigma (n : nat) (f : nat -> nat) : nat :=
+  match n with
+    O =>
+    f 0
+  | S n' =>
+    (r_Sigma n' f) + f (S n')
+  end.
+
+Compute (test_Sigma r_Sigma).
+
+(* 3.a Implement r_Sigma as an instance of nat_parafold_right: *)
+
+Definition r_Sigma_right (n : nat) (f : nat -> nat) : nat :=
+  nat_parafold_right
+    nat
+    (f 0)
+    (fun n' ih => (ih + f (S n')))
+    n.
+
+(* 3.b Test your implementation. *)
+
+Compute (test_Sigma r_Sigma_right).
+
+(* 3.c Prove that r_Sigma and r_Sigma_right are equivalent. *)
+
+Lemma fold_unfold_r_Sigma_O :
+  forall (f : nat -> nat),
+    r_Sigma O f = f 0.
+Proof.
+  fold_unfold_tactic r_Sigma.
+Qed.
+Lemma fold_unfold_r_Sigma_S :
+  forall (n' : nat)
+    (f : nat -> nat),
+    r_Sigma (S n') f = (r_Sigma n' f) + f (S n').
+Proof.
+  fold_unfold_tactic r_Sigma.
+Qed.
+
+Lemma about_r_Sigma_and_r_Sigma_right :
+  forall (n : nat)
+    (f : nat -> nat),
+    r_Sigma n f = nat_parafold_right nat (f 0) (fun n' ih : nat => ih + f (S n')) n.
+Proof.
+  intros n f.
+  induction n as [ | n' IHn' ].
+  - rewrite -> fold_unfold_r_Sigma_O.
+    rewrite -> fold_unfold_nat_parafold_right_O.
+    reflexivity.
+  - rewrite -> fold_unfold_r_Sigma_S.
+    rewrite -> fold_unfold_nat_parafold_right_S.
+    rewrite <- IHn'.
+    reflexivity.
+Qed.
+
+Theorem r_Sigma_and_r_Sigma_right_are_equivalent :
+  forall (n : nat)
+    (f : nat -> nat),
+    r_Sigma n f = r_Sigma_right n f.
+Proof.
+  intros n f.
+  unfold r_Sigma_right.
+  exact (about_r_Sigma_and_r_Sigma_right n f).
+Qed.
+
+(* ***** *)
+
+(* Tail-recursive implementation of the summation function: *)
+
+Fixpoint tr_Sigma_acc (n : nat) (f : nat -> nat) (a : nat) : nat :=
+  match n with
+    O =>
+    a
+  | S n' =>
+    tr_Sigma_acc n' f (a + f (S n'))
+  end.
+
+Lemma fold_unfold_tr_Sigma_acc_O :
+  forall (f : nat -> nat)
+    (a : nat),
+    tr_Sigma_acc 0 f a = a.
+Proof.
+  fold_unfold_tactic tr_Sigma_acc.
+Qed.
+Lemma fold_unfold_tr_Sigma_acc_S :
+  forall (n' : nat)
+    (f : nat -> nat)
+    (a : nat),
+    tr_Sigma_acc (S n') f a = tr_Sigma_acc n' f (a + f (S n')).
+Proof.
+  fold_unfold_tactic tr_Sigma_acc.
+Qed.
+
+Definition tr_Sigma (n : nat) (f : nat -> nat) : nat :=
+  tr_Sigma_acc n f (f 0).
+
+Compute (test_Sigma tr_Sigma).
+
+(* 4.a Implement tr_Sigma as an instance of nat_parafold_left: *)
+
+Definition tr_Sigma_left (n : nat) (f : nat -> nat) : nat :=
+  nat_parafold_left nat (f 0) (fun n' a => a + f (S n')) n.
+
+
+(* 4.b Test your implementation. *)
+
+Compute (test_Sigma tr_Sigma_left).
+
+(* 4.c Prove that tr_Sigma and tr_Sigma_left are equivalent. *)
+
+Lemma about_tr_Sigma_and_tr_Sigma_left :
+  forall (n : nat)
+    (f : nat -> nat),
+    tr_Sigma_acc n f (f 0) = nat_parafold_left nat (f 0) (fun n' a : nat => a + f (S n')) n.
+Proof.
+Abort.
+
+Lemma about_tr_Sigma_and_tr_Sigma_left :
+  forall (n: nat)
+    (f : nat -> nat)
+    (a : nat),
+    tr_Sigma_acc n f a = nat_parafold_left nat a (fun n' a : nat => a + f (S n')) n.
+Proof.
+  intros n f.
+  induction n as [ | n' IHn' ].
+  - intros a.
+    rewrite -> (fold_unfold_tr_Sigma_acc_O f a).
+    rewrite -> fold_unfold_nat_parafold_left_O.
+    reflexivity.
+  - intros a.
+    rewrite -> (fold_unfold_tr_Sigma_acc_S n' f a).
+    rewrite -> fold_unfold_nat_parafold_left_S.
+    exact (IHn' (a + f (S n'))).
+Qed.
+
+Theorem tr_Sigma_and_tr_Sigma_left_are_equivalent :
+  forall (n : nat)
+    (f : nat -> nat),
+    tr_Sigma n f = tr_Sigma_left n f.
+Proof.
+  intros n f.
+  unfold tr_Sigma,tr_Sigma_left.
+  exact (about_tr_Sigma_and_tr_Sigma_left n f (f 0)).
+Qed.
+(* ********** *)
+
+(* 5. Taking inspiration from the theorem about folding left and right over lists in the midterm project,
+      state and admit a similar theorem about parafolding left and right over Peano numbers. *)
+
+(* Theorem folding_left_and_right_over_lists : *)
+(*   forall (V W : Type) *)
+(*          (cons_case : V -> W -> W), *)
+(*     is_left_permutative V W cons_case -> *)
+(*     forall (nil_case : W) *)
+(*            (vs : list V), *)
+(*       list_fold_left  V W nil_case cons_case vs = *)
+(*       list_fold_right V W nil_case cons_case vs. *)
+(* Proof. *)
+(*   intros V W cons_case. *)
+(*   unfold is_left_permutative. *)
+(*   intros H_left_permutative nil_case vs. *)
+(*   induction vs as [ | v' vs' IHvs']. *)
+(*   - rewrite -> (fold_unfold_list_fold_left_nil  V W nil_case cons_case). *)
+(*     rewrite -> (fold_unfold_list_fold_right_nil V W nil_case cons_case). *)
+(*     reflexivity. *)
+(*   - rewrite -> (fold_unfold_list_fold_left_cons  V W nil_case cons_case v' vs'). *)
+(*     rewrite -> (fold_unfold_list_fold_right_cons V W nil_case cons_case v' vs'). *)
+(*     rewrite <- IHvs'. *)
+(*     rewrite -> (about_list_fold_left_with_left_permutative_cons_case *)
+(*                  V W cons_case H_left_permutative nil_case v' vs'). *)
+(*     reflexivity. *)
+(* Qed. *)
+(* Definition is_left_permutative (V W : Type) (op2 : V -> W -> W) := *)
+(*   forall (v1 v2 : V) *)
+(*          (w : W), *)
+(*     op2 v1 (op2 v2 w) = op2 v2 (op2 v1 w). *)
+(* ********** *)
+
+Definition is_left_permutative (V : Type) (op2 : nat -> V -> V) :=
+  forall (n1 n2 : nat)
+    (v : V),
+    op2 n1 (op2 n2 v) = op2 n2 (op2 n1 v).
+
+Lemma about_parafolding_l_over_peano_numbers :
+  forall (V: Type)
+    (succ_case : nat -> V -> V),
+    is_left_permutative V succ_case ->
+    forall (n : nat)
+      (zero_case : V),
+  nat_parafold_left V (succ_case n zero_case) succ_case n =
+  succ_case n (nat_parafold_left V zero_case succ_case n).
+Proof.
+  intros V succ_case H_is_left_permutative n.
+  unfold is_left_permutative in H_is_left_permutative.
+  induction n as [| n' IHn'].
+  - intro zero_case.
+    rewrite -> 2 fold_unfold_nat_parafold_left_O.
+    reflexivity.
+  - intro zero_case.
+    rewrite -> fold_unfold_nat_parafold_left_S.
+    rewrite ->H_is_left_permutative.
+    Abort. (* The lemma I stated here is a bit wrong. *)
+
+Lemma about_parafolding_left_over_peano_numbers :
+  forall (V: Type)
+    (succ_case : nat -> V -> V),
+    is_left_permutative V succ_case ->
+    forall (n m : nat)
+      (zero_case : V),
+  nat_parafold_left V (succ_case m zero_case) succ_case n =
+  succ_case m (nat_parafold_left V zero_case succ_case n).
+Proof.
+  intros V succ_case H_is_left_permutative n m.
+  unfold is_left_permutative in H_is_left_permutative.
+  induction n as [| n' IHn'].
+  - intros zero_case.
+    rewrite -> 2 fold_unfold_nat_parafold_left_O.
+    reflexivity.
+  - intros zero_case.
+    rewrite -> fold_unfold_nat_parafold_left_S.
+    rewrite -> H_is_left_permutative.
+    rewrite -> (IHn' (succ_case n' zero_case)).
+    rewrite -> fold_unfold_nat_parafold_left_S.
+    reflexivity.
+Qed.
+
+Lemma about_parafolding_right_over_peano_numbers :
+  forall (V : Type)
+    (succ_case : nat -> V -> V),
+    is_left_permutative V succ_case ->
+    forall (n m : nat)
+      (zero_case : V),
+      nat_parafold_right V (succ_case m zero_case) succ_case n =
+        succ_case m (nat_parafold_right V zero_case succ_case n).
+Proof.
+  intros V succ_case H_left_permutative n m zero_case.
+  unfold is_left_permutative in H_left_permutative.
+  induction n as [ | n' IHn' ].
+  - rewrite -> 2 fold_unfold_nat_parafold_right_O.
+    reflexivity.
+  - rewrite -> 2 fold_unfold_nat_parafold_right_S.
+    rewrite -> H_left_permutative.
+    rewrite -> IHn'.
+    reflexivity.
+Qed.
+Theorem parafolding_left_and_right_over_peano_numbers :
+  forall (V : Type)
+    (succ_case : nat -> V -> V),
+    is_left_permutative V succ_case ->
+    forall (n : nat)
+      (zero_case : V),
+      nat_parafold_left V zero_case succ_case n = nat_parafold_right V zero_case succ_case n.
+Proof.
+  intros V succ_case H_left_permutative n zero_case.
+  (* Generalizing the accumulator(?) *)
+  induction n as [ | n' IHn' ].
+  - rewrite -> fold_unfold_nat_parafold_left_O.
+    rewrite -> fold_unfold_nat_parafold_right_O.
+    reflexivity.
+  - rewrite -> fold_unfold_nat_parafold_left_S.
+    rewrite -> fold_unfold_nat_parafold_right_S.
+    rewrite <- IHn'.
+    Check (about_parafolding_left_over_peano_numbers V succ_case H_left_permutative n' n' zero_case).
+    exact (about_parafolding_left_over_peano_numbers V succ_case H_left_permutative n' n' zero_case).
+    Restart.
+    intros V succ_case H_left_permutative n.
+    (* Generalizing the accumulator(?) *)
+    induction n as [ | n' IHn' ].
+  - intro zero_case.
+    rewrite -> fold_unfold_nat_parafold_left_O.
+    rewrite -> fold_unfold_nat_parafold_right_O.
+    reflexivity.
+  - intro zero_case.
+    rewrite -> fold_unfold_nat_parafold_right_S.
+    rewrite -> fold_unfold_nat_parafold_left_S.
+    rewrite -> (IHn' (succ_case n' zero_case)).
+    exact (about_parafolding_right_over_peano_numbers
+             V
+             succ_case
+             H_left_permutative
+             n'
+             n'
+             zero_case
+          ).
+Qed.
+
+(* 6. As a corollary of your similar theorem,
+      prove that tr_fac_left and r_fac_right are equivalent
+      and that tr_Sigma_left and r_Sigma_right are equivalent. *)
+
+Lemma succ_case_of_fac_is_left_permutative :
+  is_left_permutative nat (fun n' a : nat => S n' * a).
+Proof.
+  unfold is_left_permutative.
+  intros n1 n2 v.
+  rewrite -> Nat.mul_shuffle3.
+  reflexivity.
+Qed.
+
+Corollary tr_fac_left_and_r_fac_right_are_equivalent :
+  forall (n : nat),
+    tr_fac_left n = r_fac_right n.
+Proof.
+  intros n.
+  unfold tr_fac_left.
+  unfold r_fac_right.
+  exact (parafolding_left_and_right_over_peano_numbers
+           nat
+           (fun n' a : nat => S n' * a)
+           succ_case_of_fac_is_left_permutative
+           n
+           1
+        ).
+Qed.
+
+Lemma succ_case_of_Sigma_is_left_permutative :
+  forall (f : nat -> nat),
+    is_left_permutative nat (fun n' a : nat => a + f (S n')).
+Proof.
+  intro f.
+  unfold is_left_permutative.
+  intros n1 n2 v.
+  Search (_ + _ + _).
+  rewrite -> Nat.add_shuffle0.
+  reflexivity.
+Qed.
+
+Corollary tr_Sigma_left_and_r_Sigma_right_are_equivalent :
+  forall (n : nat)
+    (f : nat -> nat),
+
+    tr_Sigma_left n f = r_Sigma_right n f.
+Proof.
+  intros n f.
+  unfold tr_Sigma_left.
+  unfold r_Sigma_right.
+  exact (parafolding_left_and_right_over_peano_numbers
+           nat
+           (fun n' a : nat => a + f (S n'))
+           (succ_case_of_Sigma_is_left_permutative f)
+           n
+           (f 0)
+        ).
+Qed.
+(* ********** *)
+
+(* 7. Prove your similar theorem. *)
+
+(* ********** *)
+
+(* end of question-for-Yadunand.v *)
diff --git a/cs3234/labs/term-project.v b/cs3234/labs/term-project.v
index 3ccaa4d..ac990ff 100644
--- a/cs3234/labs/term-project.v
+++ b/cs3234/labs/term-project.v
@@ -1536,9 +1536,41 @@ Proof.
       rewrite -> (S_run_one bcis n H_fdel_one).
       reflexivity. }
     split.
-    { intros n n' H_fdel_many.
-      rewrite -> (S_run_many bcis n n' H_fdel_many).
+    { intros n n' ds'' H_fdel_many.
+      rewrite -> (S_run_many bcis n n' ds'' H_fdel_many ).
       reflexivity. }
+    intros s H_fdel_KO.
+    rewrite -> (S_run_KO bcis s H_fdel_KO).
+    reflexivity.
+  - intro S_run.
+    assert (S_run := S_run fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification).
+    intros fdel S_fdel.
     split.
+    { intros bcis H_fdel_nil.
+      rewrite -> (there_is_at_most_one_fetch_decode_execute_loop fdel fetch_decode_execute_loop S_fdel fetch_decode_execute_loop_satifies_the_specification bcis) in H_fdel_nil.
+      destruct (S_run bcis) as [S_run_nil _].
+      rewrite -> (S_run_nil H_fdel_nil).
+      reflexivity.
+    }
+    split.
+    { intros bcis n H_fdel_one.
+      rewrite -> (there_is_at_most_one_fetch_decode_execute_loop fdel fetch_decode_execute_loop S_fdel fetch_decode_execute_loop_satifies_the_specification bcis) in H_fdel_one.
+      destruct (S_run bcis) as [_ [S_run_one _]].
+      rewrite -> (S_run_one n H_fdel_one).
+      reflexivity.
+    }
+    split.
+    { intros bcis n n' ds'' H_fdel_many.
+      rewrite -> (there_is_at_most_one_fetch_decode_execute_loop fdel fetch_decode_execute_loop S_fdel fetch_decode_execute_loop_satifies_the_specification bcis) in H_fdel_many.
+      destruct (S_run bcis) as [_ [_ [S_run_many _]]].
+      rewrite -> (S_run_many n n' ds'' H_fdel_many).
+      reflexivity.
+    }
+    intros bcis s H_fdel_KO.
+    rewrite -> (there_is_at_most_one_fetch_decode_execute_loop fdel fetch_decode_execute_loop S_fdel fetch_decode_execute_loop_satifies_the_specification bcis) in H_fdel_KO.
+    destruct (S_run bcis) as [_ [_ [_ S_run_KO]]].
+    rewrite -> (S_run_KO s H_fdel_KO).
+    reflexivity.
+Qed.
 
 (* end of term-project.v *)