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 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: a spread: spread def
Definitions occuring in definition :  length: ||as|| spread: spread def callbyvalue: callbyvalue apply: 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