At: apply alist non member 2 1 1 2 1
1. T: Type
2. as: (Label
T) List
3. u: LabelT
4. v: (LabelT) List
5. 
d:T, x:Label. 
(x 
map(
p.1of(p);v)) 
apply_alist(v;x;d) = d
6. d: T
7. x: Label
8. (x = 1of(u) 
(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
11. (x map(p.1of(p);v))
False
By:
Analyze -4
THEN
TrivialOr
Generated subgoals:None
About:
