(5steps total)
PrintForm
Definitions
Lemmas
mb
event
system
4
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-join-is-empty
1
1
1.
A
: Type
2. EqDecider(
A
)
3.
d1
:
A
List
(||filter(
a
.true
;
d1
)||=
0) = (||
d1
||=
0)
By:
RWO
Thm*
P
:(
T
),
L
:
T
List. (
x
L
.
P
(
x
))
(filter(
P
;
L
) ~
L
) 0
Generated subgoal:
1
(
x
d1
.(
a
.true
)(
x
))
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
Lemmas
mb
event
system
4
Sections
EventSystems
Doc
(||filter(
a.true
;d1)||=
P:(T
), L:T List. (
L.P(x)) 
(filter(P;L) ~ L) 0
