Nuprl - Pf member_tag

(3steps) PrintForm Definitions mb structures Sections GenAutomata Doc

E:TaggedEventStruct, tr:|E| List, x:|E|, t:Label. (x < tr > _t) (x tr) & tag(E)(x) = t

By: Unfold `tag_sublist` 0 THEN RWO "member_filter" 0 THEN Reduce 0

Generated subgoals:

1 1. E: TaggedEventStruct
2. tr: |E| List
3. x: |E|
4. t: Label
5. (x tr)
6. tag(E)(x) = t
tag(E)(x) = t

2 1. E: TaggedEventStruct
2. tr: |E| List
3. x: |E|
4. t: Label
5. (x tr)
6. tag(E)(x) = t
tag(E)(x) = t

About:

(3steps) PrintForm Definitions mb structures Sections GenAutomata Doc

1	1. `E:` `TaggedEventStruct` 2. `tr:` `\|E\| List` 3. `x:` `\|E\|` 4. `t:` `Label` 5. `(x tr)` 6. `tag(E)(x) = t` `tag(E)(x) = t`
2	1. `E:` `TaggedEventStruct` 2. `tr:` `\|E\| List` 3. `x:` `\|E\|` 4. `t:` `Label` 5. `(x tr)` 6. `tag(E)(x) = t` `tag(E)(x) = t`