Nuprl Definition : ex-evd-proof-step
ex-evd-proof-step(exname; sequent; fullevd) ==
  let H,G = sequent 
  in eval numhyps = ||H|| in
     let F,M = fullevd 
     in eval v = F M in
        ex-do-Intro(exname; H; G; numhyps; v; fullevd)?exname:n.ex-do-Elim(exname;H;G;numhyps;n;fullevd)
Definitions occuring in Statement : 
ex-do-Elim: ex-do-Elim(exname;H;G;numhyps;m';fullevd)
, 
ex-do-Intro: ex-do-Intro(exname; H; G; numhyps; val; fullevd)
, 
length: ||as||
, 
callbyvalue: callbyvalue, 
apply: f a
, 
spread: spread def
Definitions occuring in definition : 
length: ||as||
, 
spread: spread def, 
callbyvalue: callbyvalue, 
apply: f a
, 
ex-do-Intro: ex-do-Intro(exname; H; G; numhyps; val; fullevd)
, 
ex-do-Elim: ex-do-Elim(exname;H;G;numhyps;m';fullevd)
Latex:
ex-evd-proof-step(exname;  sequent;  fullevd)  ==
    let  H,G  =  sequent 
    in  eval  numhyps  =  ||H||  in
          let  F,M  =  fullevd 
          in  eval  v  =  F  M  in
                ex-do-Intro(exname;  H;  G;  numhyps;  v;  fullevd
                                        )?exname:n.ex-do-Elim(exname;H;G;numhyps;n;fullevd)
Date html generated:
2016_05_15-PM-10_32_54
Last ObjectModification:
2016_02_04-PM-02_30_01
Theory : minimal-first-order-logic
Home
Index