Nuprl - Pf mn

PrintForm Definitions myhill nerode Sections AutomataTheory Doc

n:{1...}, A:Type, L:LangOver(A), R:(A*A*Prop). Fin(A) (EquivRel x,y:A*. x R y) (n ~ (x,y:A*//(x R y))) (x,y,z:A*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:A*//(x R y))). l:A*. L(l) g(l)) (m:. m ~ (x,y:A*//(x L-induced Equiv y))) & (l:A*. Dec(L(l)))

By: Analyze 0 THEN Analyze 0 THEN Analyze 0 THEN Assert (L A*Prop)

Generated subgoals:

1 1. n: {1...}
2. A: Type
3. L: LangOver(A)
L A*Prop

2 1. n: {1...}
2. A: Type
3. L: LangOver(A)
4. L A*Prop
R:(A*A*Prop). Fin(A) (EquivRel x,y:A*. x R y) (n ~ (x,y:A*//(x R y))) (x,y,z:A*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:A*//(x R y))). l:A*. L(l) g(l)) (m:. m ~ (x,y:A*//(x L-induced Equiv y))) & (l:A*. Dec(L(l)))

About:

1	1. `n:` `{1...}` 2. `A:` `Type` 3. `L:` `LangOver(A)` `L A*Prop`
2	1. `n:` `{1...}` 2. `A:` `Type` 3. `L:` `LangOver(A)` 4. `L AProp` `R:(AAProp). Fin(A) (EquivRel x,y:A. x R y) (n ~ (x,y:A//(x R y))) (x,y,z:A. (x R y) ((z @ x) R (z @ y))) (g:((x,y:A//(x R y))). l:A. L(l) g(l)) (m:. m ~ (x,y:A//(x L-induced Equiv y))) & (l:A. Dec(L(l)))`