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