PrintForm
Definitions
action
sets
Sections
AutomataTheory
Doc
At:
counter
lpower
1
2
1
2
1.
e:
2.
L:
*
3.
n:
4.
0 < n
5.
||e:(L
n-1)|| = (n-1)
||e:L||
6.
n = 0
||e:(L
n-1) @ L|| = n
||e:L||
By:
RWH (LemmaC
Thm*
e:
, L,M:
*. ||e:L @ M|| = ||e:L||+||e:M||
) 0
Generated subgoals:
1
0
n
||e:L||
2
||e:(L
n-1)||+||e:L|| = n
||e:L||
About:
0
n
||e:L|| ||e:(L
n-1)||+||e:L|| = n||e:L|| 
*n-1)|| = (n-1)||e:L|| 
n = 0 ||e:(Ln-1) @ L|| = n||e:L|| 
e:, L,M:*. ||e:L @ M|| = ||e:L||+||e:M|| )
0 0n||e:L|| ||e:(Ln-1)||+||e:L|| = n||e:L|| 
