proposition: Lemma PROG_VARS_spec offset ts ctx n u : (offset, PROG offset) // (offset, 0 ## 0 ## enc_cs ts ## enc_cs (u :: ctx) ## enc_term (var (S n)) ## vec_nil) -+> (offset, 0 ## 0 ## enc_cs ts ## enc_cs ctx ## enc_term (var n) ## vec_nil).
proof: Proof. apply: PROG_start_spec. apply: (concat_sss_compute_trans 1). { by apply: UNPACK_spec. } rewrite /= ?(Nat.add_assoc _ _ offset). apply: mma_step. apply: mma_step. apply: (concat_sss_compute_trans 5). { by apply: CASE_VARS_spec. } by apply: sss_compute_refl. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA LambdaCalculus.Krivine LambdaCalculus.Util.Krivine_facts) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia ssreflect ssrbool ssrfun