Nuprl - Pf apply_alist_non

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

T:Type, as:(LabelT) List, d:T, x:Label. (x 1of(unzip(as))) apply_alist(as;x;d) = d

By: Analyze 0 THEN Analyze 0 THEN ListInd -1 THEN All (Unfold `unzip`) THEN All Reduce

Generated subgoals:

1 1. T: Type
2. as: (LabelT) List
d:T, x:Label. (x nil) apply_alist(nil;x;d) = d

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)) apply_alist(v;x;d) = d
d:T, x:Label. (x [1of(u) / map(p.1of(p);v)]) apply_alist([u / v];x;d) = d

About:

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

1	1. `T:` `Type` 2. `as:` `(LabelT) List` `d:T, x:Label. (x nil) apply_alist(nil;x;d) = d`
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)) apply_alist(v;x;d) = d` `d:T, x:Label. (x [1of(u) / map(p.1of(p);v)]) apply_alist([u / v];x;d) = d`