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

At: switch inv theorem 5
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:Trace(E). (switch_inv(E) No-dup-send(E))(tr) (tr':Trace(E). switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr'))
By:
((Unfold `str_trace` 0) THEN (Inst Thm* E:TaggedEventStruct, tr:Trace(E). (switch_inv(E) No-dup-send(E))(tr) (tr':Trace(E). switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr')) [E;tr])) THENA (Auto THEN (Try (Unfold `str_trace` 0)))
THEN
AllHyps (h.(Unfold `prop_and` h) THEN (Reduce h))
Generated subgoal:

16. P refines (L.Causal(E)(L) & No-dup-deliver(E)(L))
7. tr: |E| List
8. switch_inv(E)(tr)
9. No-dup-send(E)(tr)
10. tr':Trace(E). switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr')
tr':|E| List. switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr')

About:
listapplyfunctionpropimpliesandallexists

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