PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
auto2
lemma
6
1
1
1
1
1
2
1
1
1
1
1
1
1
1
1
2
1
1
1
1
1
1.
n:
2.
0 < n
3.
T:
Type
4.
R:
T
Prop
5.
f:
n
T
6.
Surj(
n; T; f)
7.
t:T. Dec(R(t))
8.
x:
(n-1)
9.
f(x) = f(n-1)
10.
a2:
n. f(x) = f(a2)
x = a2
n
False
By:
Witness10 n-1
Generated subgoal:
1
10.
f(x) = f(n-1)
x = n-1
n
False
About:
x = n-1 
n
False
PropnTn; T; f)
t:T. Dec(R(t))(n-1)a2:n. f(x) = f(a2) x = a2 n False x = n-1 n False
