PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
min
arg
iff
2
1
1.
f:
2.
n:
3.
k:
4.
MinArg(f : {0..n
}) = MinArg(f : {0..k
})
5.
f(MinArg(f : {0..n
})) = f(MinArg(f : {0..k
}))
f(n) = f(k)
By:
RWH (LemmaC
Thm*
f:(
), n:
. f(MinArg(f : {0..n
})) = f(n)) 5
Generated subgoals:
None
About:
}) = MinArg(f : {0..k}) 
})) = f(MinArg(f : {0..k}))
f(n) = f(k)
f:(), n:. f(MinArg(f : {0..n})) = f(n))
5