proposition: Fact empty_stack_spec v : (i,empty_stack) // (i,v) ->> (3+i,v[nil/x]).
proof: Proof. set (l := v#>x). generalize (eq_refl l). unfold l at 2. generalize l v; clear l v. unfold empty_stack. induction l as [ | [] l IHl ]; intros v Hv. bsm sss POP empty with x i (3+i). bsm sss stop; f_equal. apply vec_pos_ext; intros p; dest x p. bsm sss POP one with x i (3+i) l. bsm sss PUSH with x Zero. bsm sss POP zero with x i i l; rew vec. clear Hv. specialize (IHl (v[l/x])). spec in IHl. rew vec. revert IHl; rew vec. bsm sss POP zero with x i (3+i) l. clear Hv. specialize (IHl (v[l/x])). spec in IHl. rew vec. revert IHl; 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)