PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
append
segment
1
1
1
1
1
1
2
1
1
1
1
1
1
1
1
1
1
1
1
1
1.
T:
Type
2.
as:
T*
3.
i:
{0...||as||}
4.
j:
{i...||as||}
5.
k:
{j...||as||}
6.
x:
7.
0 < x
8.
k
x+i
9.
tl(nth_tl(-1+i+x;as)) = nth_tl(i+x;as)
10.
aas:
T*
11.
aas = nth_tl(-1+i+x;as)
hd(aas).firstn(-i+k+-x;tl(aas)) = firstn(1+-i+k+-x;aas)
By:
Assert (
aas = nil)
Generated subgoals:
1
aas = nil
2
12.
aas = nil
hd(aas).firstn(-i+k+-x;tl(aas)) = firstn(1+-i+k+-x;aas)
About:
aas = nilaas = nil hd(aas).firstn(-i+k+-x;tl(aas)) = firstn(1+-i+k+-x;aas)
x+i hd(aas).firstn(-i+k+-x;tl(aas)) = firstn(1+-i+k+-x;aas)aas = nil) aas = nilaas = nil hd(aas).firstn(-i+k+-x;tl(aas)) = firstn(1+-i+k+-x;aas)
