PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
min
arg
sound
1
f:(
), n:
. f(n-MinAr(f;n;n)) = f(n)
By:
RWH (LemmaC
Thm*
f:(
), n:
, i:
(n+1). f(n-MinAr(f;i;n)) = f(n)) 0
Generated subgoals:
None
About:
f:(
), n:. f(n-MinAr(f;n;n)) = f(n)f:(), n:, i:(n+1). f(n-MinAr(f;i;n)) = f(n))
0