PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: assert iff eq 1 1

1. a:
2. b:

(a b) a = b

By:
Analyze 0
THEN
Inst Thm* a,b:. (a b) a = b [a;b]


Generated subgoals:

None


About:
impliesassertequalbool