Nuprl Definition : chain_config_ind_cchead_compseq_tag_def
11,40
postcript
pdf
chain_config_ind_cchead{
chain
config
ind
cchead
compseq
tag
def
:ObjectId}
chain_config_ind_cchead
(
v11
,
v12
.
succ
(
v11
;
v12
);
v21
.
pred
(
v21
);
tail
;
head
)
== compseq(chain_config_ind(cchead();
head
;
tail
;
id
.
pred
(
id
);
id
,
num
.
succ
(
id
;
num
));
head
)
latex
Definitions
chain_config_ind(
x
;
head
;
tail
;
id
.
pred
(
id
);
id
,
num
.
succ
(
id
;
num
))
,
cchead()
origin