proposition: Theorem pcp_bsm_complete v w p : (1,simulator) // (1,v) ~~> (p,w) -> tiles_solvable lt /\ p = 0 /\ w = v[nil/s][nil/a][nil/h][nil/l].
proof: Proof. intros ((k2 & Hk2) & H1). destruct (main_init_spec Hsa Hsh Hsl Hah Hal 1 v) as (k1 & Hk1). apply subcode_sss_subcode_inv with (4 := Hk1) in Hk2; auto. 2: apply bsm_sss_fun. 2: revert H1; apply subcode_out_code; auto. destruct Hk2 as (k & ? & Hk2); subst. apply subcode_sss_steps_inv with (1 := HS2) in Hk2; auto. 2: simpl; lia. 2: revert H1; apply subcode_out_code; auto. destruct Hk2 as (k2 & k3 & (q,v') & H2 & H3 & H4 & H5). simpl fst in H5. apply ex_intro with (x := k2) in H2. apply main_loop_complete in H2; rew vec. 2: unfold out_code, code_end, snd, fst, lML; rew length; lia. destruct H2 as (? & H2 & H6); subst. split; auto. destruct (main_init_spec Hsa Hsh Hsl Hah Hal (14+lML) v') as (k4 & Hk4). apply subcode_sss_subcode_inv with (4 := Hk4) in H3; auto. 2: apply bsm_sss_fun. 2: revert H1; apply subcode_out_code; auto. destruct H3 as (k5 & ? & H7); subst. unfold simulator in H7. bsm inv POP zero with H7 s 0 0 (@nil bool); rew vec. + destruct H7 as (k6 & H7 & H8). apply sss_steps_stall in H8. 2: simpl; lia. apply proj2 in H8. inversion H8. split; auto. apply vec_pos_ext; intros x. dest x s; dest x l; dest x h; dest x a. rewrite <- H2; rew vec. + intros E. apply f_equal with (f := fst) in E. unfold fst in E. subst p. revert H1. unfold out_code, code_start, code_end, fst, snd. rewrite simulator_length. intro; lia. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs bsm_utils)