PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
min
arg
unique
1
2
1.
f:
2.
n:
3.
k:
4.
f(n) = f(k)
5.
k < n
n-MinAr(f;n;n) = k-MinAr(f;k;k)
By:
Inst
Thm*
f:(
), n:
, i:
(n+1), j:
(n-i+1). f(n-i) = f(n)
MinAr(f;j+i;n) = MinAr(f;j;n-i)+i [f;k;k-n;n]
Generated subgoal:
1
f(k-(k-n)) = f(k)
About:
f(k-(k-n)) = f(k)
k < n n-MinAr(f;n;n) = k-MinAr(f;k;k) 
f:(), n:, i:(n+1), j:(n-i+1).
f(n-i) = f(n) 
MinAr(f;j+i;n) = MinAr(f;j;n-i)+i
[f;k;k-n;n] f(k-(k-n)) = f(k)
