(12steps)
PrintForm
Definitions
Lemmas
mb
automata
1
Sections
GenAutomata
Doc
At:
apply
alist
member
2
1
1
2
2
1
1.
T:
Type
2.
as:
(Label
T) List
3.
u:
Label
T
4.
v:
(Label
T) List
5.
d:T, x:Label. (x
map(
p.1of(p);v))
( < x,apply_alist(v;x;d) >
v)
6.
d:
T
7.
x:
Label
8.
(x
map(
p.1of(p);v))
9.
apply_alist([u / v];x;d) ~ if 1of(u) =
x
2of(u) else apply_alist(v;x;d) fi
10.
1of(u) = x
Pattern
( < x,apply_alist(v;x;d) >
v)
By:
BackThruSomeHyp
Generated subgoals:
None
About:
(12steps)
PrintForm
Definitions
Lemmas
mb
automata
1
Sections
GenAutomata
Doc
T) ListTT) List
d:T, x:Label. (x 
map(
p.1of(p);v)) 
( < x,apply_alist(v;x;d) > v) map(p.1of(p);v))
x
2of(u) else apply_alist(v;x;d) fi
1of(u) = x Pattern
( < x,apply_alist(v;x;d) > v)
