Nuprl Definition : wfterm-accum

wfterm-accum(param;t)
p,vrs,v.varcase[p;
                vrs;
                v]
prm,vs,f,L.m[prm;
             vs;
             f;
             L]
p0,ws,op,sofar,bt.nextp[p0;
                        ws;
                        op;
                        sofar;
                        bt] ==
  hered-term-accum(p,vs,v.varcase[p;
                                  vs;
                                  v];
                   prm,vs,f,L.m[prm;
                                vs;
                                f;
                                L];
                   p0,ws,op,sofar,bt.nextp[p0;
                                           ws;
                                           op;
                                           sofar;
                                           bt];
                   param;
                   <[], t>)

Definitions occuring in Statement : hered-term-accum: hered-term-accum, nil: [], pair: <a, b>
Definitions occuring in definition : hered-term-accum: hered-term-accum, pair: <a, b>, nil: []
FDL editor aliases : wfterm-accum

Latex:
wfterm-accum(param;t) p,vrs,v.varcase[p; vrs; v] prm,vs,f,L.m[prm; vs; f; L] p0,ws,op,sofar,bt.nextp[p0; ws; op; sofar; bt] == hered-term-accum(p,vs,v.varcase[p; vs; v]; prm,vs,f,L.m[prm; vs; f; L]; p0,ws,op,sofar,bt.nextp[p0; ws; op; sofar; bt]; param; <[], t>) Date html generated: 2020_05_19-PM-09_58_46 Last ObjectModification: 2020_03_11-PM-04_23_12 Theory : terms Home Index