Nuprl Definition : fun-do-Elim

fun-do-Elim(exname;H;G;numhyps;m';fullevd)
==r let F,M = fullevd
    in eval m = if m' is a pair then fst(m') otherwise m' in
       eval hnum = numhyps - m + 1 in
       eval hyp = H[hnum] in
         mFOL_ind(hyp;
                  mFOatomic(P,vars)⇒ if deq-mFO() G P(vars) then <hyp, []> else <falseE on hnum, []> fi ;
                  mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"

                                               then let M' ⟵ update-fun(M[m:= Md.λx.(Md numhyps)];B;numhyps)

                                                    in <impE on hnum

                                                       , [<λM.F 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
>;

                                                          <F, M'>]

>
if knd =a "and"

                    then let M' ⟵ update-fun(update-fun(M[m:= Md.<Md (numhyps + 1), Md numhyps>];B;numhyps);A;numhyps +\000C 1)

                         in <andE on hnum, [<F, M'>]>
                  if knd =a "or"
                    then let M1 ⟵ update-fun(M[m:= Md.inl (Md numhyps)];A;numhyps)

                         in let M2 ⟵ update-fun(M[m:= Md.inr (Md numhyps) ];B;numhyps)

                            in <orE on hnum, [<F, M1>; <F, M2>]>
                  else "funny connective??"
                  fi ;
                  mFOquant(isall,v,body)⇒ _.if isall
                  then eval a = snd(m') in
                       let M' ⟵ update-fun(M[m,a := Md.Md numhyps];body;numhyps)

                       in <allE on hnum with a, [<F, M'>]>?exname:m'.fun-do-Elim(exname;H;G;numhyps;m';fullevd)

                  else eval j = new-mFO-var([G / H]) in
                       let M' ⟵ update-fun(M[m:= Md.<j, Md numhyps>];body;numhyps)
                       in <existsE on hnum with j, [<F, M'>]>
                  fi )

fun-do-Elim(exname;H;G;numhyps;m';fullevd) ==
  fix((λfun-do-Elim,m'.
                       let F,M = fullevd
                       in eval m = if m' is a pair then fst(m') otherwise m' in
                          eval hnum = numhyps - m + 1 in
                          eval hyp = H[hnum] in
                            mFOL_ind(hyp;
                                     mFOatomic(P,vars)⇒ if deq-mFO() G P(vars)
                                     then <hyp, []>
                                     else <falseE on hnum, []>
                                     fi ;
                                     mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"

                                                                  then let M' ⟵

                                                                        update-fun(M[m:= Md.λx.(Md numhyps)];B;numhyps)

                                                                       in <impE on hnum

                                                                          , [<λM.F

                                                                                 M?exname:e.if e is a pair

                                                                                            then let a,b = e

                                                                                                 in if (a =_z m)

                                                                                                    then b

                                                                                                    else ...

fi

                                                                                            otherwise exception(...; e)

                                                                             , M

>;

                                                                             <F, M'>]

if knd =a "and"

                                       then let M' ⟵ update-fun(update-fun(M[m:= Md.<Md (numhyps + 1), Md numhyps>];B;n\000Cumhyps);A;numhyps + 1)

                                            in <andE on hnum, [<F, M'>]>

if knd =a "or"

                                       then let M1 ⟵ update-fun(M[m:= Md.inl (Md numhyps)];A;numhyps)

                                            in let M2 ⟵ update-fun(M[m:= Md.inr (Md numhyps) ];B;numhyps)

                                               in <orE on hnum, [<F, M1>; <F, M2>]>

                                     else "funny connective??"
                                     fi ;
                                     mFOquant(isall,v,body)⇒ _.if isall
                                     then eval a = snd(m') in

                                          let M' ⟵ update-fun(M[m,a := Md.Md numhyps];body;numhyps)

                                          in <allE on hnum with a, [<F, M'>]>?exname:m'.fun-do-Elim m'

else eval j = new-mFO-var([G / H]) in

                                          let M' ⟵ update-fun(M[m:= Md.<j, Md numhyps>];body;numhyps)

                                          in <existsE on hnum with j, [<F, M'>]>

fi ) ))
m'

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

Latex:
fun-do-Elim(exname;H;G;numhyps;m';fullevd) ==r let F,M = fullevd in eval m = if m' is a pair then fst(m') otherwise m' in eval hnum = numhyps - m + 1 in eval hyp = H[hnum] in mFOL\_ind(hyp; mFOatomic(P,vars){}\mRightarrow{} if deq-mFO() G P(vars) then <hyp, []> else <falseE on hnum, []> fi ; mFOconnect(knd,A,B){}\mRightarrow{} $_{}$,\_$_{}$.if knd \000C=a "imp" then let M' \mleftarrow{}{} update-fun(M[m:= Md.\mlambda{}x.(Md numhyps)];B;numhyps) in <impE on hnum , [<\mlambda{}M.F M?exname:e.if e is a pair then let a,b = e in if (a =\msubz{} m) then b else ... fi otherwise exception(...; e) , M > <F, M'>] > if knd =a "and" then let M' \mleftarrow{}{} update-fun(update-fun(M[m:= Md.<Md (numhyps + 1), Md numhyps>];B;\000Cnumhyps);A;numhyps + 1) in <andE on hnum, [<F, M'>]> if knd =a "or" then let M1 \mleftarrow{}{} update-fun(M[m:= Md.inl (Md numhyps)];A;numhyps) in let M2 \mleftarrow{}{} update-fun(M[m:= Md.inr (Md numhyps) ];B;numhyps) in <orE on hnum, [<F, M1> <F, M2>]> else "funny connective??" fi ; mFOquant(isall,v,body){}\mRightarrow{} $_{}$.if isall then eval a = snd(m') in let M' \mleftarrow{}{} update-fun(M[m,a := Md.Md numhyps];body;numhyps) in <allE on hnum with a , [<F, M'>] >?exname:m'.fun-do-Elim(exname;H;G;numhyps;m';fullevd) else eval j = new-mFO-var([G / H]) in let M' \mleftarrow{}{} update-fun(M[m:= Md.<j, Md numhyps>];body;numhyps) in <existsE on hnum with j, [<F, M'>]> fi )

Latex:
fun-do-Elim(exname;H;G;numhyps;m';fullevd) == fix((\mlambda{}fun-do-Elim,m'. let F,M = fullevd in eval m = if m' is a pair then fst(m') otherwise m' in eval hnum = numhyps - m + 1 in eval hyp = H[hnum] in mFOL\_ind(hyp; mFOatomic(P,vars){}\mRightarrow{} if deq-mFO() G P(vars) then <hyp, []> else <falseE on hnum, []> fi ; mFOconnect(knd,A,B){}\mRightarrow{} $_{}$,\_$_\mbackslash{}ff7\000Cb}$.if knd =a "imp" then let M' \mleftarrow{}{} update-fun(...;B;numhyps) in <impE on hnum , [<\mlambda{}M.F M?exname:e.... , M > <F, M'>] > if knd =a "and" then let M' \mleftarrow{}{} update-fun(update-fun(M[m:= Md.<Md (numhyps + 1) , Md numhyps >];B;numhyps);A\000C;numhyps + 1) in <andE on hnum, [<F, M'>]> if knd =a "or" then let M1 \mleftarrow{}{} update-fun(M[m:= Md.inl (Md numhyps)];A;numhyps) in let M2 \mleftarrow{}{} update-fun(M[m:= Md.inr (Md numhyps) ];B;numhyps) in <orE on hnum, [<F, M1> <F, M2>]> else "funny connective??" fi ; mFOquant(isall,v,body){}\mRightarrow{} $_{}$.if isall then eval a = snd(m') in let M' \mleftarrow{}{} update-fun(M[m,a := Md.Md numhyps];body;numhyps) in <allE on hnum with a, [<F, M'>]>?exname:m'.fun-do-Elim \000Cm' else eval j = new-mFO-var([G / H]) in let M' \mleftarrow{}{} update-fun(M[m:= Md.<j, Md numhyps>];body;numhyp\000Cs) in <existsE on hnum with j, [<F, M'>]> fi ) )) m' Date html generated: 2017_01_19-PM-02_32_17 Last ObjectModification: 2017_01_18-PM-06_38_11 Theory : minimal-first-order-logic Home Index