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 ||H|| in
             eval hnum in
             eval hyp H[hnum] in
                        mFOatomic(P,vars) "stopped on 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 new-mFO-var([G H]) in
                             <existsE on hnum with j, [eliminate <j, stop(k)>]>

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 then else fi  eq_atom: =a y let: let apply: a lambda: λx.A[x] spread: spread def pair: <a, b> inr: inr  inl: inl x subtract: m add: 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
                                                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