Definitions
array
1
Doc
At:
array
append
wf
1
1
1
1.
T:
Type
2.
i:
3.
j:
{i...}
4.
k:
{j...}
5.
a:
[T]Array
6.
a.l = i
7.
a.u = j
8.
b:
[T]Array
9.
b.l = j
10.
b.u = k
a @ b
[T]Array
By:
OnHyps [8;9;5;6] Analyze
THEN
Unfold `array_append` 0
THEN
OnAllClauses AbReduce
Generated subgoal:
1
5.
n1:
6.
m1:
{n1...}
7.
a2:
{n1..m1
}
T
8.
n1 = i
9.
m1 = j
10.
n:
11.
m:
{n...}
12.
b2:
{n..m
}
T
13.
n = j
14.
m = k
< n1,m,(
i.if i < m1
a2(i) ; b2(i) fi) >
[T]Array