Nuprl Definition : probe
probe(H;exname) ==
eval numhyps = ||H|| in
λi.eval hnum = numhyps - i + 1 in
eval hyp = H[hnum] in
if (mFOconnect?(hyp) ∧b mFOconnect-knd(hyp) =a "imp") ∨b(mFOquant?(hyp) ∧b mFOquant-isall(hyp))
then λx.(exception(exname; <i, x>))
else exception(exname; i)
fi
Definitions occuring in Statement :
mFOquant-isall: mFOquant-isall(v),
mFOquant?: mFOquant?(v),
mFOconnect-knd: mFOconnect-knd(v),
mFOconnect?: mFOconnect?(v),
select: L[n],
length: ||as||,
bor: p ∨bq,
band: p ∧b q,
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
lambda: λx.A[x],
pair: <a, b>,
subtract: n - m,
add: n + m,
natural_number: $n,
token: "$token"
Definitions occuring in definition :
length: ||as||,
subtract: n - m,
add: n + m,
natural_number: $n,
callbyvalue: callbyvalue,
select: L[n],
ifthenelse: if b then t else f fi ,
bor: p ∨bq,
mFOconnect?: mFOconnect?(v),
eq_atom: x =a y,
mFOconnect-knd: mFOconnect-knd(v),
token: "$token",
band: p ∧b q,
mFOquant?: mFOquant?(v),
mFOquant-isall: mFOquant-isall(v),
lambda: λx.A[x],
pair: <a, b>
FDL editor aliases :
probe
Latex:
probe(H;exname) ==
eval numhyps = ||H|| in
\mlambda{}i.eval hnum = numhyps - i + 1 in
eval hyp = H[hnum] in
if (mFOconnect?(hyp) \mwedge{}\msubb{} mFOconnect-knd(hyp) =a "imp")
\mvee{}\msubb{}(mFOquant?(hyp) \mwedge{}\msubb{} mFOquant-isall(hyp))
then \mlambda{}x.(exception(exname; <i, x>))
else exception(exname; i)
fi
Date html generated:
2016_05_15-PM-10_33_33
Last ObjectModification:
2015_12_29-AM-11_34_45
Theory : minimal-first-order-logic
Home
Index