PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
rect
enumer
1
3
1
1
1
1.
n:
2.
m:
a1,a2:(
n
m). (
z.1of(z)
m+2of(z))(a1) = (
z.1of(z)
m+2of(z))(a2)
(n
m)
a1 = a2
By:
Reduce 0
THEN
Analyze 0
THEN
Analyze 0
Generated subgoal:
1
3.
a1:
n
m
4.
a2:
n
m
1of(a1)
m+2of(a1) = 1of(a2)
m+2of(a2)
(n
m)
a1 = a2
About:
n
mnm
1of(a1)
m+2of(a1) = 1of(a2)m+2of(a2) 
(nm) 
a1 = a2
a1,a2:(nm). (
z.1of(z)m+2of(z))(a1) = (z.1of(z)m+2of(z))(a2) (nm) a1 = a2nmnm 1of(a1)m+2of(a1) = 1of(a2)m+2of(a2) (nm) a1 = a2
