search

teorth / equational_theories

A project to map out the relations between different equational theories of Magmas.
Apache License 2.0
112 stars 29 forks source link

METATHEOREM: non-trivial implications preserve size #156

Open codyroux opened 5 hours ago

codyroux commented 5 hours ago

Formalize and prove the following meta-theorem:

Any implication of a set of equalities whose left and right hand orders are greater than n must either be of the form w = w or of the form w = w' with both sides being of order at least n.

codyroux commented 5 hours ago

claim