E:EventStruct, tr:|E| List, x,y:|E|.
Dec(x somewhere delivered before y)i,j:
, F:({i..j
}
Prop).
(k:{i..j}. Dec(F(k))) 
Dec(k:{i..j}. F(k))i,j:, F:({i..j}Prop).
(k:{i..j}. Dec(F(k))) Dec(
k:{i..j}. F(k)) Dec(Q) Dec(P & Q)| Rank | Theorem | Name |
| 8 |
Thm* E:EventStruct, tr:|E| List, x,y:|E|.
Dec(x somewhere delivered before y) | [decidable__delivered_before_somewhere] |
| cites | ||
| 7 |
Thm* i,j:, F:({i..j}Prop).
(k:{i..j}. Dec(F(k))) Dec(k:{i..j}. F(k)) | [decidable__all_int_seg] |
| 6 |
Thm* i,j:, F:({i..j}Prop).
(k:{i..j}. Dec(F(k))) Dec(k:{i..j}. F(k)) | [decidable__ex_int_seg] |
| 0 |
Thm* Dec(P) Dec(Q) Dec(P & Q) | [decidable__and] |