(164steps 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:
pre-rule
2
1
2
1
2
1
1
1.
i
: Id
2.
a
: Id
3.
T
: Type
4.
ds
:
x
:Id fp-> Type
5.
P
: State(
ds
)
T
Prop
6.
w
: World
7.
p
: FairFifo
8. FairFifo
9.
l
:IdLnk,
tg
:Id.
9.
(
w
.M(
l
,
tg
))
r if eqof(IdDeq)(source(
l
),
i
)
9. (
w
.M(
l
,
tg
))
r if
<
ds
,<[locl(
a
)],
x
.
T
>,,<[
a
],
x
.
P
>,,,,,
>
9. (
w
.M(
l
,
tg
))
r
else fi.da(rcv(
l
;
tg
))
10. (eqof(IdDeq)(
i
,
i
)) ~ true
11.
a@0
:Id,
t
:
.
11.
t'
:
.
11.
t
t'
11.
&
isnull(a(
i
;
t'
)) & kind(a(
i
;
t'
)) = locl(
a@0
)
11. &
locl(
a@0
)
dom(<[locl(
a
)],
x
.
T
>)
11. &
P@0
!= <[
a
],
x
.
P
>(
a@0
) ==>
v
:<[locl(
a
)],
x
.
T
>(locl(
a@0
))?Top.
11. &
P@0
((
x
.s(
i
;
t'
).
x
),
v
)
12.
t
:
.
12.
isnull(a(
i
;
t
))
12.
12.
(islocal(kind(a(
i
;
t
)))
12. (
12. (
(eqof(IdDeq)(
a
,act(kind(a(
i
;
t
))))
false
)
12. (
12. (
P
((
x
.s(
i
;
t
).
x
),val(a(
i
;
t
))))
12.
& (
x
:Id.
12. & (
deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(
i
;
t
)),
x
>;1of())
12. & (
12. & (
s(
i
;
t
+1).
x
= 2of()(<kind(a(
i
;
t
)),
x
>,
x
.s(
i
;
t
).
x
,val(a(
i
;
t
))))
12.
& (
l
:IdLnk.
12. & (
deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(
i
;
t
)),
l
>;1of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(
i
;
t
)),
l
>;
))
12. & (
12. & (
withlnk(
l
;m(
i
;
t
))
12. & (
=
12. & (
if source(
l
) =
i
12. & (if
concat(map(
tgf
.map(
x
.<1of(
tgf
)
12. & (if concat(map(
tgf
.map(
x
.
,
x
>;2of(
tgf
)
12. & (if concat(map(
tgf
.map(
x
.,
x
>;
((
x
.s(
i
;
t
).
x
)
12. & (if concat(map(
tgf
.map(
x
.,
x
>;
,val(a(
i
;
t
))));2of()(<kind(a(
i
;
t
)),
l
>)))
12. & (
else nil fi)
12.
& (
x
:Id.
12. & (
(deq-member(IdDeq;
x
;1of())
deq-member(KindDeq;kind(a(
i
;
t
));2of()(
x
)))
12. & (
12. & (
s(
i
;
t
).
x
= s(
i
;
t
+1).
x
)
12.
& (
l
:IdLnk,
tg
:Id.
12. & (
(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<
l
,
tg
>;1of())
12. & (
(
12. & (
(
deq-member(KindDeq;kind(a(
i
;
t
));2of()(<
l
,
tg
>)))
12. & (
12. & (
w-tagged(
tg
; onlnk(
l
;m(
i
;
t
))) = nil)
13.
x
:Id. deq-member(IdDeq;
x
;1of())
s(
i
;0).
x
= 2of()(
x
)
14.
a@0
:Action(
i
).
14.
isnull(
a@0
)
(valtype(
i
;
a@0
)
r <[locl(
a
)],
x
.
T
>(kind(
a@0
))?Top)
15.
x
:Id.
15.
vartype(
i
;
x
)
r if deq-member(IdDeq;
x
;1of(
ds
))
2of(
ds
)(
x
) else Top fi
16. IdDeq
EqDecider(Id)
17.
j
: Id
18.
t
:
19.
isnull(a(
j
;
t
)) [not for witness]
20.
j
=
i
21. kind(<
j
,
t
>) = locl(
a
)
22.
isnull(a(
j
;
t
))
valtype(<
j
,
t
>)
r
T
By:
Repeat
(Unfolds [`es-kind`;`es-loc`;`es-act`;`es-isrcv`;`es-valtype`;`es-acttype`] 0
(
THEN
(
Reduce 0)
THEN
StrongHypSubst -2 0
Generated subgoals:
1
if isrcv(locl(
a
))
rcvtype(<
j
,
t
>) else V(
j
;locl(act(locl(
a
)))) fi
r
T
9
steps
2
19.
isnull(a(
j
;
t
))
20.
j
=
i
21. kind(<
j
,
t
>) = locl(
a
)
22.
isnull(a(
j
;
t
))
23.
z
: Knd
24.
z
= locl(
a
)
(if isrcv(
z
)
rcvtype(<
j
,
t
>) else V(
j
;locl(act(
z
))) fi
r
T
)
Type{i}
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(164steps total)
PrintForm
Definitions
Lemmas
mb
event
system
6
Sections
EventSystems
Doc