(12steps) PrintForm Definitions Lemmas mb automata 1 Sections GenAutomata Doc

At: apply alist member 2 1 1 2
1. T: Type
2. as: (LabelT) List
3. u: LabelT
4. v: (LabelT) 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 = 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

< x,apply_alist(v;x;d) > = u ( < x,apply_alist(v;x;d) > v)
By: Analyze -3
Generated subgoals:

18. x = 1of(u)
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) > = u ( < x,apply_alist(v;x;d) > v)
28. (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) > = u ( < x,apply_alist(v;x;d) > v)

About:
pairproductlistconsifthenelse
lambdauniverseequalsqequalimpliesorall

(12steps) PrintForm Definitions Lemmas mb automata 1 Sections GenAutomata Doc