proposition: Lemma MMA_TM_iff {n MM} {cs : Vector.t nat n} : @MMA_HALTING n (MM, cs) <-> HaltsTM (MMA_TM.P MM) (MMA_TM.encode_counters cs).
proof: Proof. split. - by apply: MMA_TM.simulation. - by move=> [p'] [ts] /MMA_TM.inverse_simulation. Qed.
imports: Undecidability(TM.UTM TM.TM LambdaCalculus.Krivine MinskyMachines.MMA Shared.Libs.PSL.FiniteTypes.FinTypesDef) Coq(Vector ssreflect ssrbool ssrfun)