(9steps total)
PrintForm
Definitions
mb
event
system
5
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-single-effect0
wf
1
1
1.
x
: Id
2.
k
: Knd
3.
A
: Type
4.
T
: Type
5.
f
:
A
T
A
6.
s
: State(
x
:
A
)
7.
v
: ma-valtype(
k
:
T
;
k
)
f
(
s
(
x
),
v
)
x
:
A
(
x
)?Void
By:
GenConcl (
s
(
x
) =
z
) THEN Try (Complete Auto)
Generated subgoals:
1
s
(
x
)
A
3
steps
2
8.
z
:
A
9.
s
(
x
) =
z
A
f
(
z
,
v
)
x
:
A
(
x
)?Void
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(9steps total)
PrintForm
Definitions
mb
event
system
5
Sections
EventSystems
Doc
T
f(s(x),v) 
x : A(x)?Void
