PrintForm Definitions automata 5 Sections AutomataTheory Doc

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

EquivRel x,y:n*. map(f;x) E map(f;y)
By:
Unfold `equiv_rel` 0
THEN
Unfold `refl` 0
THEN
Unfold `trans` 0
THEN
Unfold `sym` 0
THEN
Unfold `equiv_rel` 7
THEN
Unfold `refl` 7
THEN
Unfold `trans` 7
THEN
Unfold `sym` 7
Generated subgoals:

17. a:Alph*. a E a
8. a,b:Alph*. (a E b) (b E a)
9. a,b,c:Alph*. (a E b) (b E c) (a E c)
10. x,y:Alph*. Dec(x E y)
11. a: n*
map(f;a) E map(f;a)
27. a:Alph*. a E a
8. a,b:Alph*. (a E b) (b E a)
9. a,b,c:Alph*. (a E b) (b E c) (a E c)
10. x,y:Alph*. Dec(x E y)
11. a: n*
12. b: n*
13. map(f;a) E map(f;b)
map(f;b) E map(f;a)
37. a:Alph*. a E a
8. a,b:Alph*. (a E b) (b E a)
9. a,b,c:Alph*. (a E b) (b E c) (a E c)
10. x,y:Alph*. Dec(x E y)
11. a: n*
12. b: n*
13. c: n*
14. map(f;a) E map(f;b)
15. map(f;b) E map(f;c)
map(f;a) E map(f;c)

About:
listnatural_numberuniversefunctionpropall