Nuprl Definition : elimination-step

elimination-step(H;eliminated;model;f;n) ==
  fix((λelimination-step,f,n. mFOL_ind(H[||H|| - n + 1];
                                       mFOatomic(P,vars)⇒ "stopped on a atomic hyp??";
                                       mFOconnect(knd,A,B)⇒ a,b.if knd =a "imp"

                                       then (if f (λx.stop(x)) is stopped at g,a then

<n, a>

                                            otherwise x.<n, "stopped on implies not applied??">)

                                       else <n, 0>
                                       fi ;
                                       mFOquant(isall,v,body)⇒ r.if isall

                                       then (if f (λx.stop(x)) is stopped at h,a then

                                            (if compute-in-context(eliminated;model;a) is stopped at g,m then

elimination-step g m
otherwise b.<n, b>)

                                            otherwise x.<n, "stopped on all not applied??">)

                                       else <n, 0>
                                       fi ) ))
  f
  n

Definitions occuring in Statement : compute-in-context: compute-in-context(constants;functions;t), mFOL_ind: mFOL_ind, select: L[n], length: ||as||, ifthenelse: if b then t else f fi , eq_atom: x =a y, apply: f a, fix: fix(F), lambda: λx.A[x], pair: <a, b>, subtract: n - m, add: n + m, natural_number: $n, token: "$token"
FDL editor aliases : elimination-step
elimination-step(H;eliminated;model;f;n) == fix((\mlambda{}elimination-step,f,n. mFOL\_ind(H[||H|| - n + 1]; mFOatomic(P,vars){}\mRightarrow{} "stopped on a atomic hyp??"; mFOconnect(knd,A,B){}\mRightarrow{} a,b.if knd =a "imp" then (if f (\mlambda{}x.stop(x)) is stopped at g,a then <n, a> otherwise x.<n, "stopped on implies not applied??">) else <n, 0> fi ; mFOquant(isall,v,body){}\mRightarrow{} r.if isall then (if f (\mlambda{}x.stop(x)) is stopped at h,a then (if compute-in-context(...;...;a) is stopped at g,m then elimination-step g m otherwise b.<n, b>) otherwise x.<n, "stopped on all not applied??">) else <n, 0> fi ) )) f n Date html generated: 2015_07_17-AM-07_57_22 Last ObjectModification: 2012_12_06-PM-05_40_15 Home Index