Nuprl Definition : fun-evd-proof
fun-evd-proof(exname;sequent;F)
==r let rule,subevd = fun-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.fun-evd-proof(exname;subgoals[i];subevd[i]);upto(n))
in <sr, L>
fun-evd-proof(exname;sequent;F) ==
fix((λfun-evd-proof,sequent,F. let rule,subevd = fun-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.(fun-evd-proof subgoals[i] subevd[i]);upto(n))
in <sr, L>))
sequent
F
Definitions occuring in Statement :
fun-evd-proof-step: fun-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 :
pair: <a, b>,
upto: upto(n),
select: L[n],
apply: f a,
lambda: λx.A[x],
map: map(f;as),
callbyvalueall: callbyvalueall,
length: ||as||,
callbyvalue: callbyvalue,
FOLeffect: FOLeffect(sr),
outl: outl(x),
fun-evd-proof-step: fun-evd-proof-step(exname;sequent;fullevd),
spread: spread def,
fix: fix(F)
FDL editor aliases :
fun-evd-proof
Latex:
fun-evd-proof(exname;sequent;F)
==r let rule,subevd = fun-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.fun-evd-proof(exname;subgoals[i];subevd[i]);upto(n))
in <sr, L>
Latex:
fun-evd-proof(exname;sequent;F) ==
fix((\mlambda{}fun-evd-proof,sequent,F. let rule,subevd = fun-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.(fun-evd-proof subgoals[i] subevd[i]);
upto(n))
in <sr, L>))
sequent
F
Date html generated:
2017_01_19-PM-02_32_25
Last ObjectModification:
2017_01_18-PM-06_42_27
Theory : minimal-first-order-logic
Home
Index