Require Import Undecidability.FOL.Syntax.Facts.
Require Import Undecidability.FOL.Semantics.Tarski.FullFacts.
Require Import Undecidability.FOL.Sets.FST.
Require Import Lia.

From Undecidability.PCP Require Import PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb.

From Undecidability Require Import Shared.ListAutomation.
Import ListAutomationNotations.

Local Set Implicit Arguments.
Local Unset Strict Implicit.


Local Definition BSRS := list(card bool).

Fixpoint shift n x :=
  match n with
  | O x
  | S n subst_term (shift n x)
  end.

Definition sing a :=
  a ::: .

Definition upair a b :=
  a ::: (b ::: ).

Notation "{ a ; b }" := (upair a b) (at level 31) : syn.
Notation "'σ' x" := (x ::: x) (at level 32) : syn.

Definition opair a b :=
  {{a; a}; {a; b}}.

Definition pairing f A :=
   $0 shift 1 f $1 shift 3 A $2 opair $1 $0.

Definition function' f A :=
  pairing f A $0 shift 2 A opair $0 $1 shift 2 f
                     opair $1 $0 shift 2f $2 $0.

Definition function f :=
   opair $2 $1 shift 3 f opair $2 $0 shift 3 f $1 $0.

Definition enc_bool (x : bool) :=
  if x then {; } else .

Fixpoint prep_string (s : string bool) a :=
  match s with
  | nil a
  | b::s opair (enc_bool b) (prep_string s a)
  end.

Definition enc_string (s : string bool) :=
  prep_string s .

Fixpoint enc_stack (B : BSRS) :=
  match B with
  | nil
  | (s,t)::B opair (enc_string s) (enc_string t) ::: enc_stack B
  end.

Definition is_rep phi a b :=
   $0 shift 1 b $0 shift 2 a .

Definition comb_rel s t :=
   $2 opair $0 $1 $3 opair (prep_string s $0) (prep_string t $1).

