E:EventStruct, x:|E| List, j,z:
||x||. Dec(j switchR(x) z)
Dec(Q) Dec(P 
Q) Dec(Q) Dec(P & Q)| Theorem | Name |
|
Thm* E:EventStruct, x:|E| List, j,z:||x||. Dec(j switchR(x) z) | [decidable__switch_inv_rel] |
| cites | |
|
Thm* Dec(P) Dec(Q) Dec(P Q) | [decidable__or] |
|
Thm* Dec(P) Dec(Q) Dec(P & Q) | [decidable__and] |