At:
trivial-arrows
2
1
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||
8.
increasing(
x.x;L[i])
9.
s:
L[i] List
10.
||s|| = k
11.
x,y:
||s||. x < y 
s[x] < s[y]
increasing(
x.s[x];k)
By:
Analyze 0
THEN
Reduce 0
THEN
EasyHyp
Generated subgoals:
None
About: