Nuprl Definition : ex-evd-proof
ex-evd-proof(exname;sequent;F)
==r let rule,subevd = ex-evd-proof-step(exname; sequent; F)
in let sr ←─ <sequent, rule>
in let subgoals ←─ outl(mFOLeffect(sr))
in eval n = ||subgoals|| in
<sr, map(λi.ex-evd-proof(exname;subgoals[i];subevd[i]);upto(n))>
ex-evd-proof(exname;sequent;F) ==
fix((λex-evd-proof,sequent,F. let rule,subevd = ex-evd-proof-step(exname; sequent; F)
in let sr ←─ <sequent, rule>
in let subgoals ←─ outl(mFOLeffect(sr))
in eval n = ||subgoals|| in
<sr, map(λi.(ex-evd-proof subgoals[i] subevd[i]);upto(n))>))
sequent
F
Definitions occuring in Statement :
ex-evd-proof-step: ex-evd-proof-step(exname; sequent; fullevd),
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 :
ex-evd-proof
Latex:
ex-evd-proof(exname;sequent;F)
==r let rule,subevd = ex-evd-proof-step(exname; sequent; F)
in let sr \mleftarrow{}{} <sequent, rule>
in let subgoals \mleftarrow{}{} outl(mFOLeffect(sr))
in eval n = ||subgoals|| in
<sr, map(\mlambda{}i.ex-evd-proof(exname;subgoals[i];subevd[i]);upto(n))>
ex-evd-proof(exname;sequent;F) ==
fix((\mlambda{}ex-evd-proof,sequent,F. let rule,subevd = ex-evd-proof-step(exname; sequent; F)
in let sr \mleftarrow{}{} <sequent, rule>
in let subgoals \mleftarrow{}{} outl(mFOLeffect(sr))
in eval n = ||subgoals|| in
<sr, map(\mlambda{}i.(ex-evd-proof subgoals[i] subevd[i]);upto(n))>)\000C)
sequent
F
Date html generated:
2015_07_17-AM-07_57_47
Last ObjectModification:
2014_06_12-PM-05_41_22
Home
Index