PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: fin alph list quo 1 1 1 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)

h:(Alph*Alph*). (x,y:Alph*. (x E y) h(x) = h(y)) & (x:Alph*. x E (h(x)))

By:
Inst Thm* q:, E:(q*q*Prop). (EquivRel x,y:q*. x E y) & (x,y:q*. Dec(x E y)) (h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x)))) [n;x,y. map(f;x) E map(f;y)]
THEN
Reduce 0


Generated subgoals:

1 EquivRel x,y:n*. map(f;x) E map(f;y)
29. x: n*
10. y: n*
Dec(map(f;x) E map(f;y))
39. h:(n*n*). (x,y:n*. (x (x,y. map(f;x) E map(f;y)) y) h(x) = h(y)) & (x:n*. x (x,y. map(f;x) E map(f;y)) (h(x)))
h:(Alph*Alph*). (x,y:Alph*. (x E y) h(x) = h(y)) & (x:Alph*. x E (h(x)))


About:
existsfunctionlistandallequal
applylambdauniversepropnatural_number