(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

(** * Minsky machines to FRACTRAN programs *)
(** ** Removal of self-loops in MMs *)

Require Import List Arith Omega.

Require Import utils pos vec. 
Require Import subcode sss mm_defs.

Set Implicit Arguments.

Tactic Notation "rew" "length" := autorewrite with length_db.

Local Notation "e #> x" := (vec_pos e x).
Local Notation "e [ v / x ]" := (vec_change e x v).

Local Notation "I // s -1> t" := (mm_sss I s t).
Local Notation "P // s -[ k ]-> t" := (sss_steps (@mm_sss _) P k s t).
Local Notation "P // s -+> t" := (sss_progress (@mm_sss _) P s t).
Local Notation "P // s ->> t" := (sss_compute (@mm_sss _) P s t).
Local Notation "P // s '~~>' t" := (sss_output (@mm_sss _) P s t).
Local Notation "P // s ↓" := (sss_terminates (@mm_sss _) P s). 

Section self_loops.

  Variables (n : nat) (P : list (mm_instr n)).

  Lemma mm_self_loop_no_term_1 i x s v : 
              (i,DEC x i::nil) <sc (1,P) 
           -> s = (i,v)
           -> v#>x = 0  
           -> ~ (1,P) // s ↓.
  Proof.
(* Goal: forall (_ : @subcode (mm_instr n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x (Init.Nat.add (S O) i)) (@cons (mm_instr n) (@mm_dec n x i) (@nil (mm_instr n))))) (@pair nat (list (mm_instr n)) (S O) P)) (_ : or (@eq (prod nat (vec nat n)) s (@pair nat (vec nat n) i v)) (@eq (prod nat (vec nat n)) s (@pair nat (vec nat n) (Init.Nat.add (S O) i) v))) (_ : @eq nat (@vec_pos nat n v x) O), not (@sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) s) *)
    intros H1 H2 H3 (s0 & H4).
(* Goal: False *)
    revert i x v H1 H2 H3.
(* Goal: forall (v : vec nat n) (_ : or (@eq (prod nat (vec nat n)) s (@pair nat (vec nat n) i v)) (@eq (prod nat (vec nat n)) s (@pair nat (vec nat n) (Init.Nat.add (S O) i) v))) (_ : @eq nat (@vec_pos nat n v x) O), False *)
    pattern s; revert H4; apply mm_term_ind.
    + intros Hs0 i x v H1 H2 H3.
(* Goal: False *)
      subst s0.
(* Goal: False *)
      revert Hs0; apply in_out_code.
(* Goal: @in_code (mm_instr n) (@fst nat (vec nat n) (@pair nat (vec nat n) i v)) (@pair nat (list (mm_instr n)) (S O) P) *)
      apply subcode_in_code with (1 := H1).
(* Goal: @in_code (mm_instr n) p (@pair nat (list (mm_instr n)) (S O) P) *)
      simpl; omega.
    + intros i ρ v j w H1 H2 H3 IH3 k x p G1 G2 G3.
(* Goal: False *)
      inversion G2; subst p k.
(* Goal: False *)
      generalize (subcode_cons_inj _ _ _ _ H1 G1); intros; subst.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
      apply mm_sss_DEC0_inv in H2; auto.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
      destruct H2; subst j w.
(* Goal: False *)
      apply (IH3 _ _ _ G1 eq_refl); auto.
  Qed.

  Lemma mm_self_loop_no_term_2 i x s v : 
              (i,DEC x (1+i)::DEC x i::nil) <sc (1,P) 
           -> s = (i,v) \/ s = (1+i,v)
           -> v#>x = 0  
           -> ~ (1,P) // s ↓.
  Proof.
(* Goal: forall (_ : @subcode (mm_instr n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x (Init.Nat.add (S O) i)) (@cons (mm_instr n) (@mm_dec n x i) (@nil (mm_instr n))))) (@pair nat (list (mm_instr n)) (S O) P)) (_ : or (@eq (prod nat (vec nat n)) s (@pair nat (vec nat n) i v)) (@eq (prod nat (vec nat n)) s (@pair nat (vec nat n) (Init.Nat.add (S O) i) v))) (_ : @eq nat (@vec_pos nat n v x) O), not (@sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) s) *)
    intros H1 H2 H3 (s0 & H4).
(* Goal: False *)
    revert v H2 H3.
(* Goal: forall (v : vec nat n) (_ : or (@eq (prod nat (vec nat n)) s (@pair nat (vec nat n) i v)) (@eq (prod nat (vec nat n)) s (@pair nat (vec nat n) (Init.Nat.add (S O) i) v))) (_ : @eq nat (@vec_pos nat n v x) O), False *)
    pattern s; revert H4; apply mm_term_ind.
    + intros Hs0 v H2 H3.
      destruct H2; subst s0; revert Hs0; apply in_out_code;
(* Goal: @in_code (mm_instr n) p (@pair nat (list (mm_instr n)) (S O) P) *)
        apply subcode_in_code with (1 := H1); simpl; omega.
    + apply subcode_cons_invert_left in H1.
(* Goal: forall (i0 : nat) (ρ : mm_instr n) (v : vec nat n) (j : nat) (w : vec nat n) (_ : @subcode (mm_instr n) (@pair nat (list (mm_instr n)) i0 (@cons (mm_instr n) ρ (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) (S O) P)) (_ : @mm_sss n ρ (@pair nat (vec nat n) i0 v) (@pair nat (vec nat n) j w)) (_ : @sss_output (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) j w) s0) (_ : forall (v0 : vec nat n) (_ : or (@eq (prod nat (vec nat n)) (@pair nat (vec nat n) j w) (@pair nat (vec nat n) i v0)) (@eq (prod nat (vec nat n)) (@pair nat (vec nat n) j w) (@pair nat (vec nat n) (Init.Nat.add (S O) i) v0))) (_ : @eq nat (@vec_pos nat n v0 x) O), False) (v0 : vec nat n) (_ : or (@eq (prod nat (vec nat n)) (@pair nat (vec nat n) i0 v) (@pair nat (vec nat n) i v0)) (@eq (prod nat (vec nat n)) (@pair nat (vec nat n) i0 v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) v0))) (_ : @eq nat (@vec_pos nat n v0 x) O), False *)
      destruct H1 as [ G0 G1 ].
