PrintForm
Definitions
action
sets
Sections
AutomataTheory
Doc
At:
counter
append
1
2
1.
e:
2.
L:
*
3.
M:
*
4.
u:
5.
v:
*
6.
||e:v @ M|| = ||e:v||+||e:M||
||e:(u.v) @ M|| = ||e:u.v||+||e:M||
By:
RW (AddrC [2] (RecUnfoldC `el_counter`)) 0
Generated subgoal:
1
if null((u.v) @ M)
0 ;e=
hd(((u.v) @ M))
1+||e:tl(((u.v) @ M))|| else ||e:tl(((u.v) @ M))|| fi = ||e:u.v||+||e:M||
About: