Nuprl Definition : deq-runEvents-witness

deq-runEvents-witness() ==
  λe1,e2. let a,y1 = e2 
          in let a1,x1 = e1 
             in if a=a1  then if x1=2 y1 then inl Ax else (inr (λ%6.Ax) )  else (inr (λ%6.Ax) )


Definitions occuring in Statement :  atom_eq: atomeqn def,  int_eq: if a=b  then c  else d,  lambda: λx.A[x],  spread: spread def,  inr: inr x ,  inl: inl x,  axiom: Ax
FDL editor aliases :  deq-runEvents-witness
Latex:
deq-runEvents-witness()  ==
    \mlambda{}e1,e2.  let  a,y1  =  e2 
                    in  let  a1,x1  =  e1 
                          in  if  a=a1    then  if  x1=2  y1  then  inl  Ax  else  (inr  (\mlambda{}\%6.Ax)  )    else  (inr  (\mlambda{}\%6.Ax)  )


Date html generated: 2015_07_23-AM-11_10_56
Last ObjectModification: 2015_01_02-PM-03_40_12

Home Index