(* Goal: forall (i0 : nat) (ρ : mm_instr n) (v : vec nat n) (j : nat) (w : vec nat n) (_ : @subcode (mm_instr n) (@pair nat (list (mm_instr n)) i0 (@cons (mm_instr n) ρ (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) (S O) P)) (_ : @mm_sss n ρ (@pair nat (vec nat n) i0 v) (@pair nat (vec nat n) j w)) (_ : @sss_output (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) j w) s0) (_ : forall (v0 : vec nat n) (_ : or (@eq (prod nat (vec nat n)) (@pair nat (vec nat n) j w) (@pair nat (vec nat n) i v0)) (@eq (prod nat (vec nat n)) (@pair nat (vec nat n) j w) (@pair nat (vec nat n) (Init.Nat.add (S O) i) v0))) (_ : @eq nat (@vec_pos nat n v0 x) O), False) (v0 : vec nat n) (_ : or (@eq (prod nat (vec nat n)) (@pair nat (vec nat n) i0 v) (@pair nat (vec nat n) i v0)) (@eq (prod nat (vec nat n)) (@pair nat (vec nat n) i0 v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) v0))) (_ : @eq nat (@vec_pos nat n v0 x) O), False *)
      intros l ρ v j w H1 H2 H3 IH3 r G2 G3.
(* Goal: False *)
      destruct G2 as [ G2 | G2 ]; inversion G2; subst l v.
      * generalize (subcode_cons_inj _ _ _ _ H1 G0); intros; subst.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
        apply mm_sss_DEC0_inv in H2; auto.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
        destruct H2; subst j w.
(* Goal: False *)
        revert G3; apply IH3; auto.
(* Goal: False *)
      * generalize (subcode_cons_inj _ _ _ _ H1 G1); intros; subst.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
        apply mm_sss_DEC0_inv in H2; auto.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
        destruct H2; subst j w.
(* Goal: False *)
        revert G3; apply IH3; auto.
  Qed.

End self_loops.

Section no_self_loops.

  Variables (n : nat).

  Definition mm_no_self_loops (Q : nat * list (mm_instr n)) := forall i x, ~ (i,DEC x i::nil) <sc Q.

  Implicit Types (P Q : list (mm_instr n)).

  Fact mm_no_self_loops_app i P Q : mm_no_self_loops (i,P) 
                                 -> mm_no_self_loops (length P +i,Q)
                                 -> mm_no_self_loops (i,P++Q).
  Proof.
(* Goal: forall (_ : mm_no_self_loops (@pair nat (list (mm_instr n)) i P)) (_ : mm_no_self_loops (@pair nat (list (mm_instr n)) (Init.Nat.add (@length (mm_instr n) P) i) Q)), mm_no_self_loops (@pair nat (list (mm_instr n)) i (@app (mm_instr n) P Q)) *)
    intros H1 H2 j x H.
