proposition: Theorem compare_stack_spec v : exists j w, (i,compare_stacks) // (i,v) ->> (j,w) /\ forall z, z <> x -> z <> y -> v#>z = w#>z /\ (v#>x = v#>y /\ j = p \/ v#>x <> v#>y /\ j = q).
proof: Proof. Proof using Hxy. destruct (list_bool_dec (v#>x) (v#>y)) as [ H | H ]. + destruct compare_stack_eq_spec with (1 := H) as (w & H1 & H2); exists p, w; auto. + destruct compare_stack_neq_spec with (1 := H) as (w & H1 & H2); exists q, w; auto. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)