Nuprl - Pf switch_inv_rel_same

(8steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc

E:TaggedEventStruct, tr:|E| List. switch_inv(E)(tr) (i,j:||tr||. (i switchR(tr) j) tag(E)(tr[i]) = tag(E)(tr[j]))

By: Auto THEN All (Unfolds [`switch_inv`;`switch_inv_rel`]) THEN All Reduce THEN ExRepD

Generated subgoals:

1 1. E: TaggedEventStruct
2. tr: |E| List
3. i,j,k:||tr||. i < j is-send(E)(tr[i]) is-send(E)(tr[j]) tag(E)(tr[i]) = tag(E)(tr[j]) tr[j] delivered at time k (k':||tr||. k' < k & tr[i] delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k]))
4. i: ||tr||
5. j: ||tr||
6. is-send(E)(tr[i])
7. is-send(E)(tr[j])
8. i < j & tr[j] somewhere delivered before tr[i] j < i & tr[i] somewhere delivered before tr[j]
tag(E)(tr[i]) = tag(E)(tr[j])

2 1. E: TaggedEventStruct
2. tr: |E| List
3. i,j:||tr||. is-send(E)(tr[i]) & is-send(E)(tr[j]) & i < j & tr[j] somewhere delivered before tr[i] j < i & tr[i] somewhere delivered before tr[j] tag(E)(tr[i]) = tag(E)(tr[j])
4. i: ||tr||
5. j: ||tr||
6. k: ||tr||
7. i < j
8. is-send(E)(tr[i])
9. is-send(E)(tr[j])
10. tag(E)(tr[i]) = tag(E)(tr[j])
11. tr[j] delivered at time k
k':||tr||. k' < k & tr[i] delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k])

About:

(8steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc