proposition: Lemma pop_exactly_spec1 (i : nat) l l' v : v #> x = l ++ l' -> v #> empty = nil -> (i, pop_exactly l i) // (i, v) ->> (2 * length l + i,v[l'/x]).
proof: Proof. Proof using neq. induction l as [ | [] l IH] in v, i, l' |- * ; cbn; intros H Hempty. - bsm sss stop. f_equal. rewrite <- H. now rewrite vec_change_same. - bsm sss POP one with x cdiff cdiff (l ++ l'). bsm sss POP empty with empty (i + 2) (i + 2). rewrite vec_change_neq; eauto. eapply subcode_sss_compute_trans. 2: eapply IH. 1:{ cbn. eexists (_ :: _ :: nil), nil. split. 2: cbn. 2: lia. cbn. rewrite app_nil_r. repeat f_equal. lia. } rewrite vec_change_eq. reflexivity. reflexivity. rewrite vec_change_neq; eauto. bsm sss stop. f_equal. lia. now rewrite vec_change_idem. - bsm sss POP zero with x (i + 2) cdiff (l ++ l'). eapply subcode_sss_compute_trans. 2: eapply IH. 1:{ cbn. eexists (_ :: _ :: nil), nil. split. 2: cbn. 2: lia. cbn. rewrite app_nil_r. repeat f_equal. lia. } rewrite vec_change_eq. reflexivity. reflexivity. rewrite vec_change_neq; eauto. bsm sss stop. f_equal. lia. now rewrite vec_change_idem. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)