| Who Cites layer rel? |
|
layer_rel |
Def layerR(E) == ((asyncR(E) delayableR(E)) send-enabledR(E))^* |
|
| Thm* E:EventStruct. layerR(E) (|E| List) (|E| List) Prop |
|
R_async |
Def asyncR(E)
== swap adjacent[ loc(E)(x) = loc(E)(y)
&  (is-send(E)(x)) &  (is-send(E)(y)) (is-send(E)(x)) & (is-send(E)(y))] |
|
| Thm* E:EventStruct. asyncR(E) (|E| List) (|E| List) Prop |
|
R_delayable |
Def delayableR(E)
== swap adjacent[ (x =msg=(E) y)
&  (is-send(E)(x)) & (is-send(E)(y)) (is-send(E)(x)) &  (is-send(E)(y))] |
|
| Thm* E:EventStruct. delayableR(E) (|E| List) (|E| List) Prop |
|
R_send_enabled |
Def send-enabledR(E)(L_1,L_2) == x:|E|. (is-send(E)(x)) & L_2 = (L_1 @ [x]) |
|
| Thm* E:EventStruct. send-enabledR(E) (|E| List) (|E| List) Prop |
|
event_str |
Def EventStruct == E:Type M:MessageStruct (E |M|) (E Label) (E  ) Top |
|
| Thm* EventStruct Type{i'} |
|
message_str |
Def MessageStruct == M:Type C:DecidableEquiv (M |C|) (M Label) (M  ) Top |
|
| Thm* MessageStruct Type{i'} |
|
carrier |
Def |S| == 1of(S) |
|
| Thm* S:Structure. |S| Type |
|
no_duplicate_send |
Def No-dup-send(E)(tr)
== i,j: ||tr||. (is-send(E)(tr[i]))  (is-send(E)(tr[j]))  (tr[i] =msg=(E) tr[j])  i = j |
|
| Thm* E:EventStruct. No-dup-send(E) (|E| List) Prop |
|
preserved_by |
Def R preserves P == x,y:T. P(x)  (x R y)  P(y) |
|
| Thm* T:Type, P:(T Prop), R:(T T Prop). R preserves P Prop |
|
rel_inverse |
Def R^-1(x,y) == y R x |
|
| Thm* T1,T2:Type, R:(T1 T2 Prop). R^-1 T2 T1 Prop |
|
rel_or |
Def (R1 R2)(x,y) == (x R1 y) (x R2 y) |
|
| Thm* T:Type, R1,R2:(T T Prop). (R1 R2) T T Prop |
|
rel_star |
Def (R^*)(x,y) == n: . x R^n y |
|
| Thm* T:Type, R:(T T Prop). (R^*) T T Prop |
|
event_is_snd |
Def is-send(E) == 1of(2of(2of(2of(2of(E))))) |
|
|
Thm* E:EventStruct. is-send(E) |E|   |
|
lbl |
Def Label == {p:Pattern| ground_ptn(p) } |
|
| Thm* Label Type |
|
dequiv |
Def DecidableEquiv == T:Type E:T T   EquivRel(T)( (_1 E _2)) Top |
|
| Thm* DecidableEquiv Type{i'} |
|
assert |
Def b == if b True else False fi |
|
| Thm* b: . b Prop |
|
swap_adjacent |
Def swap adjacent[P(x;y)](L1,L2)
== i: (||L1||-1). P(L1[i];L1[(i+1)]) & L2 = swap(L1;i;i+1) A List |
|
| Thm* A:Type, P:(A A Prop). swap adjacent[P(x,y)] (A List) (A List) Prop |
|
int_seg |
Def {i..j } == {k: | i k < j } |
|
| Thm* m,n: . {m..n } Type |
|
nat |
Def == {i: | 0 i } |
|
| Thm* Type |
|
lelt |
Def i j < k == i j & j < k |
|
le |
Def A B == B < A |
|
| Thm* i,j: . (i j) Prop |
|
not |
Def A == A  False |
|
| Thm* A:Prop. ( A) Prop |
|
event_loc |
Def loc(E) == 1of(2of(2of(2of(E)))) |
|
|
Thm* E:EventStruct. loc(E) |E| Label |
|
event_msg_eq |
Def =msg=(E)(e_1,e_2) == (msg(E)(e_1)) =(MS(E)) (msg(E)(e_2)) |
|
| Thm* E:EventStruct. =msg=(E) |E| |E|   |
|
swap |
Def swap(L;i;j) == (L o (i, j)) |
|
| Thm* T:Type, L:T List, i,j: ||L||. swap(L;i;j) T List |
|
permute_list |
Def (L o f) == mklist(||L||; i.L[(f(i))]) |
|
| Thm* T:Type, L:T List, f:( ||L||  ||L||). (L o f) T List |
|
mklist |
Def mklist(n;f) == primrec(n;nil; i,l. l @ [(f(i))]) |
|
| Thm* T:Type, n: , f:( n T). mklist(n;f) T List |
|
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 |
|
event_msg |
Def msg(E) == 1of(2of(2of(E))) |
|
|
Thm* E:EventStruct. msg(E) |E| |MS(E)| |
|
event_msg_str |
Def MS(E) == 1of(2of(E)) |
|
| Thm* E:EventStruct. MS(E) MessageStruct |
|
msg_eq |
Def =(M)(m_1,m_2)
== ((content(M)(m_1)) =(cEQ(M)) (content(M)(m_2))) sender(M)(m_1) = sender(M)(m_2)
(uid(M)(m_1)= uid(M)(m_2)) |
|
| Thm* M:MessageStruct. =(M) |M| |M|   |
|
msg_id |
Def uid(MS) == 1of(2of(2of(2of(2of(MS))))) |
|
|
Thm* M:MessageStruct. uid(M) |M|   |
|
msg_sender |
Def sender(MS) == 1of(2of(2of(2of(MS)))) |
|
|
Thm* M:MessageStruct. sender(M) |M| Label |
|
msg_content |
Def content(MS) == 1of(2of(2of(MS))) |
|
|
Thm* M:MessageStruct. content(M) |M| |cEQ(M)| |
|
msg_content_eq |
Def cEQ(MS) == 1of(2of(MS)) |
|
| Thm* M:MessageStruct. cEQ(M) DecidableEquiv |
|
eq_dequiv |
Def =(DE) == 1of(2of(DE)) |
|
| Thm* E:DecidableEquiv. =(E) |E| |E|   |
|
pi1 |
Def 1of(t) == t.1 |
|
| Thm* A:Type, B:(A Type), p:(a:A B(a)). 1of(p) A |
|
top |
Def Top == Void given Void |
|
|
Thm* Top Type |
|
select |
Def l[i] == hd(nth_tl(i;l)) |
|
|
Thm* A:Type, l:A List, n: . 0 n  n < ||l||  l[n] A |
|
length |
Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
|
|
Thm* A:Type, l:A List. ||l||  |
|
|
Thm* ||nil||  |
|
rel_exp |
Def R^n == if n= 0 x,y. x = y T else x,y. z:T. (x R z) & (z R^n-1 y) fi
(recursive) |
|
|
Thm* n: , T:Type, R:(T T Prop). R^n T T Prop |
|
pi2 |
Def 2of(t) == t.2 |
|
|
Thm* A:Type, B:(A Type), p:(a:A B(a)). 2of(p) B(1of(p)) |
|
ground_ptn |
Def ground_ptn(p)
== Case(p)
Case ptn_var(v) = >
false
Case ptn_pr( < x, y > ) = >
ground_ptn(x) ground_ptn(y)
Default = > true
(recursive) |
|
|
Thm* p:Pattern. ground_ptn(p)  |
|
ptn |
Def Pattern == rec(T.ptn_con(T)) |
|
|
Thm* Pattern Type |
|
nth_tl |
Def nth_tl(n;as) == if n 0 as else nth_tl(n-1;tl(as)) fi (recursive) |
|
|
Thm* A:Type, as:A List, i: . nth_tl(i;as) A List |
|
eq_lbl |
Def l1 = l2
== Case(l1)
Case ptn_atom(x) = >
Case(l2)
Case ptn_atom(y) = >
x= y Atom
Default = > false
Case ptn_int(x) = >
Case(l2)
Case ptn_int(y) = >
x= y
Default = > false
Case ptn_var(x) = >
Case(l2)
Case ptn_var(y) = >
x= y Atom
Default = > false
Case ptn_pr( < x, y > ) = >
Case(l2)
Case ptn_pr( < u, v > ) = >
x = u y = v
Default = > false
Default = > false
(recursive) |
|
|
Thm* l1,l2:Pattern. l1 = l2  |
|
case_ptn_var |
Def Case ptn_var(x) = > body(x) cont(x1,z)
== ( x1.inr(x2) = >
( x1.inr(x2) = >
( x1.inl(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x2 / tl(x1)])
cont
(hd(x1)
,z))
([x2 / tl(x1)])
cont
(hd(x1)
,z))
([x1]) |
|
case_ptn_int |
Def Case ptn_int(x) = > body(x) cont(x1,z)
== ( x1.inr(x2) = >
( x1.inl(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x2 / tl(x1)])
cont
(hd(x1)
,z))
([x1]) |
|
hd |
Def hd(l) == Case of l; nil "?" ; h.t h |
|
|
Thm* A:Type, l:A List. ||l|| 1  hd(l) A |
|
|
Thm* A:Type, l:A List . hd(l) A |
|
flip |
Def (i, j)(x) == if x= i j ;x= j i else x fi |
|
| Thm* k: , i,j: k. (i, j) k  k |
|
primrec |
Def primrec(n;b;c) == if n= 0 b else c(n-1,primrec(n-1;b;c)) fi (recursive) |
|
|
Thm* T:Type, n: , b:T, c:( n T T). primrec(n;b;c) T |
|
eq_int |
Def i= j == if i=j true ; false fi |
|
| Thm* i,j: . (i= j)  |
|
case_default |
Def Default = > body(value,value) == body |
|
band |
Def p q == if p q else false fi |
|
| Thm* p,q: . (p q)  |
|
case_lbl_pair |
Def Case ptn_pr( < x, y > ) = > body(x;y) cont(x1,z)
== InjCase(x1; _. cont(z,z); x2.
InjCase(x2; _. cont(z,z); x2@0. InjCase(x2@0; _. cont(z,z); x2@1. x2@1/x3,x2@2. body(x3;x2@2)))) |
|
case |
Def Case(value) body == body(value,value) |
|
ptn_con |
Def ptn_con(T) == Atom+ +Atom+(T T) |
|
| Thm* T:Type. ptn_con(T) Type |
|
equiv_rel |
Def EquivRel x,y:T. E(x;y)
== Refl(T;x,y.E(x;y)) & Sym x,y:T. E(x;y) & Trans x,y:T. E(x;y) |
|
| Thm* T:Type, E:(T T Prop). (EquivRel x,y:T. E(x,y)) Prop |
|
tl |
Def tl(l) == Case of l; nil nil ; h.t t |
|
|
Thm* A:Type, l:A List. tl(l) A List |
|
le_int |
Def i j ==  j < i |
|
| Thm* i,j: . (i j)  |
|
case_inl |
Def inl(x) = > body(x) cont(value,contvalue)
== InjCase(value; x. body(x); _. cont(contvalue,contvalue)) |
|
case_inr |
Def inr(x) = > body(x) cont(value,contvalue)
== InjCase(value; _. cont(contvalue,contvalue); x. body(x)) |
|
eq_atom |
Def x= y Atom == if x=y Atom true ; false fi |
|
| Thm* x,y:Atom. x= y Atom  |
|
case_ptn_atom |
Def Case ptn_atom(x) = > body(x) cont(x1,z)
== InjCase(x1; x2. body(x2); _. cont(z,z)) |
|
trans |
Def Trans x,y:T. E(x;y) == a,b,c:T. E(a;b)  E(b;c)  E(a;c) |
|
| Thm* T:Type, E:(T T Prop). Trans x,y:T. E(x,y) Prop |
|
sym |
Def Sym x,y:T. E(x;y) == a,b:T. E(a;b)  E(b;a) |
|
| Thm* T:Type, E:(T T Prop). Sym x,y:T. E(x,y) Prop |
|
refl |
Def Refl(T;x,y.E(x;y)) == a:T. E(a;a) |
|
| Thm* T:Type, E:(T T Prop). Refl(T;x,y.E(x,y)) Prop |
|
lt_int |
Def i < j == if i < j true ; false fi |
|
| Thm* i,j: . (i < j)  |
|
bnot |
Def  b == if b false else true fi |
|
| Thm* b: .  b  |