(31steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc
At:
M
DASH
C
DASH
S
SPACE
induction
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)))
tr:|E| List. ||tr||
0
(
m:Label. P( < tr > _m))
I(tr)
P(tr)
By:
Auto
THEN
Subst (tr = nil) 0
THEN
Try (Analyze 0)
THEN
Try (BackThru
Thm*
l:T List. ||l|| = 0
l = nil)
Generated subgoal:
1
9.
tr:
|E| List
10.
||tr||
0
11.
m:Label. P( < nil > _m)
12.
I(nil)
P(nil)
About:
(31steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc