PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
min
ar
alt
2
2
1.
f:
2.
n:
3.
i:
(n+1)
4.
f(n-i) = f(n)
5.
j:
6.
0 < j
7.
j < n-i+1
8.
MinAr(f;j-1+i;n) = MinAr(f;j-1;n-i)+i
9.
f(n-(j+i)) = f(n)
MinAr(f;j+i-1;n) = MinAr(f;j;n-i)+i
By:
Assert (j-1+i = j+i-1)
THEN
RWH (HypC 10) 8
THEN
Thin 10
Generated subgoal:
1
8.
MinAr(f;j+i-1;n) = MinAr(f;j-1;n-i)+i
9.
f(n-(j+i)) = f(n)
MinAr(f;j+i-1;n) = MinAr(f;j;n-i)+i
About:
f(n-(j+i)) = f(n)
MinAr(f;j+i-1;n) = MinAr(f;j;n-i)+i
(n+1)
f(n-(j+i)) = f(n) MinAr(f;j+i-1;n) = MinAr(f;j;n-i)+if(n-(j+i)) = f(n) MinAr(f;j+i-1;n) = MinAr(f;j;n-i)+i
