proposition: Theorem pctm_bsm2_compiler : compiler_t (pctm_sss) (@bsm_sss 2) (fun t v => tape_eq_stacks t (v#>x) (v#>y)).
proof: Proof. apply generic_compiler with icomp ilen. + intros ? ? []; simpl icomp; rew length; auto. + apply pctm_sss_total'. + apply bsm_sss_fun. + intros lnk [ d | b | j p ] i1 v1 i2 v2 w1 H1 H2 H3; simpl icomp. * case_eq (mv d v1); intros (l,b) r E. exists (l##(b::r)##vec_nil); split. - assert (i2 = 1+i1) as -> by (inversion H1; auto). apply move_tape_spec with (1 := H3); simpl. rewrite E; split; auto. - simpl. inversion H1; subst; rewrite E; split; auto. * case_eq v1; intros (l,c) r E. exists (l##(b::r)##vec_nil); split. - assert (i2 = 1+i1) as -> by (inversion H1; auto). rewrite E in H3; destruct H3 as [ H3 H4 ]. apply ovwrite_head_spec with c r; auto. apply vec_pos_ext; intros z; repeat invert pos z;unfold x, y; rew vec. - inversion H1; subst; split; rew vec. * case_eq v1; intros (l,c) r E. rewrite E in H3; destruct H3 as [ H3 H4 ]. exists w1; split. - inversion H1; subst i2 v2. apply read_head_spec with (rd v1) r; auto. ++ subst; rewrite <- H4; auto. ++ destruct (rd v1); auto. - inversion H1; subst; split; auto. Qed.
imports: List Arith Lia Bool Undecidability.Synthetic(ReducibilityFacts) Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss compiler_correction) Undecidability.StackMachines.BSM(bsm_defs) Undecidability.TM(SBTM pctm_defs)