Nuprl - Pf min_arg

PrintForm Definitions choice 1 Sections AutomataTheory Doc

f:(), n,k:. f(n) = f(k) MinArg(f : {0..n}) = MinArg(f : {0..k})

By: UnivCD THEN Analyze 0 THEN Analyze 0

Generated subgoals:

1 1. f:
2. n:
3. k:
4. f(n) = f(k)
MinArg(f : {0..n}) = MinArg(f : {0..k})

2 1. f:
2. n:
3. k:
4. MinArg(f : {0..n}) = MinArg(f : {0..k})
f(n) = f(k)

About:

1	1. `f:` 2. `n:` 3. `k:` 4. `f(n) = f(k)` `MinArg(f : {0..n}) = MinArg(f : {0..k})`
2	1. `f:` 2. `n:` 3. `k:` 4. `MinArg(f : {0..n}) = MinArg(f : {0..k})` `f(n) = f(k)`