proposition: Lemma sss_terminates_COMPUTE_eval offset v : sss_terminates (mma_sss (n:=num_counters)) (offset, COMPUTE offset) (offset, Vector.append (0 ## v) vec_zero) -> exists t, eval (Vector.fold_left (fun (s : term) (n0 : nat) => app s (nat_enc n0)) s0 v) t.
proof: Proof. Proof using Hs0. have := simulation_init offset v. move=> /sss_terminates_sss_compute_inv /[apply]. move=> /subcode_sss_terminates. set i := list_sum (firstn 3 COMPUTE_lengths) + offset. move=> /(_ (i, PROG i)). apply: unnest. { apply: (subcode_nth_compose 3). rewrite (length_compose (lengths := firstn 3 COMPUTE_lengths)) //. apply: Forall2_firstn. by apply: COMPUTE_lengths_spec. } rewrite Vector.to_list_fold_left. move=> /(sss_terminates_PROG_machine _ nil _). apply: unnest. { split; [|done]. apply /L_facts.closed_dcl. by apply: closed_many_app_nat_enc. } apply: unnest. { done. } move=> [?] /wCBV.machine_inverse_simulation. apply: unnest. { split; [|done]. apply /L_facts.closed_dcl. by apply: closed_many_app_nat_enc. } apply: unnest. { done. } rewrite flatten_term => ?. eexists. eassumption. 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