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

At: switch inv theorem 2
1. E: TaggedEventStruct
2. P: (|E| List)Prop
3. MCS(E)(P)
4. asyncR(E) preserves P
5. delayableR(E) preserves P
6. P refines (Causal(E) No-dup-deliver(E))

tr_1,tr_2:Trace(E). (tr_1 adR(E) tr_2) (tr_2 adR(E) tr_1)
By:
Fold `sym` 0
THEN
Unfolds [`str_trace`;`R_ad`] 0
THEN
BackThru Thm* R:(TTProp). Sym x,y:T. x R y Sym x,y:T. x (R^*) y
THEN
BackThru Thm* R1,R2:(TTProp). Sym x,y:T. x R1 y Sym x,y:T. x R2 y Sym x,y:T. x (R1 R2) y
THEN
Unfold `sym` 0
THEN
Try (BackThruLemma' Thm* E:EventStruct, x,y:|E| List. (x delayableR(E) y) (y delayableR(E) x))
THEN
Try (BackThruLemma' Thm* E:EventStruct, x,y:|E| List. (x asyncR(E) y) (y asyncR(E) x))
Generated subgoals:

None

About:
listapplyfunctionpropimpliesall

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