Nuprl - Pf quotient_of_nsubn 2 1 2 1 1 2 1 1 2 1 1 1 1 3 1 1 2 4

PrintForm Definitions relation autom Sections AutomataTheory Doc

At: quotient of nsubn 2 1 2 1 1 2 1 1 2 1 1 1 1 3 1 1 2 4

1. n: {1+1...}
2. E:((n-1)(n-1)Prop). (EquivRel x,y:(n-1). x E y) & (x,y:(n-1). Dec(x E y)) (m:(n-1+1). m ~ (i,j:(n-1)//(i E j)))
3. E: nnProp
4. EquivRel x,y:n. x E y
5. x,y:n. Dec(x E y)
6. EquivRel x,y:(n-1). x E y
7. m: (n-1+1)
8. f: m(i,j:(n-1)//(i E j))
9. g: (i,j:(n-1)//(i E j))m
10. InvFuns(m; i,j:(n-1)//(i E j); f; g)
11. x:m. f(x) i,j:n//(i E j)
12. a:n. a E a
13. a,b:n. (a E b) (b E a)
14. a,b,c:n. (a E b) (b E c) (a E c)
15. x,y:i,j:n//(i E j). Dec(x = y)
16. Eb: (i,j:n//(i E j))(i,j:n//(i E j))
17. x,y:i,j:n//(i E j). (x Eb y) x = y
18. k: (n-1)
19. k E (n-1)
20. x1: n
21. x2: n
22. x1 E x2
23. n-1 i,j:n//(i E j)
24. (x1 Eb (n-1))
25. (x2 Eb (n-1))

g(x1) = g(x2)

By: Assert (x1 < n-1) THEN Assert (x2 < n-1) THEN Assert (x1 = x2)

Generated subgoals:

1 x1 < n-1

2 26. x1 < n-1
x2 < n-1

3 26. x1 < n-1
27. x2 < n-1
x1 = x2 i,j:(n-1)//(i E j)

4 26. x1 < n-1
27. x2 < n-1
28. x1 = x2 i,j:(n-1)//(i E j)
g(x1) = g(x2)

About:

1	`x1 < n-1`
2	26. `x1 < n-1` `x2 < n-1`
3	26. `x1 < n-1` 27. `x2 < n-1` `x1 = x2 i,j:(n-1)//(i E j)`
4	26. `x1 < n-1` 27. `x2 < n-1` 28. `x1 = x2 i,j:(n-1)//(i E j)` `g(x1) = g(x2)`