(3steps total)
PrintForm
Definitions
mb
event
system
3
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
w-act
wf
the_w
:World,
e
:E. act(
e
)
{
a
:Action(loc(
e
))|
isnull(
a
) }
By:
Unfolds [`w-E`;`w-act`;`w-loc`] 0
Generated subgoal:
1
1.
the_w
: World
2.
e
: {
p
:(Id
)|
isnull(a(1of(
p
);2of(
p
))) }
a(1of(
e
);2of(
e
))
{
a
:Action(1of(
e
))|
isnull(
a
) }
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
mb
event
system
3
Sections
EventSystems
Doc
the_w:World, e:E. act(e) 
{a:Action(loc(e))| 
isnull(a) } the_w:World, e:E. act(e) {a:Action(loc(e))| isnull(a) }
)| isnull(a(1of(p);2of(p))) }
a(1of(e);2of(e)) {a:Action(1of(e))| isnull(a) }
