At: M DASH C DASH S SPACE induction 1 1
1. E: TaggedEventStruct
2. P: (|E| List)
Prop
3. I: (|E| List)
Prop
4. memorylessR(E) preserves P
5. (ternary) composableR(E) preserves P
6. safetyR(E) preserves P
7. safetyR(E) preserves I
8.
tr:|E| List.
I(tr) 
tr = nil 
(
L_1,L_2:|E| List.
tr = (L_1 @ L_2)
&
L_2 = nil
& (
x
L_1.(
y
L_2.
(x =msg=(E) y)))
& (
m:Label. (
x
L_2.tag(E)(x) = m)))
9. tr: |E| List
10. ||tr||
0
11.
m:Label. P( < nil > _m)
12. I(nil)
P(nil)
By:
InstHyp [any] -2
THEN
Unfold `tag_sublist` -1
THEN
Reduce -1
Generated subgoals:None
About: