proposition: Fact ovwrite_head_spec c l v w : v#>y = c::l -> w = v[(b::l)/y] -> (i,ovwrite_head) // (i,v) -+> (j,w).
proof: Proof. intros H ->. apply sss_progress_trans with (1 := ovwrite_head_1 _ H). unfold ovwrite_head. bsm sss PUSH with y b. apply subcode_sss_compute_trans with (P := (2+i,jump j)) (st2 := (j,v[(b::l)/y])); auto. 2: bsm sss stop. apply jump_spec'; rew vec. Qed.
imports: List Arith Lia Bool Undecidability.Synthetic(ReducibilityFacts) Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss compiler_correction) Undecidability.StackMachines.BSM(bsm_defs) Undecidability.TM(SBTM pctm_defs)