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