At: M DASH C DASH S SPACE induction 2 2 1 1
1. E: TaggedEventStruct
2. P: (|E| List)
Prop
3. I: (|E| List)
Prop
4. memorylessR(E) preserves P
5.
x,y,z:|E| List. P(x) 
P(y) 
(
x
x.(
y
y.
(x =msg=(E) y))) & z = (x @ y) 
P(z)
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. n: 
10. 0 < n
11.
tr:|E| List. ||tr||
n-1 
(
m:Label. P( < tr > _m)) 
I(tr) 
P(tr)
12. tr: |E| List
13. ||tr||
n
14.
tr = nil
15.
m:Label. P( < tr > _m)
16. I(tr)
17. L_1: |E| List
18. L_2: |E| List
19. tr = (L_1 @ L_2)
20.
L_2 = nil
21. (
x
L_1.(
y
L_2.
(x =msg=(E) y)))
22. m: Label
23. (
x
L_2.tag(E)(x) = m)
||L_1||
n-1
By:
Inst
Thm*
as,bs:T List. ||as @ bs|| = ||as||+||bs||
[|E|;L_1;L_2]
THEN
Inst
Thm*
L:T List.
L = nil 
0 < ||L||
[|E|;L_2]
THEN
SubstFor (L_1 @ L_2) -2
Generated subgoals:None
About: