proposition: Fact to_default_spec v w : w = v[(default_stack (v#>y))/y] -> (i,to_default) // (i,v) ->> (j,w).
proof: Proof. intros ->; unfold to_default. case_eq (v#>y); [ intros H | intros [] l H ]. + bsm sss POP empty with y (4+i) (4+i). bsm sss PUSH with y Zero. rewrite H. apply subcode_sss_compute_trans with (P := (5+i,jump j')) (st2 := (j,v[(Zero::nil)/y])); auto. bsm sss stop. + bsm sss POP one with y (4+i) (4+i) l. bsm sss PUSH with y One. rew vec; simpl default_stack. apply subcode_sss_compute_trans with (P := (2+i,jump j)) (st2 := (j,v[(One::l)/y])); auto. bsm sss stop. + bsm sss POP zero with y (4+i) (4+i) l. bsm sss PUSH with y Zero. rew vec; simpl default_stack. apply subcode_sss_compute_trans with (P := (5+i,jump j')) (st2 := (j,v[(Zero::l)/y])); auto. bsm sss stop. 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)