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