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