Nuprl Definition : pi-guarded-trans

pi-guarded-trans(compList;g)
==r λl,serial,avoid,m. if pDVfire?(m)
                      then <pi-guarded-aux(compList;g) l serial avoid, make-lg([<l, mk-tagged("msg";pDVfire())>])>
                      else <pi-guarded-trans(compList;g) l serial avoid, make-lg([])>
                      fi 
pi-guarded-trans(compList;g) ==
  fix((λpi-guarded-trans,l,serial,avoid,m. if pDVfire?(m)
                                          then <pi-guarded-aux(compList;g) l serial avoid
                                               , make-lg([<l, mk-tagged("msg";pDVfire())>])
                                               >
                                          else <pi-guarded-trans l serial avoid, make-lg([])>
                                          fi ))


Definitions occuring in Statement :  pi-guarded-aux: pi-guarded-aux(compList;g),  pDVfire?: pDVfire?(x),  pDVfire: pDVfire(),  make-lg: make-lg(L),  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  pair: <a, b>,  token: "$token",  mk-tagged: mk-tagged(tg;x)
FDL editor aliases :  pi-guarded-trans
Latex:

pi-guarded-trans(compList;g)
==r  \mlambda{}l,serial,avoid,m.  if  pDVfire?(m)
                                            then  <pi-guarded-aux(compList;g)  l  serial  avoid
                                                      ,  make-lg([<l,  mk-tagged("msg";pDVfire())>])
                                                      >
                                            else  <pi-guarded-trans(compList;g)  l  serial  avoid,  make-lg([])>
                                            fi 

Latex:
pi-guarded-trans(compList;g)  ==
    fix((\mlambda{}pi-guarded-trans,l,serial,avoid,m.  if  pDVfire?(m)
                                                                                    then  <pi-guarded-aux(compList;g)  l  serial  avoid
                                                                                              ,  make-lg([<l,  mk-tagged("msg";pDVfire())>])
                                                                                              >
                                                                                    else  <pi-guarded-trans  l  serial  avoid,  make-lg([])>
                                                                                    fi  ))


Date html generated: 2015_07_23-AM-11_59_25
Last ObjectModification: 2013_10_04-AM-00_19_36

Home Index