proposition: Lemma simulation {offset ts ctx t} : 0 < offset -> halt_cbn ts ctx t -> let v := (0 ## 0 ## (enc_cs ts) ## (enc_cs ctx) ## (enc_term t) ## Vector.nil _) in (sss_terminates (@mma_sss _) (offset, PROG offset) (offset, v)).
proof: Proof. move=> ? H. elim: H; clear ts ctx t. - move=> > _ /=. apply: sss_terminates_sss_compute. apply: sss_progress_compute. by apply: PROG_VAR0_spec. - move=> > _ /=. apply: sss_terminates_sss_compute. apply: sss_progress_compute. by apply: PROG_VARS_spec. - move=> > _ /=. apply: sss_terminates_sss_compute. apply: sss_progress_compute. by apply: PROG_APP_spec. - move=> > _ /=. apply: sss_terminates_sss_compute. apply: sss_progress_compute. by apply: PROG_LAM_spec. - move=> /= >. eexists. split. + apply: (concat_sss_compute_trans 0). { by apply: JMP_spec. } apply: (concat_sss_compute_trans 1). { by apply: UNPACK_spec. } rewrite /= ?(Nat.add_assoc _ _ offset). apply: mma_step. apply: mma_step. apply: (concat_sss_compute_trans 7). { by apply: CASE_LAM_spec'. } by apply: sss_compute_refl. + by left. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA LambdaCalculus.Krivine LambdaCalculus.Util.Krivine_facts) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia ssreflect ssrbool ssrfun