proposition: Lemma sss_terminates_sss_compute_inv P x y : P // x ->> y -> sss_terminates (mma_sss (n:=num_counters)) P x -> sss_terminates (mma_sss (n:=num_counters)) P y.
proof: Proof. move=> ? [st] [Hx ?]. exists st. split; [|done]. apply: sss_compute_inv; [|eassumption..]. by apply: mma_defs.mma_sss_fun. 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