### 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