proposition: Fact decoder_spec_ok s i ll th tl lr lc v st : v#>c = list_repeat Zero (length ll) ++ One :: lc -> st = (s,v[lc/c][(th++v#>h)/h][(tl++v#>l)/l]) -> (i,decoder s i (ll++(th,tl)::lr)) // (i,v) ->> st.
proof: Proof. Proof using Hhl Hcl Hch. intros; subst; apply decoder_spec_rec with ll th tl lr lc; 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)