(16steps total)
PrintForm
Definitions
Lemmas
mb
event
system
6
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sframe-rule
1
1
1
1
1
1.
i
: Id
2.
L
: Knd List
3.
l
: IdLnk
4.
tg
: Id
5.
w
: World
6. FairFifo
7. FairFifo
8.
j
: Id
9.
t
:
10.
j
=
i
11.
null(filter(
m
.mtag(
m
) =
tg
;sends(
l
;<
j
,
t
>)))
12.
isnull(a(
i
;
t
))
13. islocal(kind(a(
i
;
t
)))
13.
13.
deq-member(IdDeq;act(kind(a(
i
;
t
)));1of())
13.
13.
2of()(act(kind(a(
i
;
t
))),
x
.s(
i
;
t
).
x
,val(a(
i
;
t
)))
14.
x
:Id.
14.
deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(
i
;
t
)),
x
>;1of())
14.
14.
s(
i
;
t
+1).
x
= 2of()(<kind(a(
i
;
t
)),
x
>,
x
.s(
i
;
t
).
x
,val(a(
i
;
t
)))
15.
l@0
:IdLnk.
15.
deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(
i
;
t
)),
l@0
>;1of())
15.
15.
withlnk(
l@0
;m(
i
;
t
))
15.
=
15.
if source(
l@0
) =
i
15. if
concat(map(
tgf
.map(
x
.<1of(
tgf
),
x
>;2of(
tgf
)
15. if concat(map(
tgf
.map(
x
.<1of(
tgf
),
x
>;
((
x
.s(
i
;
t
).
x
)
15. if concat(map(
tgf
.map(
x
.<1of(
tgf
),
x
>;
,val(a(
i
;
t
))));2of()
15. if concat(map(
tgf
.map(
x
.<1of(
tgf
),
x
>;,val(a(
i
;
t
))));
(<kind(a(
i
;
t
)),
l@0
>)))
15.
else nil fi
16.
x
:Id.
16.
(deq-member(IdDeq;
x
;1of())
deq-member(KindDeq;kind(a(
i
;
t
));2of()(
x
)))
16.
16.
s(
i
;
t
).
x
= s(
i
;
t
+1).
x
17.
l@0
:IdLnk,
tg@0
:Id.
17.
((eqof(product-deq(IdLnk;Id;IdLnkDeq;IdDeq))(<
l
,
tg
>,<
l@0
,
tg@0
>)
false
)
17.
(
17.
(
deq-member(KindDeq;kind(a(
i
;
t
));
L
))
17.
17.
w-tagged(
tg@0
; onlnk(
l@0
;m(
i
;
t
))) = nil
18. (kind(a(
i
;
t
))
L
)
(kind(<
j
,
t
>)
L
)
By:
Unfold `w-ekind` 0 THEN Unfold `w-act` 0 THEN Reduce 0
Generated subgoal:
1
(kind(a(
j
;
t
))
L
)
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(16steps total)
PrintForm
Definitions
Lemmas
mb
event
system
6
Sections
EventSystems
Doc