fact: Definition BSM_HALTING (P : BSM_PROBLEM) := match P with existT _ n (existT _ i (existT _ P v)) => (i,P) // (i,v) ↓ end.
imports: Undecidability.StackMachines.BSM List Bool Lia Nat Undecidability.Shared.Libs.DLW(list_bool pos vec sss)