Nuprl - Pf lang_power_functionality 1 1 1 2 1 1 1 2

PrintForm Definitions languages Sections AutomataTheory Doc

At: lang power functionality 1 1 1 2 1 1 1 2

1. Alph: Type
2. L: LangOver(Alph)
3. L': LangOver(Alph)
4. n':
5. L = L'
6. n:
7. 0 < n
8. (Ln-1) = (L'n-1)
9. l: Alph*
10. n = 0

((Ln-1)L)(l) ((L'n-1)L')(l)

By: RWH (HypC 8) 0

Generated subgoals:

1 ((Ln-1)L) Alph*Prop

2 ((L'n-1)L) Alph*Prop

3 ((L'n-1)L') Alph*Prop

4 ((L'n-1)L') Alph*Prop

5 ((L'n-1)L') = ((L'n-1)L') Alph*Prop

6 ((L'n-1)L)(l) ((L'n-1)L')(l)

About:

1	`((Ln-1)L) Alph*Prop`
2	`((L'n-1)L) Alph*Prop`
3	`((L'n-1)L') Alph*Prop`
4	`((L'n-1)L') Alph*Prop`
5	`((L'n-1)L') = ((L'n-1)L') Alph*Prop`
6	`((L'n-1)L)(l) ((L'n-1)L')(l)`