PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: fin alph list quo 1 1 1 1 1 3 1 1 1 1 1 1 1 1 1 1 1
1. Alph: Type
2. E: Alph*Alph*Prop
3. n:
4. f: nAlph
5. g: Alphn
6. g o f = Id
7. f o g = Id
8. EquivRel x,y:Alph*. x E y
9. x,y:Alph*. Dec(x E y)
10. h: n*n*
11. x,y:n*. (map(f;x) E map(f;y)) h(x) = h(y)
12. x:n*. map(f;x) E map(f;h(x))
13. x: Alph*
14. y: Alph*
15. (x E y) h(map(g;x)) = h(map(g;y))

h(map(g;x)) = h(map(g;y)) map(f;h(map(g;x))) = map(f;h(map(g;y)))
By:
Analyze 0
THEN
Analyze 0
Generated subgoals:

116. h(map(g;x)) = h(map(g;y))
map(f;h(map(g;x))) = map(f;h(map(g;y)))
216. map(f;h(map(g;x))) = map(f;h(map(g;y)))
h(map(g;x)) = h(map(g;y))

About:
equallistnatural_numberapplyuniversefunctionpropall