Nuprl - Pf fin_alph_list

PrintForm Definitions automata 5 Sections AutomataTheory Doc

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)

2 9. x: n*
10. y: n*
Dec(map(f;x) E map(f;y))

3 9. 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:

1	`EquivRel x,y:n*. map(f;x) E map(f;y)`
2	9. `x:` `n` 10. `y:` `n` `Dec(map(f;x) E map(f;y))`
3	9. `h:(nn). (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:(AlphAlph). (x,y:Alph. (x E y) h(x) = h(y)) & (x:Alph. x E (h(x)))`