PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
min
el
unique
1
1.
E:
2.
n:
3.
k:
4.
EquivRel x,y:
. x E y
5.
n E k
Min{ x | xEn } = Min{ x | xEk }
By:
Unfold `min_el` 0
Generated subgoal:
1
MinArg(E(n) : {0..n
}) = MinArg(E(k) : {0..k
})
About:
MinArg(E(n) : {0..n
}) = MinArg(E(k) : {0..k}) 
. x E y Min{ x | xEn } = Min{ x | xEk } MinArg(E(n) : {0..n}) = MinArg(E(k) : {0..k}) 
