PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
auto2
lemma
6
1
1
1
1
1
2
1
1
1
1
1
1
1
2
2
1
1
1
1
1
1
1.
n:
2.
0 < n
3.
T:
Type
4.
R:
T
Prop
5.
f:
n
T
6.
Inj(
n; T; f)
7.
t:T. Dec(R(t))
8.
b:
T
9.
b = f(n-1)
10.
a:
n. f(a) = b
a:
(n-1). f(a) = b
{t:T|
t = f(n-1) }
By:
Analyze 10
Generated subgoal:
1
10.
a:
n
11.
f(a) = b
a:
(n-1). f(a) = b
{t:T|
t = f(n-1) }
About:
n
a:(n-1). f(a) = b 
{t:T| 
t = f(n-1) }
PropnTn; T; f)
t:T. Dec(R(t))b = f(n-1)a:n. f(a) = b a:(n-1). f(a) = b {t:T| t = f(n-1) }n a:(n-1). f(a) = b {t:T| t = f(n-1) }
