proposition: Fact main_loop_ko_spec v ln lc : v#>h = nil -> v#>l = nil -> v#>a = nil -> v#>s = 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) ) \/ Forall (fun x => x < length lt) ln /\ lc = nil /\ let (hh,ll) := tile_concat ln lt in hh <> ll) -> (i,main_loop) // (i,v) ->> (i,v[(list_bool_next (v#>s))/s]).
proof: Proof. Proof using Hsl Hsh Hsa Hhl Hal Hah. intros H0 H1 H2 H3 [ H4 | (H4 & ? & H5) ]. destruct (@full_decoder_ko_spec _ _ _ Hah Hal Hhl (lFD+16+i) (lFD+26+i) (16+i)) with (v := v[(list_nat_bool ln ++ lc)/a]) (2 := H4) as (w & Hw1 & Hw2); rew vec. unfold main_loop. apply sss_compute_trans with (st2 := (16+i,v[(list_nat_bool ln++lc)/a])). apply subcode_sss_compute with (P := (i,copy_stack s a h i)); auto. apply copy_stack_spec with (list_nat_bool ln++lc); auto. rewrite H2, app_nil_r; auto. apply subcode_sss_compute_trans with (2 := Hw1); auto. apply subcode_sss_compute with (P := (lFD+26+i,increment_erase (lFD + 26 + i) i)); auto. apply increment_erase_spec with (1 := list_bool_next_spec (v#>s)); auto. rewrite <- Hw2; auto; rew vec. apply vec_pos_ext; intros x. dest x a; dest x l; dest x h; dest x s. rewrite <- Hw2; auto; rew vec. unfold main_loop. subst lc. rewrite app_nil_r in H3. case_eq (tile_concat ln lt). intros hh ll E; rewrite E in H5. destruct (compare_stack_neq_spec Hhl (lFD+16+i) p (lFD+26+i) (v[nil/a][hh/h][ll/l])) as (w & Hw1 & Hw2); rew vec. 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 sss_compute_trans with (st2 := (lFD+26+i,w)). apply subcode_sss_compute with (P := (lFD+16+i,compare_stacks h l (lFD+16+i) p (lFD+26+i))); auto. apply subcode_sss_compute with (P := (lFD+26+i,increment_erase (lFD + 26 + i) i)); auto. apply increment_erase_spec with (1 := list_bool_next_spec (v#>s)); auto. rewrite <- Hw2; auto; rew vec. apply vec_pos_ext; intros x. dest x a; dest x l; dest x h; dest x s. 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)