Nuprl - Pf lang_rel

PrintForm Definitions myhill nerode Sections AutomataTheory Doc

1. A: Type
2. L: LangOver(A)

a,b,c:A*. (z:A*. L(z @ a) L(z @ b)) (z:A*. L(z @ b) L(z @ c)) (z:A*. L(z @ a) L(z @ c))

By: Unfold `languages` 2

Generated subgoals:

1 2. L: A*Prop
3. a: A*
4. b: A*
5. c: A*
6. z:A*. L(z @ a) L(z @ b)
7. z:A*. L(z @ b) L(z @ c)
8. z: A*
9. L(z @ a)
L(z @ c)

2 2. L: A*Prop
3. a: A*
4. b: A*
5. c: A*
6. z:A*. L(z @ a) L(z @ b)
7. z:A*. L(z @ b) L(z @ c)
8. z: A*
9. L(z @ c)
L(z @ a)

About:

1	2. `L:` `AProp` 3. `a:` `A` 4. `b:` `A` 5. `c:` `A` 6. `z:A. L(z @ a) L(z @ b)` 7. `z:A. L(z @ b) L(z @ c)` 8. `z:` `A*` 9. `L(z @ a)` `L(z @ c)`
2	2. `L:` `AProp` 3. `a:` `A` 4. `b:` `A` 5. `c:` `A` 6. `z:A. L(z @ a) L(z @ b)` 7. `z:A. L(z @ b) L(z @ c)` 8. `z:` `A*` 9. `L(z @ c)` `L(z @ a)`