fact: Definition StateWhileTM (l1 : F1) : TM sig n := {| start := liftState (start (projT1 (pM l1))); trans := StateWhile_trans; halt := StateWhile_halt; |}.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts