PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
phole
aux
2
1
1
1
2
1
2
1.
n:
{2...}
2.
f:(
n
(-1+n)).
i:
n, j:
i. f(i) = f(j)
3.
f:
(1+n)
n
4.
ii:{1..(1+n)
}, jj:
ii.
f(ii) = f(jj)
5.
i:
n
6.
j:
i
7.
f(i) = n-1
8.
f(j) = n-1
f(n) = f(j)
(-1+n)
(
i:
1, j:
i. f(i) = f(j))
By:
Inst [n;j] 4
Generated subgoal:
1
9.
f(n) = f(j)
f(n)
(-1+n)
About:
f(n) = f(j)
f(n) 
(-1+n)
f:(n
(-1+n)). 
i:n, j:i. f(i) = f(j)(1+n)nii:{1..(1+n)
}, jj:ii. f(ii) = f(jj)nif(j) = n-1 f(n) = f(j) (-1+n) 
(i:1, j:i. f(i) = f(j))f(n) = f(j) f(n) (-1+n)
