proposition: Lemma PROG_VAR0_spec offset vs x xs w : (offset, PROG offset) // (offset, Vector.append w (0 ## 0 ## 0 ## enc_vs vs ## 0 ## enc_closure (closure (x :: xs) (var 0)) ## vec_nil)) -+> (offset, Vector.append w (0 ## 0 ## 0 ## enc_vs vs ## 0 ## enc_closure x ## vec_nil)).
proof: Proof. rewrite [enc_closure _]/=. rewrite ?vec_simpl. apply: (compose_sss_progress_trans 0). { by apply: ZERO_spec'. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 1). { by apply: UNPACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 2). { by apply: UNPACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 3). { by apply: DEC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 4). { by apply: DEC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 5). { by apply: CASE_VAR0_spec. } rewrite ?vec_simpl. by apply: sss_compute_refl. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA L.L) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability(MinskyMachines.Util.MMA_pairing L.AbstractMachines.wCBV) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun