PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
auto2
lemma
6
1
1
1
1
1
2
1
1
1
1
1
2
2
1.
n:
2.
0 < n
3.
T:
Type
4.
R:
T
Prop
5.
f:
n
T
6.
Bij(
n; T; f)
7.
t:T. Dec(R(t))
8.
(
t:{t:T|
t = f(n-1) }. R(t))
Dec(
t:T. R(t))
By:
Witness7 f(n-1)
Generated subgoal:
1
7.
(
t:{t:T|
t = f(n-1) }. R(t))
8.
Dec(R(f(n-1)))
Dec(
t:T. R(t))
About:
(
t:{t:T| t = f(n-1) }. R(t))
Dec(t:T. R(t))
Prop
nTn; T; f)
t:T. Dec(R(t))(t:{t:T| t = f(n-1) }. R(t)) Dec(t:T. R(t))(t:{t:T| t = f(n-1) }. R(t)) Dec(t:T. R(t))
