Definitions
array
1
Doc
At:
array
el
wf
1
1
1.
T:
Type
2.
a:
n:
m:{n...}
{n..m
}
T
3.
i:
{1of(a)..1of(2of(a))
}
a[i]
T
By:
Analyze 2
THEN
Analyze 3
Generated subgoal:
1
2.
n:
3.
m:
{n...}
4.
a2:
{n..m
}
T
5.
i:
{1of( < n,m,a2 > )..1of(2of( < n,m,a2 > ))
}
< n,m,a2 > [i]
T