PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
min
el
iff
2
1
1
1
1
1
1.
E:
2.
n:
3.
k:
4.
Refl(
;x,y.x E y)
5.
a,b:
. (a E b)
(b E a)
6.
Trans x,y:
. x E y
7.
Min{ x | xEn } = Min{ x | xEk }
8.
n E Min{ x | xEk }
9.
k E Min{ x | xEk }
n E k
By:
FwdThru 5 [9]
Generated subgoal:
1
10.
Min{ x | xEk } E k
n E k
About:
n E k
a,b:
(b E a)
