At: quotient of nsubn 2 1 2 1 1 2 1 1 2 1 1 2 2 3 3 1 2 2 1 2 1 1 1
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. g o f = Id
11. f o g = Id
12. x:m. f(x) 
i,j:n//(i E j)
13. a:n. a E a
14. a,b:n. (a E b) (b E a)
15. a,b,c:n. (a E b) (b E c) (a E c)
16. x,y:i,j:n//(i E j). Dec(x = y)
17. Eb: (i,j:n//(i E j))(i,j:n//(i E j))
18. x,y:i,j:n//(i E j). (x Eb y) 
x = y
19. 
(k:(n-1). k E (n-1))
20. n-1 i,j:n//(i E j)
21. f1: (m+1)(i,j:n//(i E j))
22. f1 = (
x.if x=
m
n-1 else f(x) fi)
23. g1: (i,j:n//(i E j))(m+1)
24. g1 = (x.if x Eb (n-1) m else g(x) fi)
25. x: i,j:n//(i E j)
26. x = n-1
27. x i,j:(n-1)//(i E j)
28. g(x) = m
29. z: (i,j:(n-1)//(i E j))(i,j:(n-1)//(i E j))
30. z(x) i,j:(n-1)//(i E j)
z(x) i,j:n//(i E j)
By: Inst
Thm* n:{1...}, m:n, E:(nnProp).
(EquivRel x,y:n. x E y) (z:x,y:m//(x E y). z x,y:n//(x E y))
[n;n-1;E;z(x)]
Generated subgoals:None
About:
