Nuprl - Pf no_dup_send

(2steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

1. E: EventStruct
2. A: Type
3. evt: A|E|
4. tg: ALabel
5. tr_l: A List
6. i,j:||map(evt;tr_l)||. is-send(E)(map(evt;tr_l)[i]) is-send(E)(map(evt;tr_l)[j]) (map(evt;tr_l)[i] =msg=(E) map(evt;tr_l)[j]) i = j
7. i: ||tr_l||
8. j: ||tr_l||
9. is-send( < A,evt,tg > (E))(tr_l[i])
10. is-send( < A,evt,tg > (E))(tr_l[j])
11. tr_l[i] =msg=( < A,evt,tg > (E)) tr_l[j]

i = j

By: Inst Thm* f:(AB), as:A List. ||map(f;as)|| = ||as|| [A;|E|;evt;tr_l] THEN AllHyps (h.(Unfold `induced_tagged_event_str` h) THEN (Reduce h)) THEN BackThruSomeHyp THEN RWO "map_select" 0 THEN All (h.(Unfold `event_msg_eq` h) THEN (Reduce h))

Generated subgoals:

None

About:

(2steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc