Nuprl - Pf strong_switch_inv

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

E:TaggedEventStruct. (switch_inv(E) Causal(E) AD-normal(E) No-dup-deliver(E)) refines switch-decomposable(E)

By: Auto THEN Unfold `tr_refines` 0 THEN Try (Fold `trace_property` 0) THEN Unfold `prop_and` -1 THEN Reduce -1 THEN ExRepD THEN Unfold `switch_decomposable` 0 THEN Reduce 0 THEN Decide null(tr) THEN RW assert_pushdownC -1 THEN SimpConcl

Generated subgoal:

1 1. E: TaggedEventStruct
2. tr: |E| List
3. switch_inv(E)(tr)
4. Causal(E)(tr)
5. AD-normal(E)(tr)
6. No-dup-deliver(E)(tr)
7. tr = nil
Q:(||tr||Prop). (i:||tr||. Dec(Q(i))) & (i:||tr||. Q(i)) & (i:||tr||. Q(i) is-send(E)(tr[i])) & (i,j:||tr||. Q(i) Q(j) tag(E)(tr[i]) = tag(E)(tr[j])) & (i,j:||tr||. Q(i) ij C(Q)(j))

About:

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