Definitions
array
1
Doc
At:
array
seg
wf
1
1
1
1.
T:
Type
2.
i:
3.
j:
{i...}
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
By:
OnClauses [7;0] AbReduce
THEN
Analyze 7
Generated subgoal:
1
7.
n1 = i
8.
m1 = j
9.
m:
{i..j
}
10.
n:
{m..j
}
< m,n,a2 >
n:
m:{n...}
{n..m
}
T