PrintForm Definitions choice 1 Sections AutomataTheory Doc

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

n E k
By:
Inst Thm* E:(), n:. (EquivRel x,y:. x E y) (n E Min{ x | xEn }) [E;n]
THEN
Inst Thm* E:(), n:. (EquivRel x,y:. x E y) (n E Min{ x | xEn }) [E;k]
Generated subgoal:

16. n E Min{ x | xEn }
7. k E Min{ x | xEk }
n E k

About:
assertfunctionboolequal