Does `witness` apply for removing duplicates

Stream: Equational

[Eric Taucher]

For

A script for generating them may be found here.

specifically lines 70 to 73

https://github.com/teorth/equational_theories/blob/main/scripts/generate_eqs_list.py#L70-L73

is used to remove duplicate expressions. Was hoping for a comment with mathematical meaning.

In Prolog there is the predicate distinct/1 which notes

True if Goal is true and no previous solution of Goal bound Witness to the same value.

Since the word witness helps in finding other related information that does not always appear when witness is not used, wondering if witness is applicable? My answer is yes, just want to verify.

[Eric Taucher]

Never mind.

A search in this topic for witness creates a substantial list, so obviously it applies.

[Amir Livne Bar-on]

These lines guarantee that each equation is emitted only once, by looking up all the variations in the set of previous outputs.

The exact definition of variation is: (1) flipping the two sides of the equation (2) renaming variables

[Eric Taucher]

@Amir Livne Bar-on

Thanks. I do agree your definition gives the understanding a mathematical basis.