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

Require Import List Arith Omega.

Require Import utils pos vec.
Require Import subcode sss.
Require Import list_bool 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 "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).

(** ** Simulating Binary Stacks with numbers *)

Section Minsky_Machine_utils.

  Variable (n : nat).
  
  Ltac dest x y := destruct (pos_eq_dec x y) as [ | ]; [ subst x | ]; rew vec.

  Section mm_null.

    Variable (src zero : pos n) (Hsz : src <> zero).

    Definition mm_null i := DEC src (2+i) :: DEC zero i :: nil.

    Fact mm_null_length i : length (mm_null i) = 2.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
    Proof. auto. Qed.
    
    Let mm_null_spec i k v w : v#>src = k 
                               -> v#>zero = 0 
                               -> w = v[0/src]
                               -> (i,mm_null i) // (i,v) -+> (2+i,w).
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v src) k) (_ : @eq nat (@vec_pos nat n v zero) O) (_ : @eq (vec nat n) w (@vec_change nat n v src O)), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (mm_null i)) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S O)) i) w) *)
      unfold mm_null.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v src) (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) (_ : @eq nat (@vec_pos nat n v rem) O) (_ : @eq (vec nat n) w (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo (Init.Nat.add k (@vec_pos nat n v quo))) rem (S O))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      revert v w.
(* Goal: forall (v w : vec nat n) (_ : @eq nat (@vec_pos nat n v src) k) (_ : @eq nat (@vec_pos nat n v zero) O) (_ : @eq (vec nat n) w (@vec_change nat n v src O)), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S O)) i)) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S O)) i) w) *)
      induction k as [ | k IHk ]; intros v w H1 H2 H3; subst w.
      
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S O)) i)) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S O)) i) (@vec_change nat n v src O)) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S O)) i)) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S O)) i) (@vec_change nat n v src O)) *)
      mm sss DEC 0 with src (2+i).
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) k (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O)) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      mm sss stop; f_equal.
(* Goal: @eq (vec nat n) v (@vec_change nat n v src O) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S O)) i)) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S O)) i) (@vec_change nat n v src O)) *)
      apply vec_pos_ext; intros z; dest z src.

(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S O)) i)) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S O)) i) (@vec_change nat n v src O)) *)
      mm sss DEC S with src (2+i) k.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) i))) (@vec_change nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (@vec_pos nat n (@vec_change nat n v src k) dst))) dst' (S (@vec_pos nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (@vec_pos nat n (@vec_change nat n v src k) dst))) dst')))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      mm sss DEC 0 with zero i; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i (@vec_change nat n (@vec_change nat n v src k) dst (S (S (@vec_pos nat n v dst))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      apply sss_progress_compute.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S O)) i)) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))) (@pair nat (vec nat n) i (@vec_change nat n v src k)) (@pair nat (vec nat n) (Init.Nat.add (S (S O)) i) (@vec_change nat n v src O)) *)
      apply IHk; rew vec.
    Qed.

    Fact mm_null_progress i v st : 
             v#>zero = 0 
          -> st = (2+i,v[0/src])
          -> (i,mm_null i) // (i,v) -+> st.
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v zero) O) (_ : @eq (prod nat (vec nat n)) st (@pair nat (vec nat n) (Init.Nat.add (S (S O)) i) (@vec_change nat n v src O))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (mm_null i)) (@pair nat (vec nat n) i v) st *)
      intros; subst.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply mm_null_spec with (1 := eq_refl); auto.
    Qed.

  End mm_null.

  Hint Rewrite mm_null_length : length_db.

  Section mm_nullify.

    (* Make every register in the list lr become 0 *)
 
    Variable (zero : pos n).

    Fixpoint mm_nullify i lr := 
      match lr with
        | nil   => nil 
        | x::lr => mm_null x zero i ++ mm_nullify (2+i) lr
      end.

    Fact mm_nullify_length i lr : length (mm_nullify i lr) = 2*length lr.
    Proof.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      revert i; induction lr as [ | x lr IH ]; simpl; intros i; auto.
(* Goal: @eq nat (S (S (@length (mm_instr n) (mm_nullify (S (S i)) lr)))) (S (Init.Nat.add (@length (pos n) lr) (S (Init.Nat.add (@length (pos n) lr) O)))) *)
      rewrite IH; omega.
    Qed.

    Fact mm_nullify_compute i lr v w :
            v#>zero = 0
         -> (forall p, In p lr -> p <> zero)
         -> (forall p, In p lr -> w#>p = 0)
         -> (forall p, ~ In p lr -> w#>p = v#>p)
         -> (i,mm_nullify i lr) // (i,v) ->> (length (mm_nullify i lr)+i,w).
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v zero) O) (_ : forall (p : pos n) (_ : @In (pos n) p lr), not (@eq (pos n) p zero)) (_ : forall (p : pos n) (_ : @In (pos n) p lr), @eq nat (@vec_pos nat n w p) O) (_ : forall (p : pos n) (_ : not (@In (pos n) p lr)), @eq nat (@vec_pos nat n w p) (@vec_pos nat n v p)), @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (mm_nullify i lr)) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (@length (mm_instr n) (mm_nullify i lr)) i) w) *)
      rewrite mm_nullify_length.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v zero) O) (_ : forall (p : pos n) (_ : @In (pos n) p lr), not (@eq (pos n) p zero)) (_ : forall (p : pos n) (_ : @In (pos n) p lr), @eq nat (@vec_pos nat n w p) O) (_ : forall (p : pos n) (_ : not (@In (pos n) p lr)), @eq nat (@vec_pos nat n w p) (@vec_pos nat n v p)), @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (mm_nullify i lr)) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (Init.Nat.mul (S (S O)) (@length (pos n) lr)) i) w) *)
      revert i v w; induction lr as [ | x lr IH ]; intros i v w H1 H2 H3 H4.

