proposition: Theorem full_decoder_ok_spec i ln lt v : v#>c = list_nat_bool ln -> v#>h = nil -> v#>l = nil -> Forall (fun x => x < length lt) ln -> let (hh,ll) := tile_concat ln lt in (i,full_decoder i lt) // (i,v) ->> (p,v[nil/c][hh/h][ll/l]).
proof: Proof. Proof using Hhl Hcl Hch. intros H1 H2 H3 H4. rewrite <- app_nil_r in H1. generalize (@full_dec_spec_rec i ln nil lt v H1 H4). destruct (tile_concat ln lt) as (hh,ll). intros E. apply sss_compute_trans with (1 := E); auto. rewrite H2, H3; repeat rewrite app_nil_r. apply full_dec_start_spec_0; rew vec. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)