proposition: Lemma PROG_simulation offset x vs y n w : machine x vs y -> flatten y = L.nat_enc n -> (offset, PROG offset) // (offset, Vector.append w (0 ## 0 ## 0 ## enc_vs vs ## 0 ## enc_closure x ## vec_nil)) ->> (PROG_len+offset, vec_change (Vector.append w vec_zero) Fin.F1 n).
proof: Proof. elim=> > ?; [..|by apply: PROG_LAM_spec] => IH ?. all: apply: sss_compute_trans; [|by apply: IH]. all: apply: sss_progress_compute. - by apply: PROG_VAR0_spec. - by apply: PROG_VARS_spec. - by apply: PROG_APP_spec. - by apply: PROG_LAM_SWAP_spec. - by apply: PROG_LAM_SUBST_spec. 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