Nuprl Definition : Wcmp

Wcmp(A;a.B[a];leq) ==
  fix((λWcmp,leq,w1,w2. if leq
                       then let a,f = w1 
                            in ∀x:B[a]. ((f x) (Wcmp ff) w2)
                       else let a,f = w2 
                            in ∃x:B[a]. (w1 (Wcmp tt) (f x))
                       fi )) 
  leq


Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  bfalse: ff,  btrue: tt,  infix_ap: x f y,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  all: ∀x:A. B[x],  bfalse: ff,  spread: spread def,  exists: ∃x:A. B[x],  infix_ap: x f y,  btrue: tt,  apply: f a
FDL editor aliases :  Wcmp
Latex:
Wcmp(A;a.B[a];leq)  ==
    fix((\mlambda{}Wcmp,leq,w1,w2.  if  leq
                                              then  let  a,f  =  w1 
                                                        in  \mforall{}x:B[a].  ((f  x)  (Wcmp  ff)  w2)
                                              else  let  a,f  =  w2 
                                                        in  \mexists{}x:B[a].  (w1  (Wcmp  tt)  (f  x))
                                              fi  )) 
    leq


Date html generated: 2016_05_14-AM-06_15_47
Last ObjectModification: 2015_09_22-PM-05_47_19

Theory : co-recursion


Home Index