Nuprl Definition : ex-do-Intro

ex-do-Intro(exname; H; G; numhyps; val; fullevd) ==
  let F,M fullevd 
  in mFOL_ind(G;
              mFOatomic(P,vars) "should not happen??";
              mFOconnect(knd,A,B) _,__.if knd =a "imp"
                                           then let M' ←─ note-is-function(A;numhyps;M)
                                                in <impI, [<λM.(F modelEval(exname;M;numhyps)), M'>]>
              if knd =a "and" then <andI, [<λM.(fst((F M))), M>; <λM.(snd((F M))), M>]>
              if knd =a "or"
                then case val of inl(_) => <orI left, [<λM.outl(F M), M>]> inr(_) => <orI right, [<λM.outr(F M), M>]>
              else "funny connective??"
              fi ;
              mFOquant(isall,v,body) _.if isall
              then eval new-mFO-var(H) in
                   <allI with m, [<λM.(F m), M>]>
              else eval fst(val) in
                   <existsI with j, [<λM.(snd((F M))), M>]>

Definitions occuring in Statement :  note-is-function: note-is-function(A;hnum;M) modelEval: modelEval(exname;M;n) new-mFO-var: new-mFO-var(H) mRuleorI: mRuleorI(left) mRuleexistsI: existsI with var mRuleallI: allI with var mRuleimpI: impI mRuleandI: andI mFOL_ind: mFOL_ind cons: [a b] nil: [] callbyvalueall: callbyvalueall callbyvalue: callbyvalue outr: outr(x) outl: outl(x) ifthenelse: if then else fi  eq_atom: =a y bfalse: ff btrue: tt pi1: fst(t) pi2: snd(t) apply: a lambda: λx.A[x] spread: spread def pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] token: "$token"
ex-do-Intro(exname;  H;  G;  numhyps;  val;  fullevd)  ==
    let  F,M  =  fullevd 
    in  mFOL\_ind(G;
                            mFOatomic(P,vars){}\mRightarrow{}  "should  not  happen??";
                            mFOconnect(knd,A,B){}\mRightarrow{}  $_{}$,\_$_{}$.if  knd  =a  "\000Cimp"
                                                                                  then  let  M'  \mleftarrow{}{}  note-is-function(A;numhyps;M)
                                                                                            in  <impI,  [<\mlambda{}M.(F  M  modelEval(exname;M;numhyps)),  M'>]\000C>
                            if  knd  =a  "and"  then  <andI,  [<\mlambda{}M.(fst((F  M))),  M>  <\mlambda{}M.(snd((F  M))),  M>]>
                            if  knd  =a  "or"
                                then  case  val
                                            of  inl($_{}$)  =>
                                            <orI  left,  [<\mlambda{}M.outl(F  M),  M>]>
                                            |  inr($_{}$)  =>
                                            <orI  right,  [<\mlambda{}M.outr(F  M),  M>]>
                            else  "funny  connective??"
                            fi  ;
                            mFOquant(isall,v,body){}\mRightarrow{}  $_{}$.if  isall
                            then  eval  m  =  new-mFO-var(H)  in
                                      <allI  with  m,  [<\mlambda{}M.(F  M  m),  M>]>
                            else  eval  j  =  fst(val)  in
                                      <existsI  with  j,  [<\mlambda{}M.(snd((F  M))),  M>]>
                            fi  ) 

Date html generated: 2015_07_17-AM-07_57_42
Last ObjectModification: 2014_06_12-PM-05_50_35

Home Index