(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) k (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O)) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      mm sss stop; f_equal.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply vec_pos_ext; intros; rewrite H4; auto.
      
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (mm_nullify i (@cons (pos n) x lr))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (Init.Nat.mul (S (S O)) (@length (pos n) (@cons (pos n) x lr))) i) w) *)
      rew length.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (mm_nullify i (@cons (pos n) x lr))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (Init.Nat.mul (S (S O)) (S (@length (pos n) lr))) i) w) *)
      unfold mm_nullify; fold mm_nullify.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_null x zero i) (mm_nullify (Init.Nat.add (S (S O)) i) lr))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (Init.Nat.mul (S (S O)) (S (@length (pos n) lr))) i) w) *)
      apply sss_compute_trans with (2+i,v[0/x]).
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply subcode_sss_compute with (P := (i,mm_null x zero i)); auto.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply sss_progress_compute, mm_null_progress; auto.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply H2; left; auto.
  
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_null x zero i) (mm_nullify (Init.Nat.add (S (S O)) i) lr))) (@pair nat (vec nat n) (Init.Nat.add (S (S O)) i) (@vec_change nat n v x O)) (@pair nat (vec nat n) (Init.Nat.add (Init.Nat.mul (S (S O)) (S (@length (pos n) lr))) i) w) *)
      apply subcode_sss_compute with (P := (2+i,mm_nullify (2+i) lr)).
(* Goal: @subcode (mm_instr n) (@pair nat (list (mm_instr n)) (Init.Nat.add (S (S O)) i) (mm_nullify (Init.Nat.add (S (S O)) i) lr)) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_null x zero i) (mm_nullify (Init.Nat.add (S (S O)) i) lr))) *)
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (Init.Nat.add (S (S O)) i) (mm_nullify (Init.Nat.add (S (S O)) i) lr)) (@pair nat (vec nat n) (Init.Nat.add (S (S O)) i) (@vec_change nat n v x O)) (@pair nat (vec nat n) (Init.Nat.add (Init.Nat.mul (S (S O)) (S (@length (pos n) lr))) i) w) *)
      subcode_tac; solve list eq.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (Init.Nat.add (S (S O)) i) (mm_nullify (Init.Nat.add (S (S O)) i) lr)) (@pair nat (vec nat n) (Init.Nat.add (S (S O)) i) (@vec_change nat n v x O)) (@pair nat (vec nat n) (Init.Nat.add (Init.Nat.mul (S (S O)) (S (@length (pos n) lr))) i) w) *)
      replace (2*S (length lr)+i) with (2*(length lr)+(2+i)) by omega.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (Init.Nat.add (S (S O)) i) (mm_nullify (Init.Nat.add (S (S O)) i) lr)) (@pair nat (vec nat n) (Init.Nat.add (S (S O)) i) (@vec_change nat n v x O)) (@pair nat (vec nat n) (Init.Nat.add (Init.Nat.mul (S (S O)) (@length (pos n) lr)) (Init.Nat.add (S (S O)) i)) w) *)
      apply IH.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n v x O) zero) O *)
(* Goal: forall (p : pos n) (_ : @In (pos n) p lr), not (@eq (pos n) p zero) *)
(* Goal: forall (p : pos n) (_ : @In (pos n) p lr), @eq nat (@vec_pos nat n w p) O *)
(* Goal: forall (p : pos n) (_ : not (@In (pos n) p lr)), @eq nat (@vec_pos nat n w p) (@vec_pos nat n (@vec_change nat n v x O) p) *)
      specialize (H2 x (or_introl eq_refl)); rew vec.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      intros; apply H2; right; auto.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      intros; apply H3; right; auto.
(* Goal: forall (p : pos n) (_ : not (@In (pos n) p lr)), @eq nat (@vec_pos nat n w p) (@vec_pos nat n (@vec_change nat n v x O) p) *)
      intros p Hp.
(* Goal: @eq nat (@vec_pos nat n w p) (@vec_pos nat n (@vec_change nat n v x O) p) *)
      dest p x.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply H3; left; auto.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply H4; intros [|]; auto.
    Qed.

  End mm_nullify.

  Section transfert.

    Variables (src dst zero : pos n).

    Hypothesis (Hsd : src <> dst) (Hsz : src <> zero) (Hdz : dst <> zero).

    Definition mm_transfert i := DEC src (3+i) :: INC dst :: DEC zero i :: nil.

    Fact mm_transfert_length i : length (mm_transfert i) = 3.
    Proof. reflexivity. Qed.

    Let mm_transfert_spec i v w k x :  v#>src = k
                                    -> v#>dst = x
                                    -> v#>zero = 0
                                    -> w = v[0/src][(k+x)/dst]
                                    -> (i,mm_transfert i) // (i,v) -+> (3+i,w).
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v src) k) (_ : @eq nat (@vec_pos nat n v dst) x) (_ : @eq nat (@vec_pos nat n v zero) O) (_ : @eq (vec nat n) w (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.add k x))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (mm_transfert i)) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S O))) i) w) *)
      unfold mm_transfert.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v src) k) (_ : @eq nat (@vec_pos nat n v dst) x) (_ : @eq nat (@vec_pos nat n v zero) O) (_ : @eq (vec nat n) w (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.add k x))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n)))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S O))) i) w) *)
      revert v w x.
(* Goal: forall (v w : vec nat n) (x : nat) (_ : @eq nat (@vec_pos nat n v src) k) (_ : @eq nat (@vec_pos nat n v dst) x) (_ : @eq nat (@vec_pos nat n v zero) O) (_ : @eq (vec nat n) w (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.add k x))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n)))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S O))) i) w) *)
      induction k as [ | k IHk ]; intros v w x H1 H2 H3 H4; subst w.

(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n)))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S O))) i) (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.add O x))) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n)))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S O))) i) (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.add (S k) x))) *)
      mm sss DEC 0 with src (3+i).
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      mm sss stop; f_equal; auto.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n v p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.add (Init.Nat.mul (S (S O)) O) (@vec_pos nat n v dst))) p) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      dest p dst; dest p src.

