proposition: Lemma pop_many_spec (k : nat) (i : nat) v : (i, pop_many k i) // (i, v) ->> (k + i,v[(skipn k (v#>x))/x]).
proof: Proof. induction k in v, i |- *; cbn. - bsm sss stop. f_equal. now rewrite vec_change_same. - destruct (v #> x) as [ | [] l] eqn:E. + bsm sss POP empty with x (i + 1) (S (k + i)). bsm sss stop. rewrite <- E. f_equal. now rewrite vec_change_same. + bsm sss POP one with x (i + 1) (S (k + i)) l. eapply subcode_sss_compute_trans. 2: eapply IHk. 1:{ cbn. eexists (_ :: nil), nil. split. 2: cbn. 2: lia. cbn. rewrite app_nil_r. reflexivity. } bsm sss stop. f_equal. lia. rewrite vec_change_idem. now rewrite vec_change_eq. + bsm sss POP zero with x (i + 1) (S (k + i)) l. eapply subcode_sss_compute_trans. 2: eapply IHk. 1:{ cbn. eexists (_ :: nil), nil. split. 2: cbn. 2: lia. cbn. rewrite app_nil_r. repeat f_equal. lia. } bsm sss stop. f_equal. lia. rewrite vec_change_idem. now rewrite vec_change_eq. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)