PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
min
el
iff
1
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:
BackThru
Thm*
E:(
), n,k:
. (EquivRel x,y:
. x E y)
(n E k)
Min{ x | xEn } = Min{ x | xEk }
Generated subgoals:
None
About:
. x E y
Min{ x | xEn } = Min{ x | xEk }
E:(), n,k:.
(EquivRel x,y:. x E y) 
(n E k) Min{ x | xEn } = Min{ x | xEk }