Nuprl Definition : full-evd-proof-step

full-evd-proof-step:
sequent;
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 a 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 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")


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 b then t else f fi ,  eq_atom: x =a y,  bfalse: ff,  btrue: tt,  let: let,  spreadn: spread3,  ispair: if z is a pair then a otherwise b,  islambda: if z is lambda then a otherwise b,  isinr: isinr def,  isinl: isinl def,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  token: "$token"
FDL editor aliases :  full-evd-proof-step
full-evd-proof-step:
sequent;
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)
          fi 
          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]>)
                                                              fi 
                                              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