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