proposition: Fact decoder_spec_nok_2 s i ll lc v k : v#>c = list_repeat Zero k ++ lc -> length ll <= k -> exists r, (i,decoder s i ll) // (i,v) ->> (q,v[(list_repeat Zero r ++ lc)/c]).
proof: Proof. revert i lc v k. induction ll as [ | (t1,t2) ll IHll ]; intros i lc v k H1 H2. simpl; unfold decoder_error. exists k. bsm sss PUSH with c Zero. bsm sss POP zero with c q q (v#>c); rew vec. bsm sss stop. f_equal. apply vec_pos_ext; intros z; dest z c. unfold decoder; fold decoder. destruct k as [ | k ]. simpl in H2; lia. simpl in H1, H2. destruct (IHll (3 + length (tile h l t1 t2) + i) lc (v[(list_repeat Zero k++lc)/c]) k) as (r & Hr); rew vec. lia. exists r. bsm sss POP zero with c (3 + length (tile h l t1 t2) + i) q (list_repeat Zero k++lc). revert Hr; rew vec; apply subcode_sss_compute; auto. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)