proposition: Fact read_head_spec v (b : bool) l w k : v = w -> v#>y = b::l -> k = (if b then j else p) -> (i,read_head) // (i,v) -+> (k,w).
proof: Proof. intros <- H ->. destruct b. + eapply read_head_One; eauto. + eapply read_head_Zero; eauto. 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)