Definition is_bunion a b c :=
  a c b c $0 c`[] $0 a`[] $0 b`[].

Fixpoint combinations (B : BSRS) a b :=
  match B with
  | nil b
  | (s,t)::B is_bunion $0 $1 (shift 2 b) combinations B (shift 2 a) $1
                    is_rep (comb_rel s t) (shift 2 a) $0
  end.

Definition solutions (B : BSRS) f n :=
  opair (enc_stack B) f $2 shift 3 n opair $2 $1 shift 3 f
                combinations B $1 $0 opair (σ $2) $0 shift 3 f.

Definition transitive t :=
   $0 shift 1 t $0 shift 1 t.

Definition htransitive t :=
  transitive t $0 shift 1 t transitive $0.

Definition solvable (B : BSRS) :=
   htransitive $3 function $2 solutions B $2 $3 opair $3 $0 $2 opair $1 $1 $0.

Lemma bool_bound b n :
  bounded_t n (enc_bool b).
Proof.
  destruct b; repeat solve_bounds.
Qed.


Lemma prep_string_bound s t n :
  bounded_t n t bounded_t n (prep_string s t).
Proof.
  intros Ht. induction s; cbn; trivial.
  repeat solve_bounds; trivial.
  all: apply bool_bound.
Qed.


Lemma string_bound s n :
  bounded_t n (enc_string s).
Proof.
  apply prep_string_bound. solve_bounds.
Qed.


Lemma stack_bound B n :
  bounded_t n (enc_stack B).
Proof.
  induction B as [|[s t] B IH]; cbn; repeat solve_bounds; trivial.
  all: apply string_bound.
Qed.


Lemma combinations_bound (B : BSRS) n k l :
  n > 3 + l n > 4 + k bounded n (combinations B $k $l).
Proof.
  revert n k l. induction B as [|[s t] B IH]; cbn; intros n k l ; solve_bounds.
  apply IH; . all: apply prep_string_bound; solve_bounds.
Qed.


Lemma solvabe_bound B :
  bounded 0 (solvable B).
Proof.
  repeat solve_bounds.
  - apply stack_bound.
  - apply combinations_bound; .
Qed.



Declare Scope sem.
Open Scope sem.

Arguments Vector.nil {_}, _.
Arguments Vector.cons {_} _ {_} _, _ _ _ _.

Notation "x ∈ y" := (@i_atom _ _ _ _ elem (Vector.cons x (Vector.cons y Vector.nil))) (at level 35) : sem.
Notation "x ≡ y" := (@i_atom _ _ _ _ equal (Vector.cons x (Vector.cons y Vector.nil))) (at level 35) : sem.
Notation "x ⊆ y" := ( z, z x z y) (at level 34) : sem.

Notation "∅" := (@i_func FST_func_sig ZFSignature.ZF_pred_sig _ _ eset Vector.nil) : sem.
Notation "x ::: y " := (@i_func FST_func_sig _ _ _ adj (Vector.cons x (Vector.cons y Vector.nil))) (at level 31) : sem.

Notation "{ x ; y }" := (x ::: (y ::: )) (at level 31) : sem.
Notation "'σ' x" := (x ::: x) (at level 32) : sem.


Section FST.

  Context { V : Type }.
  Context { M : interp V }.

  Hypothesis M_FST : rho, FST.
  Hypothesis VIEQ : extensional M.

  Lemma M_ext x y :
    x y y x x = y.
  Proof.
    rewrite VIEQ. apply (@M_FST ( _ ) ax_ext). cbn; tauto.
  Qed.


  Lemma M_eset x :
     x .
  Proof.
    refine (@M_FST ( _ ) ax_eset _ x). cbn; tauto.
  Qed.


  Lemma M_adj x y z :
    x y ::: z x = y x z.
  Proof.
    rewrite VIEQ. apply (@M_FST ( _ ) ax_adj). cbn; tauto.
  Qed.


  Lemma M_pair x y z :
    x {y; z} x = y x = z.
  Proof.
    rewrite M_adj. rewrite M_adj. intuition. now apply M_eset in H.
  Qed.


  Definition M_is_rep R x y :=
     v, v y u, u x R u v.


  Definition M_sing x :=
    {x; x}.

  Definition M_opair x y := ({{x; x}; {x; y}}).

  Lemma sing_el x y :
    x M_sing y x = y.
  Proof.
    split.
    - now intros [H|H] % M_pair.
    - intros . apply M_pair. now left.
  Qed.


  Lemma M_pair1 x y :
    x {x; y}.
  Proof.
    apply M_pair. now left.
  Qed.


  Lemma M_pair2 x y :
    y {x; y}.
  Proof.
    apply M_pair. now right.
  Qed.


  Lemma sing_pair x y z :
    {x; x} = {y; z} x = y x = z.
  Proof.
    intros He. split.
    - assert (H : y {y; z}) by apply M_pair1.
      rewrite He in H. apply M_pair in H. intuition.
    - assert (H : z {y; z}) by apply M_pair2.
      rewrite He in H. apply M_pair in H. intuition.
  Qed.


  Lemma opair_inj1 x x' y y' :
    M_opair x y = M_opair x' y' x = x'.
  Proof.
    intros He. assert (H : {x; x} M_opair x y) by apply M_pair1.
    rewrite He in H. apply M_pair in H as [H|H]; apply (sing_pair H).
  Qed.


  Lemma opair_inj2 x x' y y' :
    M_opair x y = M_opair x' y' y = y'.
  Proof.
    intros He. assert (y = x' y = y') as [| ]; trivial.
    - assert (H : {x; y} M_opair x y) by apply M_pair2.
      rewrite He in H. apply M_pair in H as [H|H].
      + symmetry in H. apply sing_pair in H. intuition.
      + assert (H' : y {x; y}) by apply M_pair2.
        rewrite H in H'. now apply M_pair in H'.
    - assert (x = x') as by now apply opair_inj1 in He.
      assert (H : {x'; y'} M_opair x' y') by apply M_pair2.
      rewrite He in H. apply M_pair in H as [H|H]; apply (sing_pair (eq_sym H)).
  Qed.


  Lemma opair_inj x x' y y' :
    M_opair x y = M_opair x' y' x = x' y = y'.
  Proof.
    intros H. split.
    - eapply opair_inj1; eassumption.
    - eapply opair_inj2; eassumption.
  Qed.


  Lemma sigma_el x y :
    x σ y x y x = y.
  Proof.
    rewrite M_adj. tauto.
  Qed.


  Lemma sigma_eq x :
    x σ x.
  Proof.
    apply sigma_el. now right.
  Qed.


  Lemma sigma_sub x :
    x σ x.
  Proof.
    intros y H. apply sigma_el. now left.
  Qed.


  Lemma pair_com x y :
    {x; y} = {y; x}.
  Proof.
    apply M_ext; intros z [| ] % M_pair; apply M_pair; auto.
  Qed.





  Fixpoint numeral n :=
    match n with
    | O
    | S n σ (numeral n)
    end.

  Definition trans x :=
     y, y x y x.

  Lemma numeral_trans n :
    trans (numeral n).
  Proof.
    induction n; cbn.
    - intros x H. now apply M_eset in H.
    - intros x [H| ] % sigma_el; try apply sigma_sub.
      apply IHn in H. intuition eauto using sigma_sub.
  Qed.


  Lemma numeral_wf n :
     numeral n numeral n.
  Proof.
    induction n.
    - apply M_eset.
    - intros [H|H] % sigma_el; fold numeral in *.
      + apply IHn. eapply numeral_trans; eauto. apply sigma_eq.
      + assert (numeral n numeral (S n)) by apply sigma_eq.
        now rewrite H in .
  Qed.


  Lemma numeral_lt k l :
    k < l numeral k numeral l.
  Proof.
    induction 1; cbn; apply sigma_el; auto.
  Qed.


  Lemma numeral_inj k l :
    numeral k = numeral l k = l.
  Proof.
    intros Hk. assert (k = l k < l l < k) as [H|[H|H]] by ; trivial.
    all: apply numeral_lt in H; rewrite Hk in H; now apply numeral_wf in H.
  Qed.


  Definition htrans x :=
    trans x y, y x trans y.

  Lemma numeral_numeral n x :
    x numeral n k, x = numeral k.
  Proof.
    intros H. induction n; cbn in *.
    - now apply M_eset in H.
    - apply sigma_el in H as [H|H].
      + apply IHn, H.
      + exists n. apply H.
  Qed.


  Lemma numeral_htrans n :
    htrans (numeral n).
  Proof.
    split; try apply numeral_trans.
    intros y [k ] % numeral_numeral. apply numeral_trans.
  Qed.


  Lemma numeral_trans_sub x n :
    ( x y, (x y) + ( x y)) x numeral n trans x sig ( n x = numeral n).
  Proof.
    intros d. induction n; cbn.
    - intros H _. exists 0. cbn. apply M_ext; trivial. intros y [] % M_eset.
    - intros Hn Hx. destruct (d (numeral n) x) as [H|H].
      + exists (S n). cbn. apply M_ext; trivial.
        intros y [Hy| ] % sigma_el; trivial.
        now apply (Hx (numeral n)).
      + apply IHn; trivial. intros y Hy.
        specialize (Hn y Hy). apply sigma_el in Hn as [Hn| ]; tauto.
  Qed.




  Definition M_enc_bool (x : bool) :=
    if x then {; } else .

  Fixpoint M_prep_string (s : string bool) x :=
    match s with
    | nil x
    | b::s M_opair (M_enc_bool b) (M_prep_string s x)
    end.

  Definition M_enc_string (s : string bool) :=
    M_prep_string s .

  Definition M_enc_card s t :=
    M_opair (M_enc_string s) (M_enc_string t).

  Fixpoint M_enc_stack (B : BSRS) :=
    match B with
    | nil
    | (s,t)::B M_enc_card s t ::: M_enc_stack B
    end.


  Lemma enc_bool_inj b c :
    M_enc_bool b = M_enc_bool c b = c.
  Proof.
    destruct b, c; trivial; cbn.
    - intros H. contradiction (@M_eset ).
      pattern at 2. rewrite H. apply M_pair; auto.
    - intros H. contradiction (@M_eset ).
      pattern at 2. rewrite H. apply M_pair; auto.
  Qed.


  Lemma enc_string_inj s t :
    M_enc_string s = M_enc_string t s = t.
  Proof.
    induction s in t|-*; destruct t as [|b t]; cbn; trivial.
    - intros H. contradiction (M_eset (x:=M_sing (M_enc_bool b))).
      rewrite H. apply M_pair. now left.
    - intros H. contradiction (M_eset (x:=M_sing (M_enc_bool a))).
      rewrite H. apply M_pair. now left.
    - intros [ ] % opair_inj. apply IHs in as .
      apply enc_bool_inj in as . reflexivity.
  Qed.



  Lemma eval_opair rho x y :
    eval (opair x y) = M_opair (eval x) (eval y).
  Proof.
    cbn. reflexivity.
  Qed.


  Lemma eval_enc_bool rho b :
    eval (enc_bool b) = M_enc_bool b.
  Proof.
    destruct b; reflexivity.
  Qed.


  Lemma eval_prep_string rho s x :
    eval (prep_string s x) = M_prep_string s (eval x).
  Proof.
    induction s; trivial. cbn [prep_string].
    now rewrite eval_opair, IHs, eval_enc_bool.
  Qed.


  Lemma eval_enc_string rho s :
    eval (enc_string s) = M_enc_string s.
  Proof.
    unfold enc_string. now rewrite eval_prep_string.
  Qed.


  Lemma eval_enc_stack rho B :
    eval (enc_stack B) = M_enc_stack B.
  Proof.
    induction B; cbn; trivial. destruct a. cbn. unfold M_enc_card.
    now rewrite IHB, !eval_enc_string with (:=), eval_opair.
  Qed.



  Lemma enc_stack_el' x A :
    x M_enc_stack A s t, (s, t) A x = M_enc_card s t.
  Proof.
    induction A as [|[s t] A IH]; cbn.
    - now intros H % M_eset.
    - intros [|H] % M_adj.
      + exists s, t. intuition.
      + destruct (IH H) as (u&v&H'&). exists u, v. intuition.
  Qed.


  Lemma enc_stack_el B s t :
    (s, t) B M_enc_card s t M_enc_stack B.
  Proof.
    induction B as [|[u b] B IH]; cbn; auto.
    intros [[=]|H]; subst; apply M_adj; auto.
  Qed.


  Lemma M_prep_enc s s' :
    M_prep_string s (M_enc_string s') = M_enc_string (s s').
  Proof.
    induction s; cbn; trivial.
    now rewrite IHs.
  Qed.




  Definition append_all A (c : card bool) :=
    map ( p (fst c fst p, snd c snd p)) A.

  Definition derivation_step B C :=
    flat_map (append_all C) B.

  Fixpoint derivations B n :=
    match n with
    | O B
    | S n derivation_step B (derivations B n)
    end.

  Lemma derivable_derivations B s t :
    derivable B s t n, (s, t) derivations B n.
  Proof.
    induction 1.
    - exists 0. apply H.
    - destruct IHderivable as [n Hn]. exists (S n).
      apply in_flat_map. exists (x, y). split; trivial.
      apply in_map_iff. exists (u,v). cbn. split; trivial.
  Qed.


  Fixpoint M_enc_derivations B n :=
    match n with
    | O M_sing (M_opair (M_enc_stack B))
    | S n M_opair (numeral (S n)) (M_enc_stack (derivations B (S n))) ::: M_enc_derivations B n
    end.

  Lemma enc_derivations_base B n :
    M_opair (M_enc_stack B) M_enc_derivations B n.
  Proof.
    induction n; cbn.
    - now apply sing_el.
    - apply M_adj. now right.
  Qed.


  Lemma enc_derivations_bound B n k x :
    M_opair k x M_enc_derivations B n k σ (numeral n).
  Proof.
    induction n; cbn.
    - intros H % sing_el. apply opair_inj in H as [ _].
      apply sigma_el. now right.
    - intros [H|H] % M_adj.
      + apply opair_inj in H as [ _]. apply sigma_eq.
      + apply sigma_el. left. apply IHn, H.
  Qed.


  Lemma enc_derivations_fun B n :
     k x y, M_opair k x M_enc_derivations B n M_opair k y M_enc_derivations B n x = y.
  Proof.
    induction n; cbn -[derivations]; intros k x y.
    - intros % sing_el % sing_el.
      rewrite in . now apply opair_inj in .
    - intros [|] % M_adj [|] % M_adj.
      + rewrite in . now apply opair_inj in .
      + exfalso. apply enc_derivations_bound in .
        destruct (opair_inj ) as [ _]. now apply (@numeral_wf (S n)).
      + exfalso. apply enc_derivations_bound in .
        destruct (opair_inj ) as [ _]. now apply (@numeral_wf (S n)).
      + now apply (IHn k x y).
  Qed.


  Lemma enc_derivations_el B n k x :
    M_opair k x M_enc_derivations B n l, k = numeral l x = M_enc_stack (derivations B l).
  Proof.
    induction n; cbn.
    - intros H % sing_el. exists 0. apply (opair_inj H).
    - intros [H|H] % M_adj.
      + exists (S n). apply (opair_inj H).
      + apply IHn, H.
  Qed.


  Lemma enc_derivations_step B n l :
    numeral l numeral n
     M_opair (σ (numeral l)) (M_enc_stack (derivations B (S l))) M_enc_derivations B n.
  Proof.
    induction n; cbn -[derivations].
    - now intros H % M_eset.
    - intros [H|H] % M_adj; apply M_adj.
      + left. now apply numeral_inj in H as .
      + right. apply IHn, H.
  Qed.


  Definition M_is_bunion a b c :=
    a c b c d, d c d a d b.

  Lemma M_enc_stack_app A B :
    M_is_bunion (M_enc_stack A) (M_enc_stack B) (M_enc_stack (A B)).
  Proof.
    induction A as [|[s t] A IH]; cbn.
    - repeat split; auto. intros x [] % M_eset.
    - repeat split.
      + intros x [|H] % M_adj; apply M_adj; auto. right. now apply IH in H.
      + intros x H. apply M_adj. right. now apply IH in H.
      + intros x [|H] % M_adj; rewrite M_adj; auto. apply IH in H. tauto.
  Qed.


  Lemma M_bunion_unique a b c c' :
    M_is_bunion a b c M_is_bunion a b c' c = c'.
  Proof.
    intros . apply M_ext; firstorder.
  Qed.


  Lemma enc_stack_combinations B rho C x X Y :
     combinations B X Y eval X = M_enc_stack C eval Y = x x = M_enc_stack (derivation_step B C).
  Proof.
    induction B as [|[s t] B IH] in ,C,x,X,Y |-*.
    - cbn. rewrite VIEQ. now intros _ .
    - intros [[[[ ]]]] ; fold sat in *.
      assert (M_is_bunion x).
      { rewrite . cbn in . destruct as [[ ] ]. repeat split; intros y.
        - specialize ( y). rewrite !eval_comp in . apply .
        - specialize ( y). rewrite !eval_comp in . apply .
        - specialize ( y). rewrite !eval_comp in . apply . } clear .
      cbn. fold (derivation_step B C).
      enough ( = M_enc_stack (derivation_step B C)) as .
      + enough ( = M_enc_stack (append_all C (s, t))) as .
        { eapply M_bunion_unique; try apply H. rewrite , . apply M_enc_stack_app. }
        apply M_ext; intros u Hu.
        * apply in Hu as [v [Hv[a [b Ha]]]].
          cbn in Hv. erewrite !eval_comp, eval_ext, in Hv; trivial.
          apply enc_stack_el' in Hv as (s'&t'&Hst&Hv).
          enough (u = M_enc_card (ss') (tt')) as .
          { apply enc_stack_el. apply in_map_iff. now exists (s', t'). }
          cbn in Ha. rewrite !VIEQ in Ha. destruct Ha as [ ].
          rewrite in Hv. unfold M_enc_card in Hv. apply opair_inj in Hv as [ ].
          rewrite ; unfold M_enc_card, M_opair; repeat f_equal.
          all: rewrite eval_prep_string; cbn. all: apply M_prep_enc.
        * apply enc_stack_el' in Hu as (s'&t'&Hst&).
          unfold append_all in H. eapply in_map_iff in Hst as [[a b][Ha Hb]].
          cbn in H. apply . exists (M_enc_card a b). split.
          { cbn. erewrite !eval_comp, eval_ext, ; trivial. now apply enc_stack_el. }
          exists (M_enc_string b), (M_enc_string a). split.
          -- cbn. apply VIEQ. reflexivity.
          -- cbn. apply VIEQ. rewrite !eval_prep_string. cbn.
             rewrite !M_prep_enc. injection Ha. intros . reflexivity.
      + eapply IH; eauto. unfold shift. now erewrite !eval_comp, eval_ext, .
  Qed.


  Lemma enc_derivations_solutions B n rho a b :
    (a .: b .: M_enc_derivations B n .: numeral n .: ) solutions B $2 $3.
  Proof.
    cbn. split.
    - rewrite eval_enc_stack. apply enc_derivations_base.
    - intros k x x' .
      destruct (enc_derivations_el ) as [l[ ]].
      specialize (enc_derivations_step B ).
      replace (M_enc_stack (derivations B (S l))) with x'; trivial.
      apply (enc_stack_combinations ); trivial.
  Qed.


  Lemma derivations_enc_derivations B n :
    M_opair (numeral n) (M_enc_stack (derivations B n)) M_enc_derivations B n.
  Proof.
    induction n; cbn -[derivations].
    - now apply sing_el.
    - apply M_adj. now left.
  Qed.


  Lemma derivations_el B n s t :
    (s, t) derivations B n M_enc_card s t M_enc_stack (derivations B n).
  Proof.
    apply enc_stack_el.
  Qed.


  Theorem PCP_FST1 B s :
    derivable B s s rho, solvable B.
  Proof.
    intros H . destruct (derivable_derivations H) as [n Hn]. unfold solvable.
    exists (numeral n), (M_enc_derivations B n), (M_enc_string s), (M_enc_stack (derivations B n)).
    split; [split; [split; [split |] |] |].
    - apply numeral_htrans.
    - unfold function'. intros k x y . apply VIEQ. apply (enc_derivations_fun ).
    - apply enc_derivations_solutions.
    - cbn. apply derivations_enc_derivations.
    - now apply enc_stack_el.
  Qed.




  Definition M_comb_rel s t :=
     u v u1 u2, u = M_opair v = M_opair (M_prep_string s ) (M_prep_string t ).

  Fixpoint M_combinations B x y :=
    match B with
    | nil y =
    | (s,t)::B y1 y2, M_is_bunion y M_combinations B x
                           M_is_rep (M_comb_rel s t) x
    end.

  Lemma M_combinations_spec B rho x y a b :
    M_combinations B x y eval a = x eval b = y combinations B a b.
  Proof.
    induction B in y,a,b,|-*; cbn.
    - rewrite VIEQ. now intros _ .
    - destruct as [s t]. intros (&&&&) Ha Hb. exists , . split. split. 3: split.
      + cbn. repeat split; intros d; rewrite !eval_comp; unfold funcomp; cbn.
        all: change (eval ( x x) b) with (eval b); rewrite Hb; apply .
      + eapply (IHB _ ); trivial. erewrite !eval_comp. unfold funcomp. cbn.
        change (eval ( x x) a) with (eval a). now rewrite Ha.
      + intros (u & Hu & c & d' & H) % . exists u. split.
        * cbn. erewrite !eval_comp. erewrite eval_ext, Ha; trivial.
        * exists d', c. cbn. rewrite !VIEQ, !eval_prep_string. apply H.
      + intros (u & Hu & c & d' & H). apply . exists u. split.
        * cbn in Hu. erewrite !eval_comp in Hu. rewrite Ha. apply Hu.
        * exists d', c. cbn in H. rewrite !VIEQ, !eval_prep_string in H. apply H.
  Qed.


  Definition M_solutions B f n :=
    M_opair (M_enc_stack B) f k x y, k n M_opair k x f M_combinations B x y M_opair (σ k) y f.

  Lemma comb_rel_rep C s t :
    M_is_rep (M_comb_rel s t) (M_enc_stack C) (M_enc_stack (append_all C (s, t))).
  Proof.
    intros y. split.
    - intros (u&v&H&) % enc_stack_el'.
      unfold append_all in H. apply in_map_iff in H as [[a b][ ]]. cbn in .
      exists (M_enc_card a b). split; try now apply enc_stack_el.
      exists (M_enc_string a), (M_enc_string b). split; trivial.
      assert (u = sa) as by congruence. assert (v = tb) as by congruence.
      now rewrite !M_prep_enc.
    - intros (u&H&a&b&&). apply enc_stack_el' in H as [u[v[ ]]].
      apply opair_inj in as [ ]. rewrite !M_prep_enc. apply enc_stack_el.
      apply in_map_iff. now exists (u, v).
  Qed.


  Lemma M_combinations_step B C :
    M_combinations B (M_enc_stack C) (M_enc_stack (derivation_step B C)).
  Proof.
    induction B as [|[s t] B IH]; cbn; trivial.
    exists (M_enc_stack (derivation_step B C)), (M_enc_stack (append_all C (s, t))).
    split; try apply M_enc_stack_app. split; trivial.
    apply comb_rel_rep.
  Qed.


  Lemma solutions_derivations B f n k :
    M_solutions B f (numeral n) k n M_opair (numeral k) (M_enc_stack (derivations B k)) f.
  Proof.
    intros H Hk; induction k; cbn.
    - apply H.
    - assert (Hk' : k n) by . specialize (IHk Hk').
      destruct H as [_ H]. eapply H in IHk; eauto.
      + now apply numeral_lt.
      + apply M_combinations_step.
  Qed.


  Lemma derivations_derivable B n s t :
    (s, t) derivations B n derivable B s t.
  Proof.
    induction n in s,t|-*; cbn.
    - now constructor.
    - unfold derivation_step. intros [[u v][ ]] % in_flat_map.
      unfold append_all in . apply in_map_iff in as [[a b][ ]]. cbn in .
      assert (s = ua) as by congruence. assert (t = vb) as by congruence.
      constructor 2; trivial. apply IHn, .
  Qed.


  Definition M_function f :=
     x y y', M_opair x y f M_opair x y' f y = y'.

  Definition standard :=
     x, htrans x n, x numeral n.

  Lemma M_solutions_el B f k X p :
    standard htrans k M_function f M_solutions B f k M_opair k X f
     p X u v, p = M_enc_card u v derivable B u v.
  Proof.
    intros HS HO Hf Hk HX Hp. destruct (HS k HO) as [n % VIEQ].
    pose proof (H := solutions_derivations Hk (le_n n)).
    rewrite (Hf _ _ _ HX H) in Hp. apply enc_stack_el' in Hp as (s&t&H'&).
    exists s, t. split; trivial. eapply derivations_derivable; eauto.
  Qed.


  Theorem PCP_FST2 B rho :
    standard solvable B s, derivable B s s.
  Proof.
    intros VIN (n & f & s & X & [[[[ ] ] ] ]).
    assert ( : htrans n) by apply . clear .
    assert ( : M_opair n X f) by apply . clear .
    assert ( : M_opair s s X) by apply . clear .
    assert ( : M_function f).
    { intros x y y' H H'. apply VIEQ. eapply . apply H. apply H'. } clear .
    assert ( : M_opair (M_enc_stack B) f).
    { erewrite eval_enc_stack. apply . } destruct as [_ ].
    assert ( : k x y, k n M_opair k x f M_combinations B x y M_opair (σ k) y f).
    { intros k x y Hn Hk Hy. apply ( k x y); auto. fold sat. eapply M_combinations_spec; eauto. } clear .
    destruct (@M_solutions_el B f n X (M_opair s s)) as (u&v&&); trivial.
    now split. exists u. apply opair_inj in as [H ]. apply enc_string_inj in H as . apply .
  Qed.


End FST.


Arguments standard {_} _.

Theorem PCP_FST B :
  ( V (M : interp V), extensional M standard M rho, FST)
   PCPb B entailment_FST (solvable B).
Proof.
  intros HZF. rewrite PCPb_iff_dPCPb. split; intros H.
  - clear HZF. destruct H as [s H]. intros M HM . eapply PCP_FST1; eauto.
  - destruct HZF as (M & & & & ).
    specialize (H M ( _ @i_func _ _ _ _ eset Vector.nil) ).
    apply PCP_FST2 in H as [s Hs]; trivial. now exists s.
Qed.