fact: Definition to_Config (s : mm_state 2) : MPM2.Config := match s with | (S p, Vector.cons _ a _ (Vector.cons _ b _ _)) => (p, (a, b)) | (0, Vector.cons _ a _ (Vector.cons _ b _ _)) => (length P, (a, b)) | _ => (0, (0, 0)) end.
imports: PeanoNat Lia List Undecidability.MinskyMachines(MM MM_sss) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) ssreflect ssrbool ssrfun