Nuprl Definition : PiDataVal_ind

F((x) where  
F(id) = loc[id]  
F(id,name) = loc_tag[id; name]  
F(from,preList) = guards[from; preList]  
F(val,index) = msg[val; index]  
F(fire) = fire  
F(continue) = continue  
F(rndv1) = selex[rndv1]  
F(rndv2,counter) = request[rndv2; counter] ==
  case x
   of inl(x) =>
   loc[x]
   | inr(x) =>
   case x
    of inl(x) =>
    loc_tag[fst(x); snd(x)]
    | inr(x) =>
    case x
     of inl(x) =>
     guards[fst(x); snd(x)]
     | inr(x) =>
     case x
      of inl(x) =>
      msg[fst(x); snd(x)]
      | inr(x) =>
      case x
       of inl(x) =>
       fire
       | inr(x) =>
       case x of inl(x) => continue | inr(x) => case x of inl(x) => selex[x] | inr(x) => request[fst(x); snd(x)]


Definitions occuring in Statement :  pi1: fst(t),  pi2: snd(t),  decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases :  PiDataVal_ind PiDataVal_ind
Latex:
F((x)  where   
F(id)  =  loc[id]   
F(id,name)  =  loc$_{tag}$[id;  name]   
F(from,preList)  =  guards[from;  preList]   
F(val,index)  =  msg[val;  index]   
F(fire)  =  fire   
F(continue)  =  continue   
F(rndv1)  =  selex[rndv1]   
F(rndv2,counter)  =  request[rndv2;  counter]  ==
    case  x
      of  inl(x)  =>
      loc[x]
      |  inr(x)  =>
      case  x
        of  inl(x)  =>
        loc$_{tag}$[fst(x);  snd(x)]
        |  inr(x)  =>
        case  x
          of  inl(x)  =>
          guards[fst(x);  snd(x)]
          |  inr(x)  =>
          case  x
            of  inl(x)  =>
            msg[fst(x);  snd(x)]
            |  inr(x)  =>
            case  x
              of  inl(x)  =>
              fire
              |  inr(x)  =>
              case  x
                of  inl(x)  =>
                continue
                |  inr(x)  =>
                case  x  of  inl(x)  =>  selex[x]  |  inr(x)  =>  request[fst(x);  snd(x)]


Date html generated: 2015_07_23-AM-11_34_50
Last ObjectModification: 2012_08_30-PM-01_42_51

Home Index