Rank | Theorem | Name |
6 |
Thm* E:TaggedEventStruct. tag_splitable(E;adR(E)) | [tag_sublist_layer] |
cites |
1 |
Thm* R:(T![](FONT/dash.png) T![](FONT/dash.png) Prop), x,y,z:T. (x (R^*) y) ![](FONT/eq.png) (y (R^*) z) ![](FONT/eq.png) (x (R^*) z) | [rel_star_transitivity] |
0 |
Thm* x,y:T, R:(T![](FONT/dash.png) T![](FONT/dash.png) Prop). x = y ![](FONT/eq.png) (x (R^*) y) | [rel_star_weakening] |
0 |
Thm* R:(T![](FONT/dash.png) T![](FONT/dash.png) Prop), x,y:T. (x R y) ![](FONT/eq.png) (x (R^*) y) | [rel_rel_star] |
5 |
Thm* P:(A![](FONT/dash.png) A![](FONT/dash.png) Prop), f:(A![](FONT/dash.png) ![](FONT/then_med.png) ), L1,L2:A List.
(L1 swap adjacent[P(x,y)] L2) ![](FONT/eq.png)
(filter(f;L1) swap adjacent[P(x,y)] filter(f;L2)) filter(f;L1) = filter(f;L2) | [filter_swap_adjacent] |