(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n)))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S O))) i) (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.add (S k) x))) *)
      mm sss DEC S with src (3+i) k.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v src k)) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      mm sss INC with dst.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) i))) (@vec_change nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (@vec_pos nat n (@vec_change nat n v src k) dst))) dst' (S (@vec_pos nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (@vec_pos nat n (@vec_change nat n v src k) dst))) dst')))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      mm sss DEC 0 with zero i; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n)))))) (@pair nat (vec nat n) i (@vec_change nat n (@vec_change nat n v src k) dst (S (@vec_pos nat n v dst)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S O))) i) (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.add (S k) x))) *)
      replace (S k + x) with (k + S x) by omega.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i (@vec_change nat n (@vec_change nat n v src k) dst (S (S (@vec_pos nat n v dst))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      apply sss_progress_compute.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n)))))) (@pair nat (vec nat n) i (@vec_change nat n (@vec_change nat n v src k) dst (S (@vec_pos nat n v dst)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S O))) i) (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.add k (S x)))) *)
      apply IHk with (S x); rew vec.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n v p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.add (Init.Nat.mul (S (S O)) O) (@vec_pos nat n v dst))) p) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      dest p dst; dest p src.
    Qed.

    Fact mm_transfert_progress i v st : 
           v#>dst = 0 
        -> v#>zero = 0
        -> st = (3+i,v[0/src][(v#>src)/dst])
        -> (i,mm_transfert i) // (i,v) -+> st.
    Proof.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      intros H1 H2 ?; subst; apply mm_transfert_spec with (1 := eq_refl) (2 := eq_refl); auto.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n v src O) dst (@vec_pos nat n v src)) (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.add (@vec_pos nat n v src) (@vec_pos nat n v dst))) *)
      rewrite H1; apply vec_pos_ext; intros p; dest p dst.
    Qed.

  End transfert.

  Hint Rewrite mm_transfert_length : length_db.

  Section div2.
  
    Variables (src quo rem : pos n)
              (Hsq : src <> quo) (Hsr : src <> rem) (Hqr : quo <> rem)
              (i : nat).

    Definition mm_div2 :=
      DEC src (6+i) ::
      INC rem ::
      DEC src (i+6) ::
      DEC rem (4+i) ::
      INC quo ::
      DEC rem i ::
      nil.

    Fact mm_div2_length : length mm_div2 = 6.
    Proof. reflexivity. Qed.

    Let mm_div2_spec_0 k v w : 
         v#>src = 2*k -> v#>rem = 0 -> w = v[0/src][(k+(v#>quo))/quo] -> (i,mm_div2) // (i,v) -+> (6+i,w).
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v src) (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) (_ : @eq nat (@vec_pos nat n v rem) O) (_ : @eq (vec nat n) w (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo (Init.Nat.add k (@vec_pos nat n v quo))) rem (S O))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_div2) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      unfold mm_div2.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v src) (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) (_ : @eq nat (@vec_pos nat n v rem) O) (_ : @eq (vec nat n) w (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo (Init.Nat.add k (@vec_pos nat n v quo))) rem (S O))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      revert v w.
(* Goal: forall (v w : vec nat n) (_ : @eq nat (@vec_pos nat n v src) (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) (_ : @eq nat (@vec_pos nat n v rem) O) (_ : @eq (vec nat n) w (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo (Init.Nat.add k (@vec_pos nat n v quo))) rem (S O))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      induction k as [ | k IHk ]; intros v w H1 H4 H3.

(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      simpl in H1.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss DEC 0 with src (6+i).
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      mm sss stop; f_equal; subst.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n v p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n v src O) quo (Init.Nat.add O (@vec_pos nat n v quo))) p) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      dest p quo; dest p src.

(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      replace (2*S k) with (S (S (2*k))) in H1 by omega.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss DEC S with src (6+i) (S (2*k)).
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss INC with rem.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) i)) (@vec_change nat n (@vec_change nat n v src (S (Init.Nat.mul (S (S O)) k))) rem (S (@vec_pos nat n (@vec_change nat n v src (S (Init.Nat.mul (S (S O)) k))) rem)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss DEC S with src (i+6) (2*k); rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) i))) (@vec_change nat n (@vec_change nat n (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) rem (S (@vec_pos nat n v rem))) src (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss DEC S with rem (4+i) (v#>rem); rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) i)))) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) rem (S (@vec_pos nat n v rem))) src (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) rem (@vec_pos nat n v rem))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss INC with quo; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) i))))) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) rem (S (@vec_pos nat n v rem))) src (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) rem (@vec_pos nat n v rem)) quo (S (@vec_pos nat n v quo)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss DEC 0 with rem i; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i (@vec_change nat n (@vec_change nat n v src k) dst (S (S (@vec_pos nat n v dst))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      apply sss_progress_compute.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) rem (S (@vec_pos nat n v rem))) src (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) rem (@vec_pos nat n v rem)) quo (S (@vec_pos nat n v quo)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      apply IHk; auto; rew vec.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      subst; apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo (Init.Nat.add (S k) (@vec_pos nat n v quo))) rem (S O)) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) rem (S (@vec_pos nat n v rem))) src (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) rem (@vec_pos nat n v rem)) quo (S (@vec_pos nat n v quo))) src O) quo (Init.Nat.add k (S (@vec_pos nat n v quo)))) rem (S O)) p) *)
      dest p quo; try omega.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo (Init.Nat.add (S k) (@vec_pos nat n v quo))) rem (S O)) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) rem (S (@vec_pos nat n v rem))) src (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) rem (@vec_pos nat n v rem)) quo (S (@vec_pos nat n v quo))) src O) quo (Init.Nat.add k (S (@vec_pos nat n v quo)))) rem (S O)) p) *)
      dest p src; dest p rem.
    Qed.
    
    Let mm_div2_spec_1 k v w : 
         v#>src = 1+2*k -> v#>rem = 0 -> w = v[0/src][(k+(v#>quo))/quo][1/rem] -> (i,mm_div2) // (i,v) -+> (6+i,w).
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v src) (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) (_ : @eq nat (@vec_pos nat n v rem) O) (_ : @eq (vec nat n) w (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo (Init.Nat.add k (@vec_pos nat n v quo))) rem (S O))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_div2) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      unfold mm_div2.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v src) (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) (_ : @eq nat (@vec_pos nat n v rem) O) (_ : @eq (vec nat n) w (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo (Init.Nat.add k (@vec_pos nat n v quo))) rem (S O))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      revert v w.
(* Goal: forall (v w : vec nat n) (_ : @eq nat (@vec_pos nat n v src) (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) (_ : @eq nat (@vec_pos nat n v rem) O) (_ : @eq (vec nat n) w (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo (Init.Nat.add k (@vec_pos nat n v quo))) rem (S O))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      induction k as [ | k IHk ]; intros v w H1 H4 H3.

(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      simpl in H1.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss DEC S with src (6+i) 0.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss INC with rem.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) i)) (@vec_change nat n (@vec_change nat n v src O) rem (S (@vec_pos nat n (@vec_change nat n v src O) rem)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss DEC 0 with src (i+6); rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) (Init.Nat.add i (S (S (S (S (S (S O))))))) (@vec_change nat n (@vec_change nat n v src O) rem (S (@vec_pos nat n v rem)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss stop; f_equal; try omega.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n v src O) rem (S (@vec_pos nat n v rem))) w *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      subst; simpl.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n v p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n v src O) quo (Init.Nat.add O (@vec_pos nat n v quo))) p) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      dest p rem; dest p quo; dest p src.

