proposition: Fact ovwrite_head_1 c l v : v#>y = c::l -> (i,ovwrite_head) // (i,v) -+> (1+i,v[l/y]).
proof: Proof. intros H; unfold ovwrite_head; destruct c. + bsm sss POP one with y (1+i) (1+i) l; bsm sss stop. + bsm sss POP zero with y (1+i) (1+i) l; bsm sss stop. 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)