Definitions
array
1
Doc
At:
array
seg
wf
1
1
1.
T:
Type
2.
i:
3.
j:
{i...}
4.
a:
[T]Array
5.
a.l = i & a.u = j
6.
m:
{i..j
}
7.
n:
{m..j
}
a[m..n]
[T]Array
By:
Analyze 4
THEN
Analyze 5
THEN
Unfolds [`array_seg`;`array`] 0
Generated subgoal:
1
4.
n1:
5.
m1:
{n1...}
6.
a2:
{n1..m1
}
T
7.
< n1,m1,a2 > .l = i & < n1,m1,a2 > .u = j
8.
m:
{i..j
}
9.
n:
{m..j
}
< m,n,2of(2of( < n1,m1,a2 > )) >
n:
m:{n...}
{n..m
}
T