proposition: Lemma PROG_LAM_spec offset xs s n w : flatten (closure xs (lam s)) = L.nat_enc n -> (offset, PROG offset) // (offset, Vector.append w (0 ## 0 ## 0 ## enc_vs [] ## 0 ## enc_closure (closure xs (lam s)) ## vec_nil)) ->> (PROG_len+offset, vec_change (Vector.append w vec_zero) Fin.F1 n).
proof: Proof. move=> Hn. rewrite ?vec_simpl. apply: (compose_sss_compute_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 8). { by apply: CASE_LAM_nil_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 10). { apply: DECODE_NAT_spec. exact: Hn. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 11). { by apply: ZERO_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 12). { by apply: MOVE_spec. } apply: sss_compute_refl'. congr pair. by rewrite (Vector.eta w) /= ?vec_simpl. 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