Nuprl - Pf lang_prod_functionality

PrintForm Definitions languages Sections AutomataTheory Doc

Alph:Type, L,L',M,M':LangOver(Alph). L = L' M = M' (LM) = (L'M')

By: Unfold `languages` 0 THEN Unfold `lang_prod` 0 THEN Unfold `lang_eq` 0 THEN UnivCD THEN Reduce 0

Generated subgoal:

1 1. Alph: Type
2. L: Alph*Prop
3. L': Alph*Prop
4. M: Alph*Prop
5. M': Alph*Prop
6. l:Alph*. L(l) L'(l)
7. l:Alph*. M(l) M'(l)
8. l: Alph*
(i:{0...||l||}. L(l[0..i]) & M(l[i..||l||])) (i:{0...||l||}. L'(l[0..i]) & M'(l[i..||l||]))

About: