proposition: Lemma sss_terminates_sss_compute P x y : P // x ->> y -> sss_terminates (mma_sss (n:=5)) P y -> sss_terminates (mma_sss (n:=5)) P x.
proof: Proof. move=> H [z [Hz ?]]. exists z. split; [|done]. apply: sss_compute_trans; eassumption. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA LambdaCalculus.Krivine LambdaCalculus.Util.Krivine_facts) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia ssreflect ssrbool ssrfun