proposition: Lemma CASE_LAM_nil_spec p q w offset n s : (offset, CASE_LAM p q offset) // (offset, Vector.append w (0##0##0##0##n##enc_term s##vec_nil)) ->> (q, Vector.append w (0##0##0##0##n##enc_term (lam s)##vec_nil)).
proof: Proof. rewrite ?vec_simpl. apply: (compose_sss_compute_trans 0). { by apply: JZ_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 6). { by apply: INC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 7). { by apply: PACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 8). { by apply: JMP_spec. } 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