PrintForm Definitions choice 1 Sections AutomataTheory Doc

At: min ar alt 1 1

1. f:
2. n:
3. i: (n+1)
4. f(n-i) = f(n)

MinAr(f;i;n) = MinAr(f;0;n-i)+i

By: RW (AddrC [2] (RecUnfoldC `min_ar`)) 0

Generated subgoal:

1 if (f(n-i))=(f(n)) i else MinAr(f;i-1;n) fi = MinAr(f;0;n-i)+i


About:
equalintaddnatural_numbersubtract
functionboolapplyifthenelse