Nuprl - Pf lang_rel

PrintForm Definitions myhill nerode Sections AutomataTheory Doc

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

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

By: Unfold `languages` 2

Generated subgoals:

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

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

About:

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