proposition: Fact main_loop_ok_spec v ln : v#>h = nil -> v#>l = nil -> v#>a = nil -> v#>s = list_nat_bool ln -> Forall (fun x => x < length lt) ln -> (let (hh,ll) := tile_concat ln lt in hh = ll) -> exists w, (i,main_loop) // (i,v) ->> (p,w) /\ forall x, x <> a -> x <> h -> x <> l -> v#>x = w#> x.
proof: Proof. Proof using Hsa Hhl Hal Hah Hsh. intros H0 H1 H2 H3 H4 H5. case_eq (tile_concat ln lt). intros hh ll E; rewrite E in H5. destruct (compare_stack_eq_spec Hhl (lFD+16+i) p (lFD+26+i) (v[nil/a][hh/h][ll/l])) as (w & Hw1 & Hw2); rew vec. exists w; split. unfold main_loop. apply sss_compute_trans with (st2 := (16+i,v[(list_nat_bool ln)/a])). apply subcode_sss_compute with (P := (i,copy_stack s a h i)); auto. apply copy_stack_spec with (list_nat_bool ln); auto. rewrite H2, app_nil_r; auto. apply sss_compute_trans with (st2 := (lFD+16+i,v[nil/a][hh/h][ll/l])). apply subcode_sss_compute with (P := (16+i,full_decoder a h l (lFD+16+i) (lFD+26+i) (16+i) lt)); auto. generalize (@full_decoder_ok_spec _ _ _ Hah Hal Hhl (lFD+16+i) (lFD+26+i) (16+i) ln lt (v[(list_nat_bool ln)/a])); intros H6. do 3 (spec in H6; [ rew vec | ]). spec in H6; auto. rewrite E in H6. eq goal H6; do 2 f_equal; rew vec. apply subcode_sss_compute with (P := (lFD+16+i,compare_stacks h l (lFD+16+i) p (lFD+26+i))); auto. intros x E1 E2 E3; generalize (Hw2 _ E2 E3); 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)