PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: surj is inj 1 2 2

1. n:
2. f: nn
3. Surj(n; n; f)
4. a1: n
5. a2: n
6. f(a1) = f(a2)
7. a1 = a2
8. h:(n(n+1)). Surj(n; (n+1); h)

a1 = a2

By: Analyze 8

Generated subgoal:

18. h: n(n+1)
9. Surj(n; (n+1); h)
a1 = a2


About:
equalnatural_numberfunctionapplyexistsadd