PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
phole
aux
2
2
1.
n:
{1+1...}
2.
f:(
(n-1+1)
(n-1)).
i:
(n-1+1), j:
i. f(i) = f(j)
3.
f:
(n+1)
n
4.
iii:
(n+1). (
ii:{(iii+1)..(n+1)
}, jj:
ii.
f(ii) = f(jj))
(
i:
(iii+1), j:
i. f(i) = f(j))
i:
(n+1), j:
i. f(i) = f(j)
By:
Inst [n] 4
Generated subgoals:
None
About:
f:(
(n-1+1)
(n-1)). 
i:(n-1+1), j:i. f(i) = f(j)(n+1)niii:(n+1). (ii:{(iii+1)..(n+1)
}, jj:ii. 
f(ii) = f(jj)) 
(i:(iii+1), j:i. f(i) = f(j))
i:(n+1), j:i. f(i) = f(j)
