PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
min
el
unique
1
1
1
1
1.
E:
2.
n:
3.
k:
4.
EquivRel x,y:
. x E y
5.
n E k
6.
E(n) = E(k)
MinArg(E(k) : {0..n
}) = MinArg(E(k) : {0..k
})
By:
BackThru
Thm*
f:(
), n,k:
. f(n) = f(k)
MinArg(f : {0..n
}) = MinArg(f : {0..k
})
Generated subgoal:
1
E(k,n) = E(k,k)
About:
E(k,n) = E(k,k)
. x E y MinArg(E(k) : {0..n
}) = MinArg(E(k) : {0..k}) 
f:(), n,k:.
f(n) = f(k) 
MinArg(f : {0..n}) = MinArg(f : {0..k}) E(k,n) = E(k,k)
