PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
fin
is
decid
1
1
1
1
1
1
1
1
1
1
1.
T:
Type
2.
n:
3.
f:
n
T
4.
a1,a2:
n. f(a1) = f(a2)
a1 = a2
5.
x:
T
6.
y:
T
7.
a:
n
8.
f(a) = x
9.
a1:
n
10.
f(a1) = y
Dec(x = y)
By:
Decide (a = a1)
Generated subgoals:
1
11.
a = a1
Dec(x = y)
2
11.
a = a1
Dec(x = y)
About:
Dec(x = y)
a = a1 Dec(x = y)
n
T
a1,a2:n. f(a1) = f(a2) 
a1 = a2nn Dec(x = y) Dec(x = y)a = a1 Dec(x = y)
