Nuprl - Pf surj_is_inj 1 2 1 1 1 2 1

PrintForm Definitions automata 5 Sections AutomataTheory Doc

1. n:
2. f: nn
3. 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)

By: Witness3 b

Generated subgoals:

1 3. a1: n
4. a2: n
5. f(a1) = f(a2)
6. a1 = a2
7. b: (n+1)
8. b = n (n+1)
b < n

2 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. f(a) = b n
a:n. if a2=a n else f(a) fi = b (n+1)

About:

1	3. `a1:` `n` 4. `a2:` `n` 5. `f(a1) = f(a2)` 6. `a1 = a2` 7. `b:` `(n+1)` 8. `b = n (n+1)` `b < n`
2	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. f(a) = b n` `a:n. if a2=a n else f(a) fi = b (n+1)`