PrintForm Definitions choice 1 Sections AutomataTheory Doc

At: min el unique 1 1 1 1 1 1 1 1 1 1
1. E:
2. n:
3. k:
4. a,b:. (a E b) (b E a)
5. Trans x,y:. x E y
6. n E k
7. E(n) = E(k)
8. k E n
9. (k E n) = true
10. k E k

E(k,n) = E(k,k)
By: FwdThru Thm* b:. b b = true [10]
Generated subgoal:

111. (k E k) = true
E(k,n) = E(k,k)

About:
equalboolapplyfunctionallimpliesassertbtrue