proposition: Lemma inverse_simulation ts ctx t : let v := (0 ## 0 ## (enc_cs ts) ## (enc_cs ctx) ## (enc_term t) ## Vector.nil _) in all (map eclosed ts) -> eclosed (closure ctx t) -> (sss_terminates (@mma_sss _) (1, PROG 1) (1, v)) -> halt_cbn ts ctx t.
proof: Proof. move=> v. move Ex: (1, v) => x ++ H. subst v. move: x H ts ctx t Ex. apply: sss_terminates_ind; [ exact: mma_defs.mma_sss_fun | |]. { move=> [? ?] /= ? > []. lia. } move=> [i' v'] IH ts ctx t [? ?]. move => /(_ _ _ (subcode.subcode_refl (1, PROG 1)) _ _ _ _ erefl) in IH. subst i' v'. case: t IH. - case. + case: ctx => [|[ctx' t'] ctx'']. { move=> IH _ /= [/term_facts.boundE]. lia. } move=> IH ? /= [?] [? ?]. constructor. apply: IH; [|done|done]. by apply: PROG_VAR0_spec. + move=> n. case: ctx => [|[ctx' t'] ctx'']. { move=> IH _ /= [/term_facts.boundE]. lia. } move=> IH ? /= [/boundS ?] [? ?]. constructor. apply: IH; [|done|done]. by apply: PROG_VARS_spec. - move=> s t IH /= ? [/term_facts.boundE [? ?] ?]. constructor. apply: IH; [|done|done]. by apply: PROG_APP_spec. - move=> s. case: ts => [|t' ts']. { move=> *. by constructor. } move=> IH /= [? ?] [/term_facts.boundE ? ?]. constructor. apply: IH; [|done|done]. by apply: PROG_LAM_spec. 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