Nuprl Definition : mFOLeffect
The effect of a given rule r on a given mFOL sequent s.
If the rule does not apply, then it `fails` by producing the effect ⌜inr ⋅ ⌝
otherwise it succeeds and produces ⌜inl L⌝where L is the list of subgoal sequents.⋅
mFOLeffect(sr) ==
  let s,r = sr 
  in let hyps,concl = s 
     in case(r)
        andI => let a,b = dest-"and"(concl) in
                inl [<hyps, a> <hyps, b>]
        impI => let a,b = dest-"imp"(concl) in
                inl [<[a / hyps], b>]
        allI with v => if ¬bv ∈b mFOL-sequent-freevars(<hyps, concl>) then let x,b = dest-all(concl); in inl [<hyps, b[v\000C/x]>] else inr ⋅  fi 
        existsI with v => if v ∈b mFOL-sequent-freevars(<hyps, concl>) then let x,b = dest-exists(concl); in inl [<hyps,\000C b[v/x]>] else inr ⋅  fi 
        orI (left?x) => let a,b = dest-"or"(concl) in
                        inl [<hyps, if x then a else b fi >]
        hyp => if concl ∈b hyps then inl [] else inr ⋅  fi 
        andE @i => if i <z ||hyps|| then let a,b = dest-"and"(hyps[i]) in inl [<[a; [b / hyps]], concl>] else inr ⋅  fi 
        orE @i => if i <z ||hyps|| then let a,b = dest-"or"(hyps[i]) in inl [<[a / hyps], concl> <[b / hyps], concl>] e\000Clse inr ⋅  fi 
        impE @i => if i <z ||hyps|| then let a,b = dest-"imp"(hyps[i]) in inl [<hyps, a> <[b / hyps], concl>] else inr \000C⋅  fi 
        allE @i with v => if i <z ||hyps|| ∧b v ∈b mFOL-sequent-freevars(<hyps, concl>)
                          then let x,b = dest-all(hyps[i]); in
                                inl [<[b[v/x] / hyps], concl>]
                          else inr ⋅ 
                          fi 
        existsE @i with v => if i <z ||hyps|| ∧b (¬bv ∈b mFOL-sequent-freevars(<hyps, concl>))
                             then let x,b = dest-exists(hyps[i]); in
                                   inl [<[b[v/x] / hyps], concl>]
                             else inr ⋅ 
                             fi 
        falseE @i => inr ⋅ 
Definitions occuring in Statement : 
mFOL-sequent-freevars: mFOL-sequent-freevars(s)
, 
FOLRule_ind: FOLRule_ind, 
mFOL-subst: fmla[nw/old]
, 
deq-mFO: deq-mFO()
, 
mFO-dest-quantifier: mFO-dest-quantifier, 
mFO-dest-connective: mFO-dest-connective, 
select: L[n]
, 
length: ||as||
, 
deq-member: x ∈b L
, 
cons: [a / b]
, 
nil: []
, 
int-deq: IntDeq
, 
band: p ∧b q
, 
bnot: ¬bb
, 
ifthenelse: if b then t else f fi 
, 
lt_int: i <z j
, 
bfalse: ff
, 
btrue: tt
, 
it: ⋅
, 
spread: spread def, 
pair: <a, b>
, 
inr: inr x 
, 
inl: inl x
, 
token: "$token"
Definitions occuring in definition : 
cons: [a / b]
, 
pair: <a, b>
, 
inl: inl x
, 
token: "$token"
, 
select: L[n]
, 
mFO-dest-connective: mFO-dest-connective, 
length: ||as||
, 
lt_int: i <z j
, 
ifthenelse: if b then t else f fi 
, 
it: ⋅
, 
inr: inr x 
, 
nil: []
, 
deq-mFO: deq-mFO()
, 
deq-member: x ∈b L
, 
mFOL-subst: fmla[nw/old]
, 
bfalse: ff
, 
mFO-dest-quantifier: mFO-dest-quantifier, 
mFOL-sequent-freevars: mFOL-sequent-freevars(s)
, 
int-deq: IntDeq
, 
btrue: tt
, 
bnot: ¬bb
, 
FOLRule_ind: FOLRule_ind, 
spread: spread def, 
band: p ∧b q
FDL editor aliases : 
mFOLeffect
Latex:
mFOLeffect(sr)  ==
    let  s,r  =  sr 
    in  let  hyps,concl  =  s 
          in  case(r)
                andI  =>  let  a,b  =  dest-"and"(concl)  in
                                inl  [<hyps,  a>  <hyps,  b>]
                impI  =>  let  a,b  =  dest-"imp"(concl)  in
                                inl  [<[a  /  hyps],  b>]
                allI  with  v  =>  if  \mneg{}\msubb{}v  \mmember{}\msubb{}  mFOL-sequent-freevars(<hyps,  concl>)  then  let  x,b  =  dest-all(concl)\000C;  in  inl  [<hyps,  b[v/x]>]  else  inr  \mcdot{}    fi 
                existsI  with  v  =>  if  v  \mmember{}\msubb{}  mFOL-sequent-freevars(<hyps,  concl>)
                                                    then  let  x,b  =  dest-exists(concl);  in
                                                                inl  [<hyps,  b[v/x]>]
                                                    else  inr  \mcdot{} 
                                                    fi 
                orI  (left?x)  =>  let  a,b  =  dest-"or"(concl)  in
                                                inl  [<hyps,  if  x  then  a  else  b  fi  >]
                hyp  =>  if  concl  \mmember{}\msubb{}  hyps  then  inl  []  else  inr  \mcdot{}    fi 
                andE  @i  =>  if  i  <z  ||hyps||
                                      then  let  a,b  =  dest-"and"(hyps[i])  in
                                                inl  [<[a;  [b  /  hyps]],  concl>]
                                      else  inr  \mcdot{} 
                                      fi 
                orE  @i  =>  if  i  <z  ||hyps||
                                    then  let  a,b  =  dest-"or"(hyps[i])  in
                                              inl  [<[a  /  hyps],  concl>  <[b  /  hyps],  concl>]
                                    else  inr  \mcdot{} 
                                    fi 
                impE  @i  =>  if  i  <z  ||hyps||
                                      then  let  a,b  =  dest-"imp"(hyps[i])  in
                                                inl  [<hyps,  a>  <[b  /  hyps],  concl>]
                                      else  inr  \mcdot{} 
                                      fi 
                allE  @i  with  v  =>  if  i  <z  ||hyps||  \mwedge{}\msubb{}  v  \mmember{}\msubb{}  mFOL-sequent-freevars(<hyps,  concl>)
                                                    then  let  x,b  =  dest-all(hyps[i]);  in
                                                                inl  [<[b[v/x]  /  hyps],  concl>]
                                                    else  inr  \mcdot{} 
                                                    fi 
                existsE  @i  with  v  =>  if  i  <z  ||hyps||  \mwedge{}\msubb{}  (\mneg{}\msubb{}v  \mmember{}\msubb{}  mFOL-sequent-freevars(<hyps,  concl>))
                                                          then  let  x,b  =  dest-exists(hyps[i]);  in
                                                                      inl  [<[b[v/x]  /  hyps],  concl>]
                                                          else  inr  \mcdot{} 
                                                          fi 
                falseE  @i  =>  inr  \mcdot{} 
Date html generated:
2016_07_08-PM-05_22_15
Last ObjectModification:
2015_09_23-PM-06_51_40
Theory : minimal-first-order-logic
Home
Index