NUM_RING : term -> thm
# NUM_RING `(x + y) EXP 2 = x EXP 2 ==> y = 0 \/ y + 2 * x = 0`;; 1 basis elements and 0 critical pairs Translating certificate to HOL inferences val it : thm = |- (x + y) EXP 2 = x EXP 2 ==> y = 0 \/ y + 2 * x = 0
# NUM_RING `(x + y) EXP 2 = x EXP 2 ==> y = 0 \/ x = 0`;; 2 basis elements and 1 critical pairs 3 basis elements and 2 critical pairs 3 basis elements and 1 critical pairs 4 basis elements and 1 critical pairs 4 basis elements and 0 critical pairs Exception: Failure "find".