Nuprl Definition : q-rel-decider
q-rel-decider(r;x) ==
if ((r =z 0) ∧b qeq(0;x)) ∨b((r =z 1) ∧b (qeq(0;x) ∨bqpositive(x))) ∨b(((¬b(r =z 0)) ∧b (¬b(r =z 1))) ∧b qpositive(x))
then inl ⋅
else inr (λx.⋅)
fi
Definitions occuring in Statement :
qpositive: qpositive(r),
qeq: qeq(r;s),
bor: p ∨bq,
band: p ∧b q,
bnot: ¬bb,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
it: ⋅,
lambda: λx.A[x],
inr: inr x ,
inl: inl x,
natural_number: $n
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
bor: p ∨bq,
qeq: qeq(r;s),
band: p ∧b q,
bnot: ¬bb,
eq_int: (i =z j),
natural_number: $n,
qpositive: qpositive(r),
inl: inl x,
inr: inr x ,
lambda: λx.A[x],
it: ⋅
FDL editor aliases :
q-rel-decider
Latex:
q-rel-decider(r;x) ==
if ((r =\msubz{} 0) \mwedge{}\msubb{} qeq(0;x))
\mvee{}\msubb{}((r =\msubz{} 1) \mwedge{}\msubb{} (qeq(0;x) \mvee{}\msubb{}qpositive(x)))
\mvee{}\msubb{}(((\mneg{}\msubb{}(r =\msubz{} 0)) \mwedge{}\msubb{} (\mneg{}\msubb{}(r =\msubz{} 1))) \mwedge{}\msubb{} qpositive(x))
then inl \mcdot{}
else inr (\mlambda{}x.\mcdot{})
fi
Date html generated:
2016_05_15-PM-11_17_50
Last ObjectModification:
2015_09_23-AM-08_28_16
Theory : rationals
Home
Index