proposition: Lemma PROG_APP_spec offset vs xs s t w : (offset, PROG offset) // (offset, Vector.append w (0 ## 0 ## 0 ## enc_vs vs ## 0 ## enc_closure (closure xs (app s t)) ## vec_nil)) -+> (offset, Vector.append w (0 ## 0 ## 0 ## enc_vs ((true, (closure xs t)) :: vs) ## 0 ## enc_closure (closure xs s) ## vec_nil)).
proof: Proof. rewrite [enc_vs (_ :: _)]/=. 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 7). { by apply: DEC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 9). { by apply: CASE_APP_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