PrintForm Definitions choice 1 Sections AutomataTheory Doc

At: comp choice 1 1 1 1 1 1 1 2
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:. n r Min{ x | xrn }
By:
Analyze 0
THEN
BackThru Thm* E:(), n:. (EquivRel x,y:. x E y) (n E Min{ x | xEn })
Generated subgoals:

None

About:
allassertfunctionpropbool