PrintForm
Definitions
action
sets
Sections
AutomataTheory
Doc
At:
el
counter
wf
1
2
1.
n:
2.
L:
*
3.
u:
4.
v:
*
5.
||n:v||
||n:u.v||
By:
RecCaseSplit `el_counter`
THEN
Inst
Thm*
a:A, as:A*. ||a.as|| = ||as||+1 [
;u;v]
Generated subgoal:
1
6.
u.v = nil
7.
n = hd((u.v))
8.
||u.v|| = ||v||+1
||n:v||
About:
u.v = nil
||n:v|| 
** 
||n:u.v|| 
a:A, as:A*. ||a.as|| = ||as||+1
[;u;v]u.v = nil ||n:v|| 
