PrintForm Definitions choice 1 Sections AutomataTheory Doc

At: min el unique 1 1 1 1 1 1

1. E:
2. n:
3. k:
4. Refl(;x,y.x E y)
5. a,b:. (a E b) (b E a)
6. Trans x,y:. x E y
7. n E k
8. E(n) = E(k)

E(k,n) = E(k,k)

By: FwdThru 5 [7]

Generated subgoal:

19. k E n
E(k,n) = E(k,k)


About:
equalboolapplyfunctionassertallimplies