proposition: Theorem pcp_bsm_sound v : tiles_solvable lt -> (1,simulator) // (1,v) ->> (0,v[nil/s][nil/a][nil/h][nil/l]).
proof: Proof. intros H1; unfold simulator. apply subcode_sss_compute_trans with (2 := main_init_spec Hsa Hsh Hsl Hah Hal 1 v); auto. destruct (main_loop_sound Hsa Hsh Hsl Hah Hal Hhl) with (lt := lt) (i := 14) (p := 14+lML) (v := v[(Zero::nil)/s][nil/a][nil/h][nil/l]) as (w & Hw1 & Hw2); rew vec. apply subcode_sss_compute_trans with (2 := Hw1); auto. apply subcode_sss_compute_trans with (2 := main_init_spec Hsa Hsh Hsl Hah Hal (14+lML) _); auto. bsm sss POP zero with s 0 0 nil; rew vec. bsm sss stop; f_equal. apply vec_pos_ext; intros x. dest x a; dest x l; dest x h; dest x s. rewrite <- Hw2; 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 bsm_utils)