proposition: Lemma CASE_VAR0_spec vs x ctx p w offset : (offset, CASE_VAR0 p offset) // (offset, Vector.append w (0##0##0##enc_vs vs##enc_cs (x :: ctx)##0##vec_nil)) ->> (p, Vector.append w (0##0##0##enc_vs vs##0##(enc_closure x)##vec_nil)).
proof: Proof. rewrite [enc_cs _]/=. apply: (compose_sss_compute_trans 0). { by apply: UNPACK_spec. } apply: (compose_sss_compute_trans 1). { by apply: ZERO_spec. } apply: (compose_sss_compute_trans 2). { by apply: JMP_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