proposition: Fact read_head_Zero v l : v#>y = Zero::l -> (i,read_head) // (i,v) -+> (p,v).
proof: Proof. unfold read_head; intros H. bsm sss POP zero with y (4+i) j l. bsm sss PUSH with y Zero. apply subcode_sss_compute_trans with (P := (5+i,jump p)) (st2 := (p,v)); auto. 2: bsm sss stop. apply jump_spec'. rew vec; rewrite <- H; 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)