Nuprl - Pf list_quo_choice

PrintForm Definitions automata 5 Sections AutomataTheory Doc

1. q:
2. E: q*q*Prop
3. EquivRel x,y:q*. x E y
4. x,y:q*. Dec(x E y)
5. f: q*
6. g: q*
7. g o f = Id
8. f o g = Id

(EquivRel x,y:. x (x,y. (g(x)) E (g(y))) y) & (x,y:. Dec(x (x,y. (g(x)) E (g(y))) y))

By: Unfold `equiv_rel` 0 THEN Reduce 0 THEN Unfold `refl` 0 THEN Unfold `sym` 0 THEN Unfold `trans` 0 THEN Analyze 3 THEN Analyze 4 THEN Unfold `refl` 3 THEN Unfold `sym` 4 THEN Unfold `trans` 5

Generated subgoals:

1 3. a:q*. a E a
4. a,b:q*. (a E b) (b E a)
5. a,b,c:q*. (a E b) (b E c) (a E c)
6. x,y:q*. Dec(x E y)
7. f: q*
8. g: q*
9. g o f = Id
10. f o g = Id
11. a:
(g(a)) E (g(a))

2 3. a:q*. a E a
4. a,b:q*. (a E b) (b E a)
5. a,b,c:q*. (a E b) (b E c) (a E c)
6. x,y:q*. Dec(x E y)
7. f: q*
8. g: q*
9. g o f = Id
10. f o g = Id
11. a:
12. b:
13. (g(a)) E (g(b))
(g(b)) E (g(a))

3 3. a:q*. a E a
4. a,b:q*. (a E b) (b E a)
5. a,b,c:q*. (a E b) (b E c) (a E c)
6. x,y:q*. Dec(x E y)
7. f: q*
8. g: q*
9. g o f = Id
10. f o g = Id
11. a:
12. b:
13. c:
14. (g(a)) E (g(b))
15. (g(b)) E (g(c))
(g(a)) E (g(c))

About:

1	3. `a:q. a E a` 4. `a,b:q. (a E b) (b E a)` 5. `a,b,c:q. (a E b) (b E c) (a E c)` 6. `x,y:q. Dec(x E y)` 7. `f:` `q` 8. `g:` `q` 9. `g o f = Id` 10. `f o g = Id` 11. `a:` `(g(a)) E (g(a))`
2	3. `a:q. a E a` 4. `a,b:q. (a E b) (b E a)` 5. `a,b,c:q. (a E b) (b E c) (a E c)` 6. `x,y:q. Dec(x E y)` 7. `f:` `q` 8. `g:` `q` 9. `g o f = Id` 10. `f o g = Id` 11. `a:` 12. `b:` 13. `(g(a)) E (g(b))` `(g(b)) E (g(a))`
3	3. `a:q. a E a` 4. `a,b:q. (a E b) (b E a)` 5. `a,b,c:q. (a E b) (b E c) (a E c)` 6. `x,y:q. Dec(x E y)` 7. `f:` `q` 8. `g:` `q` 9. `g o f = Id` 10. `f o g = Id` 11. `a:` 12. `b:` 13. `c:` 14. `(g(a)) E (g(b))` 15. `(g(b)) E (g(c))` `(g(a)) E (g(c))`