(43steps total)
PrintForm
Definitions
Lemmas
mb
event
system
7
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
s-pre-init-rule1
1
1
1. Id
2. Id
3.
x
: Id
4.
A
: Type
5.
T
: Type
6.
A
7.
P
:
A
T
Prop
8.
s
: State(
x
:
A
)
(
v
.
P
(
s
(
x
),
v
))
T
Prop
By:
GenConcl (
s
(
x
) =
b
)
Generated subgoals:
1
s
(
x
)
A
2
steps
2
A
Type
Auto
3
9.
b
:
A
10.
s
(
x
) =
b
A
(
v
.
P
(
b
,
v
))
T
Prop
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(43steps total)
PrintForm
Definitions
Lemmas
mb
event
system
7
Sections
EventSystems
Doc
T
(
v.P(s(x),v)) 
T
