PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: surj is inj 1 2 2 1 1 1 1 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)
9. b:(n+1). a:n. h(a) = b
10. f1: (n+1)n
11. b:(n+1). h(f1(b)) = b
12. n = 0

a1 = a2
By: Inst Thm* n:{1...}, f:((n+1)n). i:(n+1), j:i. f(i) = f(j) [n;f1]
Generated subgoal:

113. i:(n+1), j:i. f1(i) = f1(j)
a1 = a2

About:
equalnatural_numberallfunctionaddexistsapplyint