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

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

origin