Nuprl Definition : ci-or

ci1 ci2 ==
  let dd1,A,f ci1 in 
  let dd2,B,g ci2 in 
  mk_ci(es-decl-set-join(dd1;dd2);one_or_both(A;B);λx.oob-apply(λx.if es-info-loc(x) ∈b |dd1|
                                                                      ∧b es-info-kind(x) ∈ dom(da(dd1;es-info-loc(x)))
                                                                   then x
                                                                   else inr ⋅ 
                                                                   fi ;
                                                                λx.if es-info-loc(x) ∈b |dd2|
                                                                      ∧b es-info-kind(x) ∈ dom(da(dd2;es-info-loc(x)))
                                                                   then x
                                                                   else inr ⋅ 
                                                                   fi ;
                                                                x))



Definitions occuring in Statement :  mk_ci: mk_ci(dd;T;f) id-deq: IdDeq deq-member: x ∈b L band: p ∧b q ifthenelse: if then else fi  it: spreadn: spread3 apply: a lambda: λx.A[x] inr: inr  one_or_both: one_or_both(A;B)
FDL editor aliases :  ci-or ci-or

Latex:
ci1  |  ci2  ==
    let  dd1,A,f  =  ci1  in 
    let  dd2,B,g  =  ci2  in 
    mk\_ci(es-decl-set-join(dd1;dd2);one\_or\_both(A;B);
                \mlambda{}x.oob-apply(\mlambda{}x.if  es-info-loc(x)  \mmember{}\msubb{}  |dd1|  \mwedge{}\msubb{}  es-info-kind(x)  \mmember{}  dom(da(dd1;es-info-loc(x)))
                                                then  f  x
                                                else  inr  \mcdot{} 
                                                fi  ;
                                          \mlambda{}x.if  es-info-loc(x)  \mmember{}\msubb{}  |dd2|  \mwedge{}\msubb{}  es-info-kind(x)  \mmember{}  dom(da(dd2;es-info-loc(x)))
                                                then  g  x
                                                else  inr  \mcdot{} 
                                                fi  ;
                                          x))



Date html generated: 2016_05_16-AM-10_05_50
Last ObjectModification: 2013_03_25-PM-01_54_13

Theory : new!event-ordering


Home Index