Nuprl - Pf P_causal

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

1. E: EventStruct
2. tr: |E| List
3. i:||tr||. j:||tr||. ji & is-send(E)(tr[j]) & (tr[j] =msg=(E) tr[i])
4. tr': |E| List
5. tr' tr
6. x: |E|
7. i:
8. i < ||tr'||
9. x = tr'[i]
10. ||tr'||||tr||

y:|E|. (i:. i < ||tr'|| & y = tr'[i]) & is-send(E)(y) & (y =msg=(E) x)

By: AllHyps (RWO "iseg_select") THEN ExRepD THEN InstHyp [i] 3 THEN ExRepD THEN InstConcl [tr[j]]

Generated subgoals:

1 5. ||tr'||||tr||
6. i:. i < ||tr'|| tr'[i] = tr[i]
7. x: |E|
8. i:
9. i < ||tr'||
10. x = tr'[i]
11. ||tr'||||tr||
12. j: ||tr||
13. ji
14. is-send(E)(tr[j])
15. tr[j] =msg=(E) tr[i]
i:. i < ||tr'|| & tr[j] = tr'[i]

2 5. ||tr'||||tr||
6. i:. i < ||tr'|| tr'[i] = tr[i]
7. x: |E|
8. i:
9. i < ||tr'||
10. x = tr'[i]
11. ||tr'||||tr||
12. j: ||tr||
13. ji
14. is-send(E)(tr[j])
15. tr[j] =msg=(E) tr[i]
tr[j] =msg=(E) x

About:

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

1	5. `\|\|tr'\|\|\|\|tr\|\|` 6. `i:. i < \|\|tr'\|\| tr'[i] = tr[i]` 7. `x:` `\|E\|` 8. `i:` 9. `i < \|\|tr'\|\|` 10. `x = tr'[i]` 11. `\|\|tr'\|\|\|\|tr\|\|` 12. `j:` `\|\|tr\|\|` 13. `ji` 14. `is-send(E)(tr[j])` 15. `tr[j] =msg=(E) tr[i]` `i:. i < \|\|tr'\|\| & tr[j] = tr'[i]`
2	5. `\|\|tr'\|\|\|\|tr\|\|` 6. `i:. i < \|\|tr'\|\| tr'[i] = tr[i]` 7. `x:` `\|E\|` 8. `i:` 9. `i < \|\|tr'\|\|` 10. `x = tr'[i]` 11. `\|\|tr'\|\|\|\|tr\|\|` 12. `j:` `\|\|tr\|\|` 13. `ji` 14. `is-send(E)(tr[j])` 15. `tr[j] =msg=(E) tr[i]` `tr[j] =msg=(E) x`