Nuprl Definition : chain_config_ind_cchead_compseq_tag_def 11,40
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

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

origin