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:
equalconsaddintlistifthenelsenatural_number