Nuprl Definition : pi-new-trans

pi-new-trans(x;P;g)
==r λl,serial,avoid,m. if pDVfire?(m)
                      then let n = maybe-new-local(serial;x;avoid) in
                            let P' = pi-simple-subst(n;x;P) in
                            <g P' l serial avoid ∪ pi-names(P), make-lg([<l, mk-tagged("msg";pDVfire())>])>
                      else <pi-new-trans(x;P;g) l serial avoid, make-lg([])>
                      fi 
pi-new-trans(x;P;g) ==
  fix((λpi-new-trans,l,serial,avoid,m. if pDVfire?(m)
                                      then let n = maybe-new-local(serial;x;avoid) in
                                            let P' = pi-simple-subst(n;x;P) in
                                            <g P' l serial avoid ∪ pi-names(P), make-lg([<l, mk-tagged("msg";pDVfire())>\000C])>
                                      else <pi-new-trans l serial avoid, make-lg([])>
                                      fi ))


Definitions occuring in Statement :  maybe-new-local: maybe-new-local(me;s;avoid),  pDVfire?: pDVfire?(x),  pDVfire: pDVfire(),  pi-simple-subst: pi-simple-subst(t;x;P),  pi-names: pi-names(p),  make-lg: make-lg(L),  name-deq: NameDeq,  l-union: as ∪ bs,  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  let: let,  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-new-trans
Latex:

pi-new-trans(x;P;g)
==r  \mlambda{}l,serial,avoid,m.  if  pDVfire?(m)
                                            then  let  n  =  maybe-new-local(serial;x;avoid)  in
                                                        let  P'  =  pi-simple-subst(n;x;P)  in
                                                        <g  P'  l  serial  avoid  \mcup{}  pi-names(P)
                                                        ,  make-lg([<l,  mk-tagged("msg";pDVfire())>])
                                                        >
                                            else  <pi-new-trans(x;P;g)  l  serial  avoid,  make-lg([])>
                                            fi 

Latex:
pi-new-trans(x;P;g)  ==
    fix((\mlambda{}pi-new-trans,l,serial,avoid,m.  if  pDVfire?(m)
                                                                            then  let  n  =  maybe-new-local(serial;x;avoid)  in
                                                                                        let  P'  =  pi-simple-subst(n;x;P)  in
                                                                                        <g  P'  l  serial  avoid  \mcup{}  pi-names(P)
                                                                                        ,  make-lg([<l,  mk-tagged("msg";pDVfire())>])
                                                                                        >
                                                                            else  <pi-new-trans  l  serial  avoid,  make-lg([])>
                                                                            fi  ))


Date html generated: 2015_07_23-AM-11_59_12
Last ObjectModification: 2013_10_04-AM-01_35_06

Home Index