proposition: Fact PROG_spec (i : Fin.t (S (num_states M))) t : (j + c * !i, PROG i) // (j + c * !i, enc_tape t) -+> match δ (i, curr t) with None => (END, enc_tape t) | Some (q', w, m) => (j + c * !q' , enc_tape (mv m (wr w t))) end.
proof: Proof. set (off := j + c * !i). destruct t as [[ls [ [] | ]] rs] eqn:Eq_tape. - cbn [curr]. eapply sss_progress_compute_trans. exists 1. split. lia. econstructor. 2:econstructor. eapply subcode_sss_step with (P := (off, [POP CURR (26 + off) (51 + off)])). auto. eapply in_sss_step with (l := []). cbn; lia. econstructor 3. reflexivity. unfold PROG. destruct (δ (i, Some true)) as [ [[q' w] m] | ] eqn:Eq_nxt. + edestruct (@case_Some_false w) as [ [H H0] | [H H0]]. * rewrite H. bsm sss PUSH with CURR false. destruct m eqn:Eq_mv. -- eapply subcode_sss_compute_trans with (P := (2+off, MOVE_L (2 + off))). now apply sc_skipn, sc_firstn. cbn - [plus mult]. eapply (MOVE_L_spec (2 + off) (ls, Some Zero, rs)). bsm sss POP empty with ZERO (j + c * ! q') (j + c * ! q'). bsm sss stop. rewrite H0. reflexivity. -- eapply subcode_sss_compute_trans with (P := (2+off, MOVE_R (2 + off))). now apply sc_skipn, sc_firstn. cbn - [plus mult]. eapply (MOVE_R_spec (2 + off) (ls, Some Zero, rs)). bsm sss POP empty with ZERO (j + c * ! q') (j + c * ! q'). bsm sss stop. rewrite H0. reflexivity. -- bsm sss POP empty with ZERO (25 + off) (25 + off). bsm sss POP empty with ZERO (j + c * !q') (j + c * !q'). bsm sss stop. subst; reflexivity. * rewrite H. bsm sss PUSH with CURR true. destruct m eqn:Eq_mv. -- eapply subcode_sss_compute_trans with (P := (2+off, MOVE_L (2 + off))). now apply sc_skipn, sc_firstn. cbn - [plus mult]. eapply (MOVE_L_spec (2 + off) (ls, Some One, rs)). bsm sss POP empty with ZERO (j + c * ! q') (j + c * ! q'). bsm sss stop. destruct w as [ [] | ]; try reflexivity. easy. -- eapply subcode_sss_compute_trans with (P := (2+off, MOVE_R (2 + off))). now apply sc_skipn, sc_firstn. cbn - [plus mult]. eapply (MOVE_R_spec (2 + off) (ls, Some One, rs)). bsm sss POP empty with ZERO (j + c * ! q') (j + c * ! q'). bsm sss stop. destruct w as [ [] | ]; try reflexivity. easy. -- bsm sss POP empty with ZERO (25 + off) (25 + off). bsm sss POP empty with ZERO (j + c * !q') (j + c * !q'). bsm sss stop. destruct w as [ [] | ]; try reflexivity. easy. + bsm sss PUSH with CURR true. bsm sss POP empty with ZERO (25 + off) (25 + off). bsm sss POP empty with ZERO END END. bsm sss stop. - cbn [curr]. eapply sss_progress_compute_trans. exists 1. split. lia. econstructor. 2:econstructor. eapply subcode_sss_step with (P := (off, [POP CURR (26 + off) (51 + off)])). now apply sc_firstn. eapply in_sss_step with (l := []). cbn; lia. econstructor 2. reflexivity. unfold PROG. eapply subcode_sss_compute_trans; try eapply subcode1. 2:{ bsm sss stop. } destruct (δ (i, Some false)) as [ [[q' w] m] | ] eqn:Eq_nxt. + edestruct (@case_Some_true w) as [ [] | []]. * rewrite H. change (j + 76 * !i) with off. bsm sss PUSH with CURR true. destruct m eqn:Eq_mv. -- eapply subcode_sss_compute_trans with (P := (27+off, MOVE_L (27 + off))). now auto. eapply (MOVE_L_spec (27 + off) (ls, Some One, rs)). replace (23 + (27 + off)) with (24 + (26 + off)) by lia. bsm sss POP empty with ZERO (j + c * ! q') (j + c * ! q'). bsm sss stop. rewrite H0. reflexivity. -- eapply subcode_sss_compute_trans with (P := (27 +off, MOVE_R (27 + off))). now auto. eapply (MOVE_R_spec (27 + off) (ls, Some One, rs)). replace (23 + (27 + off)) with (24 + (26 + off)) by lia. bsm sss POP empty with ZERO (j + c * ! q') (j + c * ! q'). bsm sss stop. rewrite H0. reflexivity. -- bsm sss POP empty with ZERO (50 + off) (50 + off). replace (50 + off) with (24 + (26 + off)) by lia. bsm sss POP empty with ZERO (j + c * !q') (j + c * !q'). bsm sss stop. subst; reflexivity. * rewrite H. change (j + 76 * !i) with off. bsm sss PUSH with CURR false. destruct m eqn:Eq_mv. -- eapply subcode_sss_compute_trans with (P := (27+off, MOVE_L (27 + off))). replace (27 + off) with (1 + (26 + off)) at 1 by lia. eauto. eapply (MOVE_L_spec (27 + off) (ls, Some false, rs)). replace (23 + (27 + off)) with (24 + (26 + off)) by lia. bsm sss POP empty with ZERO (j + c * ! q') (j + c * ! q'). bsm sss stop. destruct w as [ [] | ]; try reflexivity. easy. -- eapply subcode_sss_compute_trans with (P := (27 +off, MOVE_R (27 + off))). replace (27 + off) with (1 + (26 + off)) at 1 by lia. now apply sc_skipn, sc_firstn. eapply (MOVE_R_spec (27 + off) (ls, Some false, rs)). replace (23 + (27 + off)) with (24 + (26 + off)) by lia. bsm sss POP empty with ZERO (j + c * ! q') (j + c * ! q'). bsm sss stop. destruct w as [ [] | ]; try reflexivity. easy. -- bsm sss POP empty with ZERO (50 + off) (50 + off). replace (50 + off) with (24 + (26 + off)) by lia. bsm sss POP empty with ZERO (j + c * !q') (j + c * !q'). bsm sss stop. destruct w as [ [] | ]; try reflexivity. easy. + change (j + 76 * !i) with off. bsm sss PUSH with CURR false. bsm sss POP empty with ZERO (50 + off) (50 + off). replace (50 + off) with (24 + (26 + off)) by lia. bsm sss POP empty with ZERO END END. bsm sss stop. - cbn [curr]. eapply sss_progress_compute_trans. exists 1. split. lia. econstructor. 2:econstructor. eapply subcode_sss_step with (P := (off, [POP CURR (26 + off) (51 + off)])). now apply sc_firstn. eapply in_sss_step with (l := []). cbn; lia. econstructor 1. reflexivity. unfold PROG. eapply subcode_sss_compute_trans; try eapply subcode2. 2:{ bsm sss stop. } destruct (δ (i, None)) as [ [[q' w] m] | ] eqn:Eq_nxt. + edestruct (@case_None w) as [ [] | []]. * rewrite H. change (j + 76 * !i) with off. bsm sss POP empty with ZERO (52 + off) (52 + off). destruct m eqn:Eq_mv. -- eapply subcode_sss_compute_trans with (P := (52+off, MOVE_L (52 + off))). now auto. eapply (MOVE_L_spec (52 + off) (ls, None, rs)). replace (23 + (52 + off)) with (24 + (51 + off)) by lia. bsm sss POP empty with ZERO (j + c * ! q') (j + c * ! q'). bsm sss stop. rewrite H0. reflexivity. -- eapply subcode_sss_compute_trans with (P := (52 +off, MOVE_R (52 + off))). now auto. eapply (MOVE_R_spec (52 + off) (ls, None, rs)). replace (23 + (52 + off)) with (24 + (51 + off)) by lia. bsm sss POP empty with ZERO (j + c * ! q') (j + c * ! q'). bsm sss stop. rewrite H0. reflexivity. -- replace (52 + off) with (1 + (51 + off)) by lia. bsm sss POP empty with ZERO (75 + off) (75 + off). replace (75 + off) with (24 + (51 + off)) by lia. bsm sss POP empty with ZERO (j + c * !q') (j + c * !q'). bsm sss stop. subst; reflexivity. * destruct w eqn:Eq_w. -- change (j + 76 * !i) with off. bsm sss PUSH with CURR b. destruct m eqn:Eq_mv. ++ eapply subcode_sss_compute_trans with (P := (52+off, MOVE_L (52 + off))). replace (52 + off) with (1 + (51 + off)) at 1 by lia. eauto. eapply (MOVE_L_spec (52 + off) (ls, Some b, rs)). replace (23 + (52 + off)) with (24 + (51 + off)) by lia. bsm sss POP empty with ZERO (j + c * ! q') (j + c * ! q'). bsm sss stop. ++ eapply subcode_sss_compute_trans with (P := (52 +off, MOVE_R (52 + off))). replace (52 + off) with (1 + (51 + off)) at 1 by lia. now apply sc_skipn, sc_firstn. eapply (MOVE_R_spec (52 + off) (ls, Some b, rs)). replace (23 + (52 + off)) with (24 + (51 + off)) by lia. bsm sss POP empty with ZERO (j + c * !q') (j + c * ! q'). bsm sss stop. ++ bsm sss POP empty with ZERO (75 + off) (75 + off). replace (75 + off) with (24 + (51 + off)) by lia. bsm sss POP empty with ZERO (j + c * !q') (j + c * !q'). bsm sss stop. -- change (j + 76 * !i) with off. bsm sss POP empty with ZERO (52 + off) (52 + off). destruct m eqn:Eq_mv. ++ eapply subcode_sss_compute_trans with (P := (52+off, MOVE_L (52 + off))). replace (52 + off) with (1 + (51 + off)) at 1 by lia. eauto. eapply (MOVE_L_spec (52 + off) (ls, None, rs)). replace (23 + (52 + off)) with (24 + (51 + off) ) by lia. bsm sss POP empty with ZERO (j + c * !q') (j + c * ! q'). bsm sss stop. ++ eapply subcode_sss_compute_trans with (P := (52 +off, MOVE_R (52 + off))). replace (52 + off) with (1 + (51 + off)) at 1 by lia. easy. eapply (MOVE_R_spec (52 + off) (ls, None, rs)). replace (23 + (52 + off)) with (24 + (51 + off)) by lia. bsm sss POP empty with ZERO (j + c * !q') (j + c * ! q'). bsm sss stop. ++ replace (52 + off) with (1 + (51 + off)) by lia. bsm sss POP empty with ZERO (75 + off) (75 + off). replace (75 + off) with (24 + (51 + off)) by lia. bsm sss POP empty with ZERO (j + c * !q') (j + c * !q'). bsm sss stop. + change (j + 76 * !i) with off. bsm sss POP empty with ZERO END END. bsm sss stop. Qed.
imports: Undecidability.TM.KOSBTM.KOSBTM Undecidability.Shared.Libs.PSL.Vectors.FinNotation Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.Shared.Libs.PSL.EqDec List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(bsm_defs)