PrintForm Definitions choice 1 Sections AutomataTheory Doc

At: min el iff 2 1 1
1. E:
2. n:
3. k:
4. EquivRel x,y:. x E y
5. Min{ x | xEn } = Min{ x | xEk }
6. n E Min{ x | xEn }
7. k E Min{ x | xEk }

n E k
By:
Analyze 4
THEN
Analyze 5
Generated subgoal:

14. Refl(;x,y.x E y)
5. Sym x,y:. x E y
6. Trans x,y:. x E y
7. Min{ x | xEn } = Min{ x | xEk }
8. n E Min{ x | xEn }
9. k E Min{ x | xEk }
n E k

About:
assertfunctionboolequal