Nuprl Definition : full-evd-proof-step

fullevd ==
  let H,G sequent 
  in let evd,eliminated,model fullevd in 
     (if compute-in-context(eliminated;model;evd) is stopped at f,n then
     if eq_term(f; λx.x) then <hyp, []> else do-elimination-step(H; G; eliminated; model; evd; f; n) fi 
     otherwise evd.let incurrent = λe.<e, eliminated, model> in
                       if evd is pair
                       then let left,right evd 
                            in if mFOconnect?(G) ∧b mFOconnect-knd(G) =a "and"
                               then <andI, [incurrent left; incurrent right]>
                               else (if compute-in-context(eliminated;model;left) is stopped at f,n then
                                    do-elimination-step(H; G; eliminated; model; evd; f; n)
                                    otherwise w.<existsI with w, [incurrent right]>)
                               fi  otherwise if evd is lambda then if mFOconnect?(G) ∧b mFOconnect-knd(G) =a "imp"
                                             then eval ||H|| in
                                                  <impI, [incurrent (evd stop(k))]>
                                             else eval new-mFO-var(H) in
                                                  <allI with new-mFO-var(H), [incurrent (evd m)]>
                                             fi  otherwise if evd is inl then <orI left, [incurrent outl(evd)]>
                                                           else if evd is inr then <orI right, [incurrent outr(evd)]>
                                                                else "can't happen if evd is correct")

Definitions occuring in Statement :  do-elimination-step: do-elimination-step(H; G; eliminated; model; evd; f; n) compute-in-context: compute-in-context(constants;functions;t) new-mFO-var: new-mFO-var(H) mRulehyp: hyp mRuleorI: mRuleorI(left) mRuleexistsI: existsI with var mRuleallI: allI with var mRuleimpI: impI mRuleandI: andI mFOconnect-knd: mFOconnect-knd(v) mFOconnect?: mFOconnect?(v) length: ||as|| cons: [a b] nil: [] band: p ∧b q callbyvalue: callbyvalue outr: outr(x) outl: outl(x) ifthenelse: if then else fi  eq_atom: =a y bfalse: ff btrue: tt let: let spreadn: spread3 ispair: if is pair then otherwise b islambda: if is lambda then otherwise b isinr: isinr def isinl: isinl def apply: a lambda: λx.A[x] spread: spread def pair: <a, b> token: "$token"
FDL editor aliases :  full-evd-proof-step
fullevd  ==
    let  H,G  =  sequent 
    in  let  evd,eliminated,model  =  fullevd  in 
          (if  compute-in-context(eliminated;model;evd)  is  stopped  at  f,n  then
          if  eq\_term(f;  \mlambda{}x.x)
          then  <hyp,  []>
          else  do-elimination-step(H;  G;  eliminated;  model;  evd;  f;  n)
          otherwise  evd.let  incurrent  =  \mlambda{}e.<e,  eliminated,  model>  in
                                              if  evd  is  a  pair
                                              then  let  left,right  =  evd 
                                                        in  if  mFOconnect?(G)  \mwedge{}\msubb{}  mFOconnect-knd(G)  =a  "and"
                                                              then  <andI,  [incurrent  left;  incurrent  right]>
                                                              else  (if  compute-in-context(...;model;left)  is  stopped  at  f,n  then
                                                                        do-elimination-step(H;  G;  eliminated;  model;  evd;  f;  n)
                                                                        otherwise  w.<existsI  with  w,  [incurrent  right]>)
                                              otherwise  if  evd  is  lambda  then  if  mFOconnect?(G)
                                                                                                                    \mwedge{}\msubb{}  mFOconnect-knd(G)  =a  "imp"
                                                                  then  eval  k  =  ||H||  in
                                                                            <impI,  [incurrent  (evd  stop(k))]>
                                                                  else  eval  m  =  new-mFO-var(H)  in
                                                                            <allI  with  new-mFO-var(H),  [incurrent  (evd  m)]>
                                                                  fi    otherwise  if  evd  is  inl  then  <orI  left,  [incurrent  outl(evd)]>
                                                                                              else  if  evd  is  inr  then  <orI  right
                                                                                                                                              ,  [incurrent  outr(evd)]
                                                                                                        else  "can't  happen  if  evd  is  correct")

Date html generated: 2015_07_17-AM-07_57_25
Last ObjectModification: 2012_12_06-PM-09_00_33

Home Index