PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
auto2
lemma
6
1
1
1
1
1
2
1
1
1
1
1
2
2
1
2
1
1
1
1
1
1
1
1
2
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.
R(f(n-1))
8.
t:
T
9.
R(t)
10.
a:
n
11.
f(a) = t
12.
a = n-1
n
13.
t = f(n-1)
False
By:
RWH (HypC 13) 11
Generated subgoal:
1
11.
f(a) = f(n-1)
12.
a = n-1
n
13.
t = f(n-1)
False
About:
a = n-1 
n
False
PropnTn; T; f)R(f(n-1))na = n-1 n Falsea = n-1 n False
