Nuprl Definition : ex-do-Elim
ex-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)⇒ <hyp, []>;
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then let M' ←─ note-is-function(B;numhyps;M[m:= λx.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' ←─ note-is-function(A;numhyps + 1;note-is-function(B;numhyps;M[m:= <numhyps
+ 1,numhyps>]))
in <andE on hnum, [<F, M'>]>
if knd =a "or"
then let M1 ←─ note-is-function(A;numhyps;M[m:= inl(numhyps)])
in let M2 ←─ note-is-function(B;numhyps;M[m:= inr(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' ←─ note-is-function(body;numhyps;M[m(a) :=numhyps])
in <allE on hnum with a, [<F, M'>]>?exname:m'.ex-do-Elim(exname;H;G;numhyps;m';fullevd)
else eval j = new-mFO-var([G / H]) in
let M' ←─ note-is-function(body;numhyps;M[m:= <dj,numhyps>])
in <existsE on hnum with j, [<F, M'>]>
fi )
ex-do-Elim(exname;H;G;numhyps;m';fullevd) ==
fix((λex-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)⇒ <hyp, []>;
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then let M' ←─
note-is-function(B;numhyps;M[m:= λx.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' ←─ note-is-function(A;numhyps
+ 1;note-is-function(B;numhyps;M[m:= <numhyps + 1,numhyps>]))
in <andE on hnum, [<F, M'>]>
if knd =a "or"
then let M1 ←─ note-is-function(A;numhyps;M[m:= inl(numhyps)])
in let M2 ←─ note-is-function(B;numhyps;M[m:= inr(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' ←─ note-is-function(body;numhyps;M[m(a) :=numhyps])
in <allE on hnum with a, [<F, M'>]>?exname:m'.ex-do-Elim m'
else eval j = new-mFO-var([G / H]) in
let M' ←─ note-is-function(body;numhyps;M[m:= <dj,numhyps>])
in <existsE on hnum with j, [<F, M'>]>
fi ) ))
m'
Definitions occuring in Statement :
note-is-function: note-is-function(A;hnum;M),
modelUpdate: M[fnum(x) :=n],
modelAdd: M[n:= lbl,i,j],
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,
mRulehyp: hyp,
mFOL_ind: mFOL_ind,
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>,
subtract: n - m,
add: n + m,
natural_number: $n,
token: "$token"
FDL editor aliases :
ex-do-Elim
Latex:
ex-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{} <hyp, []>
mFOconnect(knd,A,B){}\mRightarrow{} $_{}$,\_$_{}$.if knd \000C=a "imp"
then let M' \mleftarrow{}{}
note-is-function(B;numhyps;M[m:= \mlambda{}x.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 exception
(<exname, e>
)
fi
otherwise exception(<exname
, e
>)
, M
>
<F, M'>]
>
if knd =a "and"
then let M' \mleftarrow{}{} note-is-function(A;numhyps
+ 1;note-is-function(B;numhyps;M[m:= <numhyps + 1,numhyps>]))
in <andE on hnum, [<F, M'>]>
if knd =a "or"
then let M1 \mleftarrow{}{} note-is-function(A;numhyps;M[m:= inl(numhyps)])
in let M2 \mleftarrow{}{} note-is-function(B;numhyps;M[m:= inr(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{}{} note-is-function(body;numhyps;M[m(a) :=numhyps])
in <allE on hnum with a
, [<F, M'>]
>?exname:m'.ex-do-Elim(exname;H;G;numhyps;m';fullevd)
else eval j = new-mFO-var([G / H]) in
let M' \mleftarrow{}{} note-is-function(body;numhyps;M[m:= <dj,numhyps>])
in <existsE on hnum with j, [<F, M'>]>
fi )
ex-do-Elim(exname;H;G;numhyps;m';fullevd) ==
fix((\mlambda{}ex-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{} <hyp, []>
mFOconnect(knd,A,B){}\mRightarrow{} $_{}$,\_$_{\000C}$.if knd =a "imp"
then let M' \mleftarrow{}{}
note-is-function(B;numhyps;...)
in <impE on hnum
, [<\mlambda{}M.F M?exname:e....
, M
>
<F, M'>]
>
if knd =a "and"
then let M' \mleftarrow{}{} note-is-function(A;numhyps
+ 1;note-is-function(B;numhyps;M[m:= <numhyps
+ 1,numhyps>]))
in <andE on hnum, [<F, M'>]>
if knd =a "or"
then let M1 \mleftarrow{}{} note-is-function(A;numhyps;M[m:= inl(numhyps)])
in let M2 \mleftarrow{}{}
note-is-function(B;numhyps;M[m:= inr(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{}{} note-is-function(body;numhyps;M[m(a) :=numhyps])
in <allE on hnum with a, [<F, M'>]>?exname:m'.ex-do-Elim m'
else eval j = new-mFO-var([G / H]) in
let M' \mleftarrow{}{}
note-is-function(body;numhyps;M[m:= <dj,numhyps>])
in <existsE on hnum with j, [<F, M'>]>
fi ) ))
m'
Date html generated:
2015_07_17-AM-07_57_44
Last ObjectModification:
2015_03_25-AM-10_45_27
Home
Index