PrintForm Definitions action sets Sections AutomataTheory Doc

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

if e=u 1+||e:v @ M|| else ||e:v @ M|| fi = ||e:u.v||+||e:M||
By: SplitOnConclITE
Generated subgoals:

17. e = u
1+||e:v @ M|| = ||e:u.v||+||e:M||
27. e = u
||e:v @ M|| = ||e:u.v||+||e:M||

About:
equalifthenelseaddnatural_numberconsintlist