PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: surj is inj 1 2 1 1 1 2 1 2 1 1 1 2

1. n:
2. f: nn
3. a1: n
4. a2: n
5. f(a1) = f(a2)
6. a1 = a2
7. b: (n+1)
8. b = n (n+1)
9. a: n
10. f(a) = b n
11. a = a2
12. a2 = a1

f(a1) = b (n+1)

By: RWH (HypC 11) 10

Generated subgoals:

None


About:
equalnatural_numberaddapplyfunctionint