Definitions
array
1
Doc
At:
array
shift
wf
1
1
1
1.
T:
Type
2.
i:
3.
j:
{i...}
4.
n:
5.
m1:
{n...}
6.
a2:
{n..m1
}
T
7.
< n,m1,a2 > .l = i & < n,m1,a2 > .u = j
8.
m:
< ( < n,m1,a2 > .l+m),( < n,m1,a2 > .u+m),(
j. < n,m1,a2 > [(j-m)]) >
n:
m:{n...}
{n..m
}
T
By:
Unfolds [`array_el`;`array_lb`;`array_ub`] 0
THEN
Rewrite (DepthC (pi1_evalC ORELSEC pi2_evalC)) 0
THEN
Reduce 0
Generated subgoal:
1
< (n+m),(m1+m),(
j.a2(j-m)) >
n:
m:{n...}
{n..m
}
T
< (n+m),(m1+m),(
j.a2(j-m)) > 
n:
m:{n...}{n..m
}
T