Fix #3563

[Drodt]

Related Issue

This pull request fixes #3563.

Intended Change

Add a new taclet equalityOfSingleton, which resolves singleton(o1, f1) = singleton(o2, f2) to o1 = o2 & f1 = f2.

Type of pull request

• There are changes to the taclet rule base

Ensuring quality

• I have tested the feature as follows: Proven the taclet sound.

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[Drodt]

This PR is the result of #3565 at the 2025 HacKeYthon.
Thanks to @frereit et al.

[mattulbrich]

If it is proven, the taclet should be marked as \lemma such that the correctness proof becomes part of the CI tests.

[Drodt]

So that's what lemma does! Interesting.

[Drodt]

The error is the same merge rule that fails on #3543 but it fails on ubuntu, not Windows.

[mattulbrich]

The error is the same merge rule that fails on #3543 but it fails on ubuntu, not Windows.

I assume that this is a "heisenbug". It might have to do with the order in which branches are traversed. It's my conjecture since the merge rules spans over several branches unlike most other rules.