proposition: Theorem iPCPb_to_BSM_HALTING : iPCPb ⪯ Halt_BSM.
proof: Proof. exists f. intros lt. rewrite <- tiles_solvable_iBPCP. rewrite Halt_BSM_iff. unfold BSM_HALTING; split. * intros H. apply pcp_bsm_sound with (v := vec_set_pos (fun _ => nil)) in H. match type of H with _ // _ ->> (?q,?w) => exists (q, w) end. split; auto. simpl; lia. * intros ((q & w) & H). apply pcp_bsm_complete in H; tauto. Qed.
imports: List Arith Lia Undecidability.Synthetic.Definitions Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs bsm_utils bsm_pcp) Undecidability.PCP(PCP PCP_facts)