fact: Definition PROG (i : Fin.t (S (num_states M))) := let off := j + c * !i in [ POP CURR (26 + off) (51 + off) ; PUSH CURR (if! δ (i, Some true) is Some (_, Some false, _) then false else true) ] ++ match δ (i, Some true) with Some (_, _, Rmove) => MOVE_R (2 + off) | Some (_, _, Lmove) => MOVE_L (2 + off) | _ => repeat (JMP (25 + off)) 23 end ++ [ JMP (match δ (i, Some true) with None => END | Some (q', _, _) => (j + c * ! q') end) ; PUSH CURR (if! δ (i, Some false) is Some (_, Some true, _) then true else false) ] ++ match δ (i, Some false) with Some (_, _, Rmove) => MOVE_R (27 + off) | Some (_, _, Lmove) => MOVE_L (27 + off) | _ => repeat (JMP (50 + off)) 23 end ++ [ JMP (match δ (i, Some false) with None => END | Some (q', _, _) => (j + c * ! q') end) ; match δ (i, None) with None => JMP END | Some (_, Some w, _) => PUSH CURR w | Some _ => JMP (52 + off) end ] ++ match δ (i, None) with Some (_, _, Rmove) => MOVE_R (52 + off) | Some (_, _, Lmove) => MOVE_L (52 + off) | _ => repeat (JMP (75 + off)) 23 end ++ [ JMP (match δ (i, None) with None => END | Some (q', _, _) => (j + c * ! q') end ) ] .
imports: Undecidability.TM.KOSBTM.KOSBTM Undecidability.Shared.Libs.PSL.Vectors.FinNotation Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.Shared.Libs.PSL.EqDec List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(bsm_defs)