(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      replace (1 + 2*S k) with (S (S (1+2*k))) in H1 by omega.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss DEC S with src (6+i) (S (1+2*k)).
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss INC with rem.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) i)) (@vec_change nat n (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) rem (S (@vec_pos nat n (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) rem)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss DEC S with src (i+6) (1+2*k); rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) i))) (@vec_change nat n (@vec_change nat n (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) rem (S (@vec_pos nat n v rem))) src (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss DEC S with rem (4+i) (v#>rem); rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) i)))) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) rem (S (@vec_pos nat n v rem))) src (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) rem (@vec_pos nat n v rem))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss INC with quo; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) i))))) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) rem (S (@vec_pos nat n v rem))) src (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) rem (@vec_pos nat n v rem)) quo (S (@vec_pos nat n v quo)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      mm sss DEC 0 with rem i; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i (@vec_change nat n (@vec_change nat n v src k) dst (S (S (@vec_pos nat n v dst))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      apply sss_progress_compute.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S O)))))) i)) (@cons (mm_instr n) (@mm_inc n rem) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add i (S (S (S (S (S (S O)))))))) (@cons (mm_instr n) (@mm_dec n rem (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n quo) (@cons (mm_instr n) (@mm_dec n rem i) (@nil (mm_instr n))))))))) (@pair nat (vec nat n) i (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) rem (S (@vec_pos nat n v rem))) src (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) rem (@vec_pos nat n v rem)) quo (S (@vec_pos nat n v quo)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) w) *)
      apply IHk; auto; rew vec.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      subst; apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo (Init.Nat.add (S k) (@vec_pos nat n v quo))) rem (S O)) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) rem (S (@vec_pos nat n v rem))) src (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) rem (@vec_pos nat n v rem)) quo (S (@vec_pos nat n v quo))) src O) quo (Init.Nat.add k (S (@vec_pos nat n v quo)))) rem (S O)) p) *)
      dest p quo; try omega.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo (Init.Nat.add (S k) (@vec_pos nat n v quo))) rem (S O)) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src (S (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k)))) rem (S (@vec_pos nat n v rem))) src (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) k))) rem (@vec_pos nat n v rem)) quo (S (@vec_pos nat n v quo))) src O) quo (Init.Nat.add k (S (@vec_pos nat n v quo)))) rem (S O)) p) *)
      dest p src; dest p rem.
    Qed.

    Fact mm_div2_progress v :
           v#>quo = 0 
        -> v#>rem = 0  
        -> let (k,b) := div2 (v#>src) 
           in  (i,mm_div2) // (i,v) -+> (6+i,v[0/src][k/quo][(if b then 1 else 0)/rem]).
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v quo) O) (_ : @eq nat (@vec_pos nat n v rem) O), let (k, b) := div2 (@vec_pos nat n v src) in @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_div2) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo k) rem (if b then S O else O))) *)
      intros H2 H3.
(* Goal: let (k, b) := div2 (@vec_pos nat n v src) in @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_div2) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo k) rem (if b then S O else O))) *)
      generalize (div2_spec (v#>src)).
(* Goal: forall _ : let (p, b) := div2 (@vec_pos nat n v src) in if b then @eq nat (@vec_pos nat n v src) (Init.Nat.add (Init.Nat.mul (S (S O)) p) (S O)) else @eq nat (@vec_pos nat n v src) (Init.Nat.mul (S (S O)) p), let (k, b) := div2 (@vec_pos nat n v src) in @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_div2) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo k) rem (if b then S O else O))) *)
      destruct (div2 (v#>src)) as (k,[]); intros H4.

(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply mm_div2_spec_1 with k; auto.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul (S (S O)) (S k)) (@vec_pos nat n v dst)) (Init.Nat.add (Init.Nat.mul (S (S O)) k) (S (S (@vec_pos nat n v dst)))) *)
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n v src O) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (S (@vec_pos nat n v dst)))) src O) p) *)
      omega.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      apply vec_pos_ext; intros p.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul (S (S O)) (S k)) (@vec_pos nat n v dst)) (Init.Nat.add (Init.Nat.mul (S (S O)) k) (S (S (@vec_pos nat n v dst)))) *)
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n v src O) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (S (@vec_pos nat n v dst)))) src O) p) *)
      dest p rem; dest p quo; omega.

(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply mm_div2_spec_0 with k; auto.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      apply vec_pos_ext; intros p.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul (S (S O)) (S k)) (@vec_pos nat n v dst)) (Init.Nat.add (Init.Nat.mul (S (S O)) k) (S (S (@vec_pos nat n v dst)))) *)
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n v src O) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (S (@vec_pos nat n v dst)))) src O) p) *)
      dest p rem; dest p quo; omega.
    Qed.

    Corollary mm_div2_progress_1 v k st :
           v#>quo = 0 
        -> v#>rem = 0
        -> div2 (v#>src) = (k,true)  
        -> st = (6+i,v[0/src][k/quo][1/rem])
        -> (i,mm_div2) // (i,v) -+> st.
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v quo) O) (_ : @eq nat (@vec_pos nat n v rem) O) (_ : @eq (prod nat bool) (div2 (@vec_pos nat n v src)) (@pair nat bool k false)) (_ : @eq (prod nat (vec nat n)) st (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo k) rem O))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_div2) (@pair nat (vec nat n) i v) st *)
      intros H2 H3 H4 ?; subst.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_div2) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo k) rem O)) *)
      generalize (mm_div2_progress _ H2 H3).
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      rewrite H4; auto.
    Qed.

    Corollary mm_div2_progress_0 v k st : 
           v#>quo = 0 
        -> v#>rem = 0
        -> div2 (v#>src) = (k,false)  
        -> st = (6+i,v[0/src][k/quo][0/rem])
        -> (i,mm_div2) // (i,v) -+> st.
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v quo) O) (_ : @eq nat (@vec_pos nat n v rem) O) (_ : @eq (prod nat bool) (div2 (@vec_pos nat n v src)) (@pair nat bool k false)) (_ : @eq (prod nat (vec nat n)) st (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo k) rem O))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_div2) (@pair nat (vec nat n) i v) st *)
      intros H2 H3 H4 ?; subst.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_div2) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) quo k) rem O)) *)
      generalize (mm_div2_progress _ H2 H3).
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      rewrite H4; auto.
    Qed.

  End div2.

  Hint Rewrite mm_div2_length : length_db.

  Section mul2.

    Variables (src dst zero : pos n) 
              (Hsd : src <> dst) (Hsz : src <> zero) (Hdz : dst <> zero)
              (i : nat).

    Let dst' := dst.

    Definition mm_mul2 := DEC src (4+i) :: INC dst :: INC dst' :: DEC zero i :: nil.

    Fact mm_mul2_length : length mm_mul2 = 4.
    Proof. reflexivity. Qed.

    Let mm_mul2_spec k v w :
        v#>src = k -> v#>zero = 0 -> w = v[0/src][(2*k+(v#>dst))/dst] -> (i,mm_mul2) // (i,v) -+> (4+i,w).
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v src) k) (_ : @eq nat (@vec_pos nat n v zero) O) (_ : @eq (vec nat n) w (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.add (Init.Nat.mul (S (S O)) k) (@vec_pos nat n v dst)))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_mul2) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      unfold mm_mul2.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v src) k) (_ : @eq nat (@vec_pos nat n v zero) O) (_ : @eq (vec nat n) w (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.add (Init.Nat.mul (S (S O)) k) (@vec_pos nat n v dst)))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      revert v w; induction k as [ | k IHk ]; intros v w H1 H2 H3.

(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      mm sss DEC 0 with src (4+i).
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      mm sss stop; f_equal; subst.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n v p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.add (Init.Nat.mul (S (S O)) O) (@vec_pos nat n v dst))) p) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      dest p dst; dest p src.

(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      mm sss DEC S with src (4+i) k.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v src k)) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      mm sss INC with dst.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) i)) (@vec_change nat n (@vec_change nat n v src k) dst (S (@vec_pos nat n (@vec_change nat n v src k) dst)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      mm sss INC with dst'.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) i))) (@vec_change nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (@vec_pos nat n (@vec_change nat n v src k) dst))) dst' (S (@vec_pos nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (@vec_pos nat n (@vec_change nat n v src k) dst))) dst')))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      mm sss DEC 0 with zero i; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i (@vec_change nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (@vec_pos nat n v dst))) dst' (S (@vec_pos nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (@vec_pos nat n v dst))) dst')))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      unfold dst'; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i (@vec_change nat n (@vec_change nat n v src k) dst (S (S (@vec_pos nat n v dst))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      apply sss_progress_compute.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S O)))) i)) (@cons (mm_instr n) (@mm_inc n dst) (@cons (mm_instr n) (@mm_inc n dst') (@cons (mm_instr n) (@mm_dec n zero i) (@nil (mm_instr n))))))) (@pair nat (vec nat n) i (@vec_change nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (@vec_pos nat n v dst))) dst' (S (@vec_pos nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (@vec_pos nat n v dst))) dst')))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) w) *)
      apply IHk; unfold dst'; rew vec.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      subst; apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.add (Init.Nat.mul (S (S O)) (S k)) (@vec_pos nat n v dst))) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (S (@vec_pos nat n v dst)))) src O) dst (Init.Nat.add (Init.Nat.mul (S (S O)) k) (S (S (@vec_pos nat n v dst))))) p) *)
      dest p dst.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul (S (S O)) (S k)) (@vec_pos nat n v dst)) (Init.Nat.add (Init.Nat.mul (S (S O)) k) (S (S (@vec_pos nat n v dst)))) *)
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n v src O) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (S (@vec_pos nat n v dst)))) src O) p) *)
      omega.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n (@vec_change nat n v src (stack_enc (@cons bool false s))) src (S (@vec_pos nat n (@vec_change nat n v src (stack_enc (@cons bool false s))) src))) p) (@vec_pos nat n (@vec_change nat n v src (stack_enc (@cons bool true s))) p) *)
      dest p src.
    Qed.

    Fact mm_mul2_progress v st : 
         v#>dst = 0 
      -> v#>zero = 0 
      -> st = (4+i,v[0/src][(2*(v#>src))/dst])
      -> (i,mm_mul2) // (i,v) -+> st.
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v dst) O) (_ : @eq nat (@vec_pos nat n v zero) O) (_ : @eq (prod nat (vec nat n)) st (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S O)))) i) (@vec_change nat n (@vec_change nat n v src O) dst (Init.Nat.mul (S (S O)) (@vec_pos nat n v src))))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_mul2) (@pair nat (vec nat n) i v) st *)
      intros H1 H2 ?; subst.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply mm_mul2_spec with (1 := eq_refl); auto.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul (S (S O)) (S k)) (@vec_pos nat n v dst)) (Init.Nat.add (Init.Nat.mul (S (S O)) k) (S (S (@vec_pos nat n v dst)))) *)
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n v src O) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (S (@vec_pos nat n v dst)))) src O) p) *)
      rewrite H1; f_equal; omega.
    Qed.
   
  End mul2.

  Hint Rewrite mm_mul2_length : length_db.

  Fixpoint stack_enc (s : list bool) : nat :=
    match s with 
      | nil     => 1
      | One::s  => 1+2*stack_enc s
      | Zero::s =>   2*stack_enc s
    end.

  Fact stack_enc_S s : { k | stack_enc s = S k }.
  Proof.
(* Goal: @sig nat (fun k : nat => @eq nat (stack_enc s) (S k)) *)
    induction s as [ | [] s (k & Hk) ].
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
    exists 0; auto.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
    exists (2*stack_enc s); auto.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul (S (S O)) (S k)) (@vec_pos nat n v dst)) (Init.Nat.add (Init.Nat.mul (S (S O)) k) (S (S (@vec_pos nat n v dst)))) *)
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n v src O) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (S (@vec_pos nat n v dst)))) src O) p) *)
    exists (S (2*k)); simpl; omega.
  Qed.

  Section push.

    Variables (src tmp zero : pos n) 
              (Hst : src <> tmp) (Hsz : src <> zero) (Htz : tmp <> zero) 
              (i : nat).

    Definition mm_push_Zero :=
      mm_transfert src tmp zero i ++ mm_mul2 tmp src zero (3+i).

    Fact mm_push_Zero_length : length mm_push_Zero = 7.
    Proof. reflexivity. Qed.

    Fact mm_push_Zero_progress s v :
         v#>tmp  = 0
      -> v#>zero = 0
      -> v#>src  = stack_enc s
      -> (i,mm_push_Zero) // (i,v) -+> (7+i,v[(stack_enc (Zero::s))/src]).
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v tmp) O) (_ : @eq nat (@vec_pos nat n v zero) O) (_ : @eq nat (@vec_pos nat n v src) (stack_enc s)), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_push_One) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S O)))))))) i) (@vec_change nat n v src (stack_enc (@cons bool true s)))) *)
      intros H1 H2 H3.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_push_Zero) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S O))))))) i) (@vec_change nat n v src (stack_enc (@cons bool false s)))) *)
      unfold mm_push_Zero.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp zero i) (mm_mul2 tmp src zero (Init.Nat.add (S (S (S O))) i)))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S O))))))) i) (@vec_change nat n v src (stack_enc (@cons bool false s)))) *)
      apply sss_progress_trans with (st2 := (3+i,v[0/src][(v#>src)/tmp])).
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply subcode_sss_progress with (P := (i,mm_transfert src tmp zero i)); auto.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply mm_transfert_progress; auto.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply subcode_sss_progress with (P := (3+i,mm_mul2 tmp src zero (3 + i))); auto.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (Init.Nat.add (S (S (S O))) i) (mm_mul2 tmp src zero (Init.Nat.add (S (S (S O))) i))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S O))) i) (@vec_change nat n (@vec_change nat n v src O) tmp (@vec_pos nat n v src))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S O))))))) i) (@vec_change nat n v src (stack_enc (@cons bool false s)))) *)
      apply mm_mul2_progress; auto; rew vec.
(* Goal: @eq (prod nat (vec nat n)) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) (Init.Nat.add (S (S (S O))) i)) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) tmp1 O) src (stack_enc s)) tmp2 (S O))) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      f_equal.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n (@vec_change nat n v src (stack_enc (@cons bool false s))) src (S (@vec_pos nat n (@vec_change nat n v src (stack_enc (@cons bool false s))) src))) p) (@vec_pos nat n (@vec_change nat n v src (stack_enc (@cons bool true s))) p) *)
      dest p src.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      rewrite H3; auto.
(* Goal: @eq nat (@vec_pos nat n v p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n v src O) tmp O) p) *)
      dest p tmp.
    Qed.

    Definition mm_push_One := mm_push_Zero ++ INC src :: nil.

    Hint Rewrite mm_push_Zero_length : length_db.

    Fact mm_push_One_length : length mm_push_One = 8.
    Proof. reflexivity. Qed.

    Fact mm_push_One_progress s v :
         v#>tmp  = 0
      -> v#>zero = 0
      -> v#>src  = stack_enc s
      -> (i,mm_push_One) // (i,v) -+> (8+i,v[(stack_enc (One::s))/src]).
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v tmp) O) (_ : @eq nat (@vec_pos nat n v zero) O) (_ : @eq nat (@vec_pos nat n v src) (stack_enc s)), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_push_One) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S O)))))))) i) (@vec_change nat n v src (stack_enc (@cons bool true s)))) *)
      intros H1 H2 H3.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_push_One) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S O)))))))) i) (@vec_change nat n v src (stack_enc (@cons bool true s)))) *)
      unfold mm_push_One.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) mm_push_Zero (@cons (mm_instr n) (@mm_inc n src) (@nil (mm_instr n))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S O)))))))) i) (@vec_change nat n v src (stack_enc (@cons bool true s)))) *)
      apply sss_progress_trans with (7+i,v[(stack_enc (Zero::s))/src]).
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply subcode_sss_progress with (P := (i,mm_push_Zero)); auto.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply mm_push_Zero_progress; auto.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) mm_push_Zero (@cons (mm_instr n) (@mm_inc n src) (@nil (mm_instr n))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S O))))))) i) (@vec_change nat n v src (stack_enc (@cons bool false s)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S O)))))))) i) (@vec_change nat n v src (stack_enc (@cons bool true s)))) *)
      mm sss INC with src.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      mm sss stop; f_equal; auto.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n (@vec_change nat n v src (stack_enc (@cons bool false s))) src (S (@vec_pos nat n (@vec_change nat n v src (stack_enc (@cons bool false s))) src))) p) (@vec_pos nat n (@vec_change nat n v src (stack_enc (@cons bool true s))) p) *)
      dest p src.
    Qed.

  End push.

  Hint Rewrite mm_push_Zero_length mm_push_One_length : length_db.

  Section pop.