(* Goal: or (@ex (mm_instr n) (fun ρ' : mm_instr n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) ρ' (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) (S O) P)) (@eq (mm_instr (S n)) ρ (f (Init.Nat.add (S O) (@length (mm_instr n) P)) j ρ')))) (or (and (@eq nat j (Init.Nat.add (S O) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) O))) (or (and (@eq nat j (Init.Nat.add (S (S O)) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S (S (S O))) (@length (mm_instr n) P))))) (and (@eq nat j (Init.Nat.add (S (S (S O))) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S (S O)) (@length (mm_instr n) P))))))) *)
    apply subcode_app_invert_right in H.
(* Goal: False *)
    destruct H as [ H | H ]; revert H.
    + apply H1.
    + apply H2.
  Qed.

End no_self_loops.

Section remove_self_loops.

  (** To safely remove self loops from (1,P) 
        1/ we map them to 2+lP 
        2/ we map outside jumps to 0
        3/ we append to P to 3 following instructions
             1+lP: DEC nv 0; DEC nv 3+lP; DEC nv 2+lP 

           where nv is a new and unused variable
    *)

  Variables (n : nat).

  Implicit Types (P Q : list (mm_instr n)).

  Let f k i (ρ : mm_instr n) := 
    match ρ with
      | INC x   => INC (pos_nxt x)
      | DEC x j => DEC (pos_nxt x) (if eq_nat_dec i j     then 1+k 
                                    else if le_lt_dec k j then 0
                                                          else j)
    end.

  Let Fixpoint g k i P := 
    match P with
      | nil  => nil
      | ρ::P => f k i ρ :: g k (S i) P
    end.

  Let g_app k i P Q : g k i (P++Q) = g k i P ++ g k (length P + i) Q.
  Proof.
(* Goal: @eq (list (mm_instr (S n))) (g k i (@app (mm_instr n) P Q)) (@app (mm_instr (S n)) (g k i P) (g k (Init.Nat.add (@length (mm_instr n) P) i) Q)) *)
    revert i; induction P as [ | ? P IHP ]; intros i; simpl; f_equal; auto.
(* Goal: @eq (list (mm_instr (S n))) (g k (S i) (@app (mm_instr n) P Q)) (@app (mm_instr (S n)) (g k (S i) P) (g k (S (Init.Nat.add (@length (mm_instr n) P) i)) Q)) *)
    rewrite IHP; do 2 f_equal; omega.
  Qed.

  Let g_app_inv k i P l r : g k i P = l ++ r -> exists L R, P = L++R /\ l = g k i L /\ r = g k (length l+i) R.
  Proof.
(* Goal: forall _ : @eq (list (mm_instr (S n))) (g k i P) (@app (mm_instr (S n)) l r), @ex (list (mm_instr n)) (fun L : list (mm_instr n) => @ex (list (mm_instr n)) (fun R : list (mm_instr n) => and (@eq (list (mm_instr n)) P (@app (mm_instr n) L R)) (and (@eq (list (mm_instr (S n))) l (g k i L)) (@eq (list (mm_instr (S n))) r (g k (Init.Nat.add (@length (mm_instr (S n)) l) i) R))))) *)
    revert i l r.
(* Goal: forall (i : nat) (l r : list (mm_instr (S n))) (_ : @eq (list (mm_instr (S n))) (g k i P) (@app (mm_instr (S n)) l r)), @ex (list (mm_instr n)) (fun L : list (mm_instr n) => @ex (list (mm_instr n)) (fun R : list (mm_instr n) => and (@eq (list (mm_instr n)) P (@app (mm_instr n) L R)) (and (@eq (list (mm_instr (S n))) l (g k i L)) (@eq (list (mm_instr (S n))) r (g k (Init.Nat.add (@length (mm_instr (S n)) l) i) R))))) *)
    induction P as [ | ρ P IHP ]; intros i l r; simpl.
    + intros H; symmetry in H; exists nil, nil; simpl.
(* Goal: and (@eq (list (mm_instr n)) (@nil (mm_instr n)) (@nil (mm_instr n))) (and (@eq (list (mm_instr (S n))) l (@nil (mm_instr (S n)))) (@eq (list (mm_instr (S n))) r (@nil (mm_instr (S n))))) *)
      apply app_eq_nil in H; tauto.
    + destruct l as [ | y l ]; simpl.
      * exists nil, (ρ::P); simpl in *; auto.
      * intros H; injection H; clear H; intros H1 H2.
(* Goal: @ex (list (mm_instr n)) (fun L : list (mm_instr n) => @ex (list (mm_instr n)) (fun R : list (mm_instr n) => and (@eq (list (mm_instr n)) (@cons (mm_instr n) ρ P) (@app (mm_instr n) L R)) (and (@eq (list (mm_instr (S n))) (@cons (mm_instr (S n)) y l) (g k i L)) (@eq (list (mm_instr (S n))) r (g k (S (Init.Nat.add (@length (mm_instr (S n)) l) i)) R))))) *)
        destruct IHP with (1 := H1) as (L & R & G1 & G2 & G3); subst.
(* Goal: @ex (list (mm_instr n)) (fun L0 : list (mm_instr n) => @ex (list (mm_instr n)) (fun R0 : list (mm_instr n) => and (@eq (list (mm_instr n)) (@cons (mm_instr n) ρ (@app (mm_instr n) L R)) (@app (mm_instr n) L0 R0)) (and (@eq (list (mm_instr (S n))) (@cons (mm_instr (S n)) (f k i ρ) (g k (S i) L)) (g k i L0)) (@eq (list (mm_instr (S n))) (g k (Init.Nat.add (@length (mm_instr (S n)) (g k (S i) L)) (S i)) R) (g k (S (Init.Nat.add (@length (mm_instr (S n)) (g k (S i) L)) i)) R0))))) *)
        exists (ρ::L), R; simpl; repeat (split; auto).
(* Goal: @eq (mm_instr (S n)) (f k (Init.Nat.add (@length (mm_instr (S n)) l) i) ρ') (f k j ρ') *)
        f_equal; omega.
  Qed.
 
  Let length_g l i P : length (g l i P) = length P.
  Proof. revert i; induction P; simpl; auto. Qed. 

  Let g_subcode k i P j ρ : (j,ρ::nil) <sc (i,P) -> (j, f k j ρ::nil) <sc (i,g k i P).
  Proof.
(* Goal: forall _ : @subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) ρ (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i P), @subcode (mm_instr (S n)) (@pair nat (list (mm_instr (S n))) j (@cons (mm_instr (S n)) (f k j ρ) (@nil (mm_instr (S n))))) (@pair nat (list (mm_instr (S n))) i (g k i P)) *)
    intros (l & r & H1 & H2); subst P.
(* Goal: @subcode (mm_instr (S n)) (@pair nat (list (mm_instr (S n))) j (@cons (mm_instr (S n)) (f k j ρ) (@nil (mm_instr (S n))))) (@pair nat (list (mm_instr (S n))) i (g k i (@app (mm_instr n) l (@app (mm_instr n) (@cons (mm_instr n) ρ (@nil (mm_instr n))) r)))) *)
    rewrite g_app; simpl.
    exists (g k i l), (g k (S (length l+i)) r); split.
    + do 3 f_equal; omega.
    + rewrite length_g; auto.
  Qed.

  Let subcode_g k i P j ρ : (j,ρ::nil) <sc (i,g k i P) -> exists ρ', (j,ρ'::nil) <sc (i,P) /\ ρ = f k j ρ'.
  Proof.
(* Goal: forall _ : @subcode (mm_instr (S n)) (@pair nat (list (mm_instr (S n))) j (@cons (mm_instr (S n)) ρ (@nil (mm_instr (S n))))) (@pair nat (list (mm_instr (S n))) i (g k i P)), @ex (mm_instr n) (fun ρ' : mm_instr n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) ρ' (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i P)) (@eq (mm_instr (S n)) ρ (f k j ρ'))) *)
    intros (l & r & H1 & H2).
(* Goal: @ex (mm_instr n) (fun ρ' : mm_instr n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) ρ' (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i P)) (@eq (mm_instr (S n)) ρ (f k j ρ'))) *)
    apply g_app_inv in H1.
(* Goal: @ex (mm_instr n) (fun ρ' : mm_instr n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) ρ' (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i P)) (@eq (mm_instr (S n)) ρ (f k j ρ'))) *)
    destruct H1 as (L & [ | ρ' R ] & H1 & H3 & H4); try discriminate.
(* Goal: @ex (mm_instr n) (fun ρ' : mm_instr n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) ρ' (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i P)) (@eq (mm_instr (S n)) ρ (f k j ρ'))) *)
    simpl in H4; inversion H4.
(* Goal: @ex (mm_instr n) (fun ρ'0 : mm_instr n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) ρ'0 (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i P)) (@eq (mm_instr (S n)) (f k (Init.Nat.add (@length (mm_instr (S n)) l) i) ρ') (f k j ρ'0))) *)
    exists ρ'; split; auto.
    + exists L, R; simpl; split; auto.
(* Goal: @eq nat j (Init.Nat.add i (@length (mm_instr n) L)) *)
      rewrite H3, length_g in H2; auto.
    + f_equal; omega.
  Qed.

  Let g_loops k i P : 1 <= i -> i+length P <= k -> mm_no_self_loops (i,g k i P).
  Proof.
(* Goal: forall (_ : le (S O) i) (_ : le (Init.Nat.add i (@length (mm_instr n) P)) k), @mm_no_self_loops (S n) (@pair nat (list (mm_instr (S n))) i (g k i P)) *)
    intros H0 H1 j x H2.
(* Goal: False *)
    apply subcode_g in H2.
(* Goal: False *)
    destruct H2 as ([ y | y q ] & H2 & H3); simpl in H3; try discriminate.
(* Goal: False *)
    inversion H3; subst; simpl in H1.
    apply subcode_in_code with (i:= j) in H2; simpl in H2 |- *; try omega.
(* Goal: False *)
    destruct (eq_nat_dec j q); try omega.
(* Goal: False *)
    destruct (le_lt_dec k q); omega.
  Qed.

  Variable P : list (mm_instr n).

  Notation lP := (length P).

  Let R : list (mm_instr (S n)) := DEC pos0 0 
                                :: DEC pos0 (3+lP)
                                :: DEC pos0 (2+lP)
                                :: nil.

  Let sc_R_1 : (1+lP, DEC pos0 0 :: nil) <sc (1+lP, R).
  Proof. unfold R; auto. Qed.

  Let sc_R_2 : (2+lP, DEC pos0 (1+(2+lP)) :: DEC pos0 (2+lP) :: nil) <sc (1+lP, R).
  Proof. 
(* Goal: @subcode (mm_instr (S n)) (@pair nat (list (mm_instr (S n))) (Init.Nat.add (S (S O)) (@length (mm_instr n) P)) (@cons (mm_instr (S n)) (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S O) (Init.Nat.add (S (S O)) (@length (mm_instr n) P)))) (@cons (mm_instr (S n)) (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S (S O)) (@length (mm_instr n) P))) (@nil (mm_instr (S n)))))) (@pair nat (list (mm_instr (S n))) (Init.Nat.add (S O) (@length (mm_instr n) P)) R) *)
    unfold R; rewrite plus_assoc; simpl plus.
(* Goal: @subcode (mm_instr (S n)) (@pair nat (list (mm_instr (S n))) (S (S (@length (mm_instr n) P))) (@cons (mm_instr (S n)) (@mm_dec (S n) (@pos_fst n) (S (S (S (@length (mm_instr n) P))))) (@cons (mm_instr (S n)) (@mm_dec (S n) (@pos_fst n) (S (S (@length (mm_instr n) P)))) (@nil (mm_instr (S n)))))) (@pair nat (list (mm_instr (S n))) (S (@length (mm_instr n) P)) (@cons (mm_instr (S n)) (@mm_dec (S n) (@pos_fst n) O) (@cons (mm_instr (S n)) (@mm_dec (S n) (@pos_fst n) (S (S (S (@length (mm_instr n) P))))) (@cons (mm_instr (S n)) (@mm_dec (S n) (@pos_fst n) (S (S (@length (mm_instr n) P)))) (@nil (mm_instr (S n))))))) *)
    exists (DEC pos0 0 :: nil), nil; simpl; split; auto; omega.
  Qed.

  Let R_sc i rho : (i,rho::nil) <sc (1+lP,R) -> i = 1+lP /\ rho = DEC pos0 0
                                             \/ i = 2+lP /\ rho = DEC pos0 (3+lP)
                                             \/ i = 3+lP /\ rho = DEC pos0 (2+lP).
  Proof.
(* Goal: forall _ : @subcode (mm_instr (S n)) (@pair nat (list (mm_instr (S n))) i (@cons (mm_instr (S n)) rho (@nil (mm_instr (S n))))) (@pair nat (list (mm_instr (S n))) (Init.Nat.add (S O) (@length (mm_instr n) P)) R), or (and (@eq nat i (Init.Nat.add (S O) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) rho (@mm_dec (S n) (@pos_fst n) O))) (or (and (@eq nat i (Init.Nat.add (S (S O)) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) rho (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S (S (S O))) (@length (mm_instr n) P))))) (and (@eq nat i (Init.Nat.add (S (S (S O))) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) rho (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S (S O)) (@length (mm_instr n) P)))))) *)
    unfold R; intros ([ | u [ | v [ | w l ] ] ] & r & H1 & H2); inversion H1; subst i; simpl.
    + do 0 right; left; split; auto; omega.
    + do 1 right; left; split; auto; omega.
    + do 2 right; split; auto; omega.
    + destruct l; discriminate.
  Qed.

  Let R_no_self_loops : mm_no_self_loops (1+lP,R).
  Proof.
(* Goal: @mm_no_self_loops (S n) (@pair nat (list (mm_instr (S n))) (Init.Nat.add (S O) (@length (mm_instr n) P)) R) *)
    intros i rho H.
(* Goal: False *)
    apply R_sc in H.
(* Goal: lt j (Init.Nat.add (S O) (Init.Nat.add (@length (mm_instr n) P) (S (S (S O))))) *)
    destruct H as [ (H1 & H2) | H ].
(* Goal: @in_code (mm_instr n) (Init.Nat.add (S O) i) (@pair nat (list (mm_instr n)) (S O) P) *)
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
    { inversion H2; omega. }
(* Goal: lt j (Init.Nat.add (S O) (Init.Nat.add (@length (mm_instr n) P) (S (S (S O))))) *)
    destruct H as [ (H1 & H2) | H ].
(* Goal: @in_code (mm_instr n) (Init.Nat.add (S O) i) (@pair nat (list (mm_instr n)) (S O) P) *)
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
    { inversion H2; omega. }
(* Goal: lt j (Init.Nat.add (S O) (Init.Nat.add (@length (mm_instr n) P) (S (S (S O))))) *)
    destruct H as (H1 & H2).
(* Goal: @in_code (mm_instr n) (Init.Nat.add (S O) i) (@pair nat (list (mm_instr n)) (S O) P) *)
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
    { inversion H2; omega. }
  Qed.
 
  Let Q := g (1+lP) 1 P ++ R.

  Let Q_no_self_loops : mm_no_self_loops (1,Q).
  Proof.
(* Goal: @mm_no_self_loops (S n) (@pair nat (list (mm_instr (S n))) (S O) Q) *)
    apply mm_no_self_loops_app.
    + apply g_loops; simpl; omega. 
    + rewrite length_g, plus_comm; auto.
  Qed.

  Let sc_Q_1 j ρ : (j,ρ::nil) <sc (1,P) -> (j, f (1+lP) j ρ::nil) <sc (1,Q).
  Proof. intro; apply subcode_app_end, g_subcode; auto. Qed.

  Let sc_Q_2 : (1+lP, DEC pos0 0 :: DEC pos0 (3+lP) :: DEC pos0 (2+lP) :: nil) <sc (1,Q).
  Proof. apply subcode_right; rewrite length_g; auto. Qed.

  Let sc_Q_3 : (2+lP, DEC pos0 (3+lP) :: DEC pos0 (2+lP) :: nil) <sc (1,Q).
  Proof. apply subcode_trans with (2 := sc_Q_2); auto. Qed.
 
  Let Q_sc j ρ : (j,ρ::nil) <sc (1,Q) 
              -> (exists ρ', (j,ρ'::nil) <sc (1,P) /\ ρ = f (1+lP) j ρ')
              \/ j = 1+lP /\ ρ = DEC pos0 0
              \/ j = 2+lP /\ ρ = DEC pos0 (3+lP)
              \/ j = 3+lP /\ ρ = DEC pos0 (2+lP).
  Proof.
(* Goal: forall _ : @subcode (mm_instr (S n)) (@pair nat (list (mm_instr (S n))) j (@cons (mm_instr (S n)) ρ (@nil (mm_instr (S n))))) (@pair nat (list (mm_instr (S n))) (S O) Q), or (@ex (mm_instr n) (fun ρ' : mm_instr n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) ρ' (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) (S O) P)) (@eq (mm_instr (S n)) ρ (f (Init.Nat.add (S O) (@length (mm_instr n) P)) j ρ')))) (or (and (@eq nat j (Init.Nat.add (S O) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) O))) (or (and (@eq nat j (Init.Nat.add (S (S O)) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S (S (S O))) (@length (mm_instr n) P))))) (and (@eq nat j (Init.Nat.add (S (S (S O))) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S (S O)) (@length (mm_instr n) P))))))) *)
    intros H.
(* Goal: or (@ex (mm_instr n) (fun ρ' : mm_instr n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) ρ' (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) (S O) P)) (@eq (mm_instr (S n)) ρ (f (Init.Nat.add (S O) (@length (mm_instr n) P)) j ρ')))) (or (and (@eq nat j (Init.Nat.add (S O) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) O))) (or (and (@eq nat j (Init.Nat.add (S (S O)) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S (S (S O))) (@length (mm_instr n) P))))) (and (@eq nat j (Init.Nat.add (S (S (S O))) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S (S O)) (@length (mm_instr n) P))))))) *)
    apply subcode_app_invert_right in H.
(* Goal: or (@ex (mm_instr n) (fun ρ' : mm_instr n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) ρ' (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) (S O) P)) (@eq (mm_instr (S n)) ρ (f (Init.Nat.add (S O) (@length (mm_instr n) P)) j ρ')))) (or (and (@eq nat j (Init.Nat.add (S O) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) O))) (or (and (@eq nat j (Init.Nat.add (S (S O)) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S (S (S O))) (@length (mm_instr n) P))))) (and (@eq nat j (Init.Nat.add (S (S (S O))) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S (S O)) (@length (mm_instr n) P))))))) *)
    destruct H as [ H | H ].
    + apply subcode_g in H; auto.
    + rewrite length_g, plus_comm in H. 
(* Goal: or (@ex (mm_instr n) (fun ρ' : mm_instr n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) ρ' (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) (S O) P)) (@eq (mm_instr (S n)) ρ (f (Init.Nat.add (S O) (@length (mm_instr n) P)) j ρ')))) (or (and (@eq nat j (Init.Nat.add (S O) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) O))) (or (and (@eq nat j (Init.Nat.add (S (S O)) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S (S (S O))) (@length (mm_instr n) P))))) (and (@eq nat j (Init.Nat.add (S (S (S O))) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S (S O)) (@length (mm_instr n) P))))))) *)
      apply R_sc in H; auto.
  Qed. 

  Let Q_length : length Q = length P + 3.
  Proof. 
(* Goal: @eq nat (@length (mm_instr (S n)) Q) (Init.Nat.add (@length (mm_instr n) P) (S (S (S O)))) *)
    unfold Q; rewrite app_length, length_g.
(* Goal: @eq nat (Init.Nat.add (@length (mm_instr n) P) (@length (mm_instr (S n)) R)) (Init.Nat.add (@length (mm_instr n) P) (S (S (S O)))) *)
    unfold R; auto.
  Qed.

  Let Q_bound i x j : (i,DEC x j::nil) <sc (1,Q) -> j < 1+length Q.
  Proof.
(* Goal: forall _ : @subcode (mm_instr (S n)) (@pair nat (list (mm_instr (S n))) j (@cons (mm_instr (S n)) ρ (@nil (mm_instr (S n))))) (@pair nat (list (mm_instr (S n))) (S O) Q), or (@ex (mm_instr n) (fun ρ' : mm_instr n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) ρ' (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) (S O) P)) (@eq (mm_instr (S n)) ρ (f (Init.Nat.add (S O) (@length (mm_instr n) P)) j ρ')))) (or (and (@eq nat j (Init.Nat.add (S O) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) O))) (or (and (@eq nat j (Init.Nat.add (S (S O)) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S (S (S O))) (@length (mm_instr n) P))))) (and (@eq nat j (Init.Nat.add (S (S (S O))) (@length (mm_instr n) P))) (@eq (mm_instr (S n)) ρ (@mm_dec (S n) (@pos_fst n) (Init.Nat.add (S (S O)) (@length (mm_instr n) P))))))) *)
    rewrite Q_length; intros H.
(* Goal: lt j (Init.Nat.add (S O) (Init.Nat.add (@length (mm_instr n) P) (S (S (S O))))) *)
    apply Q_sc in H.
(* Goal: lt j (Init.Nat.add (S O) (Init.Nat.add (@length (mm_instr n) P) (S (S (S O))))) *)
    destruct H as [ (rho & H1 & H2) | H ].
(* Goal: @in_code (mm_instr n) (Init.Nat.add (S O) i) (@pair nat (list (mm_instr n)) (S O) P) *)
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
    { destruct rho as [ | y p ]; try discriminate.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
      unfold f in H2.
(* Goal: lt j (Init.Nat.add (S O) (Init.Nat.add (@length (mm_instr n) P) (S (S (S O))))) *)
      destruct (eq_nat_dec i p).
(* Goal: @in_code (mm_instr n) (Init.Nat.add (S O) i) (@pair nat (list (mm_instr n)) (S O) P) *)
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
      { inversion H2; omega. }
      destruct (le_lt_dec (1+lP) p); inversion H2; omega. }
(* Goal: lt j (Init.Nat.add (S O) (Init.Nat.add (@length (mm_instr n) P) (S (S (S O))))) *)
    destruct H as [ (H1 & H2) | H ].
(* Goal: @in_code (mm_instr n) (Init.Nat.add (S O) i) (@pair nat (list (mm_instr n)) (S O) P) *)
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
    { inversion H2; omega. }
(* Goal: lt j (Init.Nat.add (S O) (Init.Nat.add (@length (mm_instr n) P) (S (S (S O))))) *)
    destruct H as [ (H1 & H2) | H ].
(* Goal: @in_code (mm_instr n) (Init.Nat.add (S O) i) (@pair nat (list (mm_instr n)) (S O) P) *)
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
    { inversion H2; omega. }
(* Goal: lt j (Init.Nat.add (S O) (Init.Nat.add (@length (mm_instr n) P) (S (S (S O))))) *)
    destruct H as (H1 & H2).
(* Goal: @in_code (mm_instr n) (Init.Nat.add (S O) i) (@pair nat (list (mm_instr n)) (S O) P) *)
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
    { inversion H2; omega. }
  Qed.

  Let P_imp_Q s s0 : in_code (fst s) (1,P) -> (1,P) // s ~~> s0 -> (1,Q) // (fst s, 0##snd s) ↓.
  Proof.
(* Goal: forall (_ : @in_code (mm_instr n) (@fst nat (vec nat n) s) (@pair nat (list (mm_instr n)) (S O) P)) (_ : @sss_output (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) s s0), @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) (@fst nat (vec nat n) s) (@vec_cons nat n O (@snd nat (vec nat n) s))) *)
    intros H1 H; revert H1.
(* Goal: forall _ : @in_code (mm_instr n) (@fst nat (vec nat n) s) (@pair nat (list (mm_instr n)) (S O) P), @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) (@fst nat (vec nat n) s) (@vec_cons nat n O (@snd nat (vec nat n) s))) *)
    pattern s; revert s H; apply mm_term_ind.
    + simpl; intros; omega.
    + intros i [ x | x p ] v j w H1 H2 H3 H5 H4; unfold fst, snd in *. 
      * apply mm_sss_INC_inv in H2.
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
        destruct H2 as (G1 & G2).
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
        destruct (eq_nat_dec i lP) as [ Hi | Hi ].
        - exists (0,0##w); split; try (simpl; omega).
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
          apply sc_Q_1 in H1; simpl f in H1.
(* Goal: @sss_compute (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) (@pair nat (vec nat (S n)) O (@vec_cons nat n O w)) *)
          mm sss INC with (pos_nxt x).
(* Goal: @sss_compute (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) (Init.Nat.add (S O) i) (@vec_change nat (S n) (@vec_cons nat n O v) (@pos_nxt n x) (S (@vec_pos nat (S n) (@vec_cons nat n O v) (@pos_nxt n x))))) (@pair nat (vec nat (S n)) O (@vec_cons nat n O w)) *)
          subst i; clear H1; mm sss DEC 0 with pos0 0.
(* Goal: @sss_compute (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) O (@vec_change nat (S n) (@vec_cons nat n O v) (@pos_nxt n x) (S (@vec_pos nat (S n) (@vec_cons nat n O v) (@pos_nxt n x))))) (@pair nat (vec nat (S n)) O (@vec_cons nat n O w)) *)
          mm sss stop; f_equal; simpl; subst; auto. 
        - spec in H5. { subst j; simpl in H4 |- *; omega. }
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
          apply sc_Q_1 in H1; simpl f in H1.
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
          apply subcode_sss_terminates_instr with (2 := H1) (3 := H5).
(* Goal: @mm_sss (S n) (@mm_inc (S n) (@pos_nxt n x)) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) (@pair nat (vec nat (S n)) j (@vec_cons nat n O w)) *)
          subst; constructor.
      * generalize H1; intros H6.
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
        apply sc_Q_1 in H6; unfold f in H6.
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
        case_eq (v#>x).
        ++ intros Hx.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
           destruct (eq_nat_dec i p) as [ Hip | Hip ].
           -- subst p.
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
              destruct mm_self_loop_no_term_1 with (s := (i,v)) (v := v) (1 := H1); auto.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
              exists s0.
(* Goal: @sss_output (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) s0 *)
              destruct H3 as [ H3 H7 ]; split; auto.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) s0 *)
              apply subcode_sss_compute_instr with (1 := H2) (3 := H3); auto.
           -- destruct (le_lt_dec (1+lP) p) as [ Hp1 | Hp1 ];
                [ | destruct (eq_nat_dec p 0) as [ Hp2 | Hp2 ] ].
              ** exists (0,0##v); split; try (simpl; omega).
(* Goal: @sss_compute (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) (@pair nat (vec nat (S n)) O (@vec_cons nat n O v)) *)
                 mm sss DEC 0 with (pos_nxt x) 0.
(* Goal: @sss_compute (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) O (@vec_cons nat n O v)) (@pair nat (vec nat (S n)) O (@vec_cons nat n O v)) *)
                 mm sss stop.
              ** subst p; exists (0,0##v); split; try (simpl; omega).
(* Goal: @sss_compute (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) (@pair nat (vec nat (S n)) O (@vec_cons nat n O v)) *)
                 mm sss DEC 0 with (pos_nxt x) 0.
(* Goal: @sss_compute (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) O (@vec_cons nat n O v)) (@pair nat (vec nat (S n)) O (@vec_cons nat n O v)) *)
                 mm sss stop.
              ** apply mm_sss_DEC0_inv with (1 := Hx) in H2.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
                 destruct H2; subst j w.
(* Goal: @in_code (mm_instr n) p (@pair nat (list (mm_instr n)) (S O) P) *)
                 spec in H5. { simpl; omega. }
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
                 apply subcode_sss_terminates_instr with (2 := H6) (3 := H5).
(* Goal: @mm_sss (S n) (@mm_dec (S n) (@pos_nxt n x) p) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) (@pair nat (vec nat (S n)) p (@vec_cons nat n O v)) *)
                 constructor; simpl; auto.
        ++ intros u Hx.
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
           apply mm_sss_DEC1_inv with (1 := Hx) in H2.
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
           destruct H2 as [ ? H2 ]; subst j.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
           destruct (eq_nat_dec i lP) as [ Hi | Hi ].
           -- exists (0,0##w); split; simpl; auto.
              apply subcode_sss_compute_instr with (2 := H6) (st2 := (1+i,0##w)); auto.
              ** replace (0##w) with ((0##v)[u/pos_nxt x]); subst; auto; constructor; auto.
              ** subst i; mm sss DEC 0 with pos0 0; mm sss stop.
           -- spec in H5. { simpl in H4 |- *; omega. }
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
              apply subcode_sss_terminates_instr with (2 := H6) (3 := H5); auto.
(* Goal: @mm_sss (S n) (@mm_dec (S n) (@pos_nxt n x) (if Nat.eq_dec i p then Init.Nat.add (S O) (Init.Nat.add (S O) (@length (mm_instr n) P)) else if le_lt_dec (Init.Nat.add (S O) (@length (mm_instr n) P)) p then O else p)) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) (@pair nat (vec nat (S n)) (Init.Nat.add (S O) i) (@vec_cons nat n O w)) *)
              replace (0##w) with ((0##v)[u/pos_nxt x]); subst; auto; constructor; auto.
  Qed.

  Let Q_imp_P s s0 : in_code (fst s) (1,P) -> (snd s)#>pos0 = 0 -> (1,Q) // s ~~> s0 -> (1,P) // (fst s, vec_tail (snd s)) ↓.
  Proof.
(* Goal: forall (_ : @in_code (mm_instr n) (@fst nat (vec nat (S n)) s) (@pair nat (list (mm_instr n)) (S O) P)) (_ : @eq nat (@vec_pos nat (S n) (@snd nat (vec nat (S n)) s) (@pos_fst n)) O) (_ : @sss_output (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) s s0), @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) (@fst nat (vec nat (S n)) s) (@vec_tail nat n (@snd nat (vec nat (S n)) s))) *)
    intros H1 H2 H3; revert H1 H2.
(* Goal: forall (_ : @in_code (mm_instr n) (@fst nat (vec nat (S n)) s) (@pair nat (list (mm_instr n)) (S O) P)) (_ : @eq nat (@vec_pos nat (S n) (@snd nat (vec nat (S n)) s) (@pos_fst n)) O), @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) (@fst nat (vec nat (S n)) s) (@vec_tail nat n (@snd nat (vec nat (S n)) s))) *)
    pattern s; revert s H3; apply mm_term_ind.
    + simpl; intros; omega.
    + intros i ρ v j w H1 H2 H3 H4 H5 H6; unfold fst, snd in *.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i (@vec_tail nat n v)) *)
      rewrite (vec_head_tail v) in H2, H6.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i (@vec_tail nat n v)) *)
      revert H2 H6.
(* Goal: forall (_ : @mm_sss (S n) ρ (@pair nat (vec nat (S n)) i (@vec_cons nat n (@vec_head nat n v) (@vec_tail nat n v))) (@pair nat (vec nat (S n)) j w)) (_ : @eq nat (@vec_pos nat (S n) (@vec_cons nat n (@vec_head nat n v) (@vec_tail nat n v)) (@pos_fst n)) O), @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i (@vec_tail nat n v)) *)
      generalize (vec_head v) (vec_tail v); clear v; intros x v; simpl; intros H2 H6; subst x.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
      destruct Q_sc with (1 := H1) as [ ([ x | x p ] & G1 & G2) | G1 ]; try subst ρ.
      * unfold f in H2.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
        apply mm_sss_INC_inv in H2.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
        destruct H2 as (? & H2); subst j w.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
        revert H4; rew vec; simpl; intros H4.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
        destruct (eq_nat_dec i lP) as [ Hi | Hi ].
        - exists (S i, v[(S (v#>x))/x]); split; try (simpl; omega).
(* Goal: @sss_compute (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) O (@vec_cons nat n O v)) (@pair nat (vec nat (S n)) O (@vec_cons nat n O v)) *)
          mm sss INC with x; mm sss stop.
        - spec in H4. simpl in H5; omega. spec in H4; auto.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
          apply subcode_sss_terminates_instr with (2 := G1) (3 := H4); auto; constructor.
      * unfold f in H2; case_eq (v#>x).
        - intros Hx.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
          apply mm_sss_DEC0_inv in H2; auto.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
          destruct H2; subst j w.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
          destruct (eq_nat_dec i p) as [ Hip | Hip ].
          ** subst p; exfalso.
(* Goal: False *)
             generalize (ex_intro _ s0 H3); simpl.
             change (~ (1,Q) // (2+lP,0##v) ↓).
(* Goal: not (@sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) (Init.Nat.add (S (S O)) (@length (mm_instr n) P)) (@vec_cons nat n O v))) *)
             apply mm_self_loop_no_term_2 with (v := 0##v) (1 := sc_Q_3); auto.
          ** destruct (le_lt_dec (1+lP) p) as [ Hp | Hp ];
               [ | destruct (eq_nat_dec p 0) as [ Hp2 | Hp2 ] ].
             ++ exists (p,v); split; try (simpl; omega).
(* Goal: @sss_compute (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) O (@vec_cons nat n O v)) (@pair nat (vec nat (S n)) O (@vec_cons nat n O v)) *)
                mm sss DEC 0 with x p; mm sss stop.
             ++ exists (p,v); split; try (simpl; omega).
(* Goal: @sss_compute (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) O (@vec_cons nat n O v)) (@pair nat (vec nat (S n)) O (@vec_cons nat n O v)) *)
                mm sss DEC 0 with x p; mm sss stop.
             ++ spec in H4. simpl in H5 |- *; omega.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
                spec in H4; auto.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
                apply subcode_sss_terminates_instr with (2 := G1) (3 := H4); auto; constructor.
(* Goal: @eq nat (@vec_pos nat n (@vec_tail nat n (@vec_cons nat n O v)) x) O *)
                simpl; auto.
        - intros u Hx.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
          apply mm_sss_DEC1_inv with (u := u) in H2; auto.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
          destruct H2; subst j w.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
          simpl in H4.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
          destruct (eq_nat_dec i lP) as [ Hi | Hi ].
          ** exists (S i, v[u/x]); split; try (simpl; omega).
(* Goal: @sss_compute (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) O (@vec_cons nat n O v)) (@pair nat (vec nat (S n)) O (@vec_cons nat n O v)) *)
             mm sss DEC S with x p u; mm sss stop.
          ** spec in H4. simpl in H5; omega.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
             spec in H4; auto.
(* Goal: @sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) i v) *)
             apply subcode_sss_terminates_instr with (2 := G1) (3 := H4); auto.
(* Goal: @mm_sss n (@mm_dec n x p) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (S i) (@vec_change nat n v x u)) *)
             constructor; auto.
      * destruct G1 as [ (? & _) | [ (? & _) | (? & _) ] ]; simpl in H5; omega.
  Qed.

(* Goal: @in_code (mm_instr n) (Init.Nat.add (S O) i) (@pair nat (list (mm_instr n)) (S O) P) *)
(* Goal: @sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) i (@vec_cons nat n O v)) *)
  Theorem mm_remove_self_loops : { Q |  mm_no_self_loops (1,Q)
                                     /\ (forall i x j, (i,DEC x j::nil) <sc (1,Q) -> j < 1+length Q)
                                     /\ forall v, (1,P) // (1,v) ↓ <-> (1,Q) // (1,0##v) ↓ }.
  Proof.
(* Goal: @sig (list (mm_instr (S n))) (fun Q : list (mm_instr (S n)) => and (@mm_no_self_loops (S n) (@pair nat (list (mm_instr (S n))) (S O) Q)) (and (forall (i : nat) (x : pos (S n)) (j : nat) (_ : @subcode (mm_instr (S n)) (@pair nat (list (mm_instr (S n))) i (@cons (mm_instr (S n)) (@mm_dec (S n) x j) (@nil (mm_instr (S n))))) (@pair nat (list (mm_instr (S n))) (S O) Q)), lt j (Init.Nat.add (S O) (@length (mm_instr (S n)) Q))) (forall v : vec nat n, iff (@sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) (S O) v)) (@sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) Q) (@pair nat (vec nat (S n)) (S O) (@vec_cons nat n O v)))))) *)
    destruct (eq_nat_dec lP 0) as [ HlP | HlP ].
    +  exists nil.
(* Goal: and (@mm_no_self_loops (S n) (@pair nat (list (mm_instr (S n))) (S O) (@nil (mm_instr (S n))))) (and (forall (i : nat) (x : pos (S n)) (j : nat) (_ : @subcode (mm_instr (S n)) (@pair nat (list (mm_instr (S n))) i (@cons (mm_instr (S n)) (@mm_dec (S n) x j) (@nil (mm_instr (S n))))) (@pair nat (list (mm_instr (S n))) (S O) (@nil (mm_instr (S n))))), lt j (Init.Nat.add (S O) (@length (mm_instr (S n)) (@nil (mm_instr (S n)))))) (forall v : vec nat n, iff (@sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) (S O) v)) (@sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) (@nil (mm_instr (S n)))) (@pair nat (vec nat (S n)) (S O) (@vec_cons nat n O v))))) *)
       split; [ | split ].
       - intros i rho ([ | ] & ? & ? & ?); discriminate.
       - intros i x j ([ | ] & ? & ? & ?); discriminate.
       - destruct P; try discriminate.
(* Goal: forall v : vec nat n, iff (@sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) (@nil (mm_instr n))) (@pair nat (vec nat n) (S O) v)) (@sss_terminates (mm_instr (S n)) (vec nat (S n)) (@mm_sss (S n)) (@pair nat (list (mm_instr (S n))) (S O) (@nil (mm_instr (S n)))) (@pair nat (vec nat (S n)) (S O) (@vec_cons nat n O v))) *)
         split.
         * exists (1,0##v); split; simpl; try omega; mm sss stop.
         * exists (1,v); split; simpl; try omega; mm sss stop.
    + exists Q; split; auto; split; auto; intros v; split.
(* Goal: @in_code (mm_instr n) p (@pair nat (list (mm_instr n)) (S O) P) *)
      * intros (s0 & H); revert H; apply P_imp_Q; simpl; omega.
(* Goal: @in_code (mm_instr n) p (@pair nat (list (mm_instr n)) (S O) P) *)
      * intros (s0 & H); revert H; apply Q_imp_P; simpl; omega.
  Qed.

End remove_self_loops.

  
