PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
phole
lemma
1
1.
n:
{1...}
2.
m:
{n+1...}
3.
f:
m
n
i,j:
m. i < j & f(i) = f(j)
By:
Inst
Thm*
n:{1...}, f:(
(n+1)
n).
i:
(n+1), j:
i. f(i) = f(j) [n;f]
Generated subgoal:
1
4.
i:
(n+1), j:
i. f(i) = f(j)
i,j:
m. i < j & f(i) = f(j)
About:
i:
(n+1), j:i. f(i) = f(j)
i,j:m. i < j & f(i) = f(j)m
n i,j:m. i < j & f(i) = f(j)
n:{1...}, f:((n+1)n). i:(n+1), j:i. f(i) = f(j)
[n;f]i:(n+1), j:i. f(i) = f(j) i,j:m. i < j & f(i) = f(j)
