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