Nuprl - Pf apply_alist

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

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

By: Auto THEN Unfold `apply_alist` 0 THEN Inst Thm* P:(T), as:T List, d:T. ((first a as s.t. P(a) else d) as) (first a as s.t. P(a) else d) = d [LabelT;p.1of(p) = x;as; < x,d > ] THEN ParallelOp -1

Generated subgoals:

1 1. T: Type
2. as: (LabelT) List
3. d: T
4. x: Label
5. ((first a as s.t. (p.1of(p) = x)(a) else < x,d > ) as)
(2of((first p as s.t. 1of(p) = x else < x,d > )) 2of(unzip(as)))

2 1. T: Type
2. as: (LabelT) List
3. d: T
4. x: Label
5. (first a as s.t. (p.1of(p) = x)(a) else < x,d > ) = < x,d >
2of((first p as s.t. 1of(p) = x else < x,d > )) = d

About:

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

1	1. `T:` `Type` 2. `as:` `(LabelT) List` 3. `d:` `T` 4. `x:` `Label` 5. `((first a as s.t. (p.1of(p) = x)(a) else < x,d > ) as)` `(2of((first p as s.t. 1of(p) = x else < x,d > )) 2of(unzip(as)))`
2	1. `T:` `Type` 2. `as:` `(LabelT) List` 3. `d:` `T` 4. `x:` `Label` 5. `(first a as s.t. (p.1of(p) = x)(a) else < x,d > ) = < x,d >` `2of((first p as s.t. 1of(p) = x else < x,d > )) = d`