proposition: Lemma MMA_computable_R : MMA_computable R.
proof: Proof. Proof using Hs0 Hs0R H's0R. eexists _, (COMPUTE 1). move=> v m. have /wCBV.machine_correctness H := closed_many_app_nat_enc (Vector.to_list v) Hs0. split. - move=> /Hs0R. rewrite Vector.to_list_fold_left. move=> /H [y] [/simulation] /[apply] {}H. do 2 eexists. split. { by apply: H. } right. rewrite /= COMPUTE_len_spec. lia. - move=> [n] [v'] Hmv'. apply /Hs0R. rewrite Vector.to_list_fold_left. apply /H. apply /wCBV.machine_correctness. { by apply: closed_many_app_nat_enc. } have [t] : exists t, eval (Vector.fold_left (fun (s : term) (n : nat) => app s (nat_enc n)) s0 v) t. { apply: sss_terminates_COMPUTE_eval. eexists. by eassumption. } move=> /[dup] /H's0R [m' ->]. rewrite Vector.to_list_fold_left. move=> Hm'. suff: m = m' by move ->. move: Hm' => /H [y] [/simulation] /[apply] /(_ 1) {}H. have : sss_output (mma_sss (n:=num_counters)) (1, COMPUTE 1) (1, Vector.append (0 ## v) vec_zero) (COMPUTE_len + 1, m' ## vec_zero). { split; [done|]. right. rewrite /= COMPUTE_len_spec. lia. } move: Hmv' (@mma_defs.mma_sss_fun num_counters) => /sss_output_fun /[apply] /[apply]. by case. 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