Definitions
array
1
Doc
At:
array
el
wfp
1
1
1
1
1.
T:
Type
2.
i:
3.
j:
{i...}
4.
n:
5.
m:
{n...}
6.
a2:
{n..m
}
T
7.
< n,m,a2 > .l = i
8.
< n,m,a2 > .u = j
9.
k:
{i..j
}
< n,m,a2 > [k]
T
By:
Unfold `array_lb` 7
THEN
Unfold `array_ub` 8
THEN
Unfold `array_el` 0
THEN
OnClauses [7;8;0] (Rewrite (DepthC (pi1_evalC ORELSEC pi2_evalC)))
Generated subgoal:
1
7.
n = i
8.
m = j
9.
k:
{i..j
}
a2(k)
T