Nuprl Definition : chain_config_ind_cctail_compseq_tag_def 11,40
chain_config_ind_cctail{chain config ind cctail compseq tag def:ObjectId}
chain_config_ind_cctail(v11,v12.succ(v11;v12); v21.pred(v21); tail; head)
== compseq(chain_config_ind(cctail();head;tail;id.pred(id);id,num.succ(id;num)); tail) 
latex

Definitionschain_config_ind(x;head;tail;id.pred(id);id,num.succ(id;num)), cctail()

origin