---

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

---

Definitions :  spread: spread def,  int_eq: if a=b  then c  else d,  atom_eq: atomeqn def,  inl: inl x ,  inr: inr x ,  lambda: x.A[x],  axiom: Ax
FDL editor aliases :  deq-runEvents-witness

---

deq-runEvents-witness()  ==
    \mlambda{}e1,e2.
      let  a,x1  =  e1  in
          let  a1,y1  =  e2  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: 2010_08_27-PM-06_16_46
Last ObjectModification: 2010_04_29-PM-11_09_28

Home Index