diff --git a/theories/PostsProblem/limit_computability.v b/theories/PostsProblem/limit_computability.v
new file mode 100644
index 0000000..7b8313c
--- /dev/null
+++ b/theories/PostsProblem/limit_computability.v
@@ -0,0 +1,399 @@
+From SyntheticComputability Require Import ArithmeticalHierarchySemantic PostsTheorem reductions SemiDec TuringJump OracleComputability Definitions partial Pigeonhole.
+
+Require Import stdpp.list Vectors.VectorDef Arith.Compare_dec Lia.
+Import Vector.VectorNotations.
+
+Local Notation vec := Vector.t.
+
+
+(* ########################################################################## *)
+(** * Limit Computability *)
+(* ########################################################################## *)
+
+(** This file contains the definition of limit computable and proves the
+Limit Lemma, i.e., limit computable is equivalence to reduciable to halting
+problem.
+
+Convention:
+
+   limit: limit computable
+   semi_dec(_K): semi decidable (on K)
+   turing_red_K: turing reduciable to halting problem
+   char[_X]: extensionality of X
+
+ **)
+
+  (* Definition of limit ciomputable *)
+
+  Definition limit_computable {X} (P: X → Prop) :=
+    ∃ f: X → nat → bool, ∀ x,
+      (P x ↔ ∃ N, ∀ n, n ≥ N → f x n = true) ∧
+        (¬ P x ↔ ∃ N, ∀ n, n ≥ N → f x n = false).
+
+  Definition char_rel_limit_computable {X} (P: X → bool → Prop) :=
+    ∃ f: X → nat → bool, ∀ x y, P x y ↔ ∃ N, ∀ n, n ≥ N → f x n = y.
+
+  Definition char_rel_limit_computable' {X} (P: X → bool → Prop) :=
+    ∃ f: X → nat → bool, ∀ x y, P x y → ∃ N, ∀ n, n ≥ N → f x n = y.    
+
+  Lemma char_rel_limit_equiv {X} (P: X → Prop):
+    char_rel_limit_computable (char_rel P) ↔ limit_computable P.
+  Proof.
+    split; intros [f Hf]; exists f; intros x.
+    - split; firstorder.
+    - intros []; destruct (Hf x) as [h1 h2]; eauto.
+  Qed.
+
+  Lemma char_rel_limit_equiv' {X} (P: X → Prop):
+    definite P → char_rel_limit_computable (char_rel P) ↔ char_rel_limit_computable' (char_rel P) .
+  Proof.
+    intros HP; split.
+    - intros [f Hf]. exists f; intros.
+      destruct (Hf x y) as [Hf' _].
+      now apply Hf'.
+    - intros [f Hf]. exists f. intros x y.
+      split. intro H. now apply Hf.
+      intros [N HN]. destruct (HP x).
+      destruct y; [easy|].
+      destruct (Hf x true H) as [N' HfN].
+      intros _. enough (true = false) by congruence.
+      specialize (HN (max N N')).
+      specialize (HfN (max N N')).
+      rewrite <- HN, <- HfN; eauto; lia.
+      destruct y; [|easy].
+      destruct (Hf x false H) as [N' HfN]. 
+      enough (true = false) by congruence.
+      specialize (HN (max N N')).
+      specialize (HfN (max N N')).
+      rewrite <- HN, <- HfN; eauto; lia.
+  Qed.
+  
+
+  (* Naming the halting problem as K *)
+  Notation K := (­{0}^(1)).
+
+
+Section LimitLemma1.
+  (* Limit computable predicate P is reduciable to K *)
+
+  Variable vec_to_nat : ∀ k, vec nat k → nat.
+  Variable nat_to_vec : ∀ k, nat → vec nat k.
+  Variable vec_nat_inv : ∀ k v, nat_to_vec k (vec_to_nat v) = v.
+  Variable nat_vec_inv : ∀ k n, vec_to_nat (nat_to_vec k n) = n.
+
+  Variable list_vec_to_nat : ∀ k, list (vec nat k) → nat.
+  Variable nat_to_list_vec : ∀ k, nat → list (vec nat k).
+  Variable list_vec_nat_inv : ∀ k v, nat_to_list_vec k (list_vec_to_nat v) = v.
+  Variable nat_list_vec_inv : ∀ k n, list_vec_to_nat (nat_to_list_vec k n) = n.
+
+  Variable nat_to_list_bool : nat → list bool.
+  Variable list_bool_to_nat : list bool → nat.
+  Variable list_bool_nat_inv : ∀ l, nat_to_list_bool (list_bool_to_nat l) = l.
+  Variable nat_list_bool_inv : ∀ n, list_bool_to_nat (nat_to_list_bool n) = n.
+
+
+  Section def_K.
+
+    Hypothesis LEM_Σ_1: LEM_Σ 1.
+
+    Lemma semi_dec_def {X} (p: X → Prop):
+      semi_decidable p → definite p.
+    Proof.
+      intros [f Hf]. unfold semi_decider in Hf.
+      destruct level1 as (_&H2&_).
+      assert principles.LPO as H by now rewrite <- H2.
+      intro x. destruct (H (f x)).
+      left. now rewrite Hf.
+      right. intros [k Hk]%Hf.
+      apply H0. now exists k.
+    Qed.
+
+    Lemma def_K: definite K.
+    Proof.
+      apply semi_dec_def. 
+      assert (isΣsem 1 (@jumpNK _ 1 1)).
+      eapply jump_in_Σn; eauto.
+      assert (@jumpNK _ 1 1 ≡ₘ ­{0}^(1)).
+      apply jumpNKspec.
+      rewrite <- semi_dec_iff_Σ1 in H.
+      destruct H0 as [_ [f Hf]].
+      unfold reduces_m in Hf.
+      destruct H as [g Hg].
+      unfold semi_decider in Hg.
+      exists (fun x => g (f x)).
+      split. now intros H%Hf%Hg. now intros H%Hg%Hf.
+    Qed.
+
+  End def_K.
+
+  (* Extensionality of Σ2, i.e. P t iff ∃ x. ∀ y. f(x, y, t) = true *)
+
+  Lemma char_Σ2 {k: nat} (P: vec nat k → Prop) :
+    (∃ f: nat → nat → vec nat k → bool, ∀ x, P x ↔ (∃ n, ∀ m, f n m x = true)) →
+    isΣsem 2 P.
+  Proof.
+    intros [f H].
+    eapply isΣsemS_ with (p := fun v => ∀ y, f (hd v) y (tl v) = true).
+    eapply isΠsemS_ with (p := fun v => f (hd (tl v)) (hd v) (tl (tl v)) = true).
+    eapply isΣsem0. all: easy.
+  Qed.
+
+  Lemma limit_Σ2 {k: nat} (P: vec nat k → Prop) :
+    limit_computable P → isΣsem 2 P ∧ isΣsem 2 (compl P).
+  Proof.
+    intros [f H]; split; eapply char_Σ2.
+    - exists (fun N n x => if lt_dec n N then true else f x n).
+      intro w. destruct (H w) as [-> _]; split; intros [N Hn]; exists N.
+      + intro m. destruct (lt_dec m N); try apply Hn; lia.
+      + intros n He. specialize (Hn n); destruct (lt_dec n N); auto; lia.
+    - exists (fun N n x => if lt_dec n N then true else negb (f x n)).
+      intro w. destruct (H w) as [_ ->]; split; intros [N Hn]; exists N.
+      + intro m. destruct (lt_dec m N); [auto| rewrite (Hn m); lia].
+      + intros n He. specialize (Hn n).
+        destruct (lt_dec n N); auto; [lia|destruct (f w n); easy].
+  Qed.
+
+  Lemma limit_semi_dec_K {k: nat} (P: vec nat k → Prop) :
+    LEM_Σ 1 →
+    limit_computable P →
+    OracleSemiDecidable K P ∧
+    OracleSemiDecidable K (compl P).
+  Proof.
+    intros LEM H%limit_Σ2.
+    rewrite <- !(Σ_semi_decidable_jump).
+    all: eauto.
+  Qed.
+
+  Lemma limit_turing_red_K' {k: nat} (P: vec nat k → Prop) :
+    LEM_Σ 1 →
+    definite K →
+    limit_computable P →
+    P ⪯ᴛ K.
+  Proof.
+    intros LEM D H % (limit_semi_dec_K LEM); destruct H as [h1 h2].
+    apply PT; try assumption.
+    apply Dec.nat_eq_dec.
+  Qed.
+
+  Fact elim_vec (P: nat → Prop):
+    P ⪯ₘ (fun x: vec nat 1 => P (hd x)) .
+  Proof. exists (fun x => [x]). now intros x. Qed.
+
+    (** ** The Limit Lemma 1 *)
+  
+  Lemma limit_turing_red_K {k: nat} (P: nat → Prop) :
+    LEM_Σ 1 →
+    limit_computable P →
+    P ⪯ᴛ K.
+  Proof.
+    intros Hc [h Hh].
+    specialize (def_K Hc) as Hk.
+    eapply Turing_transitive; last eapply (@limit_turing_red_K' 1); eauto.
+    eapply red_m_impl_red_T. apply elim_vec.
+    exists (fun v n => h (hd v) n).
+    intros x; split; 
+    destruct (Hh (hd x)) as [Hh1 Hh2]; eauto.
+  Qed.
+
+End LimitLemma1.
+
+Section Σ1Approximation.
+
+  (* Turing jump of a trivial decidable problem is semi decidable *)
+
+  Lemma semi_dec_halting : semi_decidable K.
+  Proof.
+    eapply OracleSemiDecidable_semi_decidable with (q := ­{0}).
+    - exists (λ n, match n with | O => true | _ => false end); intros [|n]; easy.
+    - eapply semidecidable_J.
+  Qed.
+
+
+  (* Stabilizing the semi decider allows the semi decider
+     to be used as a Σ1 approximation *)
+
+  Definition stable (f: nat → bool) := ∀ n m, n ≤ m → f n = true → f m = true.
+
+  Fixpoint stabilize_step {X} (f: X → nat → bool) x n :=
+    match n with
+    | O => false
+    | S n => if f x n then true else stabilize_step f x n
+    end.
+
+  Lemma stabilize {X} (P: X → Prop) :
+    semi_decidable P → ∃ f, semi_decider f P ∧ ∀ x, stable (f x).
+  Proof.
+    intros [f Hf].
+    exists (fun x n => stabilize_step f x n); split.
+    - intro x; split; intro h.
+      rewrite (Hf x) in h.
+      destruct h as [c Hc].
+      now exists (S c); cbn; rewrite Hc.
+      rewrite (Hf x).
+      destruct h as [c Hc].
+      induction c; cbn in Hc; [congruence|].
+      destruct (f x c) eqn: E; [now exists c|now apply IHc].
+    - intros x n m Lenm Hn.
+      induction Lenm; [trivial|].
+      cbn; destruct (f x m) eqn: E; [trivial|assumption].
+  Qed.
+
+  (* The Σ1 approximation output correct answers for arbitray list of questions *)
+  Definition approximation_list {A} (P: A → Prop) (f: A → bool) L :=
+    ∀ i, List.In i L → P i ↔ f i = true.
+
+  Definition approximation_Σ1 {A} (P: A → Prop) :=
+    ∃ P_ : nat → A → bool,
+    ∀ L, ∃ c, ∀ c', c' ≥ c → approximation_list P (P_ c') L.
+
+  Definition approximation_Σ1_strong {A} (P: A → Prop) :=
+     ∃ P_ : nat → A → bool,
+       (∀ L, ∃ c, ∀ c', c' ≥ c → approximation_list P (P_ c') L) ∧
+       (∀ tau q a, @interrogation _ _ _ bool tau (char_rel P) q a → ∃ n, ∀ m, m ≥ n → interrogation tau (fun q a => P_ m q = a) q a).
+
+  Definition approximation_Σ1_weak {A} (P: A → Prop) :=
+    ∃ P_ : nat → A → bool,
+      (∀ tau q a, @interrogation _ _ _ bool tau (char_rel P) q a → ∃ n, ∀ m, m ≥ n → interrogation tau (λ q a, P_ m q = a) q a).
+
+  Lemma semi_dec_approximation_Σ1 {X} (P: X → Prop) :
+    definite P →
+    semi_decidable P → approximation_Σ1 P.
+  Proof.
+    intros defP semiP; unfold approximation_Σ1, approximation_list.
+    destruct (stabilize semiP)  as [h [Hh HS]].
+    exists (fun n x => h x n). intro l. induction l as [|a l [c Hc]].
+    - exists 42; eauto.
+    - destruct (defP a) as [h1| h2].
+      + destruct (Hh a) as [H _].
+        destruct (H h1) as [N HN].
+        exists (max c N); intros c' Hc' e [->| He].
+        split; [intros _|easy].
+        eapply HS; [|eapply HN]; lia.
+        rewrite <- (Hc c'); [trivial|lia | assumption].
+      + exists c; intros c' Hc' e [->| He].
+        split; [easy| intros h'].
+        unfold semi_decider in Hh.
+        now rewrite Hh; exists c'.
+        rewrite Hc; eauto.
+  Qed.
+
+  Lemma semi_dec_approximation_Σ1_strong {X} (P: X → Prop) :
+    definite P →
+    semi_decidable P → approximation_Σ1_strong P.
+  Proof.
+    intros defP semiP.
+    destruct (semi_dec_approximation_Σ1 defP semiP) as [P_ HP_].
+    exists P_; split; [apply HP_|].
+    intros tau q ans Htau.
+    destruct (HP_ q) as [w Hw].
+    exists w. intros m Hm. rewrite interrogation_ext.
+    exact Htau. eauto.
+    intros q_ a H1.
+    specialize (Hw m Hm q_ H1).
+    unfold char_rel; cbn.
+    destruct a; eauto; split; intro h2.
+    intro h. rewrite Hw in h. congruence.
+    firstorder.
+  Qed.
+
+  Lemma approximation_Σ1_halting : definite K → approximation_Σ1 K.
+  Proof. now intros H; apply semi_dec_approximation_Σ1, semi_dec_halting. Qed.
+
+  Lemma approximation_Σ1_halting_strong: definite K → approximation_Σ1_strong K.
+  Proof. now intros H; apply semi_dec_approximation_Σ1_strong, semi_dec_halting. Qed.
+
+
+End Σ1Approximation.
+
+
+Section LimitLemma2.
+
+  (* A predicate P is reduciable to K if P is limit computable *)
+
+  Section Construction.
+
+    Variable f : nat → nat → bool.
+    Variable tau : nat → tree nat bool bool.
+    Hypothesis Hf: ∀ L, ∃ c, ∀ c', c' ≥ c → approximation_list K (f c') L.
+
+    Definition K_ n := fun i o => f n i = o.
+    Definition char_K_ n := fun i => ret (f n i).
+
+    Lemma dec_K_ n : decidable (λ i, f n i = true).
+    Proof.
+      exists (f n). easy.
+    Qed.
+
+    Lemma pcomputes_K_ n: pcomputes (char_K_ n) (λ i o, f n i = o).
+    Proof.
+      intros i o; split; intro H.
+      now apply ret_hasvalue_inv.
+      now apply ret_hasvalue'.
+    Qed.
+
+  End Construction.
+
+    (** ** The Limit Lemma 2 *)
+
+  Theorem turing_red_K_lim (P: nat → Prop) :
+    P ⪯ᴛ K →
+    definite K →
+    definite P →
+    limit_computable P.
+  Proof.
+    intros [F [H HF]] defK defP.
+    rewrite <- char_rel_limit_equiv.
+    destruct (approximation_Σ1_halting_strong defK) as [k_ [_ Hk_2]].
+    destruct H as [tau Htau].
+    pose (char_K_ n := char_K_ k_ n).
+    pose (K_ n := K_ k_ n).
+    pose (Phi x n := evalt_comp (tau x) (k_ n) n n).
+    assert (∀ x y, char_rel P x y → ∃ N : nat, ∀ n : nat, n ≥ N → (evalt_comp (tau x) (k_ n)) n n = Some (inr y)) as HL.
+    {
+    intros x y H.
+    rewrite HF in H.
+    rewrite Htau in H.
+    destruct H as (qs & ans & Hint & Out).
+    specialize (Hk_2 (tau x) qs ans Hint).
+    destruct Hk_2 as [nth Hnth].
+    assert (interrogation (tau x)
+              (fun (q : nat) (a : bool) => (k_ nth) q = a) qs ans) as Hnthbase.
+    eapply Hnth. lia.
+    edestruct (interrogation_evalt_comp_limit (tau x) k_ qs ans y) as [L Hlimt].
+    exists nth. intros. eapply Hnth. easy.
+    eapply Out.
+    exists L. intros. now apply Hlimt.
+    }
+    assert (∃ f, ∀ x y, char_rel P x y → ∃ N : nat, ∀ n : nat, n ≥ N → f x n = y) as [f HL'].
+    {
+      exists (λ x n, match (Phi x n) with
+               | Some (inr y) => y | _ => false end).
+    intros x y Hxy%HL.
+    destruct (Hxy) as [N HN].
+    exists N; intros.
+    unfold Phi. rewrite HN; eauto.
+    }
+    exists f. intros x y; split.
+    - now intros; apply HL'.
+    - intro H0. destruct y; cbn.
+      destruct (defP x); [easy|].
+      assert (char_rel P x false); [easy|].
+      apply HL' in H1.
+      destruct H0 as [N1 HN1].
+      destruct H1 as [N2 HN2].
+      specialize (HN1 (S (max N1 N2))).
+      specialize (HN2 (S (max N1 N2))).
+      enough (true = false) by congruence.
+      rewrite <- HN1, HN2; lia.
+      destruct (defP x); [|easy].
+      assert (char_rel P x true); [easy|].
+      apply HL' in H1.
+      destruct H0 as [N1 HN1].
+      destruct H1 as [N2 HN2].
+      specialize (HN1 (S (max N1 N2))).
+      specialize (HN2 (S (max N1 N2))).
+      enough (true = false) by congruence.
+      rewrite <- HN2, HN1; lia.
+  Qed.
+
+End LimitLemma2.
diff --git a/theories/PostsProblem/low_simple_predicates.v b/theories/PostsProblem/low_simple_predicates.v
new file mode 100644
index 0000000..4c40409
--- /dev/null
+++ b/theories/PostsProblem/low_simple_predicates.v
@@ -0,0 +1,196 @@
+From SyntheticComputability Require Import ArithmeticalHierarchySemantic reductions SemiDec TuringJump OracleComputability Definitions limit_computability simple.
+Require Import SyntheticComputability.Synthetic.DecidabilityFacts.
+Require Export SyntheticComputability.Shared.FinitenessFacts.
+Require Export SyntheticComputability.Shared.Pigeonhole.
+Require Export SyntheticComputability.Shared.ListAutomation.
+From SyntheticComputability Require Export lowness.
+From SyntheticComputability Require Export simpleness.
+Require Import Arith.
+Require Import SyntheticComputability.PostsTheorem.PostsTheorem.
+Require Import Vectors.VectorDef Arith.Compare_dec Lia.
+Import Vector.VectorNotations.
+Require Import stdpp.list.
+
+Local Notation vec := Vector.t.
+
+(* ########################################################################## *)
+(** * Low Simple Predicates *)
+(* ########################################################################## *)
+
+(** This file contains the definition of low simple set and proves the
+essential property of low simple, i.e. Low simple as a solution to
+Post's Problem in Turing degree. **)
+
+Section Facts.
+  Lemma m_red_complete {X Y} (P: X → Prop) (Q: Y → Prop):
+    semi_decidable P → Q ⪯ₘ P → semi_decidable Q.
+  Proof. intros [g H1] [f H2]; exists (fun x => g (f x)); firstorder. Qed.
+
+  Lemma m_red_complete_definite {X Y} (P: X → Prop) (Q: Y → Prop):
+    definite P → Q ⪯ₘ P → definite Q.
+  Proof. intros H [f H2]; firstorder. Qed.
+End Facts.
+
+
+
+  (* Definition of low *)
+  Definition low (P: nat → Prop) := P´ ⪯ᴛ K.
+
+Section LowFacts.
+ 
+  Variable vec_to_nat : ∀ k, vec nat k → nat.
+  Variable nat_to_vec : ∀ k, nat → vec nat k.
+  Variable vec_nat_inv : ∀ k v, nat_to_vec k (vec_to_nat v) = v.
+  Variable nat_vec_inv : ∀ k n, vec_to_nat (nat_to_vec k n) = n.
+
+  Variable list_vec_to_nat : ∀ k, list (vec nat k) → nat.
+  Variable nat_to_list_vec : ∀ k, nat → list (vec nat k).
+  Variable list_vec_nat_inv : ∀ k v, nat_to_list_vec k (list_vec_to_nat v) = v.
+  Variable nat_list_vec_inv : ∀ k n, list_vec_to_nat (nat_to_list_vec k n) = n.
+
+  Variable nat_to_list_bool : nat → list bool.
+  Variable list_bool_to_nat : list bool → nat.
+  Variable list_bool_nat_inv : ∀ l, nat_to_list_bool (list_bool_to_nat l) = l.
+  Variable nat_list_bool_inv : ∀ n, list_bool_to_nat (nat_to_list_bool n) = n.
+
+  Lemma lowness (P: nat → Prop) :
+    low P → ¬ K ⪯ᴛ P.
+  Proof.
+    intros H IH.
+    eapply not_turing_red_J with (Q := P).
+    eapply Turing_transitive; [apply H| easy].
+  Qed.
+
+  Lemma DN_lowness (P: nat → Prop) :
+    ¬¬ low P → ¬ K ⪯ᴛ P.
+  Proof.
+    intros H_ IH.
+    apply H_. intros H.
+    eapply not_turing_red_J with (Q := P).
+    eapply Turing_transitive; [apply H| easy].
+  Qed.
+
+  Lemma limit_jump_lowness (A: nat → Prop) :
+    LEM_Σ 1 →
+    definite K →
+    limit_computable (A´) → ¬ K ⪯ᴛ A.
+  Proof.
+    intros LEM defK H IH.
+    apply lowness with (P := A); [|apply IH].
+    eapply limit_turing_red_K; eauto. exact 42. 
+  Qed.
+
+  Definition low_simple P := low P ∧ simple P.
+
+  Definition sol_Post's_problem (P: nat → Prop) :=
+    (¬ decidable P) ∧ (enumerable P) ∧ ¬ (K ⪯ᴛ P).
+
+  Fact low_simple_correct:
+    ∀ P, low_simple P → sol_Post's_problem P.
+  Proof.
+    intros P [H1 H2]; split; [now apply simple_undecidable|].
+    split; [destruct H2 as [H2 _]; eauto| now apply lowness].
+  Qed.
+
+
+
+    (*** Instance of low simple predicate ***)
+
+  Section LowSimplePredicate.
+
+  Variable η: nat → nat → option nat.
+  Hypothesis EA: 
+  ∀ P, semi_decidable P → exists e, ∀ x, P x ↔ ∃ n, η e n = Some x.
+
+  Hypothesis LEM_Σ_1: LEM_Σ 1.
+  Hypothesis def_K: definite K.
+
+  Theorem a_sol_Post's_problem: ∃ P, sol_Post's_problem P.
+  Proof.
+    eexists. eapply low_simple_correct; split.
+    - eapply limit_turing_red_K; eauto. exact 42.
+      apply jump_P_limit; eauto.  
+    - eapply P_simple.
+      intros. intros d. apply d.
+      apply wall_convergence. by unfold wall. 
+      assumption.
+  Qed.
+
+  End LowSimplePredicate.
+
+  Notation "(¬¬Σ⁰₁)-LEM" := 
+      ((∀ (k : nat) (p : vec nat k → Prop), isΣsem 1 p → ¬¬ definite p)) (at level 0).
+
+  Lemma m_red_K_semi_decidable {n} (P: vec nat n → Prop):
+    semi_decidable P → P ⪯ₘ K.
+  Proof.
+    intros H. unfold K. rewrite <- red_m_iff_semidec_jump_vec.
+    by apply semi_decidable_OracleSemiDecidable. eauto.
+  Qed.
+
+  Theorem PostProblem_from_neg_negLPO :
+    ∃ p: nat → Prop, ¬ decidable p ∧ semi_decidable p ∧ (¬¬ (¬¬Σ⁰₁)-LEM → ¬ K ⪯ᴛ p).
+  Proof.
+    exists (P wall).
+    repeat split.
+    - apply simple_undecidable. 
+      eapply P_simple. intro e.
+      unfold lim_to. cbn.
+      apply wall_convergence_classically.
+      by unfold wall.
+    - apply P_semi_decidable.
+    - intros L. intros G. apply L. clear L. intros L.
+      assert (~~ definite K) as hK.
+      {
+        specialize (L 1 (fun v => K (Vector.hd v))).
+        intros h. apply L. 
+        rewrite <- semi_dec_iff_Σ1.
+        eapply m_red_complete; first apply semi_dec_halting.
+        exists (fun v => Vector.hd v); done.
+        intros h1. apply h.
+        intros x. specialize (h1 (Vector.cons x Vector.nil)). exact h1.
+      }
+      apply hK. clear hK. intros hK.
+      assert (LEM_Σ 1).
+      {
+        intros n p Hs.
+        eapply m_red_complete_definite; first apply hK.
+        rewrite <- semi_dec_iff_Σ1 in Hs.
+        by eapply m_red_K_semi_decidable.
+      }
+      revert G. apply lowness. red.
+      eapply limit_turing_red_K; eauto. exact 42.
+      apply jump_P_limit; eauto.
+  Qed.
+
+End LowFacts.
+
+Check PostProblem_from_neg_negLPO.
+Print Assumptions PostProblem_from_neg_negLPO.
+
+(* general proof that (¬¬Σ⁰₁)-LEM <-> ¬¬(Σ⁰₁)-LEM under many-one complete Σ⁰₁ predicate  *)
+Section assume.
+
+  Variable enumerable : (nat → Prop) → Prop.
+
+  Variable K : nat → Prop.
+  Variable eK : enumerable K.
+  Variable cK : ∀ p : nat → Prop, enumerable p → red_m p K.
+
+  Goal
+      ¬¬ (∀ p : nat → Prop, enumerable p → ∀ x, p x ∨ ¬ p x)
+      ↔
+      (∀ p : nat → Prop, enumerable p → ¬¬ ∀ x, p x ∨ ¬ p x).
+  Proof.
+    split.
+    - firstorder.
+    - intros nnLPO H.
+      apply (nnLPO K eK). intros dK.
+      apply H.
+      intros p [f Hf] % cK x.
+      specialize (dK (f x)).
+      red in Hf. rewrite <- Hf in dK.
+      assumption.
+  Qed.
+
+End assume.
diff --git a/theories/PostsProblem/lowness.v b/theories/PostsProblem/lowness.v
new file mode 100644
index 0000000..76e18eb
--- /dev/null
+++ b/theories/PostsProblem/lowness.v
@@ -0,0 +1,301 @@
+From SyntheticComputability Require Import ArithmeticalHierarchySemantic reductions SemiDec TuringJump OracleComputability Definitions step_indexing limit_computability simple.
+Require Import SyntheticComputability.Synthetic.DecidabilityFacts.
+Require Export SyntheticComputability.Shared.FinitenessFacts.
+Require Export SyntheticComputability.Shared.Pigeonhole.
+Require Export SyntheticComputability.Shared.ListAutomation.
+Require Import Arith Arith.Compare_dec Lia Coq.Program.Equality List.
+From SyntheticComputability Require Import the_priority_method.
+From SyntheticComputability Require Import simpleness.
+
+Definition inf_exists (P: nat → Prop) := ∀ n, ∃ m, n ≤ m ∧ P m.
+
+Global Instance dec_le: ∀ m n, dec (m ≤ n).
+  Proof. intros n m; destruct (le_gt_dec n m); [by left|right; lia]. Qed.
+
+Notation "'∞∃' x .. y , p" :=
+  (inf_exists (λ x, .. (inf_exists (λ y, p)) ..))
+      (at level 200, x binder, right associativity,
+      format "'[' '∞∃'  '/  ' x  ..  y ,  '/  ' p ']'")
+  : type_scope.
+
+Notation "f ↓" := (f = Some ()) (at level 30).
+
+Section Requirements_Verification.
+
+  Variable P: nat → Prop.
+  Variable f: nat → nat → bool.
+  Hypothesis S_P: stable_semi_decider P f.
+
+  Definition Φ_ := (Φ_ f).
+
+  Fact Φ_spec e x: Ξ e (char_rel P) x → ∞∀ n, Φ_ e x n ↓.
+  Proof. intro H. unfold Φ_. apply (Φ_spec S_P H). Qed.
+  Definition Ω e n := Φ_ e e n.
+  Definition limit_decider e n: bool := Dec (Ω e n ↓).
+
+    (** ** Requirements *)
+
+  Hypothesis step_ex_spec: ∀ e, (∞∃ n, Ω e n ↓) → Ξ e (char_rel P) e.
+  Hypothesis N_requirements: ∀ e, (∞∀ n, Ω e n ↓) ∨ (∞∀ n, ¬ Ω e n ↓).
+  
+  Lemma Jump_limit : limit_computable (P´).
+  Proof.
+    exists limit_decider; split; intros.
+    - unfold J. split. 
+      intros [w Hw]%Φ_spec; exists w; intros??.
+      apply Dec_auto. by eapply Hw.
+      intros [N HN]. eapply step_ex_spec. 
+      intros m. exists (Datatypes.S N + m); split; first lia.
+      eapply Dec_true. eapply HN. lia.
+    - unfold J. split; intros H. 
+      destruct (N_requirements x) as [[k Hk]|h2].
+      enough (Ξ x (char_rel P) x) by easy.
+      eapply step_ex_spec. intros m. exists (Datatypes.S k + m).
+      split; first lia. eapply Hk. lia.
+      destruct h2 as [w Hw]. exists w.
+      intros. specialize (Hw n H0). unfold limit_decider.
+      destruct (Dec _); eauto.
+      destruct H as [w Hw].
+      intros [k Hneg]%Φ_spec.
+      set (N := Datatypes.S (max w k)).
+      assert (Ω x N ↓). { eapply Hneg. lia. }
+      enough (¬ Ω x N ↓) by eauto.
+      eapply Dec_false. eapply Hw. lia.  
+  Qed.
+
+End Requirements_Verification.
+
+Section Requirements_Meet.
+
+  Variables wall: Wall.
+
+  Definition P := P wall.
+  Definition P_func := P_func wall.
+  Instance E: Extension := simple_extension wall.
+
+  Fact P_semi_decidable: semi_decidable P.
+  Proof. eapply P_semi_decidable. Qed.
+
+  Definition χ := χ (simple_extension wall).
+  Definition P_Φ := (Φ_ χ).
+  Definition P_Ω := (Ω χ).
+
+  Section wall_greater_than_use.
+
+    Hypothesis wall_spec: forall e L n, φ (λ x, Dec (In x L)) e e n ≤ wall e L n.
+
+    Definition use := λ e n, φ (χ n) e e n.
+
+    Lemma eventally_greater_than_use_gen e:
+      (∃ n, (∀ e', e' < e → ∀ n', n < n' → ¬ (recv_att wall) e' n')) →
+      (∞∀ s, ∀ x, extendP (P_func s) s x → use e s < x).
+    Proof.
+      intros Hc. destruct Hc as [s Hs].
+      exists (S s). intros m Hm x [e_ [He_ He_']].
+      destruct (Dec (e_ < e)) as [E|E].
+      { exfalso. enough (recv_att wall e_ m).
+        unshelve eapply (Hs e_ _ m); eauto; lia.
+        split; first lia. destruct He_' as [H _].
+        apply H. }
+      assert (e ≤ e_) by lia; clear E.
+      destruct He_', H1, H1, H1, H1, H3.
+      specialize(H5 e H).
+      enough (use e m <= wall e (P_func m) m) by lia.
+      apply wall_spec.
+    Qed.
+
+    Lemma eventally_greater_than_use_classically e:
+      ¬¬ (∞∀ s, ∀ x, extendP (P_func s) s x → use e s < x).
+    Proof.
+      intros H_. eapply (@recv_at_most_once_bound_classically wall e).
+      intros H'. apply H_. 
+      by apply eventally_greater_than_use_gen.
+    Qed.
+
+
+    Fact wall_convergence_gen e : 
+      (∃ N, (∀ s, N ≤ s → ∀ x, extendP (P_func s) s x → use e s < x)
+        ∧ pdec (∃ x, N ≤ x ∧ use e x ≠ 0)) ->
+      (∃ b n: nat, ∀ m : nat, n ≤ m → use e m = b).
+    Proof.
+      intros (N & HN & Hp).
+      assert (∀ m, dec (use e m = 0)) as HD by eauto.
+      destruct Hp as [H'|H'].
+      - enough (∃ x, N ≤ x ∧ use e x ≠ 0) as H''.
+        clear H'. destruct H'' as [x [H1 H2]].
+        destruct (use e x) as [|k] eqn: H; first done; clear H2.
+        exists (S k), x. intros t Ht. induction Ht; first done.
+        rewrite <- (@φ_spec1 χ _ _ _ _ IHHt).
+        reflexivity.
+        intros; split.
+        + intros K%Dec_true. apply Dec_auto.
+          enough (incl (F_func (simple_extension wall) m) (F_func (simple_extension wall) (S m))).
+          eauto. eapply F_mono; [apply F_func_correctness|apply F_func_correctness|lia].
+        + intros K%Dec_true. specialize (F_func_correctness (simple_extension wall) (S m)) as HE.
+          inv HE. 
+          * assert (use e m < a).
+            { eapply HN. lia. enough (P_func m = l) as ->. apply H5.
+              eapply F_uni; [apply F_func_correctness|apply H4]. }
+            assert (wall e (P_func m) m ≥ S k). { rewrite <-IHHt.
+            unfold use. unfold χ, the_priority_method.χ.
+            specialize (wall_spec e (F_func (simple_extension wall) m) m).  
+            eapply wall_spec. }
+            destruct (Dec (a = x0)).
+            lia. apply Dec_auto. rewrite <- H3 in K.
+            destruct K; first done.
+            enough ((F_func (simple_extension wall) m) = l) as -> by done.
+            eapply F_uni; last apply H4; apply F_func_correctness.
+          * apply Dec_auto.
+            enough (F_func (simple_extension wall) m = F_func (simple_extension wall) (S m)) as -> by eauto. 
+            eapply F_uni; first apply F_func_correctness.
+            assumption.
+        + apply H'.
+      - exists 0. exists N. intros.
+        destruct (use e m) eqn: E; first done.
+        exfalso. apply H'. exists m. split; first done.
+        congruence.
+    Qed.
+
+
+    Fact wall_convergence_classically e : ¬¬ ∃ b n: nat, ∀ m : nat, n ≤ m → use e m = b.
+    Proof.
+      intros H. eapply (eventally_greater_than_use_classically). intros [N HN].
+      assert (¬¬ pdec (∃ x, N ≤ x ∧ use e x ≠ 0)).
+      { ccase (∃ x, N ≤ x ∧ use e x ≠ 0) as [H_|H'_]; eauto.
+        - intros Hp. apply Hp. left. done.
+        - intros Hp. apply Hp. right. done. }
+      apply H0. intros H0'.
+      apply H, wall_convergence_gen.
+      exists N; eauto.
+    Qed.
+
+    Hypothesis Σ_1_lem: LEM_Σ 1.
+
+    Lemma attention_bound:  
+      ∀ k, ∃ s, ∀ e, e < k → ∀ s', s < s' → ~ recv_att wall e s'.
+    Proof. by apply recv_at_most_once_bound. Qed.
+
+    Lemma eventally_greater_than_use e: 
+      (∞∀ s, ∀ x, extendP (P_func s) s x → use e s < x).
+    Proof. apply eventally_greater_than_use_gen, attention_bound. Qed.
+
+    Fact wall_convergence e : ∃ b n: nat, ∀ m : nat, n ≤ m → use e m = b.
+    Proof.
+      apply wall_convergence_gen.
+      destruct (eventally_greater_than_use e) as [N HN].
+      exists N. split; first done.
+      destruct level1 as (_&h2&_).
+      rewrite h2 in Σ_1_lem.
+      unfold principles.LPO in *.
+      destruct (@Σ_1_lem (λ x, Dec (N ≤ x ∧ use e x ≠ 0))) as [[N' HN']|].
+      left. exists N'. eauto.
+      right. intros [x Hx]. apply H. exists x. eauto.
+    Qed.
+
+    Corollary N_requirements e : ((∞∀ n, P_Ω e n ↓) ∨ (∞∀ n, ¬ P_Ω e n ↓)).
+    Proof.
+      destruct (wall_convergence e) as (b&n&Hn).
+      destruct b. 
+      - right. exists n. intros.
+        enough(P_Ω e m = None) by congruence.
+        unfold P_Ω, Ω.
+        apply φ_spec0'.
+        by apply Hn.
+      - left. exists n. intros.
+        unfold P_Ω, Ω.
+        apply φ_spec0_1.
+        unfold use in Hn.
+        by rewrite (Hn m H).
+    Qed.
+
+    Lemma eventally_greater_than_wall e: 
+      (∞∀ s, ∀ x, extendP (P_func s) s x → wall e (P_func s) s < x).
+    Proof.
+      destruct (@attention_bound (S e)) as [s Hs].
+      exists (S s). intros m Hm x [e_ [He_ He_']].
+      destruct (Dec (e_ < e)) as [E|E].
+      { exfalso. enough (recv_att wall e_ m).
+        unshelve eapply (Hs e_ _ m); eauto; lia.
+        split; first lia. destruct He_' as [H _].
+        apply H. }
+      assert (e ≤ e_) by lia; clear E.
+      destruct He_', H1, H1, H1, H1, H3.
+      by eapply H5.
+    Qed.
+
+    Lemma step_ex_spec: ∀ e, (∞∃ n, P_Ω e n ↓) → Ξ e (char_rel P) e.
+    Proof.
+      intros e He.
+      destruct (eventally_greater_than_wall e) as [N HN].
+      destruct (wall_convergence e) as [B [b Hb]].
+      set (M := max N b). destruct (He M) as [k [Hk Hk']].
+      eapply (@φ_spec χ e e k); first apply Hk'. 
+      intros x Hx. unfold P, simpleness.P.
+      rewrite F_with_top. split.
+      - intros (L & m & HL & HLs &HP).
+        assert (L = P_func m) as E. { eapply F_uni. apply HL. apply F_func_correctness. }
+        assert (x::L = P_func (S m)) as E'. { eapply F_uni. apply HLs. apply F_func_correctness. }
+        apply Dec_auto. destruct (Dec (S m ≤ k)) as [E_|E_].
+        enough (incl (P_func (S m)) (P_func k)). rewrite <-E' in H.
+        eauto. eapply F_mono; last apply E_; apply F_func_correctness.
+        assert (N ≤ m) as Em by lia. rewrite E in HP. specialize (HN m Em x HP).
+        assert (k ≤ m) as Ek by lia.
+        enough (x ≤ φ (χ m) e e m).
+        exfalso. assert (φ (χ m) e e m < x).
+        assert(φ (χ m) e e m  ≤ wall e (P_func m) m).
+        { specialize (wall_spec e (F_func (simple_extension wall) m) m).
+          unfold χ, the_priority_method.χ.
+          by rewrite wall_spec. }
+        lia.
+        enough (φ (χ  m) e e m = φ (χ  k) e e k) by lia.
+        assert (φ (χ m) e e m = B).  
+        { rewrite <- (Hb m). reflexivity. lia. }
+        assert (φ (χ k) e e k = B).  
+        { rewrite <- (Hb k). reflexivity. lia. }
+          lia. 
+        enough (φ (χ  m) e e m = φ (χ  k) e e k) by lia.
+        assert (φ (χ m) e e m = B).  
+        { rewrite <- (Hb m). reflexivity. lia. }
+        assert (φ (χ k) e e k = B).  
+        { rewrite <- (Hb k). reflexivity. lia. }
+        lia. 
+      - intros H%Dec_true.
+        eapply F_with_top. 
+        exists (F_func _ k), k; split; eauto.
+        eapply F_func_correctness.
+    Qed.
+
+  End wall_greater_than_use.
+
+End Requirements_Meet.
+
+Section Concret_Wall.
+
+  (** ** Construction *)
+
+    Definition wall: Wall := λ e L n, φ (λ x, Dec (In x L)) e e n.
+    Instance E_low: Extension := simple_extension wall.
+    Hypothesis Σ_1_lem: LEM_Σ 1.
+
+    Fact P_simple: simple (P wall).
+    Proof. eapply P_simple, wall_convergence_classically.
+      unfold wall. done. Qed.
+
+End Concret_Wall.
+
+Section Results.
+
+  Hypothesis LEM_Σ_1: LEM_Σ 1.
+
+  Fact jump_P_limit: limit_computable ((P wall)´).
+  Proof.
+    eapply Jump_limit; first apply F_with_χ.
+    - intros e He. 
+      eapply step_ex_spec; eauto.
+    - eapply N_requirements; eauto.
+  Qed.
+
+End Results.
+
+
+
diff --git a/theories/PostsProblem/simpleness.v b/theories/PostsProblem/simpleness.v
new file mode 100644
index 0000000..b586d87
--- /dev/null
+++ b/theories/PostsProblem/simpleness.v
@@ -0,0 +1,731 @@
+From SyntheticComputability Require Import ArithmeticalHierarchySemantic reductions SemiDec TuringJump OracleComputability Definitions limit_computability simple.
+Require Import SyntheticComputability.Synthetic.DecidabilityFacts.
+Require Export SyntheticComputability.Shared.FinitenessFacts.
+Require Export SyntheticComputability.Shared.Pigeonhole.
+Require Export SyntheticComputability.Shared.ListAutomation.
+Require Import Arith Arith.Compare_dec Lia Coq.Program.Equality List.
+From SyntheticComputability Require Import the_priority_method.
+Import SyntheticComputability.Axioms.EA.Assume_EA.
+Import ListNotations.
+
+(* ########################################################################## *)
+(** * The Simple Extension *)
+(* ########################################################################## *)
+
+Section ComplToBound.
+    Definition complToBound L b : list nat 
+        := filter (λ x, Dec (¬ In x L)) (seq 0 (S b)).
+
+    Lemma complToBound_Bound L b :
+        ∀ x, In x (complToBound L b) → x <= b.
+    Proof.
+        intros x [H % in_seq ?] % in_filter_iff. lia.
+    Qed.
+    Lemma filter_length {X} f (l : list X) :
+        length l = length (filter f l) + length (filter (λ x, (negb (f x))) l).
+    Proof.
+        induction l; cbn.
+        - reflexivity.
+        - destruct f; cbn; lia.
+    Qed.
+    Lemma filter_NoDup {X} f (l : list X) :
+        NoDup l → NoDup (filter f l).
+    Proof.
+        induction 1; cbn.
+        - econstructor.
+        - destruct f; eauto. econstructor; auto.
+            intros ? % in_filter_iff. firstorder.
+    Qed.
+    Lemma complToBound_length L b:
+        length (complToBound L b) + length L >= S b.
+    Proof.
+        rewrite <- (seq_length (S b) 0).
+        erewrite filter_length with (l := seq 0 (S b)).
+        unfold complToBound.
+        eapply Plus.plus_le_compat_l_stt.
+        generalize (seq_NoDup (S b) 0).
+        generalize (seq 0 (S b)). clear.
+        intros. erewrite filter_ext with (g := fun x => Dec (In x L)).
+        2:{ intros a. destruct Dec; cbn; destruct Dec; firstorder congruence. }
+        eapply NoDup_incl_length. now eapply filter_NoDup.
+        clear. induction l; cbn.
+        - firstorder.
+        - destruct Dec; cbn. 2: eauto.
+            intros ? [-> | ]; eauto.
+    Qed.
+    Lemma complToBound_NoDup L b:
+        NoDup (complToBound L b).
+    Proof.
+        eapply filter_NoDup, seq_NoDup.
+    Qed.
+    Lemma firstn_In {X} (l : list X) n x : In x (firstn n l) → In x l.
+    Proof.
+        induction n in x, l |- *; destruct l; cbn; firstorder.
+    Qed.
+
+    Lemma firstn_NoDup {X} (l : list X) n : NoDup l → NoDup (firstn n l).
+    Proof.
+        induction 1 in n |- *; destruct n; cbn; try now econstructor.
+        econstructor; eauto.
+        now intros ? % firstn_In.
+    Qed.
+End ComplToBound.
+
+Section Assume_EA.
+
+  Definition θ := φ.
+  Definition EA_spec := ∀ p, semi_decidable p → ∃ e, ∀ x, p x ↔ ∃ n, φ e n = Some x.
+
+  Lemma EA: EA_spec.
+  Proof.
+    intros P HP%SyntheticComputability.Axioms.EA.enum_iff.
+    rewrite W_spec in HP. destruct HP as [c Hc].
+    exists c. intros x. unfold W in Hc.
+    eapply Hc.
+  Qed.
+
+  Definition W_ n e x := φ n e = Some x.
+  Definition W e x := ∃ n, W_ e n x.
+
+  Lemma W_spec: ∀ P, semi_decidable P → ∃ e, ∀ x, P x ↔ W e x.
+  Proof. intros P [e He]%EA. exists e; intros x; now rewrite He. Qed.
+
+  Notation "'W[' s ']' e" := (λ x, ∃ n, n <= s ∧ W_ e n x) (at level 30).
+
+  Section EA_dec.
+
+    Lemma W_dec e: ∀ x n, dec (W_ e n x).
+    Proof.
+      intros x n.
+      destruct (φ e n) eqn: E.
+      - destruct (Dec (x = n0)) as [E'|E'].
+        left. now subst. right. intros H. congruence.
+      - right. intros H. congruence. 
+    Qed.
+
+    Lemma W_bounded_dec e : ∀ x s, dec ((W[s] e) x).
+    Proof.
+      intros x s. cbn. eapply exists_bounded_dec.
+      intro; apply W_dec.
+    Qed.
+
+    Lemma W_bounded_bounded e s: bounded (W[s] e).
+    Proof.
+      unfold bounded.
+      induction s.
+      - destruct (φ e 0) as [w|] eqn: E.
+        exists (S w). intros x [n [Hn1 Hn2]].
+        inv Hn1. unfold W_ in Hn2.  rewrite E in Hn2.
+        injection Hn2. lia.
+        exists 42. intros x [n [Hn1 Hn2]].
+        inv Hn1. unfold W_ in Hn2.
+        rewrite E in Hn2. congruence.
+      - destruct IHs as [N HN].
+        destruct (φ e (S s)) as [w|] eqn: E.
+        exists (max (S w) (S N)). intros x [n [Hn1 Hn2]].
+        inv Hn1. unfold W_ in Hn2. 
+        rewrite E in Hn2. injection Hn2. lia.
+        eapply Nat.lt_trans. eapply HN. exists n; split; easy. lia.
+        exists N. intros x [n [Hn1 Hn2]].
+        inv Hn1. unfold W_ in Hn2.
+        rewrite E in Hn2. congruence.
+        eapply HN. exists n. split; eauto.
+    Qed.
+
+  End EA_dec.
+
+  Definition disj_list_pred {X} (A: list X) (B: X → Prop) := ∀ x, In x A → B x → False.
+  Definition disj_pred {X} (A B: X → Prop) := ∀ x, A x → B x → False.
+  Notation "A # B" := (disj_list_pred A B) (at level 30).
+  Notation "A #ₚ B" := (disj_pred A B) (at level 30).
+
+  Lemma extra_bounded f m: Σ b, ∀ n, n < m → f n < b.
+  Proof.
+    induction m.
+    - exists 42. intros. inv H. 
+    - destruct IHm as [b' Hb'].
+      exists (S (max b' (f m))).
+      intros ? H. inv H. lia. specialize (Hb' n H1). lia.
+  Qed.
+
+  Section Assume_WALL.
+    Definition Wall := nat → list nat → nat → nat.
+    Variable wall: Wall.
+
+    Section Extension. (** ** Construction *)
+
+      Definition ext_intersect_W L n e := L # W[n] e.
+      Definition ext_has_wit L n e x := (W[n] e) x ∧ 2 * e < x ∧ ∀ i, i <= e → wall i L n < x.
+      Definition ext_pick L n e := ext_intersect_W L n e ∧ ∃ x, ext_has_wit L n e x.
+      Definition ext_choice L n e x :=  e < n ∧ least (ext_pick L n) e ∧ least (ext_has_wit L n e) x.
+      Definition ext_least_choice L n x := ∃ e, ext_choice L n e x.
+
+    End Extension.
+
+    Section Extension_Facts.
+
+      #[export]Instance ext_intersect_W_dec L n e: dec (ext_intersect_W L n e).
+      Proof.
+        apply BaseLists.list_forall_dec.
+        intro x. eapply dec_neg_dec, exists_bounded_dec; eauto.
+      Qed. 
+
+      #[export] Instance ext_wall L n e x: dec (∀ i, i <= e → wall i L n < x).
+      Proof. eapply forall_bounded_dec; eauto. Qed.
+      
+      #[export]Instance ext_has_wit_dec L n e x : dec (ext_has_wit L n e x).
+      Proof. apply and_dec; first apply exists_bounded_dec; eauto. Qed.
+
+      #[export]Instance ext_has_wit_exists_dec L n e : dec (∃ x, ext_has_wit L n e x).
+      Proof.
+        unfold ext_has_wit. eapply bounded_dec; last eapply W_bounded_bounded.
+        intro x; eapply W_bounded_dec; eauto. eauto.
+      Qed.
+
+      #[export]Instance ext_pick_dec L n e : dec (ext_pick L n e).
+      Proof.
+        eapply and_dec; first apply ext_intersect_W_dec.
+        unfold ext_has_wit.
+        eapply bounded_dec; last apply W_bounded_bounded.
+        intros x. eapply exists_bounded_dec.
+        intro; apply W_dec. eauto.
+      Qed.
+
+      #[export]Instance ext_pick_exists_dec L n: dec (∃ e, e < n ∧ least (ext_pick L n) e).
+      Proof. 
+        eapply exists_bounded_dec'. intro x.
+        eapply least_dec. intros y.
+        eapply ext_pick_dec.
+      Qed.
+
+      Fact ext_least_choice_dec L n:
+        (Σ x : nat, ext_least_choice L n x) + (∀ x : nat, ¬ ext_least_choice L n x).
+      Proof.
+        unfold ext_least_choice.
+        destruct (ext_pick_exists_dec L n) as [H|H].
+        - left. apply ewo_nat; first last.
+          destruct H as [e (h1 & [(h4 & h2) h3])].
+          eapply least_ex in h2. destruct h2 as [k h6].
+          exists k, e. split; first easy; split.
+          2: { eapply h6. }
+          split; last apply h3. split; first apply h4.
+          destruct h6. now exists k.
+          eapply ext_has_wit_dec.
+          intro x. unfold ext_choice. eapply exists_bounded_dec'.
+          intros x'. eapply and_dec.
+          apply least_dec. eapply ext_pick_dec.
+          apply least_dec. eapply ext_has_wit_dec.
+        - right. intros x [e (h1 & h2 & _)]. apply H.
+          exists e. split; eauto.
+      Qed.
+
+      Fact ext_least_choice_uni l x: unique (ext_least_choice l x).
+      Proof.
+        intros y1 y2 [? (h1 & h2 & h3)] [? (h1' & h2' & h3')].
+        assert (x0 = x1) as ->. eapply least_unique; eauto.
+        eapply least_unique; eauto.
+      Qed.
+
+      Instance simple_extension: Extension.
+      Proof.
+          unshelve econstructor.
+          - exact ext_least_choice.
+          - apply ext_least_choice_dec.
+          - apply ext_least_choice_uni.
+      Defined.
+
+      Definition P_ := F_ simple_extension.
+      Definition P_func := F_func simple_extension.
+      Definition P := F_with simple_extension.
+
+      Definition non_finite e := ¬ exhaustible (W e).
+
+      Fact In_Pf k y: In y (P_func k) → P y.
+      Proof.
+        intros H. exists (P_func k), k.
+        split; [easy| apply F_func_correctness].
+      Qed.
+
+      Definition lim_to (f: list nat → nat → nat) b := 
+          (∃ n, ∀ m, n <= m → f (P_func m) m = b).
+
+      Lemma finite_decs (P : nat → Prop) k Q :
+        ((∀ k', k' < k → pdec (P k')) → ¬ Q) → ¬ Q.
+      Proof.
+        induction k.
+        - firstorder lia.
+        - intros H Hq.
+          assert (¬¬ pdec (P k)) as Hk. { cbv. tauto. }
+          apply Hk. clear Hk. intros Hk.
+          apply IHk. 2: assumption.
+          intros Ha. apply H. intros.
+          assert (k' = k ∨ k' < k) as [-> | ] by lia.
+          assumption.
+          now apply Ha.
+      Qed.
+
+    End Extension_Facts.
+
+    Hypothesis wall_spec: ∀ e, ¬¬ ∃ b, lim_to (wall e) b.
+
+    Section Requirements.
+
+      (** ** Requirements *)
+
+      Definition P_requirements P e := non_finite e → ¬ (W e #ₚ P).
+      Definition recv_att e n := e < n ∧ least (ext_pick (P_func n) n) e.
+      Definition act e n := ¬ (P_func n) # W[n] e.
+      Definition act_by e x := ∃ k, recv_att e k ∧ ext_least_choice (P_func k) k x.
+      Definition done e n := ∀ s, n < s → ¬ recv_att e s.
+
+      #[export]Instance attend_dec e n: dec (recv_att e n).
+      Proof.
+        unfold recv_att. apply and_dec; first eauto.
+        eapply least_dec. intros y.
+        eapply ext_pick_dec.
+      Qed.
+
+    End Requirements.
+
+    Section Requirements_Facts.
+
+      (** ** Verification *)
+
+      Lemma ext_pick_witness L n e:
+        ext_pick L n e → ∃ x, least (ext_has_wit L n e) x.
+      Proof.
+        intros [H1 H2].
+        eapply least_ex. intro; eapply ext_has_wit_dec.
+        trivial.
+      Qed.
+      
+      Lemma W_incl e n m: 
+        n <= m → ∀ x,  (W[n] e) x → (W[m] e) x.
+      Proof.
+        intros H x [y [H1 H2]].
+        exists y. split; lia + easy.
+      Qed.
+
+      Lemma intersect_mono {X} (L L': list X) (P P': X → Prop) : 
+        L' # P' → incl L L' → (∀ x, P x → P' x) → L # P.
+      Proof.
+        intros H h1 h2 x Hx1 Hx2.
+        eapply (H x). now eapply h1. 
+        now apply h2.
+      Qed.
+
+      Lemma act_impl_always_act e n: act e n → ∀ m, n <= m → act e m .
+      Proof.
+        intros H m Hm Hx. apply H. 
+        eapply (intersect_mono Hx).
+        eapply F_mono; try eapply F_func_correctness; easy.
+        now eapply W_incl.
+      Qed.
+
+      Lemma recv_impl_next_act e k: recv_att e k → act e (S k).
+      Proof.
+        intros [He H] Hcontr.
+        edestruct (ext_pick_witness) as [x Hx].
+        { destruct H. eapply e0. }
+        apply (Hcontr x).
+        assert (P_ (S k) (P_func (S k))) by apply F_func_correctness.
+        inv H0. cbn in H4. assert (ext_least_choice l k x) as Hwitness.
+        exists e. assert (P_func k = l) as <-.
+        eapply F_uni. apply F_func_correctness. apply H3.
+        split; first easy. split; first easy. easy.
+        assert (x = a) as ->. eapply (@extend_uni simple_extension); cbn; eauto.
+        eauto. exfalso. eapply (H3 x). cbn.
+        exists e. enough ((P_func k) = (P_func (S k))) as <-. 
+        split; first easy. easy.
+        assert (F_ simple_extension k (P_func k)) by apply F_func_correctness.
+        eapply F_uni; eauto.
+        firstorder.
+      Qed.
+
+      Lemma act_impl_not_recv e k: act e k → ¬ recv_att e k.
+      Proof. now intros h2 [_ [[h _] _]]. Qed.
+
+      Lemma recv_impl_next_always_act e k: recv_att e k → ∀ m, k < m → act e m.
+      Proof.
+        intros. eapply act_impl_always_act.
+        apply recv_impl_next_act. apply H. lia.
+      Qed.
+
+      Lemma recv_impl_always_not_recv e k: 
+        recv_att e k → ∀ m, k < m → ¬ recv_att e m.
+      Proof.
+        intros H1 m Hm. eapply act_impl_not_recv.
+        apply (recv_impl_next_always_act H1 Hm).
+      Qed.
+
+      Lemma recv_at_most_once_gen e:
+        (pdec (∃ k, recv_att e k)) ->
+        (∃ s', ∀ s, s' < s → ¬ recv_att e s).
+      Proof.
+        intros [[w Hw]|H].
+        - exists w.
+          now eapply recv_impl_always_not_recv.
+        - exists 0.
+          intros k' Hk' Ha.
+          apply H. now exists k'.
+      Qed.
+
+      Lemma recv_at_most_once e: ¬ ¬ (∃ s', ∀ s, s' < s → ¬ recv_att e s).
+      Proof.
+        intros H.
+        assert (¬¬ (pdec (∃ k, recv_att e k))) as Hdec.
+        { unfold pdec. tauto. }
+        apply Hdec. clear Hdec. intros Hdec.
+        apply H, recv_at_most_once_gen. assumption.
+      Qed.
+
+      Lemma recv_at_most_once_bound_gen k:
+        (∀ k', k' < k → pdec (∃ k0 : nat, recv_att k' k0)) →
+        ∃ s, (∀ e, e < k → ∀ s', s < s' → ¬ recv_att e s').
+      Proof.
+        intros Hle.
+        induction k.
+        - exists 42. intros ??. lia. 
+        - destruct IHk as [s Hs].
+          { intros. eapply Hle. lia. }
+          destruct (@recv_at_most_once_gen k) as [sk Hsk].
+          { apply Hle. lia. }
+          set (max sk s) as N.
+          exists N. intros e He.
+          assert (e = k ∨ e < k) as [->|Hek] by lia.
+          intros s' Hs'. eapply Hsk. lia.
+          intros s' Hs'. eapply Hs; lia.
+      Qed.
+
+      Lemma recv_at_most_once_bound_classically k:
+        ¬ ¬ ∃ s, (∀ e, e < k → ∀ s', s < s' → ¬ recv_att e s').
+      Proof.
+        eapply finite_decs.
+        intros H % (recv_at_most_once_bound_gen (k := k)).
+        tauto.
+      Qed.
+      Lemma recv_at_most_once_bound: 
+        LEM_Σ 1 → ∀ k, ∃ s, (∀ e, e < k → ∀ s', s < s' → ¬ recv_att e s').
+      Proof.
+        intros Hlem k. apply recv_at_most_once_bound_gen.
+        intros. eapply assume_Σ_1_lem. apply Hlem. eauto. 
+      Qed.
+
+      Lemma attend_uni e: unique (recv_att e).
+      Proof.
+        intros k1 k2 H1 H2.
+        specialize (fun a b => @act_impl_not_recv _ _ (@recv_impl_next_always_act _ _ H1 a b)) as H1'.
+        specialize (fun a b => @act_impl_not_recv _ _ (@recv_impl_next_always_act _ _ H2 a b)) as H2'.
+        enough (¬ k1 < k2 ∧ ¬ k2 < k1) by lia; split.
+        intro Hk. eapply H1'. apply Hk. easy. 
+        intro Hk. eapply H2'. apply Hk. easy.
+      Qed.
+
+      Lemma pick_el_uni e: unique (act_by e).
+      Proof.
+        intros x1 x2 [k [Ht Hk]] [k' [Ht' Hk']].
+        assert (k=k') as <-. eapply attend_uni; eauto.
+        eapply (@extend_uni simple_extension); cbn; eauto.
+      Qed.
+
+    End Requirements_Facts.
+
+    Section Complement_Inf.
+
+      Lemma P_meet_spec x n : P x ∧ x <= 2*n → ∃ e, act_by e x ∧ e < n.
+      Proof.
+        intros [[L [k [Hin Hk]]] Hn].
+        dependent induction L. inv Hin.
+        destruct (Dec (a = x)) as [->|].
+        - clear IHL Hin.
+          destruct (F_pick Hk) as [k' [Hk' [e He]]].
+          exists e. split. 
+          exists k'. split; unfold recv_att.
+          + destruct He; intuition eauto. enough (P_func k' = L) as -> by eauto.
+            eapply F_uni. apply F_func_correctness. easy.
+          + exists e. unfold ext_choice.
+            enough (P_func k' = L) as -> by eauto.
+            eapply F_uni. apply F_func_correctness.
+            destruct He; intuition eauto. 
+          + destruct He. destruct H0. destruct H1. destruct H1.
+            lia.
+        - destruct (F_pop Hk) as [m' Hm']. 
+          eapply (IHL m'); eauto. firstorder. 
+      Qed.
+
+      Lemma P_extract_spec n L:
+        (∀ x, In x L → P x ∧ x <= 2 * n) → 
+        ∀ x, In x L → ∃ c, act_by c x ∧ c < n.
+      Proof.
+        intros. induction L. inv H0. 
+        destruct H0 as [-> | Hln]; last apply IHL; eauto.
+        apply P_meet_spec. now apply H.
+      Qed.
+
+      Lemma P_pullback_list n L:
+        NoDup L → (∀ x, In x L → P x ∧ x <= 2 * n) → 
+          ∃ (LC: list nat), NoDup LC ∧ length LC = length L ∧
+            ∀ c, In c LC → ∃ x, act_by c x ∧ In x L ∧ c < n.
+      Proof.
+        intros HL H1.
+        induction L.
+        - exists []; intuition.
+        - remember (@P_extract_spec n (a::L) H1 a).
+          assert (In a (a::L)) as H0 by intuition.
+          apply e in H0 as [c0 [H0 E1]].
+          assert (NoDup L) by (inversion HL; intuition).
+          apply IHL in H as [LC H].
+          exists (c0::LC). intuition.
+          + constructor; last now exact H2. 
+            intros In. inv HL.
+            apply H4 in In as [y (Hs & h2 & h3)].
+            now rewrite (pick_el_uni H0 Hs) in H6.
+          + cbn. rewrite H. trivial.
+          + destruct H3 as [->|].
+            * exists a; intuition.
+            * destruct (H4 c H3) as [y Hy].
+              exists y; intuition.
+          + intros y In1. assert (In y (a::L)) by intuition.
+            now apply H1 in H2.
+      Qed.
+
+      Definition PredListTo p : list nat → nat → Prop
+        := λ L b, ∀ x, In x L ↔ p x ∧ x <= b.
+
+      Lemma NoDupBoundH {L} b:
+          NoDup L → (∀ x, In x L → x <= b) → ∀ x, x > b → NoDup (x::L).
+      Proof.
+          intros ND H x E.
+          constructor.
+          - intros H1 % H. lia.
+          - exact ND.
+      Qed.
+
+      Lemma PredNoDupListTo_NNExist p:
+        ∀ b, ¬¬ ∃ L, PredListTo p L b ∧ NoDup L.
+      Proof.
+        destruct (F_computable simple_extension) as [f Hf].
+        induction b; intros H.
+        - ccase (p 0) as [H0 | H0]; apply H.
+          + exists [0]. split; try split.
+            * intros [E | E]; (try contradiction E).
+              rewrite <- E. intuition.
+            * intros E. assert (x = 0) by lia.
+              rewrite H1. intuition.
+            * constructor; intuition; constructor.
+          + exists nil. split; try split.
+            * contradiction.
+            * intros E. assert (x = 0) by lia.
+              rewrite H1 in E. firstorder.
+            * constructor.
+        - apply IHb. intros [L H1].
+          ccase (p (1 + b)) as [H0 | H0]; apply H.
+          + exists ((1+ b) :: L). split; try split.
+            * intros [E | E]; try (rewrite <- E; intuition).
+              apply H1 in E. intuition.
+            * intros [E1 E2]. assert (x <= b ∨ x = 1 + b) as [E | E] by lia.
+              ** right. apply H1. intuition.
+              ** left. lia.
+            * apply (@NoDupBoundH _ b).
+              ** apply H1.
+              ** intros x H3 % H1. lia.
+              ** lia.
+          + exists L. split; try split.
+            * intros E % H1. intuition.
+            * intros [E1 E2]. assert (x <= b ∨ x = 1 + b) as [E | E] by lia.
+              ** apply H1. intuition.
+              ** rewrite E in E1. firstorder.
+            * apply H1.
+      Qed.
+
+      Lemma P_bounded L n:
+        NoDup L → (∀ x, In x L → P x ∧ x <= 2 * n) → length L <= n.
+      Proof.
+        intros ND [LC H] % P_pullback_list; intuition.
+        rewrite <- H.
+        assert (incl LC (seq 0 n)). unfold incl. 
+        - intros c [e [x Hx]] % H2. apply in_seq. lia.
+        - apply pigeonhole_length in H1.
+          + now rewrite seq_length in H1.
+          + intros. decide (x1 = x2); tauto.
+          + exact H0.
+      Qed.
+
+      Lemma P_Listing:
+        ∀ n, ¬¬ ∃ L, NoDup L ∧ length L <= n ∧ PredListTo P L (2*n).
+      Proof.
+        intros n H. apply (@PredNoDupListTo_NNExist P (2*n)).
+        intros [L H1]. apply H. exists L; intuition.
+        apply P_bounded.
+        - exact H2.
+        - apply H0.
+      Qed.
+
+      Lemma complToBound_compl p L b:
+        PredListTo p L b → PredListTo (compl p) (complToBound L b) b.
+      Proof.
+      intros H x. split.
+      - intros [H1 H1'] % in_filter_iff.
+        destruct Dec; cbn in H1'; try congruence.
+        enough (x <= b).
+        + firstorder.
+        + apply in_seq in H1. lia.
+      - intros [H1 H2]. eapply in_filter_iff. split.
+        + apply in_seq; lia.
+        + destruct Dec; cbn; try tauto. exfalso. firstorder.
+      Qed.
+
+      Lemma compl_P_Listing:
+      ∀ (n: nat) , ¬¬ ∃ L, length L >= n ∧ NoDup L 
+                                    ∧ ∀ x, In x L → ¬ P x.
+      Proof.
+        intros n H.
+        apply (@P_Listing n). intros [L H1].
+        apply H. exists (complToBound L (2*n)). repeat split.
+        - remember (complToBound_length L (2*n)). lia.
+        - apply complToBound_NoDup.
+        - intros x I % (@complToBound_compl P); intuition.
+      Qed.
+
+      Lemma P_coinfinite : ¬ exhaustible (compl P).
+      Proof.
+        eapply weakly_unbounded_non_finite.
+        intros n H. eapply compl_P_Listing with (n := n).
+        intros (l & ? & ? & H2).
+        eapply H.
+        exists (firstn n l).
+        repeat split.
+        - rewrite firstn_length. lia.
+        - now eapply firstn_NoDup.
+        - intros ? ? % firstn_In. now eapply H2.
+      Qed.
+
+    End Complement_Inf.
+
+    Section Requirements_Meet.
+
+      Lemma wall_bounded' e: ¬¬ ∃ w, ∀ x, wall e (P_func x) x < w.
+      Proof.
+        intro H_. apply (@wall_spec e). intros [v [k Hk]].
+        apply H_.
+        destruct (@extra_bounded (fun k => wall e (P_func k) k) k) as [w Hw].
+        exists (S (max v w)). intros x.
+        destruct (Dec (x < k)). apply Hw in l. lia.
+        assert (wall e (P_func x) x = v). apply Hk. lia. lia.
+      Qed.
+
+      Lemma wall_bounded e: 
+          ¬¬ ∃ w, ∀ i x, i <= e → wall i (P_func x) x < w.
+      Proof.
+        intro H_. induction e.
+        - apply (@wall_bounded' 0). intros [w Hw]. apply H_. exists w.
+          intros i x ?. inv H. trivial.
+        - apply IHe. intros [w IHe_].
+          apply (@wall_bounded' (S e)). intros [w' Hw'].
+          apply H_. exists (S (max w w')). intros i x H.
+          inv H. specialize (Hw' x). lia. 
+          specialize (IHe_ i x H1). lia.
+      Qed.
+
+      Lemma non_finite_not_bounded e: 
+        non_finite e → ¬¬ ∃ k, ∃ x, (W[k] e) x ∧ 2 * e < x ∧ 
+                                      (∀ n, ∀ i, i <= e → wall i (P_func n) n < x).
+      Proof.
+        intro H. unfold non_finite in H.
+        intros He.  rewrite non_finite_nat in H.
+        apply (@wall_bounded e). intros [w Hw].
+        pose (N := max (2*e + 1) w). specialize (H N).
+        apply H. intros [m [Hm1 [k Hmk]]].
+        apply He. exists k, m.
+        repeat split. now exists k.
+        lia. intros n i Hie. specialize (Hw i n Hie). lia.
+      Qed.
+
+      Lemma ext_pick_impl_recv N e: 
+        e < N → ext_pick (P_func N) N e → 
+        (∃ w, w ≤ e ∧ recv_att w N).
+      Proof.
+        intros HeN H1.
+        assert (exists w, ext_pick (P_func N) N w) by now exists e.
+        eapply least_ex in H; last eauto.
+        destruct H as [k Hk]. assert (k <= e).
+        { enough (¬ k > e) by lia. intro Hkw.
+          destruct Hk. rewrite safe_char in H0.
+          specialize (H0 e H1). lia. }
+        exists k. do 2 (split; first lia). eapply Hk.
+      Qed.
+
+      Lemma non_finite_recv e:
+        non_finite e → ¬ ¬ (∃ k, ¬ ext_intersect_W (P_func k) k e ∨ recv_att e k) .
+      Proof.
+        intros H He.
+        eapply (non_finite_not_bounded H); intros (b & x & (Hx1 & Hx2 & Hx3)).
+        eapply (@recv_at_most_once_bound_classically e); intros [s Hs].
+        pose (N := S (max (max b s)  e)). apply He.
+        destruct (Dec (ext_intersect_W (P_func N) N e)) as [He'|He'].
+        - exists N. right.
+          assert (ext_pick (P_func N) N e).
+        { split; first easy. exists x. split.
+          eapply W_incl; last apply Hx1. lia.
+          split; first lia. eapply Hx3.
+        }
+          split. lia. split. easy.
+          intros w HEw Hw.
+          eapply ext_pick_impl_recv in Hw.
+          destruct Hw as [g [HEg Hg]].
+          eapply Hs; last apply Hg; lia. lia. 
+        - exists N. now left.
+      Qed.
+
+      Lemma ext_intersect_W_intersect k e: 
+        ¬ (P_func k # W[k] e) → W e #ₚ P → False.
+      Proof.
+        unfold ext_intersect_W.
+        intros H1 H2. apply H1.
+        intros y Hy1 [w Hy2].
+        eapply (H2 y). now exists w.
+        eapply (In_Pf Hy1).
+      Qed.
+
+      Lemma P_requirements_meet : ∀ e, P_requirements P e.
+      Proof.
+        intros e He He'.
+        eapply (non_finite_recv He).
+        intros [k [H|H]].
+        - eapply ext_intersect_W_intersect; eauto.
+        - eapply recv_impl_next_act in H.
+          eapply ext_intersect_W_intersect; eauto.
+      Qed.
+
+    End Requirements_Meet.
+
+    Section Results.
+
+      Lemma P_semi_decidable : semi_decidable P.
+      Proof. apply F_with_semi_decidable. Qed.
+
+      Theorem P_simple : simple P.
+      Proof.
+        unfold simple; repeat split.
+        - rewrite EA.enum_iff. now apply P_semi_decidable.
+        - apply P_coinfinite.
+        - intros [q (Hqenum & Hqinf & Hq)].
+          rewrite EA.enum_iff in Hqenum.
+          destruct (W_spec Hqenum) as [c HWq].
+          apply (@P_requirements_meet c).
+          intros [l Hqe]; apply Hqinf.
+          exists l. intros x Hqx. apply (Hqe x).
+          now rewrite HWq in Hqx.
+          intros x HWcx HPx. unfold W in HWcx.
+          rewrite <- (HWq x) in HWcx. apply (Hq x HWcx HPx).
+      Qed.
+
+    End Results.
+
+  End Assume_WALL.
+
+End Assume_EA.
+
+
+
+
diff --git a/theories/PostsProblem/step_indexing.v b/theories/PostsProblem/step_indexing.v
new file mode 100644
index 0000000..2a90ed7
--- /dev/null
+++ b/theories/PostsProblem/step_indexing.v
@@ -0,0 +1,1050 @@
+From SyntheticComputability Require Import ArithmeticalHierarchySemantic reductions SemiDec TuringJump OracleComputability Definitions.
+Require Import SyntheticComputability.Synthetic.DecidabilityFacts.
+Require Export SyntheticComputability.Shared.FinitenessFacts.
+Require Export SyntheticComputability.Shared.Pigeonhole.
+Require Export SyntheticComputability.Shared.ListAutomation.
+From SyntheticComputability Require Import partial Dec.
+Require Import Coq.Program.Equality.
+From stdpp Require Export list.
+Import PartialTactics.
+
+(* ########################################################################## *)
+(** * Step-Inedxed Oracle Machines *)
+(* ########################################################################## *)
+
+Notation "'Σ' x .. y , p" :=
+  (sigT (fun x => .. (sigT (fun y => p)) ..))
+      (at level 200, x binder, right associativity,
+      format "'[' 'Σ'  '/  ' x  ..  y ,  '/  ' p ']'")
+  : type_scope.
+
+Definition inf_forall (P: nat -> Prop) := exists n, forall m, n ≤ m → P m.
+  Notation "'∞∀' x .. y , p" :=
+    (inf_forall (fun x => .. (inf_forall (fun y => p)) ..))
+        (at level 200, x binder, right associativity,
+        format "'[' '∞∀'  '/  ' x  ..  y ,  '/  ' p ']'")
+    : type_scope.
+
+Lemma list_cons_or {X} (A B: list X) a :
+    A `prefix_of` B ++ [a] → A `prefix_of` B ∨ A = B ++ [a].
+Proof.
+  induction A in B |-*; intros.
+  { left. eapply prefix_nil. }
+  destruct B.
+  { right. list_simplifier.
+  set (H' := H).
+  apply prefix_cons_inv_2, prefix_nil_inv in H' as ->.
+  by apply prefix_cons_inv_1 in H as ->. } 
+  list_simplifier.
+  set (H' := H).
+  apply prefix_cons_inv_2 in H'.
+  apply prefix_cons_inv_1 in H as ->.
+  destruct (IHA _ H') as [h1 | ->].
+  + left. by eapply prefix_cons.
+  + by right.
+Qed.
+
+Section Step_Eval.
+
+  Context {Part : partiality}.
+  Context {Q A O: Type}.
+  Definition tree := (list A) ↛ (Q + O).
+
+  Print red_Turing.
+
+  Definition red_Turing' (X Y : Type) (p : X → Prop) (q : Y → Prop) :=
+    ∃ r : Functional Y bool X bool, OracleComputable r
+      ∧ (∀ (x : X) (b : bool), char_rel p x b -> r (char_rel q) x b).
+
+  Lemma red_Turing_equive (X Y : Type) (p : X → Prop) (q : Y → Prop):
+    definite p → red_Turing p q ↔ red_Turing' p q.
+  Proof.
+    intros H. split.
+    - intros [r [Hr1 Hr2]]. exists r; split; eauto.
+      intros x b Hxb. by apply Hr2.
+    - intros [r [Hr1 Hr2]]. exists r; split; eauto.
+      intros x b. 
+      assert (functional (r (char_rel q))).
+      apply OracleComputable_functional; eauto.
+      apply char_rel_functional.
+      specialize (H0 x).
+      split. by apply Hr2.
+      intros Hr. destruct b.
+      destruct (H x); first done.
+      specialize (Hr2 x false H1).
+      firstorder.
+      destruct (H x); last done.
+      specialize (Hr2 x true H1).
+      firstorder.
+  Qed.
+  
+
+  Notation Ask q := (inl q).
+  Notation Output o := (inr o).
+
+  Lemma prefix_lookup_Some {X} (l1 l2: list X)i x :
+  l1 !! i = Some x → l1 `prefix_of` l2 → l2 !! i = Some x.
+  Proof. intros ? [k ->]. rewrite lookup_app_l; eauto using lookup_lt_Some. Qed.
+
+  Lemma prefix_length_eq {X} (l1 l2: list X) :
+    l1 `prefix_of` l2 → length l2 ≤ length l1 → l1 = l2.
+  Proof.
+    intros Hprefix Hlen. assert (length l1 = length l2).
+    { apply prefix_length in Hprefix. lia. }
+    eapply list_eq_same_length with (length l1); [done..|].
+    intros i x y _ ??. assert (l2 !! i = Some x) by eauto using prefix_lookup_Some.
+    congruence.
+  Qed.
+
+  Lemma interrogation_le_eq (q: Q) (a: A) (τ: tree) R use use' ans ans' v : 
+    functional R →
+    interrogation τ R use ans → τ ans =! Output v →
+    interrogation τ R use' ans' → τ ans' =! Output v →
+    length use ≤ length use' →
+    use = use'.
+  Proof.
+    intros funR H1 H1a H2 H2a E.
+    specialize (interrogation_det _ _ _ _ _ _ funR H1 H2 E) as [HE1 HE2].
+    enough (length use' ≤ length use). 
+    { eapply prefix_length_eq; eauto. }
+    enough (¬ length use < length use') by lia. intros H.
+    unshelve rewrite (interrogation_quantifiers) in H2; eauto. 
+    destruct H2 as (H11&H12).
+    assert (length ans < length ans') as H'.
+    { unshelve rewrite (interrogation_quantifiers) in H1; eauto.
+    destruct H1 as [-> _]. lia. } induction HE2 as [sth Hs].
+    destruct (H12 _ H') as [H12' _]. rewrite Hs in H12'.
+    rewrite take_app in H12'. 
+    specialize (hasvalue_det H12' H1a). congruence.
+  Qed.
+
+  Lemma interrogation_eq (q: Q) (a: A) (τ: tree) R use use' ans ans' v : 
+    functional R →
+    interrogation τ R use ans → τ ans =! Output v →
+    interrogation τ R use' ans' → τ ans' =! Output v →
+    use = use'.
+  Proof.
+    intros funR H1 H1a H2 H2a.
+    assert (length use ≤ length use' ∨ length use' ≤ length use) as [E|E] by lia.
+    eapply interrogation_le_eq; eauto.
+    symmetry. eapply interrogation_le_eq; eauto.
+  Qed.
+
+  Fixpoint evalt_comp (τ : tree) (f : Q → A) (step depth: nat): option (Q + O) :=
+    match (seval (τ []) depth) with
+    | Some x => 
+      match step, x with
+      | 0, Ask q => Some (Ask q)
+      | S n, Ask q => evalt_comp (λ l, τ (f q :: l)) f n depth
+      | _, Output o => Some (Output o) 
+      end
+    | None => None 
+    end.
+
+  Fact evalt_comp_tail (τ: tree) f m ans v:
+    seval (τ (ans ++ [])) m = Some (Output v) → 
+    evalt_comp (λ l' : list A, τ (ans ++ l')) f 0 m = Some (Output v) .
+  Proof.
+    intros H. cbn; destruct (seval (τ (ans ++ [])) m) eqn: E; last done.
+    destruct s; done.
+  Qed.
+
+  Lemma evalt_comp_ext (τ τ': tree) f n m:
+      (∀ l n, seval (τ l) n = seval (τ' l) n) → 
+      evalt_comp τ f n m = evalt_comp τ' f n m.
+  Proof.
+    intro Heq; induction n in τ, τ', Heq |- *; cbn.
+    - by rewrite <- Heq.
+    - rewrite <- Heq.
+      destruct (seval (A:=Q + O) (τ []) m); eauto.
+      destruct s; eauto.
+  Qed.
+
+  Lemma interrogation_ter (τ: tree) f l lv v:
+      interrogation τ (λ x y, f x = y) l lv → τ lv =! v →
+      ∃ m, ∀ ans_, ans_ `prefix_of` lv → ∃ v, seval (τ ans_) m = Some v.
+  Proof.  
+    intros H1 H2.
+    induction H1 in H2, v |-*. 
+    - rewrite seval_hasvalue in H2.
+      destruct H2 as [m Hm]. exists m.
+      intros ans_ Hans_. exists v.
+      apply prefix_nil_inv in Hans_.
+      rewrite Hans_. easy.
+    - rewrite seval_hasvalue in H2.
+      destruct H2 as [m Hm].
+      destruct (IHinterrogation (Ask q) H) as [m' Hm'].
+      exists (max m m').
+      intros ans_ Hans_.
+      destruct (list_cons_or Hans_) as [h| ->].
+      + destruct (Hm' ans_ h) as [v' Hv'].
+      exists v'. eapply seval_mono.
+      eauto. lia.
+      + exists v. eapply seval_mono; [eauto| lia].
+  Qed.
+
+  (** Basic property of evalt_comp **)
+
+  Lemma evalt_comp_depth_mono (τ: tree) f n m o:
+      evalt_comp τ f n m = Some o →
+      ∀ m', m ≤ m' → evalt_comp τ f n m' = Some o.
+  Proof.
+    intros H m' Hm'.
+    induction n in H, τ, o |-*; cbn in *.
+    - destruct (seval (A:=Q + O) (τ []) m) eqn: E; try congruence.
+      assert (seval (A:=Q + O) (τ []) m' = (Some s)) as ->.
+      eapply seval_mono. exact E. lia. done.
+    - destruct (seval (A:=Q + O) (τ []) m) eqn: E; last congruence.
+      assert (seval (A:=Q + O) (τ []) m' = Some s) as ->.
+      eapply seval_mono. exact E. lia.
+      destruct s. by apply IHn. exact H.
+  Qed.
+
+  Lemma interrogation_plus_evalt_comp (τ: tree) f n m l lv v2:
+      interrogation τ (λ x y, f x = y) l lv →
+      (∀ ans_, ans_ `prefix_of` lv -> ∃ v, seval (τ ans_) m = Some v) →
+      evalt_comp (λ l', τ (lv ++ l')) f n m = Some v2 ↔ 
+      evalt_comp τ f (length l + n) m = Some v2.
+  Proof.
+    intros H H1. split; revert n; dependent induction H; try eauto.
+    - intros. cbn -[evalt]. rewrite app_length. cbn -[evalt].
+      replace (length qs + 1 + n) with (length qs + (S n)) by lia.
+      eapply IHinterrogation. intros; apply H2.
+      etransitivity. exact H4. by eapply prefix_app_r.
+      cbn. rewrite app_nil_r.
+      destruct (H2 ans); first by eapply prefix_app_r.
+      assert (exists m, seval (τ ans) m = Some x).
+      by exists m. rewrite <- seval_hasvalue in H5.
+      assert (x = Ask q). { eapply hasvalue_det; eauto. }
+      rewrite H4, H6, H1, <- H3. eapply evalt_comp_ext.
+      intros; by list_simplifier.
+    - intros. rewrite app_length in H3. cbn in H3.
+      replace (length qs + 1 + n) with (length qs + (S n)) in H3 by lia.
+      eapply IHinterrogation in H3.
+      2: { intros; apply H2. etransitivity. exact H4.
+      by eapply prefix_app_r. }
+      cbn in H3. rewrite app_nil_r in H3.
+      destruct (H2 ans); first by eapply prefix_app_r.
+      assert (exists m, seval (τ ans) m = Some x) by by exists m.
+      rewrite <- seval_hasvalue in H5.
+      assert (x = Ask q). { eapply hasvalue_det; eauto. }
+      rewrite H4, H6, H1 in H3.
+      rewrite <- H3. eapply evalt_comp_ext.
+      intros; by list_simplifier.
+  Qed.
+
+  Lemma interrogation_plus_evalt_comp_1 (τ: tree) f n m l lv v:
+    interrogation τ (λ x y, f x = y) l lv →
+    evalt_comp τ f (length l + n) m = Some v →
+    evalt_comp (λ l', τ (lv ++ l')) f n m = Some v.
+  Proof.
+    intros H. revert n; dependent induction H; try eauto.
+    intros. rewrite app_length in H2. cbn in H2.
+    replace (length qs + 1 + n) with (length qs + (S n)) in H2 by lia.
+    eapply IHinterrogation in H2.
+    cbn in H2. rewrite app_nil_r in H2.
+    destruct (seval (τ ans) m) eqn: E; last done.
+    destruct s.
+    2: { exfalso. enough (Output o = Ask q) by done.
+    eapply hasvalue_det; eauto.
+    eapply seval_hasvalue. by exists m. }
+    rewrite <- H2. eapply evalt_comp_ext.
+    assert (q = q0) as [=<-].
+    { assert (τ ans =! Ask q0) by (eapply seval_hasvalue; by exists m).
+      by specialize (hasvalue_det H0 H3) as [=<-].  } 
+    intros l_ n_. rewrite H1.
+    by replace ((ans ++ [a]) ++ l_) with (ans ++ a :: l_) by by list_simplifier.
+  Qed.
+
+
+  Lemma evalt_comp_step_mono' τ f n m o:
+    evalt_comp τ f n m = Some (Output o) →
+    evalt_comp τ f (S n) m = Some (Output o) .
+  Proof.
+    induction n in o, τ |-*.
+    - cbn. destruct (seval (τ []) m); last done.
+      by destruct s.
+    - intros H. cbn in H.
+      cbn. destruct (seval (τ []) m); last done.
+      destruct s; last done.
+      apply (IHn _ _ H).
+  Qed.
+
+  Lemma evalt_comp_step_mono'' τ f n m o:
+    evalt_comp τ f n m = Some (Output o) →
+    ∀ n', n ≤ n' → evalt_comp τ f n' m = Some (Output o) .
+  Proof.
+    intros H n' Hn'.
+    induction Hn'; first done.
+    by eapply evalt_comp_step_mono'.
+  Qed.
+
+  Lemma evalt_comp_step_mono (τ: tree) f qs ans o:
+      interrogation τ (λ x y, f x = y) qs ans →
+      τ ans =! Output o →
+      ∃ depth step, ∀ g, interrogation τ (λ x y, g x = y) qs ans →
+      ∀ n', step ≤ n' → evalt_comp τ g n' depth = Some (Output o).
+  Proof.
+    intros H1 H2.
+    destruct (interrogation_ter H1 H2) as [step Hstep].
+    exists step. exists (length qs). intros g Hg n' Hn'.
+    assert (exists v, seval (τ ans) step = Some v) as [v Hv].
+    { eapply Hstep; naive_solver. }
+    assert (v = Output o).
+    { eapply hasvalue_det; [|eapply H2]. rewrite seval_hasvalue. eauto. }
+    eapply Nat.le_exists_sub in Hn' as [k [-> _]].
+    rewrite Nat.add_comm.
+    eapply interrogation_plus_evalt_comp; eauto.
+    induction k. all: cbn; rewrite app_nil_r; by rewrite Hv, H.
+  Qed.
+
+  Lemma evalt_comp_oracle_approx (τ: tree) f l lv v:
+      interrogation τ (λ x y, f x = y) l lv →
+      τ lv =! v →
+      ∃ step depth, ∀ g, interrogation τ (λ x y, g x = y) l lv →
+      evalt_comp τ g step depth = Some v.
+  Proof.
+    intros H1 h2.
+    destruct (interrogation_ter H1 h2) as [step Hstep].
+    exists (length l + 0), step.
+    intros. eapply interrogation_plus_evalt_comp; eauto.
+    cbn. rewrite app_nil_r.
+    destruct (Hstep lv) as [v' Hv']; first done.
+    assert (∃ k, seval (A:=Q + O) (τ lv) k = Some v') by by exists step.
+    rewrite <- seval_hasvalue in H0.
+    assert (v' = v) by by eapply hasvalue_det.
+    rewrite Hv', H2. by destruct v.
+  Qed.
+
+  Lemma interrogation_evalt_comp_limit (τ: tree) f l lv v:
+      (∞∀ k, interrogation τ (λ x y, f k x = y) l lv) →
+      τ lv =! Output v →
+      ∞∀ n, evalt_comp τ (f n) n n = Some (Output v).
+  Proof.
+    intros [k h1] h2.
+    assert (interrogation τ (λ x y, f k x = y) l lv) as H.
+    apply h1. lia.
+    destruct (evalt_comp_oracle_approx H h2) as (a & b & Hab).
+    exists (max b (max a k)).
+    intros n Hn. eapply evalt_comp_depth_mono.
+    eapply evalt_comp_step_mono''.
+    eapply (Hab (f n)); eauto. eapply h1.
+    all: lia.
+  Qed.
+
+  Lemma evalt_comp_to_interrogation (τ : tree) (f : Q → A) o n depth:
+      eq_dec O → eq_dec Q →
+      (Σ qs ans, evalt_comp τ f n depth = Some (Output o) ∧
+      length qs ≤ n ∧ interrogation τ (λ q a, f q = a) qs ans ∧ τ ans =! Output o)
+       + 
+      (evalt_comp τ f n depth ≠ Some (Output o)).
+  Proof.
+    intros eq_dec_O eq_dec_Q.
+    destruct (Dec (evalt_comp τ f n depth = Some (Output o))) as [H|H]; last by right.
+    left. induction n in τ, H |- *.
+    * cbn in *. destruct (seval (τ []) depth) eqn: E.
+      exists [], []. repeat split; eauto. econstructor.
+      destruct s. congruence.  rewrite seval_hasvalue.
+      by exists depth; injection H as ->. congruence.
+    * cbn in *.  destruct (seval (τ []) depth) eqn: E; try congruence.
+      destruct s; try congruence.
+      - eapply (IHn (λ l, τ (f q :: l))) in H as (qs & ans & H3 & H1 & H2 & H').
+        exists (q :: qs), (f q :: ans). split; last split; eauto. cbn; lia. repeat split.
+        eapply interrogation_app with (q1 := [q]) (a1 := [f q]).
+        eapply Interrogate with (qs := []) (ans := []); eauto. econstructor.
+        rewrite seval_hasvalue. by exists depth.
+        eauto. eauto.
+      - exists [], []. repeat split; try split; cbn. easy. lia. eauto. econstructor.
+        rewrite seval_hasvalue.
+        by exists depth; injection H as ->.
+  Qed.
+
+  Fact sub_tree (τ: tree) f use ans ans_:
+    interrogation τ (λ x y, f x = y) use ans →
+    ans_ `prefix_of` ans →
+    ∃ use_ : list Q, interrogation τ (λ x y, f x = y) use_ ans_ ∧ 
+      length use_ = length ans_.
+  Proof.
+  intros H1 [Hl].
+  dependent induction H1.
+  - assert (ans_ = []).
+    { eapply prefix_nil_inv; eauto. exists (Hl). done. } subst.
+    exists []. split. econstructor. done.
+  - destruct Hl. list_simplifier. exists (qs ++ [q] ).
+    split. econstructor; eauto. rewrite !app_length.
+    cbn. f_equal. eapply interrogation_length. done.
+    list_simplifier.
+    apply app_eq_inv in H2. destruct H2 as [[k [Hk Hk']]|[k [Hk Hk']]].
+    + eapply (IHinterrogation k). done.
+    + assert (k = []). destruct k; first done.
+      list_simplifier. by eapply app_cons_not_nil in H2.
+      list_simplifier.  eapply (IHinterrogation []).
+      list_simplifier. done.
+  Qed.
+
+  Fact sub_tree_2 (τ: tree) f use ans use_:
+    interrogation τ (λ x y, f x = y) use ans →
+      use_ `prefix_of` use →
+    ∃ ans_ : list A, interrogation τ (λ x y, f x = y) use_ ans_ ∧ 
+      length use_ = length ans_.
+  Proof.
+  intros H1 [Hl].
+  dependent induction H1.
+  - assert (use_ = []).
+    { eapply prefix_nil_inv; eauto. exists (Hl). done. } subst.
+    exists []. split. econstructor. done.
+  - destruct Hl. list_simplifier. exists (ans ++ [f q] ).
+    split. econstructor; eauto. rewrite !app_length.
+    cbn. f_equal. eapply interrogation_length. done.
+    list_simplifier.
+    apply app_eq_inv in H2. destruct H2 as [[k [Hk Hk']]|[k [Hk Hk']]].
+    + eapply (IHinterrogation k). done.
+    + assert (k = []). destruct k; first done.
+      list_simplifier. by eapply app_cons_not_nil in H2.
+      list_simplifier.  eapply (IHinterrogation []).
+      list_simplifier. done.
+  Qed.
+
+  Fact sub_tree_3 (τ: tree) f use ans use_:
+    interrogation τ (λ x y, f x = y) use ans →
+    use_ `prefix_of` use →
+    length use_ < length use →
+    ∃ ans_ : list A, interrogation τ (λ x y, f x = y) use_ ans_ ∧ 
+      length use_ = length ans_
+      ∧ ∃ q, τ ans_ =! Ask q.
+  Proof.
+  intros H1 [Hl] Hlen.
+  dependent induction H1.
+  - assert (use_ = []).
+    { eapply prefix_nil_inv; eauto. exists (Hl). done. } subst.
+    cbn in Hlen. lia.
+  - destruct Hl. list_simplifier. lia.
+    list_simplifier.
+    apply app_eq_inv in H2. destruct H2 as [[k [Hk Hk']]|[k [Hk Hk']]].
+    + rewrite Hk in Hlen. destruct k.
+      2:{ apply (IHinterrogation (q1::k)). done. list_simplifier.
+      rewrite app_length. cbn. lia. }
+      list_simplifier. subst. exists ans. split. done.
+      split. eapply interrogation_length. done.
+      exists q. done.
+    + assert (k = []). destruct k; first done.
+      list_simplifier. by eapply app_cons_not_nil in H2.
+      list_simplifier.
+      exists ans. split. done.
+      split. eapply interrogation_length. done.
+      exists q0. done.
+  Qed.
+
+
+  Fact sub_computation_ter (τ: tree) n m f use ans v :
+    length ans ≤ n →
+    evalt_comp τ f n m = Some v →
+    interrogation τ (λ x y, f x = y) use ans →
+    ∀ ans_, ans_ `prefix_of` ans →
+    ∃ v : Q + O, seval (τ ans_) m = Some v.
+  Proof.
+    intros Hn Hcomp Hin ans_ Hans_.
+    assert (∃ k, length ans_ + k = n) as [k Hk].
+    { apply prefix_length in Hans_. exists (n - length ans_). lia. }
+    rewrite <-Hk in Hcomp.
+    specialize (sub_tree Hin Hans_) as (use_ & Huse_ & HEU).
+    rewrite <- HEU in Hcomp.
+    specialize (interrogation_plus_evalt_comp_1 Huse_ Hcomp) as H.
+    { destruct k. cbn in H. destruct (seval (τ (ans_ ++ [])) m) eqn: E; last done.
+      list_simplifier. by exists s.
+      cbn in H.  destruct (seval (τ (ans_ ++ [])) m) eqn: E; last done.
+      list_simplifier. by exists s.
+    }
+  Qed.
+
+  Lemma evalt_comp_roll_back (τ: tree) f n m v qs ans q a:
+    interrogation τ (λ x y, f x = y) (qs++[q]) (ans++[a]) →
+    length qs = n →
+    evalt_comp τ f (S n) m = Some v ↔ 
+    evalt_comp τ f n m = Some (Ask q) ∧ seval (τ (ans ++ [f q])) m = Some v.
+  Proof.
+    intro H. inv H.
+    { exfalso. by apply app_cons_not_nil in H1. }
+    apply app_inj_tail in H0. destruct H0 as [H61 H62].
+    apply app_inj_tail in H1. destruct H1 as [H71 H72]. subst.
+    intros H. subst. split.
+    - intros H.
+      assert (evalt_comp τ f (S (length qs)) m = Some v) as Hcopy by eauto.
+      replace (S (length qs)) with (length qs + 1) in H by lia.
+      eapply interrogation_plus_evalt_comp_1 in H; eauto.
+      replace ((length qs)) with (length qs + 0) by lia.
+      rewrite <- interrogation_plus_evalt_comp; eauto.
+      cbn in *.  destruct (seval (τ (ans ++ [])) m) eqn: E; last done.
+      split. 
+      destruct s; eauto.
+
+      { f_equal. eapply hasvalue_det; eauto. eapply seval_hasvalue. exists m.
+        list_simplifier. done. }
+      { f_equal. eapply hasvalue_det; eauto. eapply seval_hasvalue. exists m.
+      list_simplifier. done.  }
+      destruct s; last first.
+      { exfalso. list_simplifier. assert (Output o = Ask q).
+        eapply hasvalue_det.  eapply seval_hasvalue. exists m. done. done. congruence. }
+        enough (q = q0) as <-.
+        destruct (seval (τ (ans ++ [f q])) m); last done.
+        destruct s; eauto.
+      { list_simplifier. assert (τ ans =! Ask q0). eapply seval_hasvalue; eauto.
+        specialize (hasvalue_det H3 H0). intros [=]. eauto. }
+      unshelve eapply (sub_computation_ter _ Hcopy); eauto.
+      rewrite (interrogation_length H2); lia.
+
+    - intros [He Ho]. 
+      replace (S (length qs)) with (length qs + 1) by lia.
+      eapply interrogation_plus_evalt_comp; eauto.
+      unshelve eapply (sub_computation_ter _ He); eauto.
+      rewrite (interrogation_length H2); lia.
+      replace ((length qs)) with (length qs + 0) in He by lia.
+      eapply interrogation_plus_evalt_comp_1 in He ; eauto.
+      cbn in *. destruct (seval (τ (ans ++ [])) m); last done.
+      destruct s; last congruence.
+      injection He. intros ->.
+      destruct (seval (τ (ans ++ [f q])) m); last done.
+      destruct s; last congruence.
+      congruence.
+  Qed.
+
+  Fact boring_decomposition {X} (qs: list X) n:
+    n < length qs →
+    ∃ q other qs_, length qs_ = n ∧ qs = qs_ ++ q :: other.
+  Proof.
+    intros H.
+    induction qs in n, H |- *.
+    - cbn in *. lia.
+    - destruct n.
+      + cbn. exists a, qs, []. done.
+      + cbn. destruct (IHqs n) as [q [other [qs_ [H1 H2]]]]. cbn in H. lia.
+        exists q, other, (a :: qs_); split.
+        cbn. lia. list_simplifier. done.
+  Qed.
+
+  Lemma evalt_comp_step_length (τ: tree) f n m v qs ans:
+    interrogation τ (λ x y, f x = y) qs ans →
+    τ ans =! Output v →
+    evalt_comp τ f n m = Some (Output v) →
+    length qs ≤ n.
+  Proof.
+    intros Hin Hans Hev.
+    assert (length qs ≤ n ∨ length qs > n) as [H|H] by lia; first done.
+    destruct (@boring_decomposition _ qs n) as (q&other&qs_&Hqs_&Hq). lia.
+    assert (qs_ `prefix_of` qs) as Hqs.
+    { exists (q :: other). list_simplifier. done. }
+    replace n with (length qs_ + 0) in Hev by lia.
+    destruct (sub_tree_3 Hin Hqs) as [ans_ [Ha1 [Ha2 [q' Hq']]]]; first lia.
+    eapply interrogation_plus_evalt_comp_1 in Hev; eauto.
+    cbn in Hev. destruct (seval (τ (ans_ ++ [])))eqn: E; last done.
+    destruct s. congruence.
+    enough (Output o = Ask q') by congruence.
+    { eapply hasvalue_det. eapply seval_hasvalue. exists m. done.
+    list_simplifier. apply Hq'. }
+  Qed.
+
+  Lemma final_fact_gen (τ: tree) m f g use ans:
+  interrogation τ (λ x y, f x = y) use ans → 
+  interrogation τ (λ x y, g x = y) use ans → 
+  ∀ v n,
+    evalt_comp τ f n m = Some v →
+    length use = n →
+    (∀ u, u ∈ use -> f u = g u) →
+    evalt_comp τ g n m = Some v.
+  Proof.
+    induction 1; intros.
+    { subst. simpl in *. done. }
+    assert (interrogation τ (λ x y, f x = y) (qs ++ [q]) (ans ++ [a])) by
+      (econstructor; eauto). 
+
+    (* prepare the hypothesis *)
+    rewrite last_length in *.
+    destruct n; first congruence.
+    destruct (evalt_comp_roll_back m v H6 eq_refl) as [Hc1 _].
+    destruct (evalt_comp_roll_back m v H2 eq_refl) as [_ Hc2].
+    assert (length qs = n) as H' by lia. subst.
+    destruct (Hc1 H3) as (Hc&Hcq).
+
+    inv H2. 
+    (* inverse the second interrogation *)
+    { exfalso. by apply app_cons_not_nil in H7. }
+    apply app_inj_tail in H1. destruct H1 as [H61 H62].
+    apply app_inj_tail in H7. destruct H7 as [H71 H72]. subst.
+    specialize (IHinterrogation H8 (Ask q) (length qs) Hc eq_refl).
+
+    (* inverse the goal *)
+    apply Hc2. split.
+    + eapply IHinterrogation. intros. eapply H5. 
+      rewrite elem_of_app; by left.
+    + enough (g q = f q) as -> by done.
+      symmetry. eapply H5.
+      rewrite elem_of_app. right.
+      by rewrite elem_of_list_singleton.
+  Qed.
+
+  Fact there_is_a_computation (τ: tree) n m f use ans v:
+    interrogation τ (λ x y, f x = y) use ans → 
+    τ ans =! Output v → 
+    evalt_comp τ f n m = Some (Output v) →
+    evalt_comp τ f (length use) m = Some (Output v).
+  Proof.
+    intros H1 H2 H3.
+    specialize (evalt_comp_step_length H1 H2 H3) as Hn.
+    assert (∃ k, length use + k = n) as [k Hk] by (exists (n - length use); lia).
+    clear Hn. rewrite <- Hk in H3.
+    specialize (interrogation_plus_evalt_comp_1 H1 H3) as H.
+    assert (seval ( (λ l', τ (ans ++ l')) []) m = Some (Output v)).
+    { destruct k. cbn in H. destruct (seval (τ (ans ++ [])) m) eqn: E; last done. 
+      destruct s; congruence. cbn in H. 
+      destruct (seval (τ (ans ++ [])) m) eqn: E; last done. destruct s; eauto.
+      list_simplifier .
+      assert (τ ans =! Ask q). by eapply seval_hasvalue'.
+      specialize (hasvalue_det H2 H0). congruence. }
+    specialize (evalt_comp_tail f H0) as H'.
+    assert (length use = length use + 0) as -> by lia.
+    rewrite <- interrogation_plus_evalt_comp; eauto.
+    eapply (sub_computation_ter _ H3); eauto.
+    Unshelve. rewrite (interrogation_length H1).  lia.
+  Qed.
+
+  Lemma final_fact' (τ: tree) m f g use ans v:
+    evalt_comp τ f (length use) m = Some (Output v) →
+    interrogation τ (λ x y, f x = y) use ans → 
+    interrogation τ (λ x y, g x = y) use ans →
+    τ ans =! Output v → 
+    evalt_comp τ g (length use) m = Some (Output v).
+  Proof.
+    intros Hf H1 H2 Ho.
+    eapply (final_fact_gen H1 H2 Hf); eauto. 
+    intros u Hu. clear Ho Hf.
+    induction H1; first by apply not_elem_of_nil in Hu.
+    inv H2; first by apply app_cons_not_nil in H4.
+    apply app_inj_tail in H3.
+    apply app_inj_tail in H4.
+    destruct H3, H4; subst.
+    apply elem_of_app in Hu. 
+    destruct Hu as [Hu1| Hu2%elem_of_list_singleton]; last by rewrite Hu2, H4.
+    apply IHinterrogation; eauto.
+  Qed.
+
+  Lemma final_fact (τ: tree) n m f g use ans v:
+    evalt_comp τ f n m = Some (Output v) →
+    interrogation τ (λ x y, f x = y) use ans → 
+    interrogation τ (λ x y, g x = y) use ans →
+    τ ans =! Output v → 
+    evalt_comp τ g n m = Some (Output v).
+  Proof.
+    intros Hf H1 H2 Ho.
+    specialize (evalt_comp_step_length H1 Ho Hf) as Hn.
+    apply (there_is_a_computation H1) in Hf; last done.
+    eapply evalt_comp_step_mono''.
+    eapply final_fact'; eauto. done. 
+  Qed.
+
+End Step_Eval.
+
+Section Use_Function.
+
+Lemma extract_computation {Q O: Type} (τ: (list bool) ↛ (Q + O)) (f: Q → bool) n m v: 
+  eq_dec O → eq_dec Q →
+  evalt_comp τ f n m = Some (inr v) →  
+  Σ use ans, 
+    τ ans =! inr v ∧
+    ∀ P, (∀ q, q ∈ use → P q ↔ f q = true) → 
+    interrogation τ (char_rel P) use ans .
+Proof.
+  intros He H_ H_'.
+  destruct (evalt_comp_to_interrogation τ f v n m) as [(qs&ans&H3&_&H1&H2)|H]; try done.
+  exists qs, ans.
+  split; first done.
+  intros p Hp.
+  eapply interrogation_ext; last exact H1; eauto.
+  intros q' [|] Hqa'%elem_of_list_In; cbn; first by rewrite Hp.
+  specialize (Hp q' Hqa'). split.
+  - intros H. destruct (f q') eqn: E; last done.
+    enough (p q') by easy. by rewrite Hp.
+  - intros H H'%Hp. congruence.
+Qed.
+
+Lemma use_function' {Q O: Type} (τ: (list bool) ↛ (Q + O)) (f: Q → bool) n m v:
+  eq_dec O → eq_dec Q →
+  (evalt_comp τ f n m = Some (inr v)) + (evalt_comp τ f n m ≠ Some (inr v)).
+Proof.
+  intros h1 h2. 
+  destruct (evalt_comp_to_interrogation τ f v n m) as [(qs&ans&H3&_&H1&H2)|H]; intuition done.
+Qed.
+
+(* Lemma evalt_comp_ext_strong (τ τ': tree) f n m:
+(∀ l n, seval (τ l) n = seval (τ' l) n) → 
+(∀ (q_ : Q) (a0 : A), In q_ q → f q_ a0 ↔ f' q_ a0) →
+evalt_comp τ f n m = evalt_comp τ' f n m.
+Proof.
+intro Heq; induction n in τ, τ', Heq |- *; cbn.
+- by rewrite <- Heq.
+- rewrite <- Heq.
+  destruct (seval (A:=Q + O) (τ []) m); eauto.
+  destruct s; eauto.
+Qed. *)
+
+
+  Lemma use_function {Q O: Type} (τ: (list bool) ↛ (Q + O)) (f: Q → bool) n m v:
+    eq_dec O → eq_dec Q →
+    (Σ use, 
+    evalt_comp τ f n m = Some (inr v) ∧
+    ∀ P, (∀ q, q ∈ use → P q ↔ f q = true) → 
+      ∃ ans, interrogation τ (char_rel P) use ans ∧ τ ans =! inr v)  +
+    (evalt_comp τ f n m ≠ Some (inr v)).
+  Proof.
+    intros h1 h2. 
+    destruct (evalt_comp_to_interrogation τ f v n m) as [(qs&ans&H3&_&H1&H2)|H]; try done.
+    left. exists qs. split; first easy. intros P HqP.
+    exists ans; split; last done.
+    eapply interrogation_ext; [eauto| |apply H1].
+    intros q' [|] Hqa'%elem_of_list_In; cbn; first by rewrite HqP.
+    specialize (HqP q' Hqa'). split.
+    - intros H. destruct (f q') eqn: E; last done.
+      enough (P q') by easy. by rewrite HqP.
+    - intros H H'%HqP. congruence.
+    - right. done.
+  Qed.
+
+
+End Use_Function.
+
+Section Limit_Interrogation.
+
+  Variable Q: Type.
+  Variable P: Q → Prop.
+
+  Definition stable (f: nat → Q → bool) :=
+    ∀ q n m, n ≤ m → f n q = true → f m q = true.
+
+  Fixpoint stabilize_step (f: Q -> nat -> bool) x n :=
+    match n with
+    | O => false
+    | S n => if f x n then true else stabilize_step f x n
+    end.
+
+  Definition stable_semi_decider (f: nat → Q → bool) :=
+    semi_decider (λ x n, f n x) P ∧ stable f.
+
+  Fact semi_decider_to_stable: ∀ f, semi_decider f P → Σ g, stable_semi_decider g.
+  Proof.
+    intros f S_P. exists (λ n x, stabilize_step f x n); split.
+    - intro x; split; intro h.
+      rewrite (S_P x) in h.
+      destruct h as [c Hc].
+      by exists (S c); cbn; rewrite Hc.
+      rewrite (S_P x).
+      destruct h as [c Hc].
+      induction c; cbn in Hc; [congruence|].
+      destruct (f x c) eqn: E; [now exists c|now apply IHc].
+    - intros x n m Lenm Hn.
+      induction Lenm; [trivial|].
+      cbn; destruct (f x m) eqn: E; [trivial|assumption].
+  Qed.
+
+  Definition approx_Σ1 O  (f: nat → Q → bool) :=
+      ∀ (τ: list bool ↛ (Q + O)) qs ans,
+        interrogation τ (char_rel P) qs ans → 
+        ∞∀ m, interrogation τ (λ q a, f m q = a) qs ans.
+
+  Definition approx_Σ1_rev O (f: nat → Q → bool) :=
+      ∀ (τ: list bool ↛ (Q + O)) qs ans,
+        (∞∀ m, interrogation τ (λ q a, f m q = a) qs ans) →
+        interrogation τ (char_rel P) qs ans.
+
+  Definition approx_list (f: Q → bool) L :=
+      ∀ i, In i L → P i ↔ f i = true.
+
+  Definition approx_list_func (f g: Q → bool) L :=
+      ∀ i, In i L → f i ↔ g i.
+
+  Variable g: nat → Q → bool.
+  Hypothesis S_P: stable_semi_decider g.
+
+  Definition S_approx_Σ1: ∀ O, approx_Σ1 O g.
+  Proof.
+    destruct S_P as [H1 H2]; intros O τ qs ans Hτ.
+    induction Hτ.
+    - exists 0; intros; econstructor.
+    - destruct IHHτ as [w Hw].
+      destruct a; cbn in H0.
+      + rewrite (H1 q) in H0. destruct H0 as [m Hm].
+        exists (S (max w m)). intros m' Hm'.
+        econstructor. eapply Hw; first lia.
+        assumption. eapply H2; last apply Hm. lia.
+      + exists w; intros m Hm.
+        econstructor. eapply Hw; first done.
+        assumption. destruct (g m q) eqn: E; last done.
+        enough (P q) by done. { rewrite (H1 q). by exists m. }
+  Qed.
+
+  Lemma approx_Σ1_list: definite P → ∀ L, ∞∀ c, approx_list (g c) L.
+  Proof.
+    destruct S_P as [S_p HS].
+    intros def_p l. induction l as [|a l [c Hc]].
+    - exists 42; firstorder.
+    - destruct (def_p a) as [h1| h2].
+      + destruct (S_p a) as [H _].
+        destruct (H h1) as [N HN].
+        exists (max c N); intros c' Hc' e [->| He].
+        split; [intros _|easy].
+        eapply HS; [|eapply HN]; lia.
+        unfold approx_list in Hc.
+        rewrite (Hc c'); [trivial|lia | assumption].
+      + exists c; intros c' Hc' e [->| He].
+        split; [easy| intros h'].
+        unfold semi_decider in S_p.
+        rewrite S_p. by exists c'.
+        unfold approx_list in Hc.
+        rewrite Hc; eauto.
+  Qed.
+
+  Lemma approx_Σ1_list_rev: (∀ L, ∞∀ c, approx_list (g c) L) → definite P.
+  Proof.
+    intros H x.
+    destruct (H [x]) as [k Hk].
+    destruct (Hk k (le_n k) x); first done.
+    destruct (g k x) eqn: E.
+    left. apply H1. easy.
+    right. intro H'. 
+    by apply H0 in H'.
+  Qed.
+
+  Definition S_approx_Σ1_rev: definite P → ∀ O, approx_Σ1_rev O g.
+  Proof.
+    intros defp O τ qs ans [w Hw].
+    assert (∞∀ k, ∀ q, In q qs → P q ↔ g k q = true) as [k Hk] by by apply approx_Σ1_list.
+    assert (interrogation τ (λ q a, g (max w k) q = a) qs ans) as H by (apply Hw; lia).
+    clear Hw. induction H; first econstructor.
+    econstructor; [|done|].
+    eapply IHinterrogation.
+    { intros. rewrite Hk; try done. apply in_app_iff. by left. }
+    destruct a; cbn; rewrite Hk; try (done||lia).
+    rewrite in_app_iff; right; econstructor. done.
+    intro H'. enough (g (w`max`k) q = true) by congruence.
+    destruct S_P as [H1' H2]. eapply H2; last apply H'. lia.
+    rewrite in_app_iff; right; econstructor. done.
+  Qed.
+
+End Limit_Interrogation.
+
+
+Section Step_Eval_Spec.
+
+  (** ** Step-Inedxed Execution *)
+
+  Definition Φ_ (f: nat → nat → bool) (e x n: nat): option () :=
+    match evalt_comp (ξ () e x) (f n) n n with
+    | Some (inr ()) => Some ()
+    | _ => None 
+    end.
+
+
+
+  Variable P: nat → Prop.
+  Variable decider: nat → nat → bool.
+  Hypothesis S_P: stable_semi_decider P decider.
+
+  Fact phi_iff_evalt f e x n :
+    Φ_ f e x n = Some () ↔ evalt_comp (ξ () e x) (f n) n n = Some (inr ()).
+  Proof.
+    unfold Φ_. destruct (evalt_comp (ξ () e x) (f n) n n) eqn: E; [destruct s|].
+    - split; congruence.
+    - destruct u. done.
+    - split; congruence.
+  Qed.
+
+  Theorem Φ_spec e x:
+      Ξ e (char_rel P) x → (∞∀ n, Φ_ decider e x n = Some ()).
+  Proof.
+    unfold Ξ, rel. intros (qs & ans & Ha & Hb).
+    specialize (@S_approx_Σ1 _ _ _ S_P () (ξ _ e x) qs ans Ha) as H.
+    eapply interrogation_evalt_comp_limit in H; last apply Hb.
+    destruct H as [w Hw].
+    exists w; intros m Hm. unfold Φ_. specialize (Hw m Hm).
+    destruct (evalt_comp (ξ () e x) (decider m) m m).
+    destruct s. by injection Hw.
+    by destruct u. congruence.
+  Qed. 
+  
+  (** ** Use Functions *)
+
+    Notation "A ≡{ k }≡ B" := (∀ x, x ≤ k → A x ↔ B x) (at level 30).
+    Definition to_pred (f: nat → bool) x := f x = true.
+
+    Definition φ (f: nat → bool) (e x n: nat) :=
+      if use_function (ξ () e x) f n n () unit_eq_dec nat_eq_dec 
+        is inl H then S (list_max (projT1 H))
+        else 0.
+
+    Definition φ' (f: nat → bool) (e x n: nat) :=
+      if (use_function' (ξ () e x) f n n () unit_eq_dec nat_eq_dec) 
+        is inl H then S (list_max (projT1 (extract_computation unit_eq_dec nat_eq_dec H)))
+        else 0.
+
+  Theorem φ_spec e x n p:
+    Φ_ decider e x n = Some () →
+    p ≡{φ (decider n) e x n}≡ to_pred (decider n) →
+    Ξ e (char_rel p) x.
+  Proof.
+    intros H2 H1. rewrite phi_iff_evalt in H2. unfold φ in H1. 
+    destruct (use_function (ξ () e x) (decider n) n n _ _ _) as [(ans&Hans)|H]; last done.
+    exists ans. eapply Hans.
+    intros q [i Hq]%elem_of_list_lookup_1. rewrite H1; first done.
+    simpl. enough (q ≤ list_max (ans)) by lia.
+    eapply implementation.list_max_lookup. 
+    eapply Hq.
+  Qed.
+
+  Theorem φ'_spec e x n p:
+    Φ_ decider e x n = Some () →
+    p ≡{φ' (decider n) e x n}≡ to_pred (decider n) →
+    Ξ e (char_rel p) x.
+  Proof.
+    intros H2 H1. rewrite phi_iff_evalt in H2. unfold φ' in H1. 
+    destruct (use_function' (ξ () e x) (decider n) n n () _ _) as [H'|H]; last done.
+    destruct (extract_computation unit_eq_dec nat_eq_dec H') as [qs [ans [Hans1 Hans2]]].
+    simpl in H1.
+    exists qs, ans; split; eauto.
+    eapply Hans2.
+    intros q [i Hq]%elem_of_list_lookup_1. rewrite H1; first done.
+    simpl. enough (q ≤ list_max (qs)) by lia. 
+    eapply implementation.list_max_lookup. 
+    eapply Hq.
+  Qed.
+
+  Lemma φ_spec0_1 e x n:
+    φ (decider n) e x n ≠ 0 → Φ_ decider e x n = Some ().
+  Proof.
+    unfold φ, Φ_. intros H. 
+    destruct (use_function (ξ () e x) (decider n) n n () unit_eq_dec nat_eq_dec).
+    - clear H. by destruct s as (_&->&_). 
+    - congruence.
+  Qed.
+
+  Lemma φ_spec0_2 e x n:
+    Φ_ decider e x n = Some () → φ (decider n) e x n ≠ 0.
+  Proof.
+    unfold φ, Φ_. intros H. 
+    destruct (use_function (ξ () e x) (decider n) n n () unit_eq_dec nat_eq_dec).
+    - lia.
+    - destruct (evalt_comp (ξ () e x) (decider n) n n); last eauto.
+      destruct s; eauto. destruct u. congruence.
+  Qed.
+
+  Theorem φ_spec0 e x n: φ (decider n) e x n ≠ 0 ↔ Φ_ decider e x n = Some ().
+  Proof. split; [apply φ_spec0_1|apply φ_spec0_2]. Qed.
+
+  Theorem φ_spec0' e x n: φ (decider n) e x n = 0 ↔ Φ_ decider e x n = None.
+  Proof.
+    destruct (φ_spec0 e x n) as [H1 H2]. split; intros H.
+    - destruct (φ (decider n) e x n); eauto.
+      destruct (Φ_ decider e x n); eauto.
+      destruct u; eauto. enough (0≠0) by congruence.
+      by eapply H2.
+    - destruct (Φ_ decider e x n); try congruence.
+      destruct (φ (decider n) e x n); eauto.
+      enough (None = Some ()) by congruence.
+      by eapply H1.
+  Qed.
+
+  Fact char_rel_boring n:
+    ∀ q a, char_rel (decider n) q a ↔ (λ x y, decider n x = y) q a.
+  Proof. intros. unfold char_rel. destruct a, (decider n q); intuition. Qed. 
+
+
+  Theorem φ_spec1 e x n k :
+    φ (decider n) e x n = S k →
+    to_pred (decider n) ≡{k}≡ to_pred (decider (S n)) →
+    φ (decider (S n)) e x (S n) = S k.
+  Proof.
+    intros H H2. unfold φ in *.
+    destruct (use_function (ξ () e x) (decider n) n n) 
+      as [(use & Hu1 & Hu2)|]; last congruence. simpl in *.
+
+    assert (∀ q, q ∈ use → decider (S n) q ↔ decider n q = true) as boring1.
+      { intros q Hq. destruct (H2 q). apply elem_of_list_lookup_1 in Hq.
+      destruct Hq as [i Hi]. injection H; intros <-.
+      by eapply implementation.list_max_lookup.
+      unfold to_pred in *. destruct (decider (S n) q); intuition. }
+
+    assert (∀ q a, In q use → char_rel (decider n) q a ↔ char_rel (decider (S n)) q a) as boring2.
+      { intros q a Hq. destruct (H2 q). rewrite <-elem_of_list_In in Hq.
+        apply elem_of_list_lookup_1 in Hq. destruct Hq as [i Hi].
+        injection H; intros <-. by eapply implementation.list_max_lookup.
+        unfold to_pred, char_rel in *.  
+        destruct a, (decider (S n) q), (decider n q); intuition. }
+
+    destruct (Hu2 (decider (S n)) boring1) as [ans (Hans & Hans1)].
+
+    destruct (use_function (ξ () e x) (decider (S n)) (S n) (S n)) as [(use' & Hu1' & Hu2')|HSn].
+    + destruct (Hu2' (decider (S n))) as [ans' (Hans' & Hans1')].
+      { intros; destruct (decider (S n) q); intuition. }
+      enough (use = use') as Hanseq. 
+      { cbn. rewrite <- Hanseq. apply H. }
+      assert (functional (char_rel (decider (S n)))) as _H_. 
+      { intros ?[][]; unfold to_pred, char_rel; eauto. }
+      by edestruct (interrogation_eq 42 true _H_ Hans Hans1 Hans' Hans1').
+    + exfalso; apply HSn. 
+      assert (interrogation (ξ () e x) (λ q a, decider n q = a) use ans) as Hansn.
+      { eapply interrogation_ext; last apply Hans; first done. intros.
+        rewrite <- char_rel_boring. by apply boring2. }
+      assert (n ≤ S n) as _H_ by lia.
+      unshelve eapply (evalt_comp_depth_mono _ _H_).
+      eapply (evalt_comp_step_mono').
+      assert (interrogation (ξ () e x) (λ q a, decider (S n) q = a) use ans) as HansSn.
+      { eapply interrogation_ext; last apply Hans; first done. intros; by rewrite char_rel_boring. }
+      clear Hu2 S_P HSn boring1 boring2 H H2 _H_ Hans. 
+      eapply final_fact; eauto.
+  Qed.
+
+  Theorem φ_spec2 e x n k :
+    φ (decider n) e x n = S k →
+    to_pred (decider n) ≡{k}≡ to_pred (decider (S n)) →
+    Φ_ decider e x (S n) = Some ().
+  Proof.
+    intros H H2. unfold φ in *.
+    destruct (use_function (ξ () e x) (decider n) n n) 
+      as [(use & Hu1 & Hu2)|]; last congruence. simpl in *.
+
+    destruct (evalt_comp (ξ () e x) (decider n) n n) eqn: E1; last congruence.
+    destruct s eqn: E2; first congruence.
+    destruct u; clear Hu1 E2. 
+    unfold Φ_; enough (evalt_comp (ξ () e x) (decider (S n)) (S n) (S n) = Some (inr ())) as H'
+      by by rewrite H'.
+    eapply evalt_comp_step_mono'.
+    eapply evalt_comp_depth_mono; last exact (le_S _ _ (le_n n)).
+
+    assert (∀ q, q ∈ use → decider (S n) q ↔ decider n q = true) as boring1.
+    { intros q Hq. destruct (H2 q). apply elem_of_list_lookup_1 in Hq.
+    destruct Hq as [i Hi]. injection H; intros <-.
+    by eapply implementation.list_max_lookup.
+    unfold to_pred in *. destruct (decider (S n) q); intuition. }
+
+    assert (∀ q a, In q use → char_rel (decider n) q a ↔ char_rel (decider (S n)) q a) as boring2.
+      { intros q a Hq. destruct (H2 q). rewrite <-elem_of_list_In in Hq.
+        apply elem_of_list_lookup_1 in Hq. destruct Hq as [i Hi].
+        injection H; intros <-. by eapply implementation.list_max_lookup.
+        unfold to_pred, char_rel in *.  
+        destruct a, (decider (S n) q), (decider n q); intuition. }
+
+    destruct (Hu2 (decider (S n)) boring1) as [ans (Hans & Hans1)].
+    assert (interrogation (ξ () e x) (λ q a, decider n q = a) use ans) as Hansn.
+    { eapply interrogation_ext; last apply Hans; first done. intros.
+      rewrite <- char_rel_boring. by apply boring2. }
+    assert (n ≤ S n) as _H_ by lia.
+    assert (interrogation (ξ () e x) (λ q a, decider (S n) q = a) use ans) as HansSn.
+    { eapply interrogation_ext; last apply Hans; first done. intros; by rewrite char_rel_boring. }
+    eapply final_fact; eauto.
+  Qed.
+
+End Step_Eval_Spec.
+
+
+
+
+
+
+
diff --git a/theories/PostsProblem/the_priority_method.v b/theories/PostsProblem/the_priority_method.v
new file mode 100644
index 0000000..40fd14b
--- /dev/null
+++ b/theories/PostsProblem/the_priority_method.v
@@ -0,0 +1,512 @@
+From SyntheticComputability Require Import ArithmeticalHierarchySemantic reductions SemiDec TuringJump OracleComputability Definitions limit_computability simple.
+From stdpp Require Export list.
+Require Import SyntheticComputability.Synthetic.DecidabilityFacts.
+Require Export SyntheticComputability.Shared.FinitenessFacts.
+Require Export SyntheticComputability.Shared.Pigeonhole.
+Require Export SyntheticComputability.Shared.ListAutomation.
+Require Import Arith Arith.Compare_dec Lia Coq.Program.Equality List.
+Import ListNotations.
+
+(* ########################################################################## *)
+(** * The Priority Method *)
+(* ########################################################################## *)
+
+Notation "'Σ' x .. y , p" :=
+    (sigT (fun x => .. (sigT (fun y => p)) ..))
+        (at level 200, x binder, right associativity,
+        format "'[' 'Σ'  '/  ' x  ..  y ,  '/  ' p ']'")
+    : type_scope.
+
+Notation unique p := (forall x x', p x -> p x' -> x = x').
+
+  Class Extension :=
+  {
+      extendP: list nat -> nat -> nat -> Prop;
+      extend_dec: forall l x, (Σ y, extendP l x y) + (forall y, ~ extendP l x y);
+      extend_uni: forall l x, unique (extendP l x)
+  }.
+
+  Inductive F_ (E: Extension) : nat -> list nat -> Prop :=
+    | Base : F_ E O []
+    | ExtendS n l a : F_ E n l -> extendP l n a -> F_ E (S n) (a::l)
+    | ExtendN n l   : F_ E n l -> (forall a, ~ extendP l n a) -> F_ E (S n) l.
+
+Section Construction.
+
+    (** ** Basic Properties *)
+
+  Variable E: Extension.
+
+  Lemma F_uni n: unique (F_ E n).
+  Proof.
+    intros l1 l2.
+    dependent induction n.
+    - intros H1 H2. inv H1. now inv H2.
+    - intros H1 H2. inv H1; inv H2.
+      assert(l = l0) as -> by now apply IHn.
+      f_equal. apply (extend_uni H3 H4).
+      assert (l = l2) as -> by now apply IHn.
+      exfalso. apply (H4 a H3).
+      assert (l = l1) as -> by now apply IHn.
+      exfalso. apply (H3 a H4).
+      now apply IHn.
+  Qed.
+
+  Lemma F_mono n m l1 l2: F_ E n l1 -> F_ E m l2 -> n <= m -> incl l1 l2.
+  Proof.
+      intros H1 H2 HE.
+      revert H1 H2; induction HE in l2 |-*; intros H1 H2.
+      - now assert (l1 = l2) as -> by (eapply F_uni; eauto).
+      - inv H2; last now apply IHHE.
+        specialize (IHHE l H1 H0). eauto.
+  Qed.
+
+  Lemma F_pop n x l: F_ E n (x::l) -> exists m, F_ E m l.
+  Proof.
+    intros H. dependent induction H. 
+    - now exists n.
+    - eapply IHF_. eauto.
+  Qed.
+  
+  Lemma F_pick n x l: F_ E n (x::l) -> exists m, F_ E m l /\ extendP l m x.
+  Proof.
+    intros H. dependent induction H.
+    - exists n; eauto.
+    - eapply IHF_; eauto.
+  Qed.
+
+  Lemma F_pick' n x l: F_ E n (x::l) -> exists m, m < n ∧ F_ E m l ∧ extendP l m x.
+    Proof.
+      intros H. dependent induction H.
+      - exists n; eauto.
+      - destruct (IHF_ x l eq_refl) as [m (Hm1&Hm2&Hm3)].
+        exists m; eauto.
+    Qed.
+
+  Lemma F_computable : Σ f: nat -> list nat, 
+    forall n, F_ E n (f n) /\ length (f n) <= n.
+  Proof.
+    set (F := fix f x :=
+           match x with
+           | O => []
+           | S x => match extend_dec (f x) x with
+                   | inr _ => f x
+                   | inl aH => (projT1 aH) :: (f x)
+                   end
+           end).
+    exists F. induction n; simpl.
+    - split. constructor. easy.
+    - destruct (extend_dec (F n) n); split.
+      + eapply ExtendS; first apply IHn. now destruct s.
+      + cbn. destruct IHn. lia.
+      + now eapply ExtendN.
+      + destruct IHn. lia.
+  Qed.
+
+  Definition F_func := projT1 F_computable.
+  Lemma F_func_correctness: forall n, F_ E n (F_func n).
+  Proof.
+    intros n; unfold F_func. 
+    destruct F_computable as [f H].
+    now destruct (H n).
+  Qed.
+
+  Lemma F_func_correctness': forall n, length (F_func n) <= n.
+  Proof.
+    intros n; unfold F_func. 
+    destruct F_computable as [f H].
+    now destruct (H n).
+  Qed.
+
+  Definition F_with x := exists l n, In x l /\ (F_ E n l).
+
+  Lemma F_func_F_with x: F_with x ↔ ∃ n, In x (F_func n).
+  Proof.
+    split. intros (l&n&H1&H2).
+    exists n. assert (l = F_func n) as ->.
+    { eapply F_uni. apply H2. apply F_func_correctness. }
+    done. intros [n Hn]. exists (F_func n), n; split; first done.
+    apply F_func_correctness.
+  Qed.
+  
+
+  Lemma F_with_semi_decidable: semi_decidable F_with.
+  Proof.
+    unfold semi_decidable, semi_decider.
+    destruct F_computable as [f Hf ].
+    exists (fun x n => (Dec (In x (f n)))).
+    intros x. split.
+    - intros (l & n & Hxl & Hl).
+      exists n. rewrite Dec_auto; first easy.
+      destruct (Hf n) as [Hf' _].
+      now rewrite (F_uni Hf' Hl).
+    - intros (n & Hn%Dec_true).
+      exists (f n), n; split; eauto.
+      apply Hf.
+  Qed.
+
+  Lemma F_with_top x: F_with x <-> exists l n, (F_ E n l) /\ (F_ E (S n) (x::l)) /\ extendP l n x.
+  Proof.
+    split; last first.
+    { intros (l&n&H1&H2&H3). exists (x::l), (S n). eauto. }
+    intros [l [n [Hln Hn]]].
+    induction Hn. inversion Hln.
+    - destruct (Dec (x=a)) as [->|Ex].
+      exists l, n; split; first easy. split.
+      econstructor; easy. easy.
+      eapply IHHn. destruct Hln; congruence.
+    - now eapply IHHn.
+  Qed.
+
+  Lemma F_with_semi_decider: Σ f, semi_decider f F_with.
+  Proof.
+    destruct F_computable as [f Hf ].
+    exists (fun x n => (Dec (In x (f n)))).
+    intros x. split.
+    - intros (l & n & Hxl & Hl).
+      exists n. rewrite Dec_auto; first easy.
+      destruct (Hf n) as [Hf' _].
+      now rewrite (F_uni Hf' Hl).
+    - intros (n & Hn%Dec_true).
+      exists (f n), n; split; eauto.
+      apply Hf.
+  Qed.
+
+  Definition χ n x: bool := Dec (In x (F_func n)).
+  Definition stable {Q} (f: nat → Q → bool) :=
+    ∀ q n m, n ≤ m → f n q = true → f m q = true.
+  Definition stable_semi_decider {Q} P (f: nat → Q → bool) :=
+    semi_decider (λ x n, f n x) P ∧ stable f.
+
+  Lemma F_with_χ : stable_semi_decider F_with χ.
+  Proof.
+    split. split. 
+    - intros [n Hn]%F_func_F_with. by exists n; apply Dec_auto.
+    - intros [n Hn%Dec_true]. rewrite F_func_F_with. by exists n.
+    - intros x n m Hn Hm%Dec_true.
+      apply Dec_auto. enough (incl (F_func n) (F_func m)). eauto.
+      eapply F_mono; last exact Hn; apply F_func_correctness.
+  Qed.
+
+End Construction.
+
+Section StrongInduction.
+
+  Definition strong_induction (p: nat -> Type) :
+    (forall x, (forall y, y < x -> p y) -> p x) -> forall x, p x.
+  Proof.
+      intros H x; apply H.
+      induction x; [intros; lia| ].
+      intros; apply H; intros; apply IHx; lia.
+  Defined.
+
+End StrongInduction.
+
+Tactic Notation "strong" "induction" ident(n) := induction n using strong_induction.
+
+Section EWO.
+  Variable p: nat -> Prop.
+  Inductive T | (n: nat) : Prop := C (phi: ~p n -> T (S n)).
+
+  Definition T_elim (q: nat -> Type)
+    : (forall n, (~p n -> q (S n)) -> q n) ->
+      forall n, T n -> q n
+    := fun e => fix f n a :=
+      let (phi) := a in
+      e n (fun h => f (S n) (phi h)).
+
+  (*** EWO for Numbers *)
+
+  Lemma TI n :
+    p n -> T n.
+  Proof.
+    intros H. constructor. intros H1. destruct (H1 H).
+  Qed.
+
+  Lemma TD n :
+    T (S n) -> T n.
+  Proof.
+    intros H. constructor. intros _. exact H.
+  Qed.
+
+  Variable p_dec: forall n, dec (p n).
+
+  Definition TE (q: nat -> Type)
+    : (forall n, p n -> q n) ->
+      (forall n, ~p n -> q (S n) -> q n) ->
+      forall n, T n -> q n.
+  Proof.
+    intros e1 e2.
+    apply T_elim. intros n IH.
+    destruct (p_dec n); auto.
+  Qed.
+
+  (** From now on T will only be used through TI, TD, and TE *)
+
+  
+  Lemma T_zero n :
+    T n -> T 0.
+  Proof.
+    induction n as [|n IH].
+    - auto.
+    - intros H. apply IH. apply TD, H.
+  Qed.
+
+  Definition ewo_nat :
+    ex p -> Σ x, p x.
+  Proof.
+    intros H.
+    refine (@TE (fun _ => Σ x, p x) _ _ 0 _).
+    - eauto.
+    - easy.
+    - destruct H as [n H]. apply (@T_zero n), TI, H.
+  Qed.
+  
+End EWO.
+
+Section LeastWitness.
+
+  Definition safe p n := forall k, k < n -> ~ p k.
+  Definition least p n := p n /\ safe p n.
+
+  Fact least_unique p : unique (least p).
+  Proof.
+    intros n n' [H1 H2] [H1' H2'].
+    enough (~(n < n') /\ ~(n' < n)) by lia.
+    split; intros H.
+    - eapply H2'; eassumption.
+    - eapply H2; eassumption.
+  Qed.
+
+  Fact safe_O p :
+    safe p 0.
+  Proof.
+    hnf. lia.
+  Qed.
+
+  Fact safe_S p n :
+    safe p n -> ~p n -> safe p (S n).
+  Proof.
+    intros H1 H2 k H3. unfold safe in *.
+    assert (k < n \/ k = n) as [H|H] by lia.
+    - auto.
+    - congruence.
+  Qed.
+
+  Fact safe_char p n :
+    safe p n <-> forall k, p k -> k >= n.
+  Proof.
+    split.
+    - intros H k H1.
+      enough (k < n -> False) by lia.
+      intros H2. apply H in H2. auto.
+    - intros H k H1 H2. apply H in H2. lia.
+  Qed.
+
+  Fact safe_char_S p n :
+    safe p (S n) <-> safe p n /\ ~p n.
+  Proof.
+    split.
+    - intros H. split.
+      + intros k H1. apply H. lia.
+      + apply H. lia.
+    - intros [H1 H2]. apply safe_S; assumption.
+  Qed.
+
+  Fact safe_eq p n k :
+    safe p n -> k <= n -> p k -> k = n.
+  Proof.
+    intros H1 H2 H3. unfold safe in *.
+    enough (~(k < n)) by lia.
+    specialize (H1 k). tauto.
+  Qed.
+
+  Fact E14 x y z :
+    x - y = z <-> least (fun k => x <= y + k) z.
+  Proof.
+    assert (H: least (fun k => x <= y + k) (x - y)).
+    { split; unfold safe; lia. }
+    split. congruence.
+    eapply least_unique, H.
+  Qed.  
+
+  (*** Certifying LWOs *)
+
+  Section LWO.
+    Variable p : nat -> Prop.
+    Variable p_dec : forall x, dec (p x).
+
+    Definition lwo :
+      forall n, (Σ k, k < n /\ least p k) + safe p n.
+    Proof.
+      induction n as [|n IH].
+      - right. apply safe_O.
+      - destruct IH as [[k H1]|H1].
+        + left. exists k. destruct H1 as [H1 H2]. split. lia. exact H2.
+        + destruct (p_dec n).
+          * left. exists n. split. lia. easy.
+          * right. apply safe_S; assumption.
+    Defined.
+
+    Definition lwo' :
+      forall n, (Σ k, k <= n /\ least p k) + safe p (S n).
+    Proof.
+      intros n.
+      destruct (lwo (S n)) as [(k&H1&H2)|H].
+      - left. exists k. split. lia. exact H2.
+      - right.  exact H.
+    Qed.
+
+    Definition least_sig :
+      (Σ x, p x) -> Σ x, (least p) x.
+    Proof.
+      intros [n H].
+      destruct (lwo (S n)) as [(k&H1&H2)|H1].
+      - exists k. exact H2.
+      - exfalso. apply (H1 n). lia. exact H.
+    Qed.
+
+    Definition least_ex :
+      ex p -> ex (least p).
+    Proof.
+      intros [n H].
+      destruct (lwo (S n)) as [(k&H1&H2)|H1].
+      - exists k. exact H2.
+      - exfalso. apply (H1 n). lia. exact H.
+    Qed.
+
+    Definition safe_dec n :
+      dec (safe p n).
+    Proof.
+      destruct (lwo n) as [[k H1]|H1].
+      - right. intros H. exfalso.
+        destruct H1 as [H1 H2]. apply (H k). exact H1. apply H2.
+      - left. exact H1.
+    Defined.
+
+    Definition least_dec n :
+      dec (least p n).
+    Proof.
+      unfold least.
+      destruct (p_dec n) as [H|H].
+      2:{ right. tauto. }
+      destruct (safe_dec n) as [H1|H1].
+      - left. easy.
+      - right. tauto.
+    Qed.
+  End LWO.
+
+  Lemma exists_bounded_dec' P:
+  (forall x, dec (P x)) -> forall k, dec (exists n, n < k /\ P n).
+  Proof.
+    intros Hp k.
+    induction k. right; intros [? [? _]]; lia.
+    destruct IHk as [Hw|Hw].
+    - left. destruct Hw as [x [Hx1 Hx2]]. exists x; split; eauto; lia.
+    - destruct (Hp k). left. exists k; split; eauto; lia.
+      right. intros [x [Hx1 Hx2]].
+      assert (x = k \/ x < k) as [->|Hk] by lia; firstorder.
+  Qed.
+
+  Lemma exists_bounded_dec P:
+    (forall x, dec (P x)) -> forall k, dec (exists n, n <= k /\ P n).
+  Proof.
+    intros Hp k.
+    induction k. destruct (Hp 0). left. exists 0. eauto.
+    right. intros [x [Hx Hx']]. now assert (x=0) as -> by lia.
+    destruct IHk as [Hw|Hw].
+    - left. destruct Hw as [x [Hx1 Hx2]]. exists x; split; eauto; lia.
+    - destruct (Hp (S k)). left. exists (S k); split; eauto; lia.
+      right. intros [x [Hx1 Hx2]].
+      assert (x = S k \/ x <= k) as [->|Hk] by lia; firstorder.
+  Qed.
+
+  Definition bounded (P: nat -> Prop) := Σ N, forall x, P x -> x < N.
+
+  Fact bouned_le (P Q: nat -> Prop) N :
+    (forall x, P x -> x < N) -> 
+    (exists x, P x /\ Q x) <->  exists x, x < N /\ P x /\ Q x.
+  Proof.
+    intros Hn; split.
+    - intros [x Hx]. exists x; intuition eauto.
+    - intros (x&c&Hc). exists x; intuition eauto.
+  Qed.
+
+  Lemma bounded_dec (P Q: nat -> Prop):
+    (forall x, dec (P x)) -> (forall x, dec (Q x)) -> 
+    bounded P -> dec (exists n, P n /\ Q n).
+  Proof.
+    intros H1 H2 [N HN].
+    assert (dec (exists n, n < N /\ P n /\ Q n)) as [H|H].
+    - eapply exists_bounded_dec'. intro; eapply and_dec; eauto.
+    - left. rewrite bouned_le; eauto.
+    - right. intros H'%(@bouned_le _ _ N); easy.
+  Qed.
+  Lemma dec_neg_dec P: dec P -> dec (~ P).
+  Proof. intros [H|H]. right; eauto. now left. Qed.
+
+  Lemma forall_bounded_dec P e: 
+    (forall x, dec (P x)) -> dec(forall i, i <= e -> P i).
+  Proof.
+    intros H.
+    induction e. destruct (H 0); [left|right]; intros.
+    now inv H0. intros H'. apply n, H'. lia.
+    destruct IHe as [H1|H1].
+    destruct (H (S e)); [left|right]; intros.
+    inv H0; first easy. now apply H1.
+    intros H0. apply n. apply H0. easy.
+    right. intro H'. apply H1. intros. apply H'. lia. 
+  Qed.
+
+End LeastWitness.
+
+
+Section logic.
+
+  Definition pdec p := p ∨ ¬ p.
+
+  Definition Π_1_lem := ∀ p : nat -> Prop,
+    (∀ x, dec (p x)) -> pdec (∀ x, p x).
+  Definition Σ_1_dne := ∀ p : nat -> Prop,
+    (∀ x, dec (p x)) -> (¬¬ ∃ x, p x) → ∃ x, p x.
+  Definition Σ_1_lem := ∀ p: nat → Prop,
+    (∀ x, dec (p x)) -> pdec (∃ x, p x).
+
+  Hypothesis LEM1: LEM_Σ 1.
+
+  Fact assume_Σ_1_lem: Σ_1_lem .
+  Proof.
+    intros p Hp.
+    destruct level1 as (_&H2&_).
+    assert principles.LPO as H by by rewrite <- H2.
+    destruct (H Hp) as [[k Hk]|H1].
+    - left. exists k. destruct (Hp k); eauto.
+      cbn in Hk. congruence.
+    - right. intros [k Hk]. apply H1. 
+      exists k. destruct (Hp k); eauto.
+  Qed.
+
+  Fact assume_Σ_1_dne: Σ_1_dne.
+  Proof.
+    intros p Hp H.
+    destruct (assume_Σ_1_lem Hp) as [H1|H1]; eauto.
+    exfalso. by apply H.
+  Qed.
+
+  Fact assume_Π_1_lem: Π_1_lem.
+  Proof.
+    intros p Hp.
+    destruct level1 as (_&H2&_).
+    assert principles.LPO as H by by rewrite <- H2.
+    apply principles.LPO_to_WLPO in H.
+    assert (∀ x : nat, dec (¬ p x)) as Hp' by eauto.
+    destruct (H Hp') as [H1|H1].
+    - left. intro x.
+      specialize (H1 x).
+      apply Dec_false in H1.
+      destruct (Hp x); firstorder.
+    - right. intros H3. apply H1. intros n.
+      specialize (H3 n). destruct (Hp' n); firstorder.
+  Qed.
+
+End logic.
diff --git a/theories/PostsTheorem/PostsTheorem.v b/theories/PostsTheorem/PostsTheorem.v
index f52f00f..87dd084 100644
--- a/theories/PostsTheorem/PostsTheorem.v
+++ b/theories/PostsTheorem/PostsTheorem.v
@@ -201,6 +201,13 @@ Section PostsTheorem.
         destruct seval as [ [ | [] ] | ]eqn:E; eauto.
   Qed.
 
+  Lemma Σ_semi_decidable_in_Π_forward {k} (p: (vec nat k) -> Prop) n (DN : LEM_Π n) :
+    isΣsem (S n) p -> exists (p': vec nat (S k) -> Prop), isΠsem n p' /\ oracle_semi_decidable p' p.
+  Proof.
+    apply Σ_semi_decidable_in_Π1.
+    assumption.
+  Qed.
+
   Lemma Σ_semi_decidable_in_Π {k} (p: (vec nat k) -> Prop) n (DN : LEM_Σ n) :
     isΣsem (S n) p <-> exists (p': vec nat (S k) -> Prop), isΠsem n p' /\ oracle_semi_decidable p' p.
   Proof.
@@ -211,6 +218,18 @@ Section PostsTheorem.
 
   Hint Resolve DNEimpl.
 
+  (* Lemma Σ_semi_decidable_in_Σ_forward {k} (p: (vec nat k) -> Prop) n (DN : LEM_Π n) : *)
+  (*   isΣsem (S n) p -> exists (p': vec nat (S k) -> Prop), isΣsem n p' /\ oracle_semi_decidable p' p. *)
+  (* Proof. *)
+  (*   intros H % Σ_semi_decidable_in_Π_forward; eauto. *)
+  (*   destruct H as [p' [H S]]. eapply negΣinΠsem in H as H'. *)
+  (*   2: now eapply LEM_Σ_to_DNE_Σ. *)
+  (*   eexists. split;[apply H'|]. *)
+  (*   rewrite <- oracle_semi_decidable_complement_iff. eauto. *)
+  (*   eapply DNEimpl; eauto. *)
+  (*   now eapply LEM_Σ_to_DNE_Σ. *)
+  (* Qed. *)
+
   Lemma Σ_semi_decidable_in_Σ {k} (p: (vec nat k) -> Prop) n (DN : LEM_Σ n) :
       isΣsem (S n) p <-> exists (p': vec nat (S k) -> Prop), isΣsem n p' /\ oracle_semi_decidable p' p.
   Proof.
@@ -263,6 +282,15 @@ Section PostsTheorem.
     intros. apply red_m_impl_red_T. eapply jump_Σn_complete; eauto.
   Qed.
 
+  Lemma Σ_semi_decidable_jump_forward {k} (p: (vec nat k) -> Prop) n (DN : LEM_Σ n) :
+    isΣsem (S n) p -> oracle_semi_decidable (­{0}^(n)) p.
+  Proof.
+    intros [p' [Σp' Sp']]%Σ_semi_decidable_in_Σ.
+    eapply (Turing_transports_sdec Sp').
+    eapply jump_Σn_complete_redT.
+    all: eauto.
+  Qed.
+
   Lemma Σ_semi_decidable_jump {k} (p: (vec nat k) -> Prop) n (DN : LEM_Σ n) :
       isΣsem (S n) p <-> oracle_semi_decidable (­{0}^(n)) p.
   Proof.
diff --git a/theories/PostsTheorem/TuringJump.v b/theories/PostsTheorem/TuringJump.v
index 4b597c5..1164a96 100644
--- a/theories/PostsTheorem/TuringJump.v
+++ b/theories/PostsTheorem/TuringJump.v
@@ -275,16 +275,16 @@ Section jump.
     - unfold J. reflexivity.
   Qed.
 
+  (** Complement not semi-decidable ***)
+
   Lemma not_semidecidable_compl_J Q : ~ oracle_semi_decidable Q (compl (J Q)).
   Proof.
-    intros (F & Hcomp & H). 
+    intros (F & Hcomp & H).
     specialize (surjective Hcomp) as [c Hc].
     unfold J in H. specialize (H c).
     rewrite <- Hc in H. tauto.
   Qed.
 
-  (** Complement not semi-decidable ***)
-
   Definition 𝒥 Q := fun! ⟨c, x⟩ =>  Ξ c (char_rel Q) x.
 
   Lemma jump_gt Q :
@@ -308,6 +308,12 @@ Section jump.
       eapply not_semidecidable_compl_J; eassumption.
   Qed.
 
+  Lemma not_turing_red_J Q: ~ (J Q ⪯ᴛ Q).
+  Proof.
+    intros H % Turing_to_sdec_compl.
+    eapply not_semidecidable_compl_J; eassumption.
+  Qed.
+
   (** # <a id="J_self_J_m_red" /> #*)
   Lemma J_self_𝒥_m_red:
     forall Q, (J Q) ⪯ₘ (𝒥 Q).
@@ -324,7 +330,7 @@ Section jump.
     reflexivity. 
   Qed.
 
-  Lemma red_m_iff_semidec_jump (P : nat -> Prop) (Q : nat -> Prop): 
+  Lemma red_m_iff_semidec_jump (P : nat -> Prop) (Q : nat -> Prop):
     oracle_semi_decidable Q P <-> P ⪯ₘ (J Q).
   Proof.
     split.
@@ -398,4 +404,4 @@ Fixpoint jump_n {Part : partiality} Q n :=
   | 0 => Q
   | S n => J (jump_n Q n)
   end.
-Notation "A '^(' n ')'" := (jump_n A n) (at level 25, format "A ^( n )").
+Notation "A '^(' n ')'" := (jump_n A n) (at level 25, format "A ^( n )").
\ No newline at end of file
diff --git a/theories/TuringReducibility/OracleComputability.v b/theories/TuringReducibility/OracleComputability.v
index 7aa08ed..5d24455 100644
--- a/theories/TuringReducibility/OracleComputability.v
+++ b/theories/TuringReducibility/OracleComputability.v
@@ -1,5 +1,6 @@
 From SyntheticComputability Require Import partial Dec.
 From stdpp Require Import list.
+Require Import Coq.Program.Equality.
 Import PartialTactics.
 
 Lemma list_find_repeat_not {Y} P D x n :
@@ -812,7 +813,9 @@ Qed.
 
 Lemma interrogation_equiv_evalt Q A I O :
   forall (τ : I -> list A ↛ (Q + O)) (f : Q ↛ A) (i : I) (o : O),
-    (exists (qs : list Q) (ans : list A), interrogation (τ i) (fun x y => f x =! y) qs ans /\ τ i ans =! inr o) <-> (exists n : nat, evalt (τ i) f n =! inr o).
+  (exists (qs : list Q) (ans : list A),
+  interrogation (τ i) (fun x y => f x =! y) qs ans /\ τ i ans =! inr o) <->
+  (exists n : nat, evalt (τ i) f n =! inr o).
 Proof.
   intros τ f i o. split.
   + intros (qs & ans & Hi & Hout).
@@ -821,6 +824,241 @@ Proof.
   + intros [n H]. eapply evalt_to_interrogation in H as (? & ? & ? & ? & ?); eauto.
 Qed.
 
+
+(** A total computable version of evalt **)
+
+Fixpoint evalt_comp {Q A O} (tau : list A ↛ (Q + O))
+  (f : Q -> A) (step : nat) (depth: nat): option (Q + O) :=
+  match (seval (tau []) depth) with
+    | Some x => match step, x with
+               | 0, inl q => Some (inl q)
+               | S n, inl q => evalt_comp (fun l => tau (f q :: l)) f n depth
+               | _, inr o => Some (inr o) end
+    | None => None end.
+
+
+Lemma evalt_comp_ext {Q A O} τ τ' f n m:
+  (forall l n, seval (τ l) n = seval (τ' l) n) ->
+  evalt_comp τ f n m = @evalt_comp Q A O τ' f n m.
+Proof.
+  intro Heq; induction n in τ, τ', Heq |- *.
+  - cbn. now rewrite <- Heq.
+  - cbn. rewrite <- Heq.
+    destruct (seval (A:=Q + O) (τ []) m); cbn.
+    destruct s; eauto. easy.
+Qed.
+
+Lemma list_cons_or {X} (l l1: list X) a :
+  l `prefix_of` l1 ++ [a] ->
+  l `prefix_of` l1 \/ l = l1 ++ [a].
+Proof.
+  induction l in l1 |-*; intros.
+  - left. eapply prefix_nil.
+  - destruct l1.
+    + right. list_simplifier.
+      set (H' := H).
+      apply prefix_cons_inv_2, prefix_nil_inv in H' as ->.
+      apply prefix_cons_inv_1 in H as ->.
+      done.
+    + list_simplifier.
+      set (H' := H).
+      apply prefix_cons_inv_2 in H'.
+      apply prefix_cons_inv_1 in H as ->.
+      destruct (IHl _ H') as [h1 | ->].
+      ++ left. by eapply prefix_cons.
+      ++ now right.
+Qed.
+
+Lemma interrogation_ter {Q A O} tau f l lv v:
+  @interrogation Q A O tau (fun x y => f x = y) l lv ->
+  tau lv =! v ->
+  exists m, forall ans_, prefix ans_ lv -> exists v, seval (tau ans_) m = Some v.
+Proof.
+  intros H1 H2.
+  induction H1 in H2, v |-*.
+  - rewrite seval_hasvalue in H2.
+    destruct H2 as [m Hm]. exists m.
+    intros ans_ Hans_. exists v.
+    apply prefix_nil_inv in Hans_.
+    rewrite Hans_. easy.
+  - rewrite seval_hasvalue in H2.
+    destruct H2 as [m Hm].
+    destruct (IHinterrogation (Ask q) H) as [m' Hm'].
+    exists (max m m').
+    intros ans_ Hans_.
+    destruct (list_cons_or _ _ _ Hans_) as [h| ->].
+    + destruct (Hm' ans_ h) as [v' Hv'].
+      exists v'. eapply seval_mono.
+      eauto. lia.
+    + exists v. eapply seval_mono; [eauto| lia].
+Qed.
+
+(** Basic property of evalt_comp **)
+
+Lemma evalt_comp_depth_mono {Q A O} (tau: (list A) ↛ (Q + O)) f n m o :
+  evalt_comp tau f n m = Some o ->
+  forall m', m' >= m -> evalt_comp tau f n m' = Some o.
+Proof.
+  intros H m' Hm'.
+  induction n in H, tau, o |-*.
+  - cbn in *.
+    destruct (seval (A:=Q + O) (tau []) m) eqn: E; try congruence.
+    assert (seval (A:=Q + O) (tau []) m' = (Some s)) as ->.
+    eapply seval_mono. exact E. lia.
+    easy.
+  - cbn in *.
+    destruct (seval (A:=Q + O) (tau []) m) eqn: E.
+    + assert (seval (A:=Q + O) (tau []) m' = Some s) as ->.
+      eapply seval_mono. exact E. lia.
+      destruct s.
+      now apply IHn.
+      exact H.
+    + congruence.
+Qed.
+
+Lemma interrogation_plus_evalt_comp {Q A O} tau f n m l lv v2:
+  @interrogation Q A O tau (fun x y => f x = y) l lv ->
+  (forall ans_, prefix ans_ lv -> exists v, seval (tau ans_) m = Some v) ->
+  evalt_comp (fun l' => tau (lv ++ l')) f n m = Some v2 <->
+  evalt_comp tau f (length l + n) m = Some v2.
+Proof.
+  intros H H1. split; revert n; dependent induction H.
+  - cbn. eauto.
+  - intros.
+    cbn -[evalt]. rewrite app_length. cbn -[evalt].
+    replace (length qs + 1 + n) with (length qs + (S n)) by lia.
+    eapply IHinterrogation. intros; apply H2.
+    etransitivity. exact H4.
+    now eapply prefix_app_r.
+    cbn. rewrite app_nil_r.
+    destruct (H2 ans).
+    now eapply prefix_app_r.
+    assert (exists m, seval (tau ans) m = Some x).
+    now exists m.
+    rewrite <- seval_hasvalue in H5.
+    assert (x = Ask q).
+    eapply hasvalue_det; eauto.
+    rewrite H4, H6, H1.
+    rewrite <- H3. eapply evalt_comp_ext.
+    intros; now list_simplifier.
+  - cbn. eauto.
+  - intros.
+    rewrite app_length in H3. cbn in H3.
+    replace (length qs + 1 + n) with (length qs + (S n)) in H3 by lia.
+    eapply IHinterrogation in H3.
+    2: {
+    intros; apply H2.
+    etransitivity. exact H4.
+    now eapply prefix_app_r.
+    }
+    cbn in H3.
+    rewrite app_nil_r in H3.
+    destruct (H2 ans).
+    now eapply prefix_app_r.
+    assert (exists m, seval (tau ans) m = Some x).
+    now exists m.
+    rewrite <- seval_hasvalue in H5.
+    assert (x = Ask q).
+    eapply hasvalue_det; eauto.
+    rewrite H4, H6, H1 in H3.
+    rewrite <- H3. eapply evalt_comp_ext.
+    intros; now list_simplifier.
+Qed.
+
+Lemma evalt_comp_step_mono {Q A O} (tau: (list A) ↛ (Q + O)) f qs ans o:
+  @interrogation Q A O tau (fun x y => f x = y) qs ans ->
+  tau ans =! Output o ->
+  exists depth step,
+  forall g, @interrogation Q A O tau (fun x y => g x = y) qs ans ->
+  forall n', step <= n' -> evalt_comp tau g n' depth = Some (Output o).
+Proof.
+  intros H1 H2.
+  destruct (interrogation_ter _ _ _ _ _ H1 H2) as [step Hstep].
+  exists step. exists (length qs). intros g Hg n' Hn'.
+  assert (exists v, seval (tau ans) step = Some v) as [v Hv].
+  { eapply Hstep; naive_solver. }
+  assert (v = Output o).
+  { eapply hasvalue_det; [|eapply H2]. rewrite seval_hasvalue. eauto. }
+  eapply Nat.le_exists_sub in Hn' as [k [-> _]].
+  rewrite Nat.add_comm.
+  eapply interrogation_plus_evalt_comp; eauto.
+  induction k.
+  all: cbn; rewrite app_nil_r; by rewrite Hv, H.
+Qed.
+
+Lemma evalt_comp_oracle_approx {Q A O} tau f l lv v:
+  @interrogation Q A O tau (fun x y => f x = y) l lv ->
+  tau lv =! v ->
+  exists step depth,
+  forall g, @interrogation Q A O tau (fun x y => g x = y) l lv ->
+  evalt_comp tau g step depth = Some v.
+Proof.
+  intros H1 h2.
+  destruct (interrogation_ter _ _ _ _ _ H1 h2) as [step Hstep].
+  exists (length l + 0).
+  exists step.
+  intros.
+  eapply interrogation_plus_evalt_comp; eauto.
+  cbn. rewrite app_nil_r.
+  destruct (Hstep lv) as [v' Hv'].
+  reflexivity.
+  assert (exists k, seval (A:=Q + O) (tau lv) k = Some v').
+  exists step. easy.
+  rewrite <- seval_hasvalue in H0.
+  assert (v' = v).
+  eapply hasvalue_det; eauto.
+  rewrite Hv', H2.
+  destruct v; done.
+Qed.
+
+
+
+Lemma interrogation_evalt_comp_limit {Q A O} tau f l lv v:
+  (exists K, forall k, k >= K ->
+             @interrogation Q A O tau (fun x y => (f k) x = y) l lv) ->
+  tau lv =! Output v ->
+  exists N, forall n, n >= N -> evalt_comp tau (f n) n n = Some (Output v).
+Proof.
+  intros [k h1] h2.
+  assert (interrogation tau (fun x y => f k x = y) l lv) as H.
+  apply h1. lia.
+  destruct (evalt_comp_step_mono _ _ _ _ _ H h2) as (a' & b' & Hs).
+  destruct (evalt_comp_oracle_approx _ _ _ _ _ H h2) as (a & b & Hab).
+  exists (max b'(max a' (max (max a b) k))).
+  intros n Hn.
+  eapply evalt_comp_depth_mono.
+  eapply (Hs (f n)); eauto.
+  eapply h1.
+  all: lia.
+Qed.
+
+Lemma evalt_comp_to_interrogation:
+  ∀ {Q A I O : Type} (tau : I → (list A) ↛ (Q + O)) (f : Q -> A) (i : I) (o : O) (n depth: nat),
+    evalt_comp (tau i) f n depth = Some (Output o) →
+    ∃ (qs : list Q) (ans : list A),
+      length qs <= n /\ interrogation (tau i) (λ (x : Q) (y : A), f x = y) qs ans ∧
+        tau i ans =! Output o.
+Proof.
+  intros Q A I O tau f i o n depth H.
+  induction n in tau, H |- *.
+  * cbn in *. destruct (seval (tau i []) depth) eqn: E.
+    exists [], []. repeat split. eauto. econstructor.
+    destruct s. congruence. rewrite seval_hasvalue.
+    by exists depth; injection H as ->. congruence.
+  * cbn in *.  destruct (seval (tau i []) depth) eqn: E; try congruence.
+    destruct s; try congruence.
+    -- eapply (IHn (fun i l => tau i (f q :: l))) in H as (qs & ans & H3 & H1 & H2).
+       exists (q :: qs), (f q :: ans). split; eauto. cbn; lia. repeat split.
+       eapply interrogation_app with (q1 := [q]) (a1 := [f q]).
+       eapply Interrogate with (qs := []) (ans := []); eauto.
+       rewrite seval_hasvalue. by exists depth.
+       eauto. eauto.
+    -- exists [], []. repeat split. cbn. lia. eauto.
+       rewrite seval_hasvalue.
+       by exists depth; injection H as ->.
+Qed.
+
+
 (** ** Closure properties of Oracle computability  *)
 
 (** Computability of precomposition *)
@@ -862,7 +1100,6 @@ Proof.
   cbn. firstorder subst; psimpl.
 Qed.
 
-(** Computability of constant functions *)
 Lemma computable_ret A Q I O v :
   @OracleComputable Q A I O (fun f i o => o = v).
 Proof.
@@ -1276,6 +1513,7 @@ Proof.
     + intros []; cbn; firstorder.
 Qed.
 
+
 (** Turing reduction transports partial computability - relying on the evalt function from above *)
 Lemma Turing_transports_computable_strong {Q A I O} F tau :
   (∀ (R : Q → A → Prop) (x : I) (o : O), F R x o ↔ (∃ (qs : list Q) (ans : list A), interrogation (tau x) R qs ans ∧ tau x ans =! Output o)) ->
@@ -1346,6 +1584,7 @@ Proof.
   destruct (Turing_transports_computable_strong F tau) as [F' ]; eauto.
 Qed.
 
+
 (** Transport of decidability -- which is equivalent to Markov's principle *)
 Definition char_rel_fun {X Y} (f : X -> Y) := (fun x b => f x = b).
 
@@ -1779,3 +2018,4 @@ End part.
 
 Notation "P ⪯ᴛ Q" := (red_Turing P Q) (at level 50).
 
+Search evalt.
diff --git a/theories/TuringReducibility/SemiDec.v b/theories/TuringReducibility/SemiDec.v
index f7128d1..4b8b912 100644
--- a/theories/TuringReducibility/SemiDec.v
+++ b/theories/TuringReducibility/SemiDec.v
@@ -786,6 +786,25 @@ Proof.
   - firstorder.
 Qed.
 
+
+Lemma Turing_to_sdec_compl {Part : partiality} {X Y} (q : Y -> Prop) (p : X -> Prop) :
+  red_Turing p q ->
+  OracleSemiDecidable q (compl p).
+Proof.
+  intros [F [HF H2]].
+  exists (fun R x o => F R x false). split.
+  - eapply OracleComputable_ext.
+    eapply computable_bind. eapply HF.
+    eapply computable_if with (test := snd).
+    eapply computable_nothing.
+    eapply computable_ret with (v := tt).
+    cbn; split.
+    + intros [[]]; firstorder.
+    + destruct o. exists false; firstorder.
+  - firstorder.
+Qed.
+
+
 Lemma OracleSemiDecidable_refl {Part : partiality} X (Q : X -> Prop) :
   OracleSemiDecidable Q Q.
 Proof.