proposition: Lemma CASE_APP_spec ts ctx t p v offset : vec_pos v TS = enc_cs ts -> vec_pos v CTX = enc_cs ctx -> vec_pos v B = enc_term t -> (offset, CASE_APP p offset) // (offset, v) ->> (p, vec_change (vec_change (vec_change v TS (enc_cs ((closure ctx t)::ts))) B 0) A 0).
proof: Proof. rewrite (counters_eta v) /= => -> -> ->. rewrite /=. apply: (concat_sss_compute_trans 0). { by apply: PACK_spec. } rewrite /=. apply: (concat_sss_compute_trans 1). { by apply: MOVE_spec. } rewrite /=. apply: (concat_sss_compute_trans 2). { by apply: MOVE_spec. } rewrite /=. apply: (concat_sss_compute_trans 3). { by apply: PACK_spec. } rewrite /=. apply: (concat_sss_compute_trans 4). { by apply: UNPACK_spec. } rewrite /=. apply: (concat_sss_compute_trans 5). { by apply: ZERO_spec. } apply: (concat_sss_compute_trans 6). { by apply: JMP_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