(*

  div2 n a1 a2 addr1 addr2, suppose a1 = 0 et a2 = 0

  H 001001 B -> 001001_1 -> 0 + 01001_1 || 2*n + 0 -> 0 & n si n <> 0
  H 101001 B -> 101001_1 -> 1 + 01001_1 || 2*n + 1 -> 1 & n si n <> 0
  H ø      B -> ø_1      -> ERROR       || n = 0 (impossible) et n = 1 error

*)

    Variables (src tmp1 tmp2 zero : pos n)
              (Hs1 : src <> tmp1) (Hs2 : src <> tmp2) (Hsz : src <> zero)
              (H12 : tmp1 <> tmp2) (H1z : tmp1 <> zero) (H2z : tmp2 <> zero) 
              (i j k e : nat).
     (* e is jump when stack is empty *)
     (* j is jump when pop gives a Zero *)
     (* k is jump when pop gives a One *)

    Let src' := src.

    Definition mm_pop :=
    (*     i *)  mm_transfert src tmp1 tmp2 i ++
    (*   3+i *)  mm_div2 tmp1 src tmp2 (3+i) ++
    (*   9+i *)  DEC src (13+i) ::
    (*  10+i *)  INC src ::
    (*  11+i *)  DEC tmp2 j ::
    (*  12+i *)  DEC tmp1 k :: 
    (*  13+i *)  DEC tmp2 k ::
    (*  14+i *)  INC src' ::
    (*  15+i *)  DEC tmp2 e ::  
                 nil.

    Fact mm_pop_length : length mm_pop = 16.
    Proof. reflexivity. Qed.

    Fact mm_pop_void_progress v :
         v#>tmp1 = 0
      -> v#>tmp2 = 0 
      -> v#>src  = stack_enc nil 
      -> (i,mm_pop) // (i,v) -+> (e,v).
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v tmp1) O) (_ : @eq nat (@vec_pos nat n v tmp2) O) (_ : @eq nat (@vec_pos nat n v src) (stack_enc (@cons bool true s))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_pop) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      unfold mm_pop.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v tmp1) O) (_ : @eq nat (@vec_pos nat n v tmp2) O) (_ : @eq nat (@vec_pos nat n v src) (stack_enc (@nil bool))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) e v) *)
      intros H1 H2 H4; simpl in H4.
      
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) e v) *)
      apply sss_progress_trans with (3+i,v[0/src][1/tmp1]).
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply subcode_sss_progress with (P := (i,mm_transfert src tmp1 tmp2 i)); auto.
(* Goal: @eq (prod nat (vec nat n)) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) (Init.Nat.add (S (S (S O))) i)) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) tmp1 O) src (stack_enc s)) tmp2 (S O))) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      apply mm_transfert_progress; auto; f_equal.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      rewrite H4; auto.
      
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S O))) i) (@vec_change nat n (@vec_change nat n v src O) tmp1 (S O))) (@pair nat (vec nat n) e v) *)
      apply sss_progress_trans with (9+i,v[0/tmp1][0/src][1/tmp2]).
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply subcode_sss_progress with (P := (3+i,mm_div2 tmp1 src tmp2 (3 + i))); auto.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (Init.Nat.add (S (S (S O))) i) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S O))) i) (@vec_change nat n (@vec_change nat n v src O) tmp1 (S O))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src O) tmp2 (S O))) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src O) tmp2 (S O))) (@pair nat (vec nat n) e v) *)
      apply mm_div2_progress_1 with (k := 0); auto; rew vec.
(* Goal: @eq (prod nat (vec nat n)) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) (Init.Nat.add (S (S (S O))) i)) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) tmp1 O) src (stack_enc s)) tmp2 (S O))) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      f_equal.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) tmp1 O) src (stack_enc s)) tmp2 (S O)) p) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      dest p tmp2; dest p src; dest p tmp1.

(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src O) tmp2 (S O))) (@pair nat (vec nat n) e v) *)
      mm sss DEC 0 with src (13+i); rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src O) tmp2 (S O))) (@pair nat (vec nat n) e v) *)
      mm sss DEC S with tmp2 k 0; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src O) tmp2 O)) (@pair nat (vec nat n) e v) *)
      mm sss INC with src'; unfold src'; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i))) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src O) tmp2 O) src (S O))) (@pair nat (vec nat n) e v) *)
      mm sss DEC 0 with tmp2 e; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) k (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O)) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      mm sss stop; f_equal.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) tmp1 O) src (stack_enc s)) tmp2 (S O)) p) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      dest p tmp2; dest p src; dest p tmp1.
    Qed.

    Fact mm_pop_Zero_progress v s:
         v#>tmp1 = 0
      -> v#>tmp2 = 0 
      -> v#>src  = stack_enc (Zero::s) 
      -> (i,mm_pop) // (i,v) -+> (j,v[(stack_enc s)/src]).
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v tmp1) O) (_ : @eq nat (@vec_pos nat n v tmp2) O) (_ : @eq nat (@vec_pos nat n v src) (stack_enc (@cons bool true s))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_pop) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      unfold mm_pop.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v tmp1) O) (_ : @eq nat (@vec_pos nat n v tmp2) O) (_ : @eq nat (@vec_pos nat n v src) (stack_enc (@cons bool true s))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      intros H1 H2 H4; unfold stack_enc in H4; fold stack_enc in H4.
      
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) j (@vec_change nat n v src (stack_enc s))) *)
      apply sss_progress_trans with (3+i,v[0/src][(2*stack_enc s)/tmp1]).
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply subcode_sss_progress with (P := (i,mm_transfert src tmp1 tmp2 i)); auto.
(* Goal: @eq (prod nat (vec nat n)) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) (Init.Nat.add (S (S (S O))) i)) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) tmp1 O) src (stack_enc s)) tmp2 (S O))) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      apply mm_transfert_progress; auto; f_equal.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      rewrite H4; auto.
      
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S O))) i) (@vec_change nat n (@vec_change nat n v src O) tmp1 (Init.Nat.mul (S (S O)) (stack_enc s)))) (@pair nat (vec nat n) j (@vec_change nat n v src (stack_enc s))) *)
      apply sss_progress_trans with (9+i,v[0/tmp1][(stack_enc s)/src][0/tmp2]).
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply subcode_sss_progress with (P := (3+i,mm_div2 tmp1 src tmp2 (3 + i))); auto.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (Init.Nat.add (S (S (S O))) i) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S O))) i) (@vec_change nat n (@vec_change nat n v src O) tmp1 (Init.Nat.mul (S (S O)) (stack_enc s)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 O)) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 O)) (@pair nat (vec nat n) j (@vec_change nat n v src (stack_enc s))) *)
      apply mm_div2_progress_0 with (k := stack_enc s); auto; rew vec.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      rewrite div2_2p0; auto.
(* Goal: @eq (prod nat (vec nat n)) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) (Init.Nat.add (S (S (S O))) i)) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) tmp1 O) src (stack_enc s)) tmp2 (S O))) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      f_equal.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) tmp1 O) src (stack_enc s)) tmp2 (S O)) p) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      dest p tmp2; dest p src; dest p tmp1.
      
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      destruct (stack_enc_S s) as (q & Hq).
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      mm sss DEC S with src (13+i) q; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i)) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src q)) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      mm sss INC with src; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i))) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 O) src (S q))) (@pair nat (vec nat n) j (@vec_change nat n v src (stack_enc s))) *)
      mm sss DEC 0 with tmp2 j; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) k (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O)) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      mm sss stop; f_equal.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) p) (@vec_pos nat n (@vec_change nat n v src (stack_enc s)) p) *)
      dest p src; dest p tmp2; dest p tmp1.
    Qed.

    Fact mm_pop_One_progress v s:
         v#>tmp1 = 0
      -> v#>tmp2 = 0 
      -> v#>src  = stack_enc (One::s) 
      -> (i,mm_pop) // (i,v) -+> (k,v[(stack_enc s)/src]).
    Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v tmp1) O) (_ : @eq nat (@vec_pos nat n v tmp2) O) (_ : @eq nat (@vec_pos nat n v src) (stack_enc (@cons bool true s))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i mm_pop) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      unfold mm_pop.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v tmp1) O) (_ : @eq nat (@vec_pos nat n v tmp2) O) (_ : @eq nat (@vec_pos nat n v src) (stack_enc (@cons bool true s))), @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      intros H1 H2 H4; unfold stack_enc in H4; fold stack_enc in H4.
      
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      apply sss_progress_trans with (3+i,v[0/src][(2*stack_enc s+1)/tmp1]).
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply subcode_sss_progress with (P := (i,mm_transfert src tmp1 tmp2 i)); auto.
(* Goal: @eq (prod nat (vec nat n)) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) (Init.Nat.add (S (S (S O))) i)) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) tmp1 O) src (stack_enc s)) tmp2 (S O))) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      apply mm_transfert_progress; auto; f_equal.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul (S (S O)) (S k)) (@vec_pos nat n v dst)) (Init.Nat.add (Init.Nat.mul (S (S O)) k) (S (S (@vec_pos nat n v dst)))) *)
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n v src O) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src k) dst (S (S (@vec_pos nat n v dst)))) src O) p) *)
      rewrite H4; f_equal; omega.
      
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S O))) i) (@vec_change nat n (@vec_change nat n v src O) tmp1 (Init.Nat.add (Init.Nat.mul (S (S O)) (stack_enc s)) (S O)))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      apply sss_progress_trans with (9+i,v[0/tmp1][(stack_enc s)/src][1/tmp2]).
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      apply subcode_sss_progress with (P := (3+i,mm_div2 tmp1 src tmp2 (3 + i))); auto.
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (Init.Nat.add (S (S (S O))) i) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S O))) i) (@vec_change nat n (@vec_change nat n v src O) tmp1 (Init.Nat.add (Init.Nat.mul (S (S O)) (stack_enc s)) (S O)))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      apply mm_div2_progress_1 with (k := stack_enc s); auto; rew vec.
(* Goal: @eq nat (@length (mm_instr n) (mm_null i)) (S (S O)) *)
      rewrite div2_2p1; auto.
(* Goal: @eq (prod nat (vec nat n)) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S O)))))) (Init.Nat.add (S (S (S O))) i)) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) tmp1 O) src (stack_enc s)) tmp2 (S O))) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      f_equal.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) p) (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v src O) tmp1 O) src (stack_enc s)) tmp2 (S O)) p) *)
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      dest p tmp2; dest p src; dest p tmp1.
      
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      destruct (stack_enc_S s) as (q & Hq).
(* Goal: @sss_progress (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i) (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      mm sss DEC S with src (13+i) q; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i)) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src q)) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      mm sss INC with src; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i))) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q))) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      mm sss DEC S with tmp2 j 0; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S O) (Init.Nat.add (S (S (S (S (S (S (S (S (S O))))))))) i)))) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O)) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      mm sss DEC 0 with tmp1 k; rew vec.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i (@app (mm_instr n) (mm_transfert src tmp1 tmp2 i) (@app (mm_instr n) (mm_div2 tmp1 src tmp2 (Init.Nat.add (S (S (S O))) i)) (@cons (mm_instr n) (@mm_dec n src (Init.Nat.add (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) i)) (@cons (mm_instr n) (@mm_inc n src) (@cons (mm_instr n) (@mm_dec n tmp2 j) (@cons (mm_instr n) (@mm_dec n tmp1 k) (@cons (mm_instr n) (@mm_dec n tmp2 k) (@cons (mm_instr n) (@mm_inc n src') (@cons (mm_instr n) (@mm_dec n tmp2 e) (@nil (mm_instr n)))))))))))) (@pair nat (vec nat n) k (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O)) (@pair nat (vec nat n) k (@vec_change nat n v src (stack_enc s))) *)
      mm sss stop; f_equal.
(* Goal: @eq (vec nat n) (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) (@vec_change nat n v src (stack_enc s)) *)
      apply vec_pos_ext; intros p.
(* Goal: @eq nat (@vec_pos nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n (@vec_change nat n v tmp1 O) src (stack_enc s)) tmp2 (S O)) src (S q)) tmp2 O) p) (@vec_pos nat n (@vec_change nat n v src (stack_enc s)) p) *)
      dest p src; dest p tmp2; dest p tmp1.
    Qed.

  End pop.
  
End Minsky_Machine_utils.

Hint Rewrite mm_push_Zero_length mm_push_One_length mm_pop_length : length_db.
