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

At: apply alist non member 2 1 1 1
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)) 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

2of(u) = d
By:
Analyze -3
THEN
Sel 1 (Analyze 0)
THEN
Analyze 3
THEN
Analyze 3
THEN
Analyze -3
THEN
All Reduce
Generated subgoal:

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

About:
productlistconsifthenelselambda
universeequalsqequalimpliesorall

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