Definitions
array
1
Doc
At:
array
seg
wf
1
1.
T:
Type
2.
i:
3.
j:
{i...}
4.
a:
[T]Array{i..j
}
5.
m:
{i..j
}
6.
n:
{m..j
}
a[m..n]
[T]Array{m..n
}
By:
Analyze 4
THEN
AbSetMemEqTypeCD
Generated subgoals:
1
4.
a:
[T]Array
5.
a.l = i & a.u = j
6.
m:
{i..j
}
7.
n:
{m..j
}
a[m..n]
[T]Array
2
4.
a:
[T]Array
5.
a.l = i & a.u = j
6.
m:
{i..j
}
7.
n:
{m..j
}
a[m..n].l = m & a[m..n].u = n