(17steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
trivial-arrows
2
1
1
1.
k:
2.
L:
List
3.
i:
||L||
4.
L[i] < k
5.
n:
6.
k-1
n
7.
G:
{s:(
n List)| ||s|| = k
& (
x,y:
||s||. x < y
s[x] < s[y]) }
||L||
increasing(
x.x;L[i])
By:
BackThru
Thm*
k:
. increasing(
i.i;k)
Generated subgoals:
None
About:
(17steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
List
||L||
n
n List)| ||s|| = k 
& (
x,y:||s||. x < y 
s[x] < s[y]) }
||L||
increasing(
x.x;L[i])
k:. increasing(i.i;k)
