fact: Definition StateWhile_halt : StateWhile_states -> bool := fun q => halt (projT2 q) && match projT2 (pM (projT1 q)) (projT2 q) with | inl _ => false | inr l2 => true end.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts