proposition: Lemma sss_terminates_PROG_machine offset vs x : sss_terminates (mma_sss (n:=num_counters)) (offset, PROG offset) (offset, Vector.append vec_zero (0 ## 0 ## 0 ## enc_vs vs ## 0 ## enc_closure x ## vec_nil)) -> eclosed x -> Forall eclosed_future vs -> exists y, machine x vs y.
proof: Proof. have H' : forall (P Q : eterm -> Prop), (forall y, P y -> Q y) -> (exists y, P y) -> exists y, Q y. { firstorder done. } pose f := fun t => (offset, Vector.append vec_zero (0 ## 0 ## 0 ## enc_vs (fst t) ## 0 ## enc_closure (snd t) ## vec_nil)). pose P := fun t => eclosed (snd t) -> Forall eclosed_future (fst t) -> exists y, machine (snd t) (fst t) y. suff : forall vs_x, sss_terminates (mma_sss (n:=num_counters)) (offset, PROG offset) (f _ vs_x) -> P vs_x by move=> /(_ (vs, x)). apply: sss_terminates_mma_f_ind. { move=> [{}vs {}x]. have := PROG_len_spec offset. move: (PROG offset) => ? /= ->. rewrite /PROG_len /DEC_len. by lia. } subst P. move=> [{}vs [xs [{}x|s t|s]]] /= IH. - move: x xs IH => [|x] [|z xs] /= IH. + move=> [/boundE] /=. lia. + have := PROG_VAR0_spec offset vs z xs vec_zero. move=> /(IH (vs, z)) /= {}IH [_] [/IH] {}IH _ /IH. apply: H' => ?. by apply: machine_var_0. + move=> [/boundE]. lia. + have := PROG_VARS_spec offset vs z xs x vec_zero. move=> /(IH (vs, (closure xs (var x)))) /= {}IH. move=> [/bound_var_S_iff] ? [??] /IH. apply: unnest. { done. } apply: H' => ?. by apply: machine_var_S. - have := PROG_APP_spec offset vs xs s t vec_zero. move=> /(IH (((true, closure xs t) :: vs), (closure xs s))) /= {}IH. move=> [/boundE [??]] ??. move: IH. apply: unnest. { done. } apply: unnest. { by constructor. } apply: H' => ?. by apply: machine_app. - move: vs IH => [|[[] z] vs] /= IH. + move=> *. eexists. by apply: machine_lam. + have := PROG_LAM_SWAP_spec offset vs xs s z vec_zero. move=> /(IH (((false, closure xs s) :: vs), z)) /= {}IH. move=> [??] /Forall_cons_iff [??]. move: IH. apply: unnest. { done. } apply: unnest. { by constructor. } apply: H' => ?. by apply: machine_lam_swap. + move: z IH => [xs's s'] /= IH. have := PROG_LAM_SUBST_spec offset vs xs's xs s' s vec_zero. move=> /(IH (vs, closure (closure xs (lam s) :: xs's) s')) /= {}IH. move=> [??] /Forall_cons_iff [/= [/boundE ??] ?]. move: IH. apply: unnest. { done. } apply: unnest. { done. } apply: H' => ?. by apply: machine_lam_subst. 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