What's the algorithm used by mmj2 to represent $d pairs as $d sets ? For instance, for a given theorem, with yamma I'm producing
$d ph x $. $d k x $. $d k ph $. $d j x $. $d j k $. $d F x $. $d F k $. $d A x $. $d A k $. $d A j $. whereas mmj2 produces $d A j k x $. $d F k x $. $d k ph x $. (from 'visual' inspection, they actually represent the same relation) I've googled for 'compact representation of symmetric relations' and stuff like that, but no luck, so far. Can anybody point me in the right direction. Thanks in advance Glauco -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8c0d4863-cda4-4086-bc03-50c0a6eb106an%40googlegroups.com.
