Nuprl Definition : do-elimination-step

do-elimination-step(H; G; eliminated; model; evd; f; n) ==
  let incurrent = λe.<e, eliminated, model> in
      let m,a = elimination-step(H;eliminated;model;f;n) 
      in let eliminate = λt.<evd, [<m, t> / eliminated], model> in
             eval k = ||H|| in
             eval hnum = k - m + 1 in
             eval hyp = H[hnum] in
               mFOL_ind(hyp;
                        mFOatomic(P,vars)⇒ "stopped on a atomic hyp??";
                        mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
                                                     then <impE on hnum, [incurrent a; eliminate (λx.stop(k))]>
                        if knd =a "and" then <andE on hnum, [eliminate <stop(k + 1), stop(k)>]>
                        if knd =a "or" then <orE on hnum, [eliminate (inl stop(k)); eliminate (inr stop(k) )]>
                        else "funny connective??"
                        fi ;
                        mFOquant(isall,v,body)⇒ _.if isall
                        then eval model' = update-alist(IntDeq;model;m;[<a, stop(k)>];table.[<a, stop(k)> / table]) in
                             <allE on hnum with a, [<evd, eliminated, model'>]>
                        else eval j = new-mFO-var([G / H]) in
                             <existsE on hnum with j, [eliminate <j, stop(k)>]>
                        fi ) 


Definitions occuring in Statement :  elimination-step: elimination-step(H;eliminated;model;f;n),  new-mFO-var: new-mFO-var(H),  mRuleexistsE: existsE on hypnum with var,  mRuleallE: allE on hypnum with var,  mRuleimpE: impE on hypnum,  mRuleorE: orE on hypnum,  mRuleandE: andE on hypnum,  mFOL_ind: mFOL_ind,  update-alist: update-alist(eq;L;x;z;v.f[v]),  int-deq: IntDeq,  select: L[n],  length: ||as||,  cons: [a / b],  nil: [],  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  let: let,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  inr: inr x ,  inl: inl x,  subtract: n - m,  add: n + m,  natural_number: $n,  token: "$token"
do-elimination-step(H;  G;  eliminated;  model;  evd;  f;  n)  ==
    let  incurrent  =  \mlambda{}e.<e,  eliminated,  model>  in
            let  m,a  =  elimination-step(H;eliminated;model;f;n) 
            in  let  eliminate  =  \mlambda{}t.<evd,  [<m,  t>  /  eliminated],  model>  in
                          eval  k  =  ||H||  in
                          eval  hnum  =  k  -  m  +  1  in
                          eval  hyp  =  H[hnum]  in
                              mFOL\_ind(hyp;
                                                mFOatomic(P,vars){}\mRightarrow{}  "stopped  on  a  atomic  hyp??";
                                                mFOconnect(knd,A,B){}\mRightarrow{}  $_{}$,\_$_{}$.i\000Cf  knd  =a  "imp"
                                                                                                      then  <impE  on  hnum
                                                                                                                ,  [incurrent  a;  eliminate  (\mlambda{}x.stop(k))]
                                                                                                                >
                                                if  knd  =a  "and"  then  <andE  on  hnum,  [eliminate  <stop(k  +  1),  stop(k)>]>
                                                if  knd  =a  "or"
                                                    then  <orE  on  hnum,  [eliminate  (inl  stop(k));  eliminate  (inr  stop(k)  )]>
                                                else  "funny  connective??"
                                                fi  ;
                                                mFOquant(isall,v,body){}\mRightarrow{}  $_{}$.if  isall
                                                then  eval  model'  =  update-alist(IntDeq;model;m;[<a,  stop(k)>];table.[<a,  sto\000Cp(k)>  /  table])  in
                                                          <allE  on  hnum  with  a,  [<evd,  eliminated,  model'>]>
                                                else  eval  j  =  new-mFO-var([G  /  H])  in
                                                          <existsE  on  hnum  with  j,  [eliminate  <j,  stop(k)>]>
                                                fi  ) 


Date html generated: 2015_07_17-AM-07_57_24
Last ObjectModification: 2012_12_06-PM-08_59_58

Home Index