Who Cites R safety? | |
R_safety | Def safetyR(E)(tr_1,tr_2) == tr_2 tr_1 |
Thm* E:EventStruct. safetyR(E) (|E| List)(|E| List)Prop | |
carrier | Def |S| == 1of(S) |
Thm* S:Structure. |S| Type | |
iseg | Def l1 l2 == l:T List. l2 = (l1 @ l) |
Thm* T:Type, l1,l2:T List. l1 l2 Prop | |
pi1 | Def 1of(t) == t.1 |
Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A | |
append | Def as @ bs == Case of as; nil bs ; a.as' [a / (as' @ bs)] (recursive) |
Thm* T:Type, as,bs:T List. (as @ bs) T List |
Syntax: | safetyR(E) | has structure: | R_safety(E) |
About: