Nuprl - Pf list_quo_choice_pls 1 1 1 2 1 1 1 1 1 1 1 1

PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: list quo choice pls 1 1 1 2 1 1 1 1 1 1 1 1

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
9. h:
10. n,k:. ((g(n)) E (g(k))) h(n) = h(k)
11. n:. (g(n)) E (g(h(n)))
12. x: q*
13. y: q*
14. (x E y) h(f(x)) = h(f(y))

(x E y) (g o h o f)(x) = (g o h o f)(y)

By: Analyze 0 THEN Analyze 0

Generated subgoals:

1 15. x E y
(g o h o f)(x) = (g o h o f)(y)

2 15. (g o h o f)(x) = (g o h o f)(y)
x E y

About:

1	15. `x E y` `(g o h o f)(x) = (g o h o f)(y)`
2	15. `(g o h o f)(x) = (g o h o f)(y)` `x E y`