proposition: Lemma sss_compute_iff {n P s t} : P // s ->> t <-> clos_refl_trans _ (sss_step (@mma_sss n) P) s t.
proof: Proof. split. - case=> k. elim: k s. { move=> ? /sss_steps_0_inv <-. by apply: rt_refl. } move=> ? IH ? H. inversion H. by apply: rt_trans; [apply: rt_step|apply: IH]; eassumption. - move=> /clos_rt_rt1n_iff. elim. { move=> ?. exists 0. by constructor. } move=> > ? _ ?. apply: sss_compute_trans; [|eassumption]. exists 1. by econstructor; [eassumption|constructor]. Qed.
imports: Undecidability(TM.TM) Undecidability.MinskyMachines(MM MMA MMA.mma_defs Util.MMA_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) List PeanoNat Lia Relations ssreflect