PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: surj is inj 1 2 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. b: (n+1)
9. b = n (n+1)

a:n. if a2=a n else f(a) fi = b (n+1)
By: Unfold `surject` 3
Generated subgoal:

13. b:n. a:n. f(a) = b
4. a1: n
5. a2: n
6. f(a1) = f(a2)
7. a1 = a2
8. b: (n+1)
9. b = n (n+1)
a:n. if a2=a n else f(a) fi = b (n+1)

About:
existsnatural_numberequaladdifthenelseapplyfunction