PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
comp
choice
1
1
1
1
1
1
1
1
1.
E:
Prop
2.
x,y:
. Dec(x E y)
3.
r:
4.
x,y:
. (x r y)
(x E y)
5.
EquivRel x,y:
. x r y
n,k:
. (n r k)
Min{ x | xrn } = Min{ x | xrk }
By:
UnivCD
Generated subgoal:
1
6.
n:
7.
k:
(n r k)
Min{ x | xrn } = Min{ x | xrk }
About:
(n r k) 
Min{ x | xrn } = Min{ x | xrk }
Prop
x,y:. Dec(x E y)
x,y:. (x r y) (x E y). x r y n,k:. (n r k) Min{ x | xrn } = Min{ x | xrk } (n r k) Min{ x | xrn } = Min{ x | xrk }
