PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: list quo choice pls 1 1 1 2
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:(). (n,k:. (n (x,y. (g(x)) E (g(y))) k) h(n) = h(k)) & (n:. n (x,y. (g(x)) E (g(y))) (h(n)))

h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x)))
By:
Analyze 9
THEN
Witness g o h o f
Generated subgoal:

19. h:
10. (n,k:. (n (x,y. (g(x)) E (g(y))) k) h(n) = h(k)) & (n:. n (x,y. (g(x)) E (g(y))) (h(n)))
(x,y:q*. (x E y) (g o h o f)(x) = (g o h o f)(y)) & (x:q*. x E ((g o h o f)(x)))

About:
existsfunctionlistnatural_numberand
allequalapplyproplambda