fact: Definition sbtm_op := BR (1+i) (5+i) :: JMP (if o1 then 2+i else k) :: WR b1 :: MV d1 :: JMP j1 :: JMP (if o0 then 6+i else k) :: WR b0 :: MV d0 :: JMP j0 :: nil.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils pos subcode sss) Undecidability.Synthetic(ReducibilityFacts) Undecidability.TM(SBTM pctm_defs)