PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
append
segment
1
1.
T:
Type
2.
as:
T*
3.
i:
{0...||as||}
4.
j:
{i...||as||}
5.
k:
{j...||as||}
((as[i..j
]) @ (as[j..k
])) = (as[i..k
])
By:
Unfold `segment` 0
Generated subgoal:
1
(firstn(j-i;nth_tl(i;as)) @ firstn(k-j;nth_tl(j;as))) = firstn(k-i;nth_tl(i;as))
About:
(firstn(j-i;nth_tl(i;as)) @ firstn(k-j;nth_tl(j;as))) = firstn(k-i;nth_tl(i;as)) ((as[i..j
]) @ (as[j..k])) = (as[i..k]) (firstn(j-i;nth_tl(i;as)) @ firstn(k-j;nth_tl(j;as))) = firstn(k-i;nth_tl(i;as))
