Nuprl Definition : new-do-Elim

new-do-Elim(exname;H;G;numhyps;m';evd)
==r eval m = if m' is a pair then fst(m') otherwise m' in
    eval hnum = numhyps - m + 1 in
    eval hyp = H[hnum] in
      case(hyp)
      P(vars) => if deq-mFO() G P(vars) then <hyp, []> else <falseE on hnum, []> fi ;
      A knd B => if knd =a "imp"
                   then <impE on hnum
                        , [λM.evd M?exname:e.if e is a pair then let a,b = e

                                                                 in if (a =_z m) then b else exception(exname; e) fi

                                             otherwise exception(exname; e);

                           λM.(evd (λi.if (i =_z m) then λx.(M numhyps) else M i fi ))]

>

      if knd =a "and" then <andE on hnum, [λM.(evd (λi.if (i =_z m) then <M (numhyps + 1), M numhyps> else M i fi ))]>

      if knd =a "or"
        then <orE on hnum
             , [λM.(evd (λi.if (i =_z m) then inl (M numhyps) else M i fi ));
                λM.(evd (λi.if (i =_z m) then inr (M numhyps)  else M i fi ))]
             >
      else "funny connective??"
      fi ;
      isall v.body => if isall
      then eval a = snd(m') in
           <allE on hnum with a

           , [λM.(evd (λi.if (i =_z m) then λx.if (x =_z a) then M numhyps else M i x fi  else M i fi ))]

>?exname:m'.new-do-Elim(exname;H;G;numhyps;m';evd)
else eval j = new-mFO-var([G / H]) in

           <existsE on hnum with j, [λM.(evd (λi.if (i =_z m) then <j, M numhyps> else M i fi ))]>

fi

