Nuprl Definition : new-do-Intro

new-do-Intro(exname;H;G;numhyps;val;evd) ==
  case(G)
  P(vars) => "should not happen??";
  A knd B => if knd =a "imp" then <impI, [λM.(evd M (M numhyps))]>
  if knd =a "and" then <andI, [λM.(fst((evd M))); λM.(snd((evd M)))]>
  if knd =a "or" then case val of inl(_) => <orI left, [λM.outl(evd M)]> | inr(_) => <orI right, [λM.outr(evd M)]>
  else "funny connective??"
  fi ;
  isall v.body => if isall
  then eval m = new-mFO-var(H) in
       <allI with m, [λM.(evd M m)]>
  else eval j = fst(val) in
       <existsI with j, [λM.(snd((evd M)))]>
  fi 


Definitions occuring in Statement :  new-mFO-var: new-mFO-var(H),  fRuleorI: fRuleorI(left),  fRuleexistsI: existsI with var,  fRuleallI: allI with var,  fRuleimpI: impI,  fRuleandI: andI,  mFOL_case: mFOL_case,  cons: [a / b],  nil: [],  callbyvalue: callbyvalue,  outr: outr(x),  outl: outl(x),  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  bfalse: ff,  btrue: tt,  pi1: fst(t),  pi2: snd(t),  apply: f a,  lambda: λx.A[x],  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  token: "$token"
Definitions occuring in definition :  mFOL_case: mFOL_case,  fRuleimpI: impI,  fRuleandI: andI,  eq_atom: x =a y,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  btrue: tt,  outl: outl(x),  fRuleorI: fRuleorI(left),  bfalse: ff,  outr: outr(x),  token: "$token",  ifthenelse: if b then t else f fi ,  new-mFO-var: new-mFO-var(H),  fRuleallI: allI with var,  callbyvalue: callbyvalue,  pi1: fst(t),  pair: <a, b>,  fRuleexistsI: existsI with var,  cons: [a / b],  lambda: λx.A[x],  pi2: snd(t),  apply: f a,  nil: []
FDL editor aliases :  new-do-Intro
Latex:
new-do-Intro(exname;H;G;numhyps;val;evd)  ==
    case(G)
    P(vars)  =>  "should  not  happen??";
    A  knd  B  =>  if  knd  =a  "imp"  then  <impI,  [\mlambda{}M.(evd  M  (M  numhyps))]>
    if  knd  =a  "and"  then  <andI,  [\mlambda{}M.(fst((evd  M)));  \mlambda{}M.(snd((evd  M)))]>
    if  knd  =a  "or"
        then  case  val  of  inl($_{}$)  =>  <orI  left,  [\mlambda{}M.outl(evd  M)]>  |  inr($_\000C{}$)  =>  <orI  right,  [\mlambda{}M.outr(evd  M)]>
    else  "funny  connective??"
    fi  ;
    isall  v.body  =>  if  isall
    then  eval  m  =  new-mFO-var(H)  in
              <allI  with  m,  [\mlambda{}M.(evd  M  m)]>
    else  eval  j  =  fst(val)  in
              <existsI  with  j,  [\mlambda{}M.(snd((evd  M)))]>
    fi 


Date html generated: 2017_02_20-AM-10_57_02
Last ObjectModification: 2017_01_19-PM-04_47_52

Theory : minimal-first-order-logic


Home Index