(4steps 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:
ma-single-pre-init1
wf
1
1.
T
: Type
2.
T'
: Type
3.
x
: Id
4.
T
5. Id
6.
P
:
T
T'
Prop
7.
s
: State(
x
:
T
)
(
v
.
P
(
s
(
x
),
v
))
T'
Prop
By:
GenConcl (
s
(
x
) =
z
) THEN Try (Complete Auto)
Generated subgoal:
1
s
(
x
)
T
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
mb
event
system
6
Sections
EventSystems
Doc
T'
(
v.P(s(x),v)) 
T'
