Nuprl Definition : uniform-evd-proof
uniform-evd-proof(sequent;fullevd) ==
fix((λuniform-evd-proof,sequent,fullevd. let rule,subevd = full-evd-proof-step:
sequent;
fullevd
in let sr ←─ <sequent, rule>
in let subgoals ←─ outl(mFOLeffect(sr))
in eval n = ||subgoals|| in
<sr, map(λi.(uniform-evd-proof subgoals[i] subevd[i]);upto(n))>))
sequent
fullevd
Definitions occuring in Statement :
full-evd-proof-step: full-evd-proof-step,
mFOLeffect: mFOLeffect(sr),
upto: upto(n),
select: L[n],
map: map(f;as),
length: ||as||,
callbyvalueall: callbyvalueall,
callbyvalue: callbyvalue,
outl: outl(x),
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>
FDL editor aliases :
uniform-evd-proof
uniform-evd-proof(sequent;fullevd) ==
fix((\mlambda{}uniform-evd-proof,sequent,fullevd. let rule,subevd = full-evd-proof-step:
sequent;
fullevd
in let sr \mleftarrow{}{} <sequent, rule>
in let subgoals \mleftarrow{}{} outl(mFOLeffect(sr))
in eval n = ||subgoals|| in
<sr
, map(\mlambda{}i.(uniform-evd-proof subgoals[i]
subevd[i]);upto(n))
>))
sequent
fullevd
Date html generated:
2015_07_17-AM-07_57_28
Last ObjectModification:
2012_12_06-PM-10_36_16
Home
Index