PrintForm Definitions action sets Sections AutomataTheory Doc

At: counter append 1 2 1 1 1
1. e:
2. L: *
3. M: *
4. u:
5. v: *
6. ||e:v @ M|| = ||e:v||+||e:M||
7. e = u

1+||e:v @ M|| = ||e:u.v||+||e:M||
By: RW (AddrC [3;1] (RecUnfoldC `el_counter`)) 0
Generated subgoal:

1 1+||e:v @ M|| = if null(u.v)0 ;e=hd((u.v))1+||e:tl((u.v))|| else ||e:tl((u.v))|| fi+||e:M||

About:
equaladdnatural_numberconsintlistifthenelse