proposition: Lemma PREP_spec i v w : (i, PREP i) /MM/ (i, Vector.append (Vector.append (0 ## v) w) (0 ## 0 ## 0 ## vec_nil)) ~~> (i + (k * 14), Vector.append (Vector.append (0 ## Vector.map (fun n => stack_enc (List.repeat true n)) v) w) (0 ## 0 ## 0 ## vec_nil)).
proof: Proof. unfold PREP. pose proof (@PREP_spec_strong i 0 w k 0 v vec_nil v (myeq k)). match goal with [ |- sss_output _ _ (_, ?st) _ ] => evar (Vector.t nat (1 + k + n + 3)); enough (st = t) as ->; subst t end. 1: match goal with [ |- sss_output _ _ _ (_, ?st) ] => evar (Vector.t nat (1 + k + n + 3)); enough (st = t) as ->; subst t end. 1: apply H; try reflexivity. 3: reflexivity. 2:{ repeat f_equal. clear. induction k; cbn. - rewrite cast_eq_refl. pattern v. revert v. eapply Vector.case0. reflexivity. - eapply (Vector.caseS' v). clear v. intros x v. cbn. f_equal. rewrite IHn. eapply cast_ext. f_equal. eapply IHn. } clear. generalize (myeq k). induction v; intros E. - cbn. reflexivity. - cbn. f_equal. eapply IHv. Qed.
imports: Undecidability.MinskyMachines(MM_computable MM_sss mm_utils) Undecidability.StackMachines(BSM_computable) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Lia Vector Nat Arith List Undecidability.MinskyMachines.MM(mm_defs mm_utils mm_comp_strong)