proposition: Theorem full_decoder_ko_spec i ln lc lt v : v#>c = list_nat_bool ln ++ lc -> (Exists (fun x => length lt <= x) ln \/ Forall (fun x => x < length lt) ln /\ exists k, lc = list_repeat Zero (S k)) -> exists w, (i,full_decoder i lt) // (i,v) ->> (q,w) /\ forall z, z <> c -> z <> h -> z <> l -> v#>z = w#>z.
proof: Proof. Proof using Hhl Hcl Hch. intros H1 [ H2 | (H2 & k & H3) ]. apply full_dec_spec_rec1 with ln lc; auto. generalize (@full_dec_spec_rec i ln lc lt v H1 H2). destruct (tile_concat ln lt) as (hh,ll); intros H4. destruct (@full_dec_spec_rec2 i k lt (v[lc/c][(hh++v#>h)/h][(ll++v#>l)/l])) as (w & Hw1 & Hw2); rew vec. exists w; split. apply sss_compute_trans with (1 := H4); auto. intros x E1 E2 E3; rewrite <- Hw2; auto; 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)