(2steps 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:
assert-w-eq-E
the_w
:World,
e
,
e'
:E.
e
=
e'
e
=
e'
By:
Unfolds [`w-E`;`w-eq-E`] 0 THEN RW assert_pushdownC -1
Generated subgoal:
1
1.
the_w
: World
2.
e
: {
p
:(Id
)|
isnull(a(1of(
p
);2of(
p
))) }
3.
e'
: {
p
:(Id
)|
isnull(a(1of(
p
);2of(
p
))) }
4. 1of(
e
) = 1of(
e'
)
5. 2of(
e
) = 2of(
e'
)
e
=
e'
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
mb
event
system
3
Sections
EventSystems
Doc
the_w:World, e,e':E. e = e' 
e = e' the_w:World, e,e':E. e = e' e = e'
)| 
isnull(a(1of(p);2of(p))) }
)| isnull(a(1of(p);2of(p))) }
e = e'
