fact: Definition Canonical_Rel : pRel sig F n := fun t1 '(y, t2) => exists outc k, loopM (M := projT1 pM) (initc (projT1 pM) t1) k = Some outc /\ ctapes outc = t2 /\ projT2 pM (cstate outc) = y.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM