Nuprl Definition : rec-bind-df-program

rec-bind-df-program(A;B;dfpX;dfpY) ==
let Sx =

a.df-program-statetype(dfpX a) in
let Sy =

a.df-program-statetype(dfpY a) in
let Xinit =

a.(fst(snd(snd((dfpX a))))) in
let Yinit =

a.(fst(snd(snd((dfpY a))))) in
let Xnxt =

a.df-program-transition(dfpX a) in
let Ynxt =

a.df-program-transition(dfpY a) in

v.<B
      , rec-bind-df-statetype(A;Sx;Sy)
      , <v, rec-bind-df-init(Xinit;Yinit) v>
      , rec-bind-df-trans(Xinit;Yinit;Xnxt;Ynxt)>

Definitions occuring in Statement : rec-bind-df-trans: rec-bind-df-trans(Xinit;Yinit;Xnxt;Ynxt), rec-bind-df-init: rec-bind-df-init(ix;iy), rec-bind-df-statetype: rec-bind-df-statetype(A;Sx;Sy), df-program-transition: df-program-transition(dfp), df-program-statetype: df-program-statetype(dfp), let: let, pi1: fst(t), pi2: snd(t), apply: f a, lambda:

x.A[x], pair: <a, b>
FDL editor aliases : rec-bind-df-program rec-bind-df-program rec-bind-df-program

rec-bind-df-program(A;B;dfpX;dfpY) == let Sx = \mlambda{}a.df-program-statetype(dfpX a) in let Sy = \mlambda{}a.df-program-statetype(dfpY a) in let Xinit = \mlambda{}a.(fst(snd(snd((dfpX a))))) in let Yinit = \mlambda{}a.(fst(snd(snd((dfpY a))))) in let Xnxt = \mlambda{}a.df-program-transition(dfpX a) in let Ynxt = \mlambda{}a.df-program-transition(dfpY a) in \mlambda{}v.<B , rec-bind-df-statetype(A;Sx;Sy) , <v, rec-bind-df-init(Xinit;Yinit) v> , rec-bind-df-trans(Xinit;Yinit;Xnxt;Ynxt)> Date html generated: 2012_02_20-PM-02_43_29 Last ObjectModification: 2012_02_14-AM-01_03_48 Home Index