PrintForm Definitions automata 5 Sections AutomataTheory Doc

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

h:(Alph*Alph*). (x,y:Alph*. (x E y) h(x) = h(y) Alph*) & (x:Alph*. x E (h(x)))
By:
Witness l.map(f;h(map(g;l)))
THEN
Reduce 0
Generated subgoal:

1 (x,y:Alph*. (x E y) map(f;h(map(g;x))) = map(f;h(map(g;y)))) & (x:Alph*. x E map(f;h(map(g;x))))

About:
existsfunctionlistandallequal
applylambdauniversepropnatural_number