(17steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
trivial-arrows
1
1
1
1.
k:
2.
L:
List
3.
n:
. k-1
n
(
G:({s:(
n List)| ||s|| = k
& (
x,y:
||s||. x < y
s[x] < s[y]) }
||L||).
c:
||L||, f:(
L[c]
n). increasing(f;L[c]) & (
s:
L[c] List. ||s|| = k
(
x,y:
||s||. x < y
s[x] < s[y])
G(map(f;s)) = c))
4.
s:
{s:(
(k-1) List)| ||s|| = k
& (
x,y:
||s||. x < y
s[x] < s[y]) }
||L||
By:
Analyze -1
THEN
Analyze -1
Generated subgoal:
1
4.
s:
(k-1) List
5.
||s|| = k
6.
x,y:
||s||. x < y
s[x] < s[y]
||L||
3
steps
About:
(17steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc