proposition: Lemma subcode1 i : let off := j + c * !i in (26 + off, [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 ) ]) <sc (off, PROG i).
proof: Proof. intros ?. match goal with | [ |- (?o + ?i, ?c1) <sc (?i, ?c2) ] => exists (firstn o c2); exists []; split end. rewrite app_nil_r. 2:rewrite firstn_length, PROG_length. 2:lia. enough (firstn 26 (PROG i) = [ 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)]); subst off. rewrite H. unfold PROG. now rewrite <- !app_assoc. unfold PROG. destruct (δ (i, Some One)) as [ [ [] [] ] | ]; reflexivity. Qed.
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)