PrintForm Definitions choice 1 Sections AutomataTheory Doc

At: comp choice 1 1 1 1 1
1. E: Prop
2. EquivRel x,y:. x E y
3. x,y:. Dec(x E y)
4. r:
5. x,y:. (x r y) (x E y)

(n,k:. (n r k) Min{ x | xrn } = Min{ x | xrk }) & (n:. n r Min{ x | xrn })
By: RWH (RevHypC 5) 2
Generated subgoal:

12. 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 }) & (n:. n r Min{ x | xrn })

About:
andallassertequalfunctionpropbool