(LabelT) List

LabelT

(LabelT) List

d:T, x:Label. (x map(p.1of(p);v)) ( < x,apply_alist(v;x;d) > v)

x = 1of(u) (x map(p.1of(p);v))

apply_alist([u / v];x;d) ~ if 1of(u) = x 2of(u) else apply_alist(v;x;d) fi

1of(u) = x Pattern

1	3. u1: Label 4. u2: T 5. v: (LabelT) List 6. d:T, x:Label. (x map(p.1of(p);v)) ( < x,apply_alist(v;x;d) > v) 7. d: T 8. x: Label 9. x = u1 (x map(p.1of(p);v)) 10. apply_alist([ < u1,u2 > / v];x;d) ~ if u1 = x u2 else apply_alist(v;x;d) fi 11. u1 = x Pattern x = u1

About: