PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
auto2
list
ind
1
1
1
2
1
1
2
1.
Alph:
Type
2.
P:
Alph*
Prop
3.
n:
4.
0 < n
5.
l:Alph*. ||l|| < n-1
P(l)
6.
(
l:Alph*. ||l|| < n-1
P(l))
(
l:Alph*. ||l|| = n-1
P(l))
7.
l:
Alph*
8.
||l|| < n
9.
||l|| < n-1
P(l)
By:
Assert (||l|| = n-1)
Generated subgoals:
1
||l|| = n-1
2
10.
||l|| = n-1
P(l)
About:
||l|| = n-1 P(l)
Prop
l:Alph*. ||l|| < n-1 
P(l)l:Alph*. ||l|| < n-1 P(l)) (l:Alph*. ||l|| = n-1 P(l))
||l|| < n-1 P(l) ||l|| = n-1 P(l)
