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(FOLeffect(sr))
in eval n = ||subgoals|| in
let L ⟵ map(λi.ex-evd-proof(exname;subgoals[i];subevd[i]);upto(n))
in <sr, L>
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(FOLeffect(sr))
in eval n = ||subgoals|| in
let L ⟵ map(λi.(ex-evd-proof subgoals[i] subevd[i]);upto(n))
in <sr, L>))
sequent
F
Definitions occuring in Statement :
ex-evd-proof-step: ex-evd-proof-step(exname; sequent; fullevd),
FOLeffect: FOLeffect(sr),
upto: upto(n),
select: L[n],
length: ||as||,
map: map(f;as),
callbyvalueall: callbyvalueall,
callbyvalue: callbyvalue,
outl: outl(x),
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>
Definitions occuring in definition :
fix: fix(F),
spread: spread def,
ex-evd-proof-step: ex-evd-proof-step(exname; sequent; fullevd),
outl: outl(x),
FOLeffect: FOLeffect(sr),
callbyvalue: callbyvalue,
length: ||as||,
callbyvalueall: callbyvalueall,
map: map(f;as),
lambda: λx.A[x],
apply: f a,
select: L[n],
upto: upto(n),
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(FOLeffect(sr))
in eval n = ||subgoals|| in
let L \mleftarrow{}{} map(\mlambda{}i.ex-evd-proof(exname;subgoals[i];subevd[i]);upto(n))
in <sr, L>
Latex:
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(FOLeffect(sr))
in eval n = ||subgoals|| in
let L \mleftarrow{}{} map(\mlambda{}i.(ex-evd-proof subgoals[i] subevd[i]);
upto(n))
in <sr, L>))
sequent
F
Date html generated:
2016_05_15-PM-10_33_06
Last ObjectModification:
2015_09_25-PM-03_57_51
Theory : minimal-first-order-logic
Home
Index