fact: Definition RealiseIn n (F : Type) (pM : pTM F n) (R : pRel sig F n) (k : nat) := forall input, exists outc, loopM (initc (projT1 pM) input) k = Some outc /\ R input ((projT2 pM (cstate outc)), ctapes outc).
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM