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