Nuprl Definition : uniform-evd-proof-checks
uniform-evd-proof-checks(sequent;fullevd) ==
fix((λuniform-evd-proof-checks,sequent,fullevd. let rule,subevd = full-evd-proof-step:
sequent;
fullevd
in let sr ←─ <sequent, rule>
in case mFOLeffect(sr)
of inl(L) =>
let subgoals ←─ L
in eval n = ||subgoals|| in
(∀i∈upto(n).uniform-evd-proof-checks subgoals[i] subevd[i])_b
| inr(z) =>
ff))
sequent
fullevd
Definitions occuring in Statement :
full-evd-proof-step: full-evd-proof-step,
mFOLeffect: mFOLeffect(sr),
bl-all: (∀x∈L.P[x])_b,
upto: upto(n),
select: L[n],
length: ||as||,
callbyvalueall: callbyvalueall,
callbyvalue: callbyvalue,
bfalse: ff,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases :
uniform-evd-proof-checks
uniform-evd-proof-checks(sequent;fullevd) ==
fix((\mlambda{}uniform-evd-proof-checks,sequent,fullevd. let rule,subevd = full-evd-proof-step:
sequent;
fullevd
in let sr \mleftarrow{}{} <sequent, rule>
in case mFOLeffect(sr)
of inl(L) =>
let subgoals \mleftarrow{}{} L
in eval n = ||subgoals|| in
(\mforall{}i\mmember{}upto(n).uniform-evd-proof-checks
subgoals[i]
subevd[i])\_b
| inr(z) =>
ff))
sequent
fullevd
Date html generated:
2015_07_17-AM-07_57_27
Last ObjectModification:
2012_12_07-AM-00_12_45
Home
Index