Nuprl Definition : ex-evd-proof-check
ex-evd-proof-check(exname;sequent;F)
==r let rule,subevd = ex-evd-proof-step(exname; sequent; F)
in let sr ←─ <sequent, rule>
in case mFOLeffect(sr)
of inl(subgoals) =>
eval n = ||subgoals|| in
(∀i∈upto(n).ex-evd-proof-check(exname;subgoals[i];subevd[i]))_b
| inr(z) =>
ff
ex-evd-proof-check(exname;sequent;F) ==
fix((λex-evd-proof-check,sequent,F. let rule,subevd = ex-evd-proof-step(exname; sequent; F)
in let sr ←─ <sequent, rule>
in case mFOLeffect(sr)
of inl(subgoals) =>
eval n = ||subgoals|| in
(∀i∈upto(n).ex-evd-proof-check subgoals[i] subevd[i])_b
| inr(z) =>
ff))
sequent
F
Definitions occuring in Statement :
ex-evd-proof-step: ex-evd-proof-step(exname; sequent; fullevd),
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 :
ex-evd-proof-check
Latex:
ex-evd-proof-check(exname;sequent;F)
==r let rule,subevd = ex-evd-proof-step(exname; sequent; F)
in let sr \mleftarrow{}{} <sequent, rule>
in case mFOLeffect(sr)
of inl(subgoals) =>
eval n = ||subgoals|| in
(\mforall{}i\mmember{}upto(n).ex-evd-proof-check(exname;subgoals[i];subevd[i]))\_b
| inr(z) =>
ff
ex-evd-proof-check(exname;sequent;F) ==
fix((\mlambda{}ex-evd-proof-check,sequent,F. let rule,subevd = ex-evd-proof-step(exname; sequent; F)
in let sr \mleftarrow{}{} <sequent, rule>
in case mFOLeffect(sr)
of inl(subgoals) =>
eval n = ||subgoals|| in
(\mforall{}i\mmember{}upto(n).ex-evd-proof-check subgoals[i] subevd[i])\_b
| inr(z) =>
ff))
sequent
F
Date html generated:
2015_07_17-AM-07_57_48
Last ObjectModification:
2014_06_12-PM-05_42_42
Home
Index