new-do-Elim(exname;H;G;numhyps;m';evd) ==
  fix((λnew-do-Elim,m'. eval m = if m' is a pair then fst(m') otherwise m' in
                        eval hnum = numhyps - m + 1 in
                        eval hyp = H[hnum] in
                          case(hyp)

                          P(vars) => if deq-mFO() G P(vars) then <hyp, []> else <falseE on hnum, []> fi ;

A knd B => if knd =a "imp"
then <impE on hnum

                                            , [λM.evd M?exname:e.if e is a pair then let a,b = e

                                                                                     in if (a =_z m)

                                                                                        then b

                                                                                        else exception(exname; e)

fi

                                                                 otherwise exception(exname; e);

                                               λM.(evd (λi.if (i =_z m) then λx.(M numhyps) else M i fi ))]

                                            >
                          if knd =a "and"
                            then <andE on hnum

                                 , [λM.(evd (λi.if (i =_z m) then <M (numhyps + 1), M numhyps> else M i fi ))]

                                 >
                          if knd =a "or"
                            then <orE on hnum

                                 , [λM.(evd (λi.if (i =_z m) then inl (M numhyps) else M i fi ));

                                    λM.(evd (λi.if (i =_z m) then inr (M numhyps)  else M i fi ))]

                                 >
                          else "funny connective??"
                          fi ;
                          isall v.body => if isall
                          then eval a = snd(m') in
                               <allE on hnum with a
                               , [λM.(evd

                                      (λi.if (i =_z m) then λx.if (x =_z a) then M numhyps else M i x fi  else M i fi ))]

>?exname:m'.new-do-Elim m'
else eval j = new-mFO-var([G / H]) in

                               <existsE on hnum with j, [λM.(evd (λi.if (i =_z m) then <j, M numhyps> else M i fi ))]>

fi ))
m'

Definitions occuring in Statement : new-mFO-var: new-mFO-var(H), fRulefalseE: falseE on hypnum, fRuleexistsE: existsE on hypnum with var, fRuleallE: allE on hypnum with var, fRuleimpE: impE on hypnum, fRuleorE: orE on hypnum, fRuleandE: andE on hypnum, fRulehyp: hyp, deq-mFO: deq-mFO(), mFOL_case: mFOL_case, mFOatomic: name(vars), select: L[n], cons: [a / b], nil: [], callbyvalue: callbyvalue, ifthenelse: if b then t else f fi , eq_atom: x =a y, eq_int: (i =_z j), pi1: fst(t), pi2: snd(t), ispair: if z is a pair then a otherwise b, apply: f a, fix: fix(F), 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"
Definitions occuring in definition : eq_int: (i =_z j), ifthenelse: if b then t else f fi , lambda: λx.A[x], apply: f a, cons: [a / b], fRuleallE: allE on hypnum with var, pair: <a, b>, pi2: snd(t), callbyvalue: callbyvalue, token: "$token", nil: [], inr: inr x , inl: inl x, fRuleorE: orE on hypnum, eq_atom: x =a y, natural_number: $n, add: n + m, fRuleandE: andE on hypnum, spread: spread def, ispair: if z is a pair then a otherwise b, fRuleimpE: impE on hypnum, fRulefalseE: falseE on hypnum, fRulehyp: hyp, mFOatomic: name(vars), deq-mFO: deq-mFO(), mFOL_case: mFOL_case, select: L[n], subtract: n - m, pi1: fst(t), fix: fix(F), new-mFO-var: new-mFO-var(H), fRuleexistsE: existsE on hypnum with var
FDL editor aliases : new-do-Elim

Latex:
new-do-Elim(exname;H;G;numhyps;m';evd) ==r eval m = if m' is a pair then fst(m') otherwise m' in eval hnum = numhyps - m + 1 in eval hyp = H[hnum] in case(hyp) P(vars) => if deq-mFO() G P(vars) then <hyp, []> else <falseE on hnum, []> fi ; A knd B => if knd =a "imp" then <impE on hnum , [\mlambda{}M.evd M?exname:e.if e is a pair then let a,b = e in if (a =\msubz{} m) then b else exception(exname; e) fi otherwise exception(exname; e); \mlambda{}M.(evd (\mlambda{}i.if (i =\msubz{} m) then \mlambda{}x.(M numhyps) else M i fi ))] > if knd =a "and" then <andE on hnum , [\mlambda{}M.(evd (\mlambda{}i.if (i =\msubz{} m) then <M (numhyps + 1), M numhyps> else M i fi ))] > if knd =a "or" then <orE on hnum , [\mlambda{}M.(evd (\mlambda{}i.if (i =\msubz{} m) then inl (M numhyps) else M i fi )); \mlambda{}M.(evd (\mlambda{}i.if (i =\msubz{} m) then inr (M numhyps) else M i fi ))] > else "funny connective??" fi ; isall v.body => if isall then eval a = snd(m') in <allE on hnum with a , [\mlambda{}M.(evd (\mlambda{}i.if (i =\msubz{} m) then \mlambda{}x.if (x =\msubz{} a) then M numhyps else M i x fi else M i fi ))] >?exname:m'.new-do-Elim(exname;H;G;numhyps;m';evd) else eval j = new-mFO-var([G / H]) in <existsE on hnum with j, [\mlambda{}M.(evd (\mlambda{}i.if (i =\msubz{} m) then <j, M numhyps> else M i fi ))]> fi

Latex:
new-do-Elim(exname;H;G;numhyps;m';evd) == fix((\mlambda{}new-do-Elim,m'. eval m = if m' is a pair then fst(m') otherwise m' in eval hnum = numhyps - m + 1 in eval hyp = H[hnum] in case(hyp) P(vars) => if deq-mFO() G P(vars) then <hyp, []> else <falseE on hnum, []> fi ; A knd B => if knd =a "imp" then <impE on hnum , [\mlambda{}M.evd M?exname:e.if e is a pair then let a,b = e in if (a =\msubz{} m) then b else exception(exname; e) fi otherwise exception(exname; e); \mlambda{}M.(evd (\mlambda{}i.if (i =\msubz{} m) then \mlambda{}x.(M numhyps) else M i fi ))] > if knd =a "and" then <andE on hnum , [\mlambda{}M.(evd (\mlambda{}i.if (i =\msubz{} m) then <M (numhyps + 1), M numhyps> else M i fi ))] > if knd =a "or" then <orE on hnum , [\mlambda{}M.(evd (\mlambda{}i.if (i =\msubz{} m) then inl (M numhyps) else M i fi )); \mlambda{}M.(evd (\mlambda{}i.if (i =\msubz{} m) then inr (M numhyps) else M i fi ))] > else "funny connective??" fi ; isall v.body => if isall then eval a = snd(m') in <allE on hnum with a , [\mlambda{}M.(evd (\mlambda{}i.if (i =\msubz{} m) then \mlambda{}x.if (x =\msubz{} a) then M numhyps else M i x fi else M i fi ))] >?exname:m'.new-do-Elim m' else eval j = new-mFO-var([G / H]) in <existsE on hnum with j , [\mlambda{}M.(evd (\mlambda{}i.if (i =\msubz{} m) then <j, M numhyps> else M i fi ))] > fi )) m' Date html generated: 2017_02_20-AM-10_57_07 Last ObjectModification: 2017_01_19-PM-04_49_03 Theory : minimal-first-order-logic Home Index