PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
auto2
list
ind
1
2
1.
Alph:
Type
2.
P:
Alph*
Prop
3.
n:
. (
l:Alph*. ||l|| < n
P(l))
(
l:Alph*. ||l|| = n
P(l))
4.
l:
Alph*
5.
n:
, l:Alph*. ||l|| < n
P(l)
P(l)
By:
Witness5 ||l||+1
Generated subgoals:
1
0
||l||+1
2
5.
l@0:Alph*. ||l@0|| < ||l||+1
P(l@0)
P(l)
About:
0
||l||+1
l@0:Alph*. ||l@0|| < ||l||+1 
P(l@0) P(l)
Propn:
. (l:Alph*. ||l|| < n P(l)) (l:Alph*. ||l|| = n P(l))n:, l:Alph*. ||l|| < n P(l) P(l) 0||l||+1l@0:Alph*. ||l@0|| < ||l||+1 P(l@0) P(l)
