PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
min
arg
unique
f:(
), n,k:
. f(n) = f(k)
MinArg(f : {0..n
}) = MinArg(f : {0..k
})
By:
UnivCD
THEN
Unfold `min_arg` 0
Generated subgoal:
1
1.
f:
2.
n:
3.
k:
4.
f(n) = f(k)
n-MinAr(f;n;n) = k-MinAr(f;k;k)
About:
n-MinAr(f;n;n) = k-MinAr(f;k;k) 
f:(), n,k:. f(n) = f(k) 
MinArg(f : {0..n
}) = MinArg(f : {0..k}) n-MinAr(f;n;n) = k-MinAr(f;k;k) 
