Nuprl - Pf quotient_of_nsubn 2 1 2 1 1 2 1

PrintForm Definitions relation autom Sections AutomataTheory Doc

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. Refl(n;x,y.x E y)
13. Sym x,y:n. x E y
14. Trans x,y:n. x E y

m:(n+1). m ~ (i,j:n//(i E j))

By: Unfold `refl` 12 THEN Unfold `sym` 13 THEN Unfold `trans` 14 THEN Unfold `one_one_corr` 0

Generated subgoal:

1 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)
m:(n+1), f:(m(i,j:n//(i E j))), g:((i,j:n//(i E j))m). InvFuns(m; i,j:n//(i E j); f; g)

About: