(4steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc
At:
tag
sublist
layer
1
1.
E:
TaggedEventStruct
2.
m:
Label
tr_1,tr_2:|E| List. tr_1 = tr_2
( < tr_1 > _m ((delayableR(E)
asyncR(E))^*) < tr_2 > _m)
By:
Auto
THEN
HypSubst -1 0
THEN
BackThru
Thm*
x,y:T, R:(T
T
Prop). x = y
(x (R^*) y)
Generated subgoals:
None
About:
(4steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc
tr_1,tr_2:|E| List. tr_1 = tr_2 
( < tr_1 > _m ((delayableR(E) 
asyncR(E))^*) < tr_2 > _m)x,y:T, R:(T
TProp). x = y (x